> Surely your software cannot decide that...

The D implementation would reject such code. The DFA assumes all control paths are executed. For example,

    if (c) free(p);
    *p = 3;

is rejected as use-after-free.

    if (c) free(p);
    if (!c) *p = 3;

is also rejected as use-after-free. If the DFA is done properly, you will not be able to trick it.

Then that doesn't mean "0% of the negatives".

No, it means you have false positives. But no false negatives.

I think you are both right. It's confusing because the original claim uses different terminology than usual. It said

> 100% of the positives with 0% negatives [are treated as positives]

* The "100% positives" are actual positives that show up as positive, so it's saying that there are no positives that show up as negatives i.e. "no false negatives" (even though it uses the word "positive")

* The "0% negatives" are actual negatives that show up as positives, so it's saying that there are "no false positives" (even though it uses the word "negative").

So UncleMeat's comment 'Then that doesn't mean "0% of the negatives"' and your comment 'it means you have false positives' are actually in agreement.

And that's a "negative" in a practical sense.

An abstract interpretation that outputs Top for all programs is sound but useless. In practice, most sound static analyses for complex problems aren't too far from that.

It's not a "negative", it's a disadvantage. "Negative" has a specific meaning that should not be used in this context.

Safe Rust is also in the same boat: it has a lot of false positives that are rejected by the borrow checker even though they would be okay, and yet it's being used just fine. Think of doubly linked lists which are pretty much impossible to implement in safe Rust unless you replace pointers with integer IDs which basically disables borrow checking. Non-lexical lifetimes are an example of downright changing the definition of the language in order to remove some of these false positives.

I didn't it that way. I read it as "downside" rather than "false negative", especially because a sound static analysis is trivial and not something to be proud of in the abstract.

"Output Top" is sound for all non-inverted lattices and takes constant time. Woohoo! But it is also useless.

Ok. And if you call into non-D code, like C or assembly?

I think this is just moving potential problem under rug, which is best it can do, given Rice Theorem

Calling non-D functions means the compiler cannot check them, and will rely on the user having correctly specified and annotated the function signature.

I.e. you can have "unsafe" annotated code which the compiler doesn't check, which is indeed where the dirty deeds get swept. For example, I doubt someone could write a guaranteed safe implementation of malloc().

The idea, naturally, is to specifically mark such sections so that your crack QA team knows what to focus on, and to minimize the amount of such code.

The trick is to make the safe sections expressive enough that it is practical to write the bulk of the code in safe sections, thereby minimizing the "threat surface".

I personally would want code like this flagged by static analysis. I would fix the code by not calling free in the second 'if' body if needfree was already false (just like the call at the end of the function is guarded).

You might want it flagged-- I would--, but it would still be a false positive if it did so (assuming the constants didn't result in a double-free). :)

I think the argument is that static analyzers don't have to work on completely unchanged code, but rather rely on humans to structure the code in a way to avoid issues.

Many years ago people regularly wrote things like "if (retval = f())" but after compilers started to complain about it people changed to write "if ((retval = f()))" instead, if they want an assignment and truthfulness testing at the same time.

There’s definitely a double free, provided that nowhere you proved that your conditions can’t be simultaneously true.