3 ms·
The differences are documented at https://compcert.org/man/manual001.html#sec13 https://compcert.org/man/manual001.html#sec13
by anonydsfsfs 5y ago
The 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.