start974/framac repository overview

Frama-C with MetAcsl, Why3 and a selection of SMT solvers in a multi architecture (amd64 and arm64) image.

Available on dockerhub: https://hub.docker.com/r/start974/framac⁠

Source files available on GitHub: https://github.com/start974/docker-framac⁠

This image is directly inspired by the original docker-framac⁠ by Frédéric Boulanger (image fredblgr/framac⁠ on Docker Hub), updated to Frama-C 33 with Ivette and a desktop available from a web browser through noVNC.

⁠How to use it

If you plan to use the GUI of Why3 or Frama-C, make sure you have an X server running, and allow connections from the host (xhost +localhost). Then start the container, mounting the current working directory on /workspace in the container :

docker run --rm --tty --interactive \
           --volume "$(PWD):/workspace:rw" \
           --name framac33 \
           --env="DISPLAY=host.docker.internal:0" \
           start974/framac:33.0

Note: on Apple M1 machines, the setting of the X11 display in Docker does not seem to work yet.

⁠Using the scripts available on GitHub

It is easier to use the scripts available on GitHub⁠.

In a terminal, run make run or ./run-docker-framac.sh. On Windows, you can use run-docker-framac.ps1 with PowerShell. After pulling the image from dockerhub, you should be logged as root in the container. You can then use z3, cvc5, alt-ergo, why3, frama-c and frama-c-gui (Ivette, the new GUI of Frama-C).

The current working directory is mounted as /workspace in the container.

You may also use the frama-c, frama-c-gui and why3 proxy shell scripts to execute these commands in the container as if they were available on the host.

You will need an X server in order to use the GUI of the applications frama-c-guiand why3 ide. On MacOS, you can use XQuartz⁠, which can also be installed as a cask by brew⁠. On Windows 10, you can use VcXsrv⁠.

⁠Contents of the image

This image, based on ubuntu:24.04, contains:

• Alt-Ergo 2.6.4
• Z3 4.13.4
• CVC5 1.2.1
• Why3 1.8.2 (with why3 ide)
• Frama-C 33.0 (Arsenic) with MetAcsl 0.11
• Ivette, the Electron-based GUI of Frama-C, available as frama-c-gui (it replaces the former GTK GUI)

⁠Contents of the repository

• Dockerfile the dockerfile to build the image
• Makefile has several targets:
  • build builds the image for the architecture of the host
  • newbuilder creates a new builder for buildx and sets buildx to use it
  • buildx builds the arm64/amd64 image and pushes it to dockerhub
  • run runs the image in a new container
• run-docker-framac.sh runs the image in a new container. It also takes care of setting up things so that the container can use your X server to display GUI applications.
• run-docker-framac.ps1 Windows PowerShell version of the previous script.
• test-framac contains code and two scripts to check if frama-c and frama-c-gui work
• test-metacsl contains code and a script to check if MetAcsl works
• test-why3 contains code and two scripts to check why3 in command line and in ide/gui modes
• frama-c, frama-c-gui and why3 are shell scripts that can be used as proxy on the host machine to the corresponding programs in the container.