Oh, that's really nice. Though, as a user one should remember: The approach described here gives up at some point. So it doesn't prove the absence of a bug class (e.g. double free), but it finds some instances. Which is already a very good thing, and hugely non-trivial.

The problem with "not giving up at some point" is the computational complexity: Analyzing big code bases takes half an eternity (days), while using huge amounts of memory (>128GB). And once you enter the "least-defined state", you either throw lots of false positives (which gives the users a hard time) or you need to "give up" (and hence potentially miss bugs).

Disclaimer: I work for a company that builds static analysis tools. I don't see this as competition, though. Our tools are used in industries where "safety-critical" is really important - so the "giving up"-part of the analysis is no option for us, and solely relying only on GCC isn't an option for our customers either ;-)