Blog

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

Frama-C Docker Images
André Maroneze on 4 November 2020

Frama-C now has official Docker images in the Docker Hub! In this post we describe what they contain and how we intend to evolve them. If you have other uses for Docker images, don’t hesitate to contact us! Official Frama-C Docker Images in Docker Hub Official Frama-C Docker images are...

Read More