3 ms·
Unless all are wrong in the same way, which doesn't seem too impossible.
by hoseja 7y ago
Unless all are wrong in the same way, which doesn't seem too impossible.
- tuukkah 7y agoOne of their compilers is never wrong: "Formal Methods as Bugscreen [--] the formally-verified CompCert compiler"
- jcranmer 7y agoJohn Regehr did find 11 bugs in CompCert (the unverified portion).
- tuukkah 7y agoIf I've understood correctly, the compiling step is verified but the parsing and assembly steps are not, and no bugs have been found where valid input would have been compiled to valid but wrong assembly. I didn't see a statement about this on CompCert's web site though.
- setr 7y agoThere were no bugs that their program could find; not that there are no bugs at all :-)
- setr 7y agoThe tool isn't meant to find all bugs, but rather to suggest that bugs exist. That there exist limitations to the kinds of bugs it can find is probably acceptable. Also if everyone implements something the same way, incorrectly according to the standard, then perhaps the standard itself is wrong. But otherwise, you just need one compiler to implement more strictly according to the standard for the bug to be suggested