[ufo]

I don't think compcert avoids undefined behavior pitfalls. Its more of a way to protect yourself from compiler bugs.

[nickpsecurity]

It's a verified subset of the C standard rather than all behaviors of all compilers. There's some semantics and work covering a lot of that already that just needs to be integrated into CompCert or static analyzers. Likewise, there's static analyzers that already cover it too but not formally verified.

Here's an example of investigating that with Compcert:

http://robbertkrebbers.nl/research/articles/compcert_formali...

Here's a semantics that looks for flaws and undefined behavior:

https://www.ideals.illinois.edu/bitstream/handle/2142/34297/...

[scott_s]

Agreed - I read through their website, and I saw no mention of eliminating undefined behavior.