E-ACSL now works in Frama-C Docker imagesAndré Maroneze - 20th Dec 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 be based on Debian instead.
More variants, more flexibility
The current development version of Frama-C (available as Docker images
framac/frama-c:dev-stripped) has already switched to the Debian-based images. Users based on Frama-C’s public git branch have access to a remade dev/docker directory which contains a Makefile and a Dockerfile (plus some accessory scripts) enabling production of images based on:
- Debian (currently,
- Fedora (currently,
- Alpine (currently,
make dev.debian or
make dev-gui.fedora, for instance, allows choosing either the Debian command-line based image, or the Fedora GUI-based image. In total, there are 9 variants.
Note: until recently, Frama-C Docker images were based on
alpine:3.13. The new version of Alpine can cause behavior differences, for instance, CI pipelines based on the image may require a few changes1.
1 Details for the interested: Frama-C’s open-source-case-studies repository had a CI pipeline based on the Alpine image, with
opam as default user. A vulnerability in Git imposed changes related to permissions of
.git folders. Since Gitlab’s Docker-based runners run as
root, but Frama-C’s Docker image does not, this broke the existing pipeline, requiring a small patch to fix it. If you set up a similar Gitlab-based CI, you may need a similar patch when using the new Frama-C Docker images.
Custom images for custom plug-ins
Advanced users (mainly, plug-in developers) may want to create Docker images with their own distribution of Frama-C, including e.g. external plug-ins. For instance, if you want to build an image with MetAcsl, you can do as follows:
Internalize MetAcsl in the
src/pluginsdirectory of your Frama-C git clone, by copying it there;
dev/make-distrib.shto produce a .tar.gz archive of your current Frama-C directory (including, in this case, MetAcsl);
Put the generated
frama-c-*.tar.gzfile inside directory
cd dev/dockerand then run:
make custom.<distro> FRAMAC_ARCHIVE=frama-c-<version>.tar.gz
frama-c-<version>.tar.gzis the name of the .tar.gz archive generated by
dev/make-distrib.sh. You can, of course, choose any of the variants (
Note: if your plug-in requires the installation of other packages, or special build steps, you may need to manually edit the
dev/docker in order to make sure everything succeeds. Note that the
Dockerfile contains several stages geared towards image minimization, but depending on your purposes, you can stop at stage 4 (for the command-line version) or at stage 6 (for the GUI version). We hope in the future to propose a more streamlined way to offer users ways to build their custom images.
Also note that, if you already ran the build process in the past (and thus already have some Docker layers ready), the Docker cache may reuse it and not update e.g. the
opam repository, leading to build errors. In such cases, you may need to prefix the
make command with
BUILD_ARGS=--no-cache to force Docker to rebuild the initial steps, including
opam update to take recent changes into account.
If you use Frama-C’s Docker images (in your CI pipeline, for instance), be aware that the default images, for development and upcoming versions, will be Debian-based. Alpine-based images, now suffixed by
.alpine, will use a newer Alpine version. Fedora images will also be available, suffixed by
.fedora. The images have been tested with Singularity. Besides the added flexibility, their main advantage is supporting plug-ins such as E-ACSL, which are not musl-compatible. Finally, the simplified Dockerfile should help users create their own custom images.