Frama-C This blog post describes for the first time some options that became available in Nitrogen, continuing this series. This post also offers a benchmark but the results of this benchmark cannot be reproduced with Nitrogen. They should be reproducible with the next version of Frama-C. Alarms false alarms and redundant...
Read MoreI do not have any solution I am 100% happy with to the overflow dilemma in the previous post. Here is one of the solutions that does not make me 100% happy. The first (partial) solution is: program so that overflows correspond exactly to unwanted circumstances (and then it becomes...
Read MoreThis post is another of the methodological cheat cards that made up much of this blog at its beginnings, before I decided that controversial comparisons between static analyzers were more fun to write. The problem: detecting semantic coding rules transgressions By default, Frama-C's value analysis does not warn about integer...
Read MoreMy colleague Bernard Botella pointed out an interesting example in an offline discussion following the last quiz. The setup Consider the snippet: int s; unsigned u1 u2; ... s = u1 - u2; The programmer's intention with the assignment is to compute in variable s of type int the mathematical...
Read MoreMy presentation Friday at the U3CAT meeting was on the topic of Frama-C Csmith testing. Several posts in this blog already describe facets of this work (it has its own tag). Yet another angle can be found in this short article draft. Said draft by the way will soon need...
Read More