[cfe-dev] Confused by constraints

[Jordan Rose]

I'm not quite sure what you're trying to do, but you've constructed an expression like

($V == 0) | ($V == 1)

and the analyzer doesn't have a great way to reason about that. (Apart from generally poor bitwise operator support, it's not something people write in real code.)

We don't have a good general way to produce single disjunctive states, but in this case you can can the same effect with ($V >= 0 && $V <= 1).

Jordan


> On May 19, 2015, at 2:11 , Manuel Klimek <klimek at google.com> wrote:
> 
> +jordan who can probably answer that off the top of his head :)
> 
> On Thu, May 14, 2015 at 8:21 AM Ben Laurie <benl at google.com <mailto:benl at google.com>> wrote:
> So, I have this:
> 
>   Optional<DefinedSVal> V = ...;
>   ASTContext &Ctx = svalBuilder.getContext();
>   DefinedSVal Zero = svalBuilder.makeIntVal(0, Ctx.IntTy);
>   DefinedSVal One = svalBuilder.makeIntVal(1, Ctx.IntTy);
>   SVal isZero = svalBuilder.evalBinOp(state, BO_EQ, *V, Zero, Ctx.IntTy);
>   SVal isOne = svalBuilder.evalBinOp(state, BO_EQ, *V, One, Ctx.IntTy);
>   SVal check = svalBuilder.evalBinOp(state, BO_Or, isZero, isOne, Ctx.IntTy);
> 
>   ConstraintManager &CM = state->getStateManager().getConstraintManager();
> 
>   ProgramStateRef stateZero, stateNotZero;
>   std::tie(stateZero, stateNotZero) = CM.assumeDual(state, isZero.castAs<DefinedSVal>());
> 
>   ProgramStateRef stateOne, stateNotOne;
>   std::tie(stateOne, stateNotOne) = CM.assumeDual(state, isOne.castAs<DefinedSVal>());
> 
>   ProgramStateRef right = CM.assume(state, check.castAs<DefinedSVal>(), true);
> 
> Ignoring for a moment that I should not cast to DefinedSVal unless it actually is defined, how come if that's executed on this snippet:
> 
> if (x > 1)
>   return x;
> 
> so V ends up being the x in the return statement, check is not defined, even tho stateZero etc, are all defined and have values as you'd expect?
> 
> 
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at cs.uiuc.edu <mailto:cfe-dev at cs.uiuc.edu>
> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev <http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev>

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