Blog

New machdep mechanism in Frama-C
André Maroneze on 29 January 2024

A machdep (for machine-dependent) in Frama-C is a set of architecture-specific configurations, which include: integer sizes, predefined macros, compiler type, standard library constants, etc. They are essential when analyzing embedded, non-portable code. Thanks to some C11 features, the machdep generation mechanism has been revised in Frama-C, allowing users to more...

Read More

Cyberhackathon - Frama-C + Binsec - 28/04/23
André Maroneze on 27 March 2023

(This is an announcement for an event near Paris; first follows the French version, then an English version.) Si vous êtes près de Paris, venez au Cyber-hackathon Frama-C + Binsec, le 28/04 de 9h à 17h, au CEA List, dans le campus Paris-Saclay (Nano-Innov, 2 bd Thomas Gobert, 91120 Palaiseau)...

Read More

Using Singularity/Apptainer for easy-to-use Docker images
André Maroneze (kindly tested by D. Bühler, V. Prevosto et al) on 1 February 2023

The Frama-C Docker images are useful for continuous integration, but for interactive use, they are not very practical: by default, Docker does not provide access to the local filesystem, and running the Frama-C GUI requires using derived tools such as x11docker. In this post, we briefly show an alternative, with...

Read More

E-ACSL now works in Frama-C Docker images
André Maroneze on 20 December 2022

The Frama-C Docker images available on Docker Hub were based on Alpine Linux, which allows for minimal sizes. However, its reliance on musl instead of the GNU libc (present in most Linux distributions) led to incompatibility issues with the E-ACSL plug-in. For this reason, current and future Docker images will...

Read More

Frama-C 26 (Iron): a release with several irons in the fire
André Maroneze (reviewed by David Bühler, Valentin Perrelle) on 29 November 2022

Frama-C 26 (Iron) has been released, and as always, it contains several improvements among different plug-ins. In this blog post, we will present some of them, with very short examples. This list of features is based on the main changes since the 25.0 (Manganese) release. Kernel/Aoraï: ‘calls’ ACSL extension moved...

Read More