diff --git a/_posts/2022-12-20-frama-c-docker-e-acsl.md b/_posts/2022-12-20-frama-c-docker-e-acsl.md new file mode 100644 index 0000000000000000000000000000000000000000..9562ea463ede63a55284e77efb4503843077416b --- /dev/null +++ b/_posts/2022-12-20-frama-c-docker-e-acsl.md @@ -0,0 +1,95 @@ +--- +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.