Frama-C So 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 MoreContext A facetious colleague who claims that he should be better writing his thesis but keeps committing Coq and OCaml files on Frama-C's repository, asked me the following question: Is there a function in Frama-C's kernel that can fold[1] a function over all types that appear in a C program?...
Read MoreA high-profile maintainer to a large Open-Source project recently found himself involved in a discussion in which at some point after having explained his arguments—I think—very clearly he had to call someone else a moron. Now everyone with write access to the internet is weighting in on how this is...
Read More