Frama-C GUI on the browser, via DockerAndré Maroneze - 16th Mar 2021
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:
- Getting a GUI to run on Docker is not trivial;
- The extra GUI-related dependencies increase the image size, and they are very unlikely to be used (due to point 1);
- These images are mostly geared towards continuous integration anyway.
- 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.
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
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.
- If you use SELinux (e.g. in a Fedora-based distribution), replace
zin the command line.
- In a Windows Command Prompt, replace
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!
Thanks to Frédéric Boulanger for creating the image and Dockerfile, along with helpful explanations.