Frama-C Enthusiastic 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 MoreOn a recent occasion to visit the USA on a professional basis, I nearly declined. I had a lengthy explanation ready for my refusal, and it might even have become a rant-tagged blog post. I finally went, so that hypothetical blog post never became. Today, I feel I have been...
Read More