Frama-C This third installment discusses the diagnosis of liveness properties of particular C programs, using Frama-C's value analysis, for the RERS 2012 competition. [Note added in September 2012: the diagnostic found for the example in this post disagrees with the diagnostic found later and sent to the competition organizers. I am...
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 MoreThis blog post describes for the first time some options that became available in Nitrogen, continuing this series. This post also offers a benchmark but the results of this benchmark cannot be reproduced with Nitrogen. They should be reproducible with the next version of Frama-C. Alarms false alarms and redundant...
Read More