Tag Archives: csmith

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

Csmith testing reveals that I'm no good at probabilities (and lazy)
Pascal Cuoq on 10 August 2011

Csmith testing A typical Frama-C Csmith testing script repeats four actions in an infinite loop: getting a random program from Csmith; compiling and executing it; analyzing it with Frama-C; using the results from step 3, possibly together with those of step 2, to determine whether the program reveals something that...

Read More

We have a Csmith-proof framework
Pascal Cuoq on 30 July 2011

Csmith that I mentioned earlier in this blog is a random generator of C programs. That much sounds easy but it generates only well-defined programs which two or more compilers have no excuse for compiling into executables that produce different results. And it generates varied and interesting enough C programs...

Read More