Tag Archives: benchmarks

When benchmarking Frama-C, consider option -no-autoload-plugins
André Maroneze on 16 February 2021

When using Frama-C in a series of benchmarks or test suites, especially when they consist of several small programs, consider using -no-autoload-plugins for better performance. This post explains why it is useful, as well as its downsides. Minimize startup time with -no-autoload-plugins By default, running frama-c makes it load all...

Read More

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

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

Short, difficult programs
Pascal Cuoq on 2 November 2012

When researchers start claiming that they have a sound and complete analyzer for predicting whether a program statement is reachable, it is time to build a database of interesting programs. Goldbach's conjecture My long-time favorite is a C program that verifies Goldbach's conjecture (actual program left as an exercise to...

Read More