Frama-C This post is a sequel of this post, in which I argued that it is not possible to double-free a piece of memory, only to pass indeterminate data (specifically, a dangling pointer) to a function (specifically, free()). Broken This time I am arguing that the standardized function realloc() is broken....
Read MoreFor some reason, uses of real to denote fixed-precision floating-point numbers (in languages such as FORTRAN) irritate me, but uses of integer or int to denote bounded integers do not. One notation isn't more accurate than the other, though. Does anyone have an idea why that might be?
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 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 More