Frama-C This blog post sums up what is the alignment constraint, its meaning for (common) hardware, how it has been derived at the C level and how Frama-C has been modified in version 32.0 (Germanium) to support the verification of this constraint and to support the keywords related to memory alignment....
Read MoreThis is an invited post by Jules Massart on his 6-month internship (from March to August 2025) in the Frama-C team, where he developed the Eva Abstract Debugger under the supervision of Michele Alberti, David Bühler, and Virgile Prevosto. Building on the original idea of Abstract Debuggers [1], Jules shows...
Read MoreIn 2016, a few blog posts (part 1, part 2, part 3) presented a short tutorial on writing ACSL clauses for Eva (back then, the Value Analysis plug-in). A few things changed since then, but posting them again in this blog would lead to the same issue in the future....
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 More