Frama-C is a static analysis tool that does not just match “dangerous” function names or code patterns like RATS, and that does more than Splint’s memory management, control flow checks and reachability analysis. Frama-C uses abstract interpretation to analyse the potential values of variables and detect a whole other bunch of bugs in programs. It also provides a specification language to write assertions or pre-conditions on functions and prove that these assumptions hold. Frama-C is designed for correctness: it will report false positives (for instance fail to validate an assertion on the return value of a function) but never true negatives. It focuses on showing the absence of bugs, by proving assertions respect pre-conditions. This has applications in evaluating the safety of critical systems.
What interests us here is the combination of value analysis and slicing, as the slicing lab with my language-based security students this year was a bit… light! In my defence, I didn’t expect them to actually do their homework! We’ll work through combining value analysis and slicing on code samples, starting up with more basic aspects of Frama-C. This post is in its vast majority inspired from the contents of the Frama-C documentation. In particular, many code samples are taken or derived from the Value analysis documentation.
Update: I’ve received interesting feedback on this article from Julien Signoles, one of the many talented people behind Frama-C. I’ve amended/clarified some of the things I discuss in the post, mostly changing ambiguous vocabulary I used to avoid confusions. Julien also explained in more details some aspects of Frama-C which I had forgotten, and so I’ll try to inject his own wisdom into the original article. Thanks Julien!