[cfe-dev] evaluating a LAnd expr in the static checker

[Alexey Sidorin via cfe-dev]

For the kind of constraint you specified, ProgramStateRef 
<http://clang.llvm.org/doxygen/namespaceclang_1_1ento.html#a4e45a121820f0d80d8910093dd33a1df>::assumeInBound() 
method may also work well. 
<http://clang.llvm.org/doxygen/classclang_1_1ento_1_1ProgramState.html#a046c4b1b381d1f5fed26eda3f0646efb>


04.06.2016 20:39, Alexey Sidorin via cfe-dev пишет:
> Hello Raymond,
>
> As I understand, you need to assume OffsetIsWithinBounds later. I 
> suggest you to use another approach. Instead of making a "logical 
> and", you can try to just "assume" operands of LAnd sequentially.
>
> So, the first assume will be for OffsetIsNonNeg, and the next is for 
> OffsetIsWithinSize.
>
>
>
> 04.06.2016 00:54, McDowell, Raymond C. via cfe-dev пишет:
>>
>> I am trying to construct a constraint that says 0 <= Offset <= Size, 
>> for two SVals Offset and Size.  Here’s what I did:
>>
>>   ASTContext &ACtx = ChCtx.getASTContext();
>>
>>   SValBuilder &SVBldr = St->getStateManager().getSValBuilder();
>>
>>   SVal Zero = SVBldr.makeZeroVal(ACtx.getSizeType());
>>
>>   SVal OffsetIsNonNeg = SVBldr.evalBinOpNN(St, BO_LE, 
>> Zero.castAs<NonLoc>(), Offset.castAs<NonLoc>(), ACtx.BoolTy);
>>
>>   SVal OffsetIsWithinSize = SVBldr.evalBinOpNN(St, BO_LE, 
>> Offset.castAs<NonLoc>(), BuffSize.castAs<NonLoc>(), ACtx.BoolTy);
>>
>>   SVal OffsetIsWithinBounds = SVBldr.evalBinOpNN(St, BO_LAnd, 
>> OffsetIsNonNeg.castAs<NonLoc>(), OffsetIsWithinSize.castAs<NonLoc>(), 
>> ACtx.BoolTy);
>>
>> When I run this code, it fails with an error: Assertion `false && 
>> “Invalid Opcode.”’ failed.  This is coming from evalAPSInt in 
>> BasicValueFactory.cpp.  This function contains a comment that says 
>> “Land, LOr, Comma are handled specially by higher-level logic.”  Land 
>> does not seem to be handled by higher-level logic in this case.  I 
>> intend to work around this by asserting these as two separate 
>> constraints instead of combining them into one.  But this looks like 
>> a bug to me, so thought I should raise the issue here.
>>
>>
>>
>> _______________________________________________
>> cfe-dev mailing list
>> cfe-dev at lists.llvm.org
>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>
>
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20160604/10293db7/attachment.html>