Frama-C Quiz time What does the program below do? #include <stdio.h> int main(){ struct { int t[4]; int u; } v; v.u = 3; v.t[4] = 4; printf(\v.u=%d" v.u); return 0; } Two answers are “it prints v.u=4” and “it prints v.u=3”: $ gcc t.c && ./a.out v.u=4 $ gcc -O2...
Read MoreThere is a C quiz in the middle of this post, lost in the middle of all the reminiscing. A history of arithmetic overflows in Frama-C From the very beginnings in 2005, until after the first Open Source release in 2008, Frama-C's value analysis was assuming that all arithmetic overflows...
Read MorePreviously on this blog Although it was so brief that you may have missed it, I previously mentioned here the 2012 RERS Grey Box Challenge an interesting competition where the questions involve programs in C syntax. I pointed out that some questions were about the reachability of assertions in the...
Read MoreA context-sensitive analysis Frama-C's value analysis is context-sensitive. This means that when a function f2() is called from a caller f1() function f2() is analyzed as many times as the analyzer goes over f1(). Function f2() is analyzed each time with a different program state—the program state corresponding to the...
Read MoreIn recent posts I have shown that Frama-C's value analysis could answer many reachability questions and some questions that weren't originally phrased as reachability questions about the programs in the RERS competition. If you are vaguely familiar with the internals of Frama-C's value analysis and if you tried analyzing some...
Read More