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(), Offset.castAs(), ACtx.BoolTy);
SVal OffsetIsWithinSize = SVBldr.evalBinOpNN(St, BO_LE, Offset.castAs(), BuffSize.castAs(), ACtx.BoolTy);
SVal OffsetIsWithinBounds = SVBldr.evalBinOpNN(St, BO_LAnd, OffsetIsNonNeg.castAs(), OffsetIsWithinSize.castAs(), 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.