So, Anna brought up that the check as implemented is very nearly
path-independent, i.e. it only depends on flow-sensitive properties of the CFG.
The path-sensitivity is buying us very little; it catches this case:
> int y = x;
> int div = z / y;
> if (x) { ...}
But also warns here, which doesn't necessarily make sense:
> int foo(int x, int y, int z) {
> int div = z / y;
> if (x) return div;
> return 0;
> }
>
> foo(a, a, b); // only coincidentally the same symbol
What would you think about turning this (and/or the null dereference check)
into a CFG-based check instead? We lose the first example (and cases where
inlining would help), but fix the second, and very possibly speed up analysis.
CFG analysis is also more capable of proving that something happens on all
paths rather than just some, since that's just propagating information along
the graph.
Jordan
On Jul 10, 2014, at 9:55 , Anders Rönnholm <[email protected]> wrote:
> Great, no problem. I'll move forward with my dereference then check patch now
> that this one is commited, which will be pretty similar.
>
> //Anders
>
> .......................................................................................................................
> Anders Rönnholm Senior Engineer
> Evidente ES East AB Warfvinges väg 34 SE-112 51 Stockholm Sweden
>
> Mobile: +46 (0)70 912 42 54
> E-mail: [email protected]
>
> www.evidente.se
>
> ________________________________________
> Från: Jordan Rose [[email protected]]
> Skickat: den 10 juli 2014 18:20
> Till: Anders Rönnholm
> Cc: [email protected]; Daniel Marjamäki
> Ämne: Re: [PATCH] Division by zero
>
> Thank you for going through so many rounds of review on this. Committed in
> r212731! (The one change I made was to reset the test in isZero to use assume
> instead of assumeDual, now that my confusion has been fixed.)
>
> Jordan
_______________________________________________
cfe-commits mailing list
[email protected]
http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
