Frama-C This 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 MoreThe existence of this option to make GCC conform to C99 when compiling for the x87 floating-point instruction set is informative. The commentary that comes with the patch is quite interesting, if you are into this sort of thing. If you are not that much into the minutiae of the...
Read MoreOne thing has been peeving me for a while. It is small and does not impact me directly, so I didn't speak up, but perhaps I should. Many people, some of whom should know better, mention Floyd, Hoare and Dijkstra in the same sentence as modern verification condition generators (Frama-C's...
Read MoreSpeaking of John Carmack, in his twitter feed, he notes: In hindsight it is surprising that I disliked doing math proofs in high school despite already being a programmer. It says a lot about the French education system that I started teaching myself programming at 6 and officially switched from...
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