Frama-C 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 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 MoreIntroduction This post introduces a new series about the art of helping the value analysis to be more precise. Until now, in the numerical precision series of this blog, this was easy enough. There was a single input variable and the obvious way to get more precise output values was...
Read More