[cfe-dev] Confused by constraints

[Ben Laurie]

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?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20150514/202d5f82/attachment.html>