Can You Trust Your C Compiler?

If you are writing a hello world program, you probably aren’t too concerned about how the compiler translates your source code to machine code. However, if your code runs on something that people’s lives depend on, you will want to be a bit pickier and use something like the COMPCERT compiler.  It’s a formally verified compiler, meaning there is a mathematical proof that what you write in C will be correctly translated to machine code. The compiler can generate for PowerPC, ARM, RISC-V, and x86, accepting a subset of ISO C 99 with a few extensions. While it doesn’t produce code that runs as fast as gcc, you can be sure the generated code will do what you asked it to do.

Of course, this still provides no assurance that your code will work. It just means that if you write something such as “x=0;” the generated code will set x to zero and will not do anything else. You can apply formal methods to verify your source code and be assured that the compiler doesn’t introduce possible failures. Cases where code like “x=0;” does extra things or incorrect things are very hard to figure out because the source code is correct and an examination of the generated code would be necessary to find the compiler’s code generation bug.

Continue reading “Can You Trust Your C Compiler?”