[blog] post about new E-ACSL-compatible Docker images

_posts/2022-12-20-frama-c-docker-e-acsl.md

+---
+layout: post
+author: André Maroneze
+date: 2022-12-20 12:00 +0100
+categories: docker
+title: "E-ACSL now works in Frama-C Docker images"
+---
+
+The [Frama-C Docker images](https://hub.docker.com/r/framac/frama-c/tags)
+available on Docker Hub were based on
+[Alpine Linux](https://www.alpinelinux.org/), which allows for minimal sizes.
+However, its reliance on [musl](https://www.musl-libc.org/) instead of
+the [GNU libc](https://www.gnu.org/software/libc/) (present in most Linux
+distributions) led to incompatibility issues with the
+[E-ACSL]{% link _fc-plugins/e-acsl.md %} plug-in. For this reason, current
+and future Docker images will be based on [Debian](https://www.debian.org/)
+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](https://git.frama-c.com/pub/frama-c/-/tree/master/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](https://git.frama-c.com/pub/open-source-case-studies/-/commit/7169be755db6c7a57ad7ac4556b6b786e3951ed8)<sup>1</sup>.
+
+<sup>1</sup> Details for the interested: Frama-C's [open-source-case-studies](https://git.frama-c.com/pub/open-source-case-studies)
+repository had a CI pipeline based on the Alpine image, with `opam` as default
+user. A [vulnerability in Git](https://github.blog/2022-04-12-git-security-vulnerability-announced/)
+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](https://git.frama-c.com/pub/meta/), 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.