[PATCH] Division by zero

[Anders Rönnholm]

Huh. So, I changed it back to the way it was:

SVal Val = State->getRawSVal(*L);
if (Val == S) {
Optional<DefinedSVal> DSV = Val.getAs<DefinedSVal>();
  ConstraintManager &CM = C.getConstraintManager();
  if (!CM.assume(State, *DSV, false))
    return true;
}

and tried running the tests. No failures. Then I flipped the "false" to "true" in the assume...and still no failures. So we must never be getting into that if-case!

What would that affect?

Jordan


We don't get into the if-case because we never get a Loc from Sval therefore it always returns false and our tests are passed.

Optional<Loc> L = S.getAs<Loc>();
 if (!L)
   return false;

Um. Right, we shouldn't get a Loc at that point. But we don't need a Loc. We just need whatever NonLoc symbol is there, and we can check to see if that is 0. Why did we need a Loc again?

Anyway, we shouldn't have features that don't show up in the tests. I think this code was either trying to avoid emitting duplicate messages if the denominator is known to be 0 already (which won't happen because that's a fatal error), or trying to avoid adding the symbol to the map if it's known not to be 0 (which is not what it's doing now, or at least not what it says it's doing). The latter is kind of useful but it's just optimization.

Jordan

Are you suggesting that we use NonLoc instead of Loc? Can we get an Sval from NonLoc? We needed Loc to get sval from state instead of looping the exploded node to find the range before the division.

Or should we remove the isZero check? We reason we have this is the latter, avoid adding the symbol to the map if it's known not to be 0.

//Anders