Frama-C 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 MoreFrama-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 MoreOne 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 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 MoreA 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