Frama-C Here's a cool obfuscated C program by Andy Sloane that draws a revolving donut. You know where this is heading... I am going to suggest that someone should verify it. I will get us started. 1. Download the code 2. Determine what library functions it needs: $ frama-c -metrics donut.c...
Read MoreThis post is a backward changelog that introduces actual new features. Beat that, Emacs 19 Antinews! Shortly after the release of Carbon, I offered to my Frama-C co-developers the idea of a great clean-up of the value analysis for the next release. This would not immediately add new features (indeed,...
Read MoreThis blog post is a revised version of part of my submission to the ICPC 2011 Industry Challenge. Please go ahead and read the challenge description. I could only paraphrase it without adding anything to it and so I won't. The study was made with the April development version of...
Read MoreDo you remember the Skein tutorial? It went off to a good start (it started this blog) and then was never really completed. I blame laziness. Looking back at that first post, I notice that indeed, before Boron, we were shipping software without documentation (just think! Ahem). At the time,...
Read MoreI have recently added an article \Test driving static analysis tools in search of C code vulnerabilities" by George Chatzieleftheriou and Panagiotis Katsaros on the wiki page of publications relevant to Frama-C. This article benchmarks a number of static analysis tools that it tests for precision (warning about real issues...
Read More