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 ;-)
Per Rice's theorem, it's not giving up that's not a option; it's just a question of whether you have false positives or false negatives. (To be fair, for safety-critical code, insisting on only false positives (ie treating anything you give up on as a positive) is a pretty resonable choice.)
I’d be interested to know which company (if you’re free to say). IIUC, this is very different from the way Coverity (the biggest commercial player I’m aware of in this space) operates.
Interestingly, different industry seems to have its own leading tool even though they all check for the same type of risks or errors. Q-AC is extremely prevalent in the Automotive Industry, Polyspace's Code Prover is also quite popular as well.
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 ;-)