3 ms·
The semantics of the dialect of C that CompCert accepts are precisely defined, as are the semantics of the assembly outputted (that is, it's not strictly x86/PP
by njs12345 15y ago
The semantics of the dialect of C that CompCert accepts are precisely defined, as are the semantics of the assembly outputted (that is, it's not strictly x86/PPC/ARM or whatever but some subset with defined semantics which happen to line up perfectly with observed behaviour). The first is fine I think (accepting a subset you define formally); the second is an issue but it's currently impossible to do any better. Still, if you look at this compared to the backends of LLVM and GCC it's certainly an improvement.