Frama-C I 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 More