One of these situations where it would be easy to misuse the word 'ironic' Pascal Cuoq on 11 May 2011
I just had to privately send someone a section from an article that, this same week, was rejected from the workshop it was submitted at.
Read MoreBlog
List of the ways Frama_C_dump_each() is better than printf() Pascal Cuoq on 21 April 2011
In an older post I recommended that the value analysis be launched on existing unit and integration tests. One advantage of using a completely unrolled analysis as compared to traditional compilation-execution is that the "execution" then takes place in an environment we have complete control of. Let us say there...
Read MoreWhen is it valid to compare two pointers in C? Pascal Cuoq on 14 April 2011
This post is about the circumstances in which the value analysis considers comparing pointers is safe, and those in which it considers the comparison is dangerous and emits an alarm. The alarm, an enigmatic assert \pointer_comparable(…, …);, uses an unaxiomatized ACSL predicate. If you use the value analysis regularly, you...
Read MoreC99 promotion rules: what ?! Pascal Cuoq on 11 April 2011
I reported bug 785 after getting three-quarters sure that the problem was in Frama-C (I used two different versions of GCC as oracles). I still cannot believe how twisted integer promotion rules are in C99. I had read them before but I had not followed the precise path I followed...
Read MoreVerifying the Compression Library QuickLZ Pascal Cuoq on 5 April 2011
This new series is dedicated to the verification of the C version of Open Source compression library QuickLZ version 1.5.0 using Frama-C's Value Analysis. The source code can be downloaded from the web site. QuickLZ offers compression and decompression routines using the Lempel-Ziv (LZ) algorithm. Various options are provided at...
Read More