3 ms·
I don't think compcert avoids undefined behavior pitfalls. Its more of a way to protect yourself from compiler bugs.
by ufo 11y ago
I don't think compcert avoids undefined behavior pitfalls. Its more of a way to protect yourself from compiler bugs.
- scott_s 11y agoAgreed - I read through their website, and I saw no mention of eliminating undefined behavior.
- nickpsecurity 11y agoIt'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_formalin.pdf 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/Ellison_Charles.pdf?sequence=1 https://www.ideals.illinois.edu/bitstream/handle/2142/34297/...