[cfe-dev] Confused by constraints

[Manuel Klimek]

+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> 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
> 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/f6f937a0/attachment.html>