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, framac/frama-c-gui:dev and 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, debian:bullseye-slim)
• Fedora (currently, fedora:36)
• Alpine (currently, alpine:3.16)

With a cd to dev/docker, running 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 changes¹.

¹ 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/plugins directory of your Frama-C git clone, by copying it there;

• Run dev/make-distrib.sh to produce a .tar.gz archive of your current Frama-C directory (including, in this case, MetAcsl);

• Put the generated frama-c-*.tar.gz file inside directory dev/docker;

• cd dev/docker and then run:

    make custom.<distro> FRAMAC_ARCHIVE=frama-c-<version>.tar.gz

  Where frama-c-<version>.tar.gz is the name of the .tar.gz archive generated by dev/make-distrib.sh. You can, of course, choose any of the variants (-gui, -stripped, .fedora, .alpine, etc).

Note: if your plug-in requires the installation of other packages, or special build steps, you may need to manually edit the Dockerfile in 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.

Conclusion

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.