5 ms·
That's both funny and true, but note that the same CompCert semantics is also the basis of a verified static analysis tool that can be used to prove the absence
by tom_mellior 8y ago
That's both funny and true, but note that the same CompCert semantics is also the basis of a verified static analysis tool that can be used to prove the absence of such errors in C programs: http://compcert.inria.fr/verasco/ http://compcert.inria.fr/verasco/
If you have a program that runs successfully through both the analyzer and the compiler, you can have quite a bit of confidence in the result.