Frama-C 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 MoreThis 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 MoreI 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 MoreThis 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 MoreHow it started In the last post we started a new series about helping the value analysis be more precise. We introduced an interpolation function with the goal of verifying that it is free of run-time errors. Having launched a first value analysis we got one alarm we need to...
Read More