Blog

Tag Archives: value

From Pascal strings to Python tuples
Pascal Cuoq on 31 July 2013

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 More

Arithmetic overflows in Fluorine
Pascal Cuoq on 9 July 2013

There 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 More

RERS 2012 competition: our solutions for problems 1-9
Pascal Cuoq on 2 October 2012

Previously 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 More

A value analysis option to reuse previous function analyses
Pascal Cuoq on 6 September 2012

A 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 More

On writing a dedicated model-checker for the RERS competition
Pascal Cuoq on 24 August 2012

In 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