CompCert gets a safe interpreter mode Pascal Cuoq on 29 August 2011
Safe C interpreters galore The last release of CompCert includes a safe C interpreter based on the compiler's reference semantics. Like KCC and Frama-C's value analysis it detects a large class of undefined behaviors and some unspecified ones. Like them in order to remain useful it needs to make some...
Read More