For example if we have a graph data structure and we are visiting it and freeing nodes, how can your static analysis know that nodes will not be visited twice by my logic and freed twice?
If the compiler rejects things that have free appear twice on branching control flow paths but aren't actually broken due to dynamic control flow (like your looping example given elsewhere) then that's a false positive, isn't it?
And people thought '0% negatives' was meaning 'no false positives'.
The D implementation, in contrast, uses a well-defined rule outlined above, and it works predictably and reliably (absent implementation bugs, rather than ad hoc rule shortcomings).
Another way of putting it is that the rules of the language are changed to make 0%/100% results workable. The compiler never says "there may be a problem here". It passes or is rejected. If it is passes, it is memory safe.
for (i = 0; i < 10; ++i);
However, such a construct is a hard error in D. Whether you meant it or not, it is not allowed. This is what I meant.
A construct in D that would pass is:
for (i = 0; i < 10; ++i) { }Given these more precise definitions, the analogous theorem would be that there is no type system (or static analysis) for use-after-free which is both sound and complete.