Frama-C 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 MoreCsmith 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 MoreCsmith 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 MoreSome time back, I reported a Csmith bug against the last git version. This is in no way a rant against Csmith a fine piece of engineering. Csmith does something that I would not have thought possible if you had asked me before I saw it: it generates random C...
Read More