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 MoreFrama-C has a mailing-list. It's a place people visit for free to complain that they are not getting the quality, technical, detailed answers that they deserve, and to tell us what our priorities should be. I expressed my opinion about the mailing list a long time ago in this very...
Read MoreA privately sent question may deserve a quick blog post. Context The example is as below: int x, y, s; main(){ x = Frama_C_interval(0, 2000000000); y = 1000000000; s = x + y; Frama_C_dump_each(); } Sorry for all the zeroes. There are nine of them in each large constant, so...
Read MoreThis post offers two C programs that look analyzable. Each is self-contained, not so small that verification is trivial, but not so big that it's a man-year effort. If it was me doing the work, I would see what Frama-C's value analysis can do, but if you decide to do...
Read More