Tag Archives: value-eva

Parsing realistic code bases with Frama-C
André Maroneze on 6 July 2018

A recurring subject when using Frama-C, especially intriguing for newcomers, is how to reach the stage where parsing of a realistic code base (as in, one that uses external libraries and compiles to different architectures) succeeds. This post will show a bit of the depth involved in the subject, presenting...

Read More

Analyzing Chrony with Frama-C/Eva
André Maroneze on 19 June 2018

Chrony is an implementation of NTP which is C99-compatible, with portable code, and thus a good candidate for an analysis with tools such as Frama-C. As part of an effort sponsored by Orolia, researchers from the List, CEA Tech laboratory applied Frama-C/Eva on the Chrony source code, in an attempt...

Read More

Analysis scripts: helping automate case studies, part 2
André Maroneze on 15 February 2018

In the previous post, we used analysis-scripts to prepare our analysis of Recommender. In this post, we will run EVA on the code and see how the iterative refinement of the analysis can be done. We assume the reader has performed all of the steps in the previous post, and...

Read More

Analysis scripts: helping automate case studies, part 1
André Maroneze on 25 January 2018

(kindly reviewed by T. Antignac, D. Bühler and F. Kirchner) Among Frama-C 16 Sulfur’s new features, one of them is dedicated to help setting up and iterating case studies. In this series of posts, we will explain how to use such scripts to save time when starting a new case...

Read More

Frama-C 15 (Phosphorus) released, and open source case studies
André Maroneze on 13 June 2017

Frama-C 15 (Phosphorus) has been released, and the OPAM package is already available! A MinGW-based OPAM package, distributed by fdopen’s MinGW OPAM repository, is also available. In this post, we briefly highlight two new features in this release. We also announce the release of a new Github repository, open-source-case-studies, which...

Read More