Blog

Habemus Frama-C in Fenestris (Frama-C on Windows, with WSL)
André Maroneze on 7 June 2019

We have successfully compiled and tested the beta release of Frama-C 19 (Potassium) in the WSL (Windows Subsystem for Linux), using Debian. Installation is not trivial, especially for the graphical interface, but in the future this should provide a more robust way to run Frama-C on Windows, than relying on...

Read More

Finding unexpected bugs in the DARPA CGC corpus
André Maroneze on 26 February 2019

Recently, we’ve been running Frama-C/Eva on the DARPA challenges from the SATE VI Classic track tool evaluation, organized by NIST. The C programs come from a Linux-compatible port of the DARPA Cyber Grand Challenge. The port was made by Trail of Bits and used as one of the evaluation sets...

Read More

Setting up an analysis with the help of frama-c-script
André Maroneze on 16 January 2019

Frama-C 18 (Argon) includes a new command, frama-c-script, which contains a set of helpful scripts for setting up new analyses. The available commands will likely expand in the future. We present here a quick overview of how to use them efficiently for a very fast setup. Presentation of frama-c-script frama-c-script...

Read More

New loop unroll annotation in Frama-C 18
André Maroneze on 14 December 2018

One of the new features in Frama-C 18 (Argon) is the annotation @loop unroll, used by the Eva plug-in to replace and improve upon the usage of slevel for semantically unrolling loops. This new annotation is more stable, predictable, and overall more efficient. In this post we present the annotation...

Read More

Frama-C/Eva in SATE VI with Juliet 1.3
André Maroneze on 15 November 2018

Frama-C chose to participate in the SATE VI Ockham Sound Analysis Criteria. With the upcoming Frama-C 18 (Argon) release, results can be reproduced using the open source version of the Eva plug-in. This post briefly presents SATE, the Juliet test suite, and the results obtained with Frama-C 18. We then...

Read More