Blog

Running old Frama-C versions from Docker images
André Maroneze on 15 October 2021

There 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 sake. Whatever the reason,...

Read More

Admit and check annotations in ACSL
André Maroneze on 10 June 2021

In 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 More

Frama-C GUI on the browser, via Docker
André Maroneze on 16 March 2021

New 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 More

When benchmarking Frama-C, consider option -no-autoload-plugins
André Maroneze on 16 February 2021

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 More

Frama-C Github Action
André Maroneze on 19 November 2020

In the previous post, we mentioned the official Frama-C Docker images. In this post, we present two examples where these images allow us to incorporate Frama-C in a continuous integration process: a Frama-C Github Action, as well as integration of Frama-C in a Gitlab CI pipeline. Github Action: run Frama-C/Eva...

Read More