<html><head><meta http-equiv="Content-Type" content="text/html charset=iso-8859-1"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><br><div><div>On Jul 2, 2014, at 5:27 , Anders Rönnholm <<a href="mailto:Anders.Ronnholm@evidente.se">Anders.Ronnholm@evidente.se</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div style="font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;">Hi,<br><br>New iteration with comments addressed.<br><br>I still don't understand why this is a loop at all:<br><br>+bool TestAfterDivZeroChecker::isZero(SVal S, CheckerContext &C) const {<br>+ Optional<Loc> L;<br>+ if (!(L = S.getAs<Loc>())) return false;<br>+<br>+ const ExplodedNode *N = C.getPredecessor();<br>+ while (N) {<br>+ ProgramStateRef State = N->getState();<br>+<br>+ // Find the most recent expression bound to the symbol in the current<br>+ // context.<br>+ SVal Val = State->getRawSVal(L.getValue());<br>+ if (Val == S) {<br>+ Optional<DefinedSVal> DSV = Val.getAs<DefinedSVal>();<br>+ return !C.getConstraintManager().assume(State, *DSV, false);<br>+ }<br>+ N = N->pred_empty() ? nullptr : *(N->pred_begin());<br>+ }<br>+ return false;<br>+}<br><br>What's wrong with "Val = C.getState()->getRawSVal(*L)"?<br><br>Sorry, thought I still had to loop, I have removed it now.<br><br><br>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?<br><br>Yes it looks kinda strange. I have changed it slightly to more resemble how DivZeroChecker does it.<br></div></blockquote></div><br><div><br></div><div>Huh. So, I changed it back to the way it was:</div><div><br></div><div><div style="margin: 0px; font-size: 11px; font-family: Menlo;"> <span style="color: #4f8187">SVal</span> Val = State-><span style="color: #31595d">getRawSVal</span>(*L);</div><div style="margin: 0px; font-size: 11px; font-family: Menlo;"> <span style="color: #bb2ca2">if</span> (Val == S) {</div><div style="margin: 0px; font-size: 11px; font-family: Menlo; color: rgb(79, 129, 135);"><span style="color: #000000"> </span>Optional<span style="color: #000000"><</span>DefinedSVal<span style="color: #000000">> DSV = Val.</span><span style="color: #31595d">getAs</span><span style="color: #000000"><</span>DefinedSVal<span style="color: #000000">>();</span></div><div style="margin: 0px; font-size: 11px; font-family: Menlo; color: rgb(49, 89, 93);"><span style="color: #000000"> </span><span style="color: #4f8187">ConstraintManager</span><span style="color: #000000"> &CM = C.</span>getConstraintManager<span style="color: #000000">();</span></div><div style="margin: 0px; font-size: 11px; font-family: Menlo;"> <span style="color: #bb2ca2">if</span> (!CM.<span style="color: #31595d">assume</span>(State, *DSV, <span style="color: #bb2ca2">false</span>))</div><div style="margin: 0px; font-size: 11px; font-family: Menlo; color: rgb(187, 44, 162);"><span style="color: #000000"> </span>return<span style="color: #000000"> </span>true<span style="color: #000000">;</span></div><div style="margin: 0px; font-size: 11px; font-family: Menlo;"> }</div></div><div><br></div><div>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!</div><div><br></div><div>What would that affect?</div><div>Jordan</div></body></html>