3 ms·
On their website, the claim is more ambitious: "The main result of the project is the CompCert C verified compiler, a high-assurance compiler for _almost all_ o
by macleginn 5y ago
On their website, the claim is more ambitious: "The main result of the project is the CompCert C verified compiler, a high-assurance compiler for _almost all_ of the C language (ISO C99), generating efficient code for the PowerPC, ARM, RISC-V and x86 processors." (https://compcert.org/ https://compcert.org/)
- bombcar 5y agoThat makes me wonder even more what the missing parts are.
- anonydsfsfs 5y agoThe differences are documented at https://compcert.org/man/manual001.html#sec13 https://compcert.org/man/manual001.html#sec13
- hvdijk 5y agoInteresting that only a restricted switch is supported, but goto is apparently available unrestricted. Any switch should be trivially translatable to if-goto-else-if-goto-etc, so I wonder what the reason for that might be.
- MaxBarraclough 5y agoJust a guess, but perhaps they don't bother supporting 'unstructured switch' because they expect that input programs will most likely be written in the MISRA C subset of C anyway? I don't imagine it's due to technical challenges in formal modelling, as 'structured switch' statements still permit the default case to simply break immediately.