On Feb 20, 2012, at 16:44, Ryan Govostes wrote: > On Feb 17, 2012, at 1:11 AM, Jordy Rose <[email protected]> wrote: > >> Nice idea for a checker. The one thing I'm wondering is why you decided to >> use this less than / greater than approach...it might not matter here, but >> in general statements about equality and inequality are a bit easier for the >> analyzer to reason about than less than and greater than. It requires the >> same number of checks, too: > > Hi Jordy, > > Thanks. This is my first checker and the patch I submitted is the result of a > few iterations with Ted. Indeed I originally wrote it using equality and > inequality as you suggested, but Ted recommended the approach used now: > >> [...] I can say that you are definitely going into territory where the >> current solver isn't going to handle this well. It currently doesn't reason >> about arbitrary disjunctions. We currently accomplish that feat in the >> static analyzer by bifurcating states. > > So, we settled on (x <= 1) && (x >= 0) as you see in the patch.
Ah, I see...my strategy results in two valid states: stZero*, stNotZero stOne*, stNotZeroOrOne ...while yours only has one: stLTZero, stGEZero stGTOne, stZeroOrOne* Okay, thanks for the explanation! Jordy _______________________________________________ cfe-commits mailing list [email protected] http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
