Frama-C A contest and a self-pitying lament John Regehr was organizing a craziest undefined behavior contest and the results are in. I had an entry in the contest but I did not win. My entry apparently was too obviously dangerous. As John puts it “I would have expected a modern C...
Read MoreThis 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 More