3 ms·
If you use the Clight subset with the CompCert C Compiler, the answer is yes: http://compcert.inria.fr/compcert-C.html#subset http://compcert.inria.fr/compcert
by evangineer 15y ago
If you use the Clight subset with the CompCert C Compiler, the answer is yes:
http://compcert.inria.fr/compcert-C.html#subset http://compcert.inria.fr/compcert-C.html#subset
In any other case, the answer is almost certainly no. Most commonly used C compilers are sufficiently large and complicated that the chances of avoiding a compiler bug with a sufficiently large codebase is close to zero.
- mansr 15y agoCompcert is not without bugs either. The very blog this post references talks about some.
- evangineer 15y agoThanks for the heads up, I hadn't seen anything in the article about CompCert, but on doing a search I found there are quite a few mentions of it on other articles on the blog: http://blog.regehr.org/?s=compcert&searchsubmit=Search http://blog.regehr.org/?s=compcert&searchsubmit=Search