Frama-C 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 MoreDuring 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 MoreRecently, 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 MoreFrama-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 MoreWhen 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