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

[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

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