Blog

Analysis scripts: up-to-date information in the Frama-C User Manual
André Maroneze on 17 June 2020

The analysis scripts provided with Frama-C, which have been mentioned in this blog several times, are now documented in the Frama-C User Manual. This should provide a more complete and up-to-date experience concerning these scripts. Faster iterations with daily Frama-C snapshots Deploying analysis scripts usually required very long iteration times:...

Read More

Debugging Frama-C analyses: better privacy with C-Reduce
André Maroneze on 2 April 2020

Frama-C has a somewhat obscure plug-in called Obfuscator, whose original purpose was to help industrial users give the Frama-C developers enough information about confidential use cases, for debugging and optimizations. However, sharing proprietary code is never easy: is the obfuscation good enough? Are there legal issues involved? Is it worth...

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

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