[PATCH] Division by zero

[Jordan Rose]

On Jul 2, 2014, at 5:27 , Anders Rönnholm <Anders.Ronnholm at evidente.se> wrote:

> Hi,
> 
> New iteration with comments addressed.
> 
> I still don't understand why this is a loop at all:
> 
> +bool TestAfterDivZeroChecker::isZero(SVal S, CheckerContext &C) const {
> +  Optional<Loc> L;
> +  if (!(L = S.getAs<Loc>())) return false;
> +
> +  const ExplodedNode *N = C.getPredecessor();
> +  while (N) {
> +    ProgramStateRef State = N->getState();
> +
> +    // Find the most recent expression bound to the symbol in the current
> +    // context.
> +    SVal Val = State->getRawSVal(L.getValue());
> +    if (Val == S) {
> +      Optional<DefinedSVal> DSV = Val.getAs<DefinedSVal>();
> +      return !C.getConstraintManager().assume(State, *DSV, false);
> +    }
> +    N = N->pred_empty() ? nullptr : *(N->pred_begin());
> +  }
> +  return false;
> +}
> 
> What's wrong with "Val = C.getState()->getRawSVal(*L)"?
> 
> Sorry, thought I still had to loop, I have removed it now.
> 
> 
> Also, I'm reading your check as saying that the value is zero if there does not exist a state where DSV is not non-zero. I must be reading something wrong (since you have test cases), but what? Can you explain it to me?
> 
> Yes it looks kinda strange. I have changed it slightly to more resemble how DivZeroChecker does it.


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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20140703/2ceb8bd5/attachment.html>