Jun 15, 2017

"Deterministically locating all undefined behavior is undecidable. Static analyzers can only locate a subset of it."

It might be true but barely matters when we have tools like KCC. It's built on an executable semantics of C that runs in a framework on top of Maude rewrite engine.

http://www.kframework.org/index.php/Main_Page

https://github.com/kframework/c-semantics

http://fsl.cs.illinois.edu/FSL/papers/2015/hathhorn-ellison-...