Tag Archives: CompCert

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