Frama-C GUI on the browser, via Docker

New Frama-C Docker images, with a graphical interface, are available in the Docker Hub. They allow running Frama-C via a browser, on Windows, macOS and Linux.

Frama-C + Docker + noVNC = Frama-C GUI on a browser

The “traditional” Frama-C Docker images available on Docker Hub lack the graphical interface, for three reasons:

1. Getting a GUI to run on Docker is not trivial;
2. The extra GUI-related dependencies increase the image size, and they are very unlikely to be used (due to point 1);
3. These images are mostly geared towards continuous integration anyway.

Now, thanks to Frédéric Boulanger’s Docker images, which are themselves based on Doro Wu’s noVNC, there are a few images containing the Frama-C GUI, along with some tools to make them easy to use:

• Frédéric’s Docker images, including both amd64 and arm64 architectures;
• And a derived frama-c-gui image, which contains less features, but is easier for us to update.

These images are based on Ubuntu with a noVNC setup, which allows the GUI to be readily used via the browser, thus skipping additional configuration steps, be it on Windows, Linux or macOS.

Usage

You can download and run Frédéric’s image with:

docker run --rm -p 6080:80 -v $PWD:/workspace:rw fredblgr/framac-novnc:2021

Note that the image is larger than 1 GB.

You can also replace fredblgr/framac-novnc:2021 with framac/frama-c-gui:dev to get Frama-C’s development version.

When the image is run, it starts a local server process on port 6080. You can then go to http://localhost:6080 in your browser and you’ll see a running session of the Linux desktop LXDE. Open a terminal and run frama-c-gui to start the Frama-C GUI.

Here’s some details about the docker run command, in case you need to adapt or extend them:

• --rm: automatically remove the container when it exits;
• -p 6080:80: host port 6080 is mapped to guest port 80;
• -v <source>:<target>:rw: maps the host directory <source> to the guest directory <target>, with read-write access; this allows easily sharing files between the host and the container, as described below.

Notes:

• If you use SELinux (e.g. in a Fedora-based distribution), replace rw with z in the command line.
• In a Windows Command Prompt, replace $PWD with %cd%.

Sharing files between host and container

When running Frama-C, you typically want to feed it some source files for the analysis, or get some results back. Using the -v (volume) option suggested above, Docker will automatically mount the $PWD directory as /workspace inside the container. This allows you to edit the file in the host, e.g. add some ACSL annotations, then re-run Frama-C in the container and get the updated file.

Frédéric’s Github page has more details and options related to the Docker image.

Running Frama-C on Windows, macOS and Linux, via Docker

The Docker image can be run using Docker for Windows, and it also works on macOS, including M1 Macs, since Frédéric uploaded an arm64 image as well. Note that the framac/frama-c-gui image only exists for amd64; it has nevertheless been tested on both Linux and Windows.

Suggestions are welcome

If you have any suggestions or requests concerning Frama-C Docker images, don’t hesitate to contact us!

Acknowledgments

Thanks to Frédéric Boulanger for creating the image and Dockerfile, along with helpful explanations.