Frama-C I should have said this earlier — others might have wanted to join in the fun — but I will be sending an entry to participate in the International Conference on Program Comprehension's Industrial Challenge. My write-up will appear here shortly after the submission deadline.
Read MoreI 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 More