Frama-C I wish researchers would stop calling the plug-in they are using \Frama-C". "Frama-C" is the framework. It has very few of the properties that are attributed to it. One plug-in or the other usually is to blame or praise. This is not just because when researchers bring it up it...
Read MoreThis 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 MoreI 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 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 More