Frama-C Docker Images

Frama-C now has official Docker images in the Docker Hub! In this post we describe what they contain and how we intend to evolve them. If you have other uses for Docker images, don’t hesitate to contact us!

Official Frama-C Docker Images in Docker Hub

Official Frama-C Docker images are now available in Docker Hub! The Frama-C team registered the framac user (no hyphens in Docker Hub usernames, so don’t look for a frama-c user), and we are periodically uploading images to it.

The Frama-C Docker images aim to be as complete as possible, within a certain limit, that is: we strive to maximize the number of installed optional components in such images, avoiding a few which might incur a large increase in the image size.

The Frama-C GUI is also not included, mainly because setting up a Docker image with a GTK-based graphical interface is not trivial, and this is also not the main use case for these Docker images. When the new Frama-C GUI (based on Electron) will be production-ready, we will try to make it available from within the Docker image.

What’s included, and what’s not?

The Frama-C Docker images are based on Debian images, and include opam, a suitable OCaml compiler, and include every open-source plug-in shipped with the default Frama-C distribution, along with most optional dependencies. For Frama-C 22 (Titanium), for instance, this means that optional Eva domains based on Apron and MPFR, as well as Markdown-Report (which requires ppx_deriving), are included. The only exception is Coq, not included by default due to its large size.

We also include in these images some external solvers: Alt-Ergo, CVC4 and Z3. The specific included versions vary according to the version of Frama-C, to ensure they are compatible with Why3 and WP.

Overall, we follow the reference-configuration.md file, provided with Frama-C, to decide what’s included in each image.

Older Frama-C releases, backporting changes, and sharing Dockerfiles

So far, images with Frama-C from 18.0 to 21.1 are available. We intend to keep the latest minor release of each version, e.g., when Frama-C 22 is released, 21.0 may be removed, since 21.1 will be then the latest image from release 21.

If you’d like older Frama-C releases to be available, please contact us, we’ll be glad to upload them. Also, if additional changes could help users to benefit from such changes, we’ll consider backporting them to older releases, and uploading the new images to Docker Hub.

Finally, note that all Dockerfiles are available in the devel_tools/docker directory of the Frama-C sources. You can use them to customize your own recipes. You can also send us recommendations and change requests.

Acknowledgements

This project has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 830892 (a.k.a SPARTA). This funding allowed us to develop, among other features and as requirements for other tasks, support for these Docker images and future integration into a CI pipeline. Which will be the subject of a future blog post…