Confused by constraints

So, I have this:

Optional 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());

ProgramStateRef stateOne, stateNotOne;
std::tie(stateOne, stateNotOne) = CM.assumeDual(state, isOne.castAs());

ProgramStateRef right = CM.assume(state, check.castAs(), 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?

+jordan who can probably answer that off the top of his head :slight_smile:

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