Tag Archives: value-eva

SATE VI Workshop: Frama-C satisfies the Ockham Criteria
André Maroneze on 2 October 2019

During the SATE VI Workshop, organized by the NIST SAMATE project, Frama-C was confirmed as having satisfied the Ockham criteria for sound analysis tools. Frama-C previously satisfied the SATE V Ockham criteria (2013-2016) and found hundreds of errors in the test material. We reported in this blog about our analysis...

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