Frama-C Sven Mattsen is working at CEA until the summer. He is the author of this post. The post continues the series explaining how to guide the value analysis towards more precise conclusions. It starts where that one and that other left off. Problem This article is concerned with the Value...
Read MoreSemi-serious musings During the Frama-C random testing experiment described at length on this blog and this page we found a few bugs in Csmith too. John Regehr one of the Csmith developers and not entirely coincidentally a co-author of the article linked in the previous post is also a co-author...
Read MoreIt may be because I read an earlier draft that has had the time to sink in, but I find this article on the subject of integer overflows extremely clear and informative. It relates to the previous post. Key quote: integer overflow issues in C and C++ [...] are common...
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