Frama-C In 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 MoreThere are several reasons one might want to run an old version of Frama-C: - to test some outdated plugin which is only compatible with a previous version; - to re-run analyses mentioned in an old tutorial or blog post; - to compare results between Frama-C versions; - for nostalgia’s...
Read MoreIn Frama-C 23 (Vanadium), two new kinds of ACSL annotations are available, to complement assert: the admit and check annotations. In a nutshell, assert P is equivalent to check P; admit P. The former allows easier checking of the validity of predicates, while the latter documents the introduction of external...
Read MoreNew Frama-C Docker images, with a graphical interface, are available in the Docker Hub. They allow running Frama-C via a browser, on Windows, macOS and Linux. Frama-C + Docker + noVNC = Frama-C GUI on a browser The “traditional” Frama-C Docker images available on Docker Hub lack the graphical interface,...
Read MoreWhen 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