Frama-C This post follows that post. For cases 2 and 3 in order to get more complete execution traces we again take advantage of Frama_C_dump_each(). Before launching the analysis we insert a call to this primitive right at the end of RoCo_process() so that local variables of that function will be...
Read MoreIn 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 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