Frama-C This blog post is on the subject of “code smells” and what is wrong with them. I initially wanted to go with the title “Code smells are crap”. That made it clearer that the title was grammatically a sentence, with “code smells” a nominal group followed by a verb. But...
Read MoreMark Shroyer has discovered an interesting consequence of undefined behavior in the compiled version of a C program: a variable behaves as both true and false as a result of being uninitialized. The post is great and could not come at a better time. I needed for the talk I...
Read MoreSo I am at this conference, right? Having been looking, for a few months now, without luck, for someone who teaches C programming*, I figure this conference is as good an occasion to find em as any. But it sounds kind of stupid to go to someone and just ask...
Read MoreEnthusiastic reactions to the previous post about verifying the termination of a C program with Frama-C's value analysis lead me to write this post-scriptum. On detecting both termination and non-termination The scheme I outlined in the previous post can only confirm the termination of the program. If the program does...
Read MoreWhat's old about option -obviously-terminates Option -obviously-terminates is a value analysis option, new in Nitrogen, with some of the same effects as using an infinite slevel. This option also disables fixpoint detection and the statement-wise memorisation of analysis results. I briefly described this option in a previous post in section...
Read More