diff --git a/devel_tools/docker/.gitignore b/devel_tools/docker/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..7762191a2d2e4e1fcc7889d279426890c04f02ae
--- /dev/null
+++ b/devel_tools/docker/.gitignore
@@ -0,0 +1,10 @@
+Dockerfile.dev*
+Dockerfile.1*
+Dockerfile.2*
+Dockerfile.3*
+Dockerfile.4*
+Dockerfile.5*
+Dockerfile.6*
+Dockerfile.7*
+Dockerfile.8*
+Dockerfile.9*
diff --git a/devel_tools/docker/Dockerfile.template b/devel_tools/docker/Dockerfile.template
new file mode 100644
index 0000000000000000000000000000000000000000..e7fd0b54efd3a31167b000cca05ea94fee4ce4d0
--- /dev/null
+++ b/devel_tools/docker/Dockerfile.template
@@ -0,0 +1,211 @@
+# Inspired by https://github.com/Frederic-Boulanger-UPS/docker-framac and
+# https://gitlab.inria.fr/why3/why3/-/blob/master/misc/Dockerfile.deploy
+
+FROM @ALPINE_OPAM_BASE@ AS base
+
+# Stage 1: switch opam if needed (only for very old versions),
+# then install external provers (see .template files)
+
+FROM base AS frama-c
+
+## Install packages from reference configuration
+## Note: Python and time packages are only required for tests, but if so,
+## they need to be present before running './configure'
+RUN \
+@OPAM_CACHE_FIX@ \
+opam update -y && \
+opam install depext -y
+
+RUN @OPAM_SWITCH@
+
+# "RUN eval $(opam env)" does not work, so we manually set its variables
+@ENV@
+
+# Install external provers
+@CVC4@
+@Z3@
+
+RUN opam depext --install -y @OPAM_DEPS@
+
+RUN @WHY3_CONFIG@
+
+# from_archive: if "git", clone from public Git; if prefixed with http,
+# wget it; otherwise, use the given archive name.
+# Note: the archive must contain a root directory
+# starting with 'frama-c'
+ARG from_archive=git
+
+# The following line copies a frama-c archive if it exists, else nothing
+COPY --chown=opam:opam README.md frama-c-*.tar.gz /frama-c/
+
+RUN \
+if [ "${from_archive}" != "git" ]; then \
+  (cd /frama-c && \
+    case "${from_archive}" in \
+    "http"*) wget "${from_archive}" ;; \
+          *) ;; \
+    esac && \
+    tar xvf "${from_archive##*/}" --strip 1 && \
+    rm -f frama-c-*.tar.gz) \
+; else \
+   sudo apk add git && \
+   (cd /frama-c && rm -f * && git clone --depth 1 https://git.frama-c.com/pub/frama-c.git .) \
+; fi
+
+RUN cd /frama-c && @PATCH_FRAMAC@ && autoconf && ./configure --disable-gui
+RUN cd /frama-c && make -j && sudo make install
+
+# Run quick sanity checks
+RUN \
+printf "int g;\n//@assigns g;\nvoid f(){g = 1;}\nint main() {f(); return g;}" > /tmp/simple.c && \
+frama-c -val @WP_REPORT@ /tmp/simple.c && \
+rm -f /tmp/simple.c
+
+## Cleanup
+RUN \
+opam clean --yes --switch-cleanup && \
+rm -rf /home/opam/opam-repository && \
+rm -rf /home/opam/.opam/repo/default/.git*
+
+# Stage 3 (optional): tests
+
+FROM frama-c AS tests
+
+# Run standard Frama-C tests
+RUN @FRAMAC_TESTS@
+
+# Run an extra test for WP with provers
+# Note: we use ';' instead of '&&' because, for older Frama-C's, such directory
+#       does not exist.
+RUN cd /frama-c/ && cd src/plugins/wp/tests/; @WP_TEST@
+
+
+# Stage 4 (optional): GUI
+
+FROM frama-c AS frama-c-gui
+
+RUN sudo apk add adwaita-icon-theme font-noto gdk-pixbuf @GUI_ALPINE_DEPS@
+RUN opam depext -y --install @GUI_OPAM_DEPS@
+RUN cd /frama-c && @GUI_REMAKE@
+
+# Stage 5 (to be deployed): 'slim' image
+
+FROM @ALPINE_BASE@ AS frama-c-slim
+
+RUN adduser --disabled-password --gecos '' opam
+
+COPY --from=frama-c /bin /bin/
+COPY --from=frama-c /etc /etc/
+COPY --from=frama-c /lib /lib/
+COPY --from=frama-c /sbin /sbin/
+COPY --from=frama-c /usr /usr/
+COPY --from=frama-c --chown=opam:opam /home/opam/.opam /home/opam/.opam/
+COPY --from=frama-c /home/opam/.profile /home/opam/
+
+RUN apk add sudo
+USER opam
+WORKDIR /home/opam
+@ENV@
+
+RUN @WHY3_CONFIG@
+
+# Stage 6 (optional, to be deployed): 'slim' image with frama-c-gui
+
+FROM @ALPINE_BASE@ AS frama-c-gui-slim
+
+RUN adduser --disabled-password --gecos '' opam
+
+COPY --from=frama-c-gui /bin /bin/
+COPY --from=frama-c-gui /etc /etc/
+COPY --from=frama-c-gui /lib /lib/
+COPY --from=frama-c-gui /sbin /sbin/
+COPY --from=frama-c-gui /usr /usr/
+COPY --from=frama-c-gui --chown=opam:opam /home/opam/.opam /home/opam/.opam/
+COPY --from=frama-c-gui /home/opam/.profile /home/opam/
+
+RUN apk add sudo
+USER opam
+WORKDIR /home/opam
+@ENV@
+
+RUN @WHY3_CONFIG@
+
+# sanity check
+RUN which frama-c-gui
+
+# Stage 7: preparation of 'stripped' image (~200 MB compressed)
+# Note: this image only contains the Frama-C binaries and files closely
+# related to it; most other OCaml tools have been removed.
+# Even recompilation of Frama-C is not guaranteed to work.
+
+FROM frama-c-slim AS frama-c-stripped-prepare
+
+@ENV@
+
+# Remove all non-essential ocaml binaries
+RUN \
+mkdir -p /home/opam/.opam/minimal/bin && \
+(cd /home/opam/.opam/*/bin && \
+  cp -P $(ls -d alt-ergo ocaml ocamlc ocamlc.opt ocamlfind ocamlopt ocamlopt.opt why3 2>/dev/null) /home/opam/.opam/minimal/bin/) && \
+rm -rf /home/opam/.opam/@OCAMLV@/bin && \
+mv /home/opam/.opam/minimal/bin /home/opam/.opam/@OCAMLV@/bin/
+
+# Remove non-essential opam files
+RUN rm -rf /home/opam/.opam/repo/default/packages
+RUN rm -rf /home/opam/.opam/download-cache
+RUN rm -rf /home/opam/.opam/repo/state.cache
+
+# Further stripping: remove non-essential files from tools used by Frama-C
+# (Apron, Alt-Ergo, large OCaml compiler files, etc)
+RUN rm -f /home/opam/.opam/@OCAMLV@/share/apron/lib/*.a
+RUN rm -f /home/opam/.opam/@OCAMLV@/share/apron/lib/*_debug.so
+RUN rm -rf /home/opam/.opam/@OCAMLV@/share/apron/bin
+RUN rm -rf /home/opam/.opam/@OCAMLV@/share/apron/include
+RUN rm -rf /home/opam/.opam/@OCAMLV@/lib/alt-ergo
+RUN rm -rf /home/opam/.opam/@OCAMLV@/lib/lablgtk2
+RUN rm -rf /home/opam/.opam/@OCAMLV@/lib/ppx_tools
+RUN rm -rf /home/opam/.opam/@OCAMLV@/lib/psmt2-frontend
+RUN rm -rf /home/opam/.opam/*/lib/ocaml/expunge
+RUN rm -rf /home/opam/.opam/*/lib/ocaml-migrate-parsetree
+RUN (cd /home/opam/.opam/@OCAMLV@/lib/why3/commands && mv why3config config && rm -f why3* && mv config why3config) || true
+
+# Remove all non-essential OCaml files (everything else other than
+# *.cmxs, *.cmx and *.cmi)
+RUN find /home/opam/.opam \( -name "*.cmt*" -o -name "*.[ao]" -o -name "*.cm[ao]" -o -name "*.cmxa" \) -exec rm {} \;
+
+# Remove non-essential installed files
+RUN sudo rm -f /usr/bin/opam-2.*
+RUN sudo rm /usr/local/bin/frama-c.byte
+RUN sudo find /usr/local/lib/frama-c \( -name "*.[ao]" -o -name "*.cm[ao]" -o -name "*.cmxa" \) -exec rm {} \;
+RUN cd /usr/share && sudo rm -rf gtk-2.0 X11 xml/docbook
+
+# Remove non-essential apk libraries
+RUN sudo apk del libxcb libx11-dev graphviz pango cairo gtk+2.0-dev gtksourceview2-dev pango-dev
+
+# Stage 7 (optional): stripped, slimmest image (running Frama-C works,
+# but almost everything else does not (e.g. recompiling OCaml modules))
+
+FROM @ALPINE_BASE@ AS frama-c-stripped
+
+RUN adduser --disabled-password --gecos '' opam
+
+COPY --from=frama-c-stripped-prepare /bin /bin/
+COPY --from=frama-c-stripped-prepare /etc /etc/
+COPY --from=frama-c-stripped-prepare /lib /lib/
+COPY --from=frama-c-stripped-prepare /sbin /sbin/
+COPY --from=frama-c-stripped-prepare /usr /usr/
+COPY --from=frama-c-stripped-prepare --chown=opam:opam /home/opam/.opam /home/opam/.opam/
+COPY --from=frama-c-stripped-prepare /home/opam/.profile /home/opam/
+
+RUN apk add sudo
+USER opam
+WORKDIR /home/opam
+@ENV@
+
+RUN @WHY3_CONFIG@
+
+# Re-run quick sanity checks
+RUN \
+printf "int g;\n//@assigns g;\nvoid f(){g = 1;}\nint main() {f(); return g;}" > /tmp/simple.c && \
+frama-c -val @WP_REPORT@ /tmp/simple.c && \
+rm -f /tmp/simple.c
diff --git a/devel_tools/docker/Makefile b/devel_tools/docker/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..550e9d75a985abd730f70defbf45c3f3fc7297fc
--- /dev/null
+++ b/devel_tools/docker/Makefile
@@ -0,0 +1,878 @@
+.PHONY: *-stripped *-gui push-*
+
+help:
+	@echo "Targets: $(TARGETS)"
+
+##########################
+# LIST OF VARIABLES IN TEMPLATE FILES, TO BE REPLACED VIA SED
+# @ALPINE_BASE@
+# @ALPINE_OPAM_BASE@
+# @CVC4@
+# @CVC4_VERSION@
+# @ENV@
+# @FRAMAC_TESTS@
+# @GUI_ALPINE_DEPS@
+# @GUI_OPAM_DEPS@
+# @GUI_REMAKE@
+# @OCAMLV@
+# @OPAM_CACHE_FIX@
+# @OPAM_DEPS@
+# @OPAM_SWITCH@
+# @PATCH_FRAMAC@
+# @TEST_FLAGS@
+# @WHY3_CONFIG@
+# @WP_PROVERS@
+# @WP_REPORT@
+# @WP_TEST@
+# @Z3@
+
+
+## TEST_FLAGS:
+## PTESTS_OPTS=-error-code : if all tests pass
+## (nothing) : if tests compile, but fail
+## || true : if tests fail to compile
+
+push-dev: dev dev-gui dev-stripped
+	docker push framac/frama-c:dev
+	docker push framac/frama-c-gui:dev
+	docker push framac/frama-c:dev-stripped
+
+dev: Dockerfile.dev
+	@echo "For 'dev' builds, consider adding ARGS=--no-cache to force"
+	@echo "Docker to rebuild all layers."
+	docker build . -t framac/frama-c:dev --target frama-c-slim -f $^ $(ARGS)
+
+dev-gui: Dockerfile.dev
+	@echo "For 'dev' builds, consider adding ARGS=--no-cache to force"
+	@echo "Docker to rebuild all layers."
+	docker build . -t framac/frama-c-gui:dev --target frama-c-gui-slim -f $^ $(ARGS)
+TARGETS += dev-gui
+
+dev-stripped: Dockerfile.dev
+	@echo "For 'dev' builds, consider adding ARGS=--no-cache to force"
+	@echo "Docker to rebuild all layers."
+	docker build . -t framac/frama-c:dev-stripped --target frama-c-stripped -f $^ $(ARGS)
+TARGETS += dev-stripped
+
+# Note: alpine-3.14 has Z3 version 4.8.11, which is not supported in some
+# versions of Why3, so we remain with alpine-3.13 for now.
+Dockerfile.dev: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.08|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.7|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|opam repository set-url default https://opam.ocaml.org \&\&|g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.2.2.0 \\\
+apron.v0.9.12 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.12 \\\
+ocamlfind.1.8.1 \\\
+ocamlgraph.1.8.8 \\\
+ppx_deriving_yojson.3.5.2 \\\
+why3.1.4.0 \\\
+yojson.1.7.0 \\\
+zarith.1.9.1 \\\
+zmq.5.1.3 \\\
+conf-python-3.1.0.0 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config detect|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@||g' | \
+sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g' | \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests PTESTS_OPTS=-error-code|g' | \
+sed 's|@OCAMLV@|4.08|g' | \
+cat > $@
+
+23.1-stripped: Dockerfile.23.1
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.1-Vanadium.tar.gz $(ARGS)
+TARGETS += 23.1-stripped
+
+23.1: Dockerfile.23.1
+	docker build . -t framac/frama-c:$@ --target frama-c-slim -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.1-Vanadium.tar.gz $(ARGS)
+TARGETS += 23.1
+
+23.1-gui: Dockerfile.23.1
+	docker build . -t framac/frama-c-gui:23.1 --target frama-c-gui-slim -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.1-Vanadium.tar.gz $(ARGS)
+TARGETS += 23.1-gui
+
+push-23.1: 23.1 23.1-gui 23.1-stripped
+	docker push framac/frama-c:23.1
+	docker push framac/frama-c-gui:23.1
+	docker push framac/frama-c:23.1-stripped
+
+Dockerfile.23.1: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.08|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.7|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@||g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.2.2.0 \\\
+apron.v0.9.12 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.12 \\\
+ocamlfind.1.8.1 \\\
+ocamlgraph.1.8.8 \\\
+ppx_deriving_yojson.3.5.2 \\\
+why3.1.4.0 \\\
+yojson.1.7.0 \\\
+zarith.1.9.1 \\\
+zmq.5.1.3 \\\
+conf-python-3.1.0.0 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config detect|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@||g'| \
+sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests|g' | \
+sed 's|@OCAMLV@|4.08|g' | \
+cat > $@
+
+23.0-stripped: Dockerfile.23.0
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.0-Vanadium.tar.gz $(ARGS)
+TARGETS += 23.0-stripped
+
+23.0: Dockerfile.23.0
+	docker build . -t framac/frama-c:$@ --target frama-c-slim -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.0-Vanadium.tar.gz $(ARGS)
+TARGETS += 23.0
+
+23.0-gui: Dockerfile.23.0
+	docker build . -t framac/frama-c-gui:23.0 --target frama-c-gui-slim -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.0-Vanadium.tar.gz $(ARGS)
+TARGETS += 23.0-gui
+
+push-23.0: 23.0 23.0-gui 23.0-stripped
+	docker push framac/frama-c:23.0
+	docker push framac/frama-c-gui:23.0
+	docker push framac/frama-c:23.0-stripped
+
+Dockerfile.23.0: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.08|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.7|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@||g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.2.2.0 \\\
+apron.v0.9.12 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.12 \\\
+ocamlfind.1.8.1 \\\
+ocamlgraph.1.8.8 \\\
+ppx_deriving_yojson.3.5.2 \\\
+why3.1.4.0 \\\
+yojson.1.7.0 \\\
+zarith.1.9.1 \\\
+zmq.5.1.3 \\\
+conf-python-3.1.0.0 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config detect|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@||g'| \
+sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests|g' | \
+sed 's|@OCAMLV@|4.08|g' | \
+cat > $@
+
+22.0-stripped: Dockerfile.22.0
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-22.0-Titanium.tar.gz $(ARGS)
+TARGETS += 22.0-stripped
+
+Dockerfile.22.0: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.08|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.7|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@||g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.2.2.0 \\\
+apron.v0.9.12 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.12 \\\
+ocamlfind.1.8.1 \\\
+ocamlgraph.1.8.8 \\\
+ppx_deriving_yojson.3.5.2 \\\
+why3.1.3.3 \\\
+yojson.1.7.0 \\\
+zarith.1.9.1 \\\
+zmq.5.1.3 \\\
+conf-python-3.1.0.0 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@||g'| \
+sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests|g' | \
+sed 's|@OCAMLV@|4.08|g' | \
+cat > $@
+
+21.1-stripped: Dockerfile.21.1
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-21.1-Scandium.tar.gz $(ARGS)
+TARGETS += 21.1-stripped
+
+Dockerfile.21.1: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.07|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.7|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@||g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.2.0.0 \\\
+apron.v0.9.12 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.12 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+ppx_deriving_yojson.3.5.2 \\\
+why3.1.3.1 \\\
+yojson.1.7.0 \\\
+zarith.1.9.1 \\\
+zmq.5.1.3 \\\
+conf-python-3.1.0.0 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --full-config|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@||g'| \
+sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests|g' | \
+sed 's|@OCAMLV@|4.07|g' | \
+cat > $@
+
+# Note: Frama-C 20.0 and older do not work with GCC >= 10 due to issue with
+# handling of Unicode characters
+20.0-stripped: Dockerfile.20.0
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-20.0-Calcium.tar.gz $(ARGS)
+TARGETS += 20.0-stripped
+
+# Note: cairo2.0.6.1 is used for the GUI because the 0.6.2 requires 'dune-configurator'
+Dockerfile.20.0: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.05|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.6|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.2.0.0 \\\
+apron.20160125 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.11 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+ppx_deriving_yojson.3.5.2 \\\
+why3.1.2.0 \\\
+yojson.1.7.0 \\\
+zarith.1.9.1 \\\
+zmq.5.1.3 \\\
+conf-python-3.1.0.0 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@||g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests \|\| true |g' | \
+sed 's|@OCAMLV@|4.05|g' | \
+cat > $@
+
+19.1-stripped: Dockerfile.19.1
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-19.1-Potassium.tar.gz $(ARGS)
+TARGETS += 19.1-stripped
+
+Dockerfile.19.1: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.05|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.6|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo-free.2.0.0 \\\
+apron.20160125 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.9 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+ppx_deriving_yojson.3.5.2 \\\
+why3.1.2.0 \\\
+yojson.1.7.0 \\\
+zarith.1.7 \\\
+conf-python-3.1.0.0 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@||g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.05|g' | \
+cat > $@
+
+18.0-stripped: Dockerfile.18.0
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-18.0-Argon.tar.gz $(ARGS)
+TARGETS += 18.0-stripped
+
+Dockerfile.18.0: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.05|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+apron.20160125 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.7 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+why3.0.88.3 \\\
+yojson.1.7.0 \\\
+zarith.1.7 \\\
+conf-python-3.1.0.0 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.05|g' | \
+cat > $@
+
+17.1-stripped: Dockerfile.17.1
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Chlorine-20180502.tar.gz $(ARGS)
+TARGETS += 17.1-stripped
+
+# frama-c-script is not shipped from here on, so no need for conf-python
+Dockerfile.17.1: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.05|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+apron.20160125 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.7 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+why3.0.88.3 \\\
+yojson.1.7.0 \\\
+zarith.1.7 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.05|g' | \
+cat > $@
+
+16.0-stripped: Dockerfile.16.0
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Sulfur-20171101.tar.gz $(ARGS)
+TARGETS += 16.0-stripped
+
+# yojson is no longer marked in the opam depends from here on
+Dockerfile.16.0: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.05|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+apron.20160125 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.7 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+why3.0.88.3 \\\
+zarith.1.7 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.05|g' | \
+cat > $@
+
+15.0-stripped: Dockerfile.15.0
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Phosphorus-20170501.tar.gz $(ARGS)
+TARGETS += 15.0-stripped
+
+Dockerfile.15.0: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+apron.20160125 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.7 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+why3.0.88.3 \\\
+zarith.1.7 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.02|g' | \
+cat > $@
+
+14.0-stripped: Dockerfile.14.0
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Silicon-20161101.tar.gz $(ARGS)
+TARGETS += 14.0-stripped
+
+Dockerfile.14.0: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+apron.20160125 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.7 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+why3.0.88.3 \\\
+zarith.1.7 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's#@WP_TEST@#! ( frama-c -wp wp_usage/reads.i -wp-timeout 1 -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" )#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.02|g' | \
+cat > $@
+
+13.0-stripped: Dockerfile.13.0
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Aluminium-20160502.tar.gz $(ARGS)
+TARGETS += 13.0-stripped
+
+Dockerfile.13.0: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+apron.20160125 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.7 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+why3.0.88.3 \\\
+zarith.1.7 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's#@WP_TEST@#! ( frama-c -wp wp_usage/reads.i -wp-timeout 1 -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" )#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.02|g' | \
+cat > $@
+
+12.0-stripped: Dockerfile.12.0
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Magnesium-20151002.tar.gz $(ARGS)
+TARGETS += 12.0-stripped
+
+# apron is not shipped with Frama-C, from here on
+Dockerfile.12.0: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+conf-graphviz.0.1 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+why3.0.88.3 \\\
+zarith.1.7 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's#@WP_TEST@#! ( frama-c -wp wp_usage/reads.i -wp-timeout 1 -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" )#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.02|g' | \
+cat > $@
+
+11.0-stripped: Dockerfile.11.0
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Sodium-20150201.tar.gz $(ARGS)
+TARGETS += 11.0-stripped
+
+Dockerfile.11.0: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+conf-graphviz.0.1 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+why3.0.88.3 \\\
+zarith.1.7 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's#@WP_TEST@# ! ( printf "int g;\\n//@assigns g;\\nvoid f(){g = 1;}\\nint main() {f(); return g;}" > /tmp/simple.c; frama-c -wp /tmp/simple.c -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" ); rm -f /tmp/simple.c#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.02|g' | \
+cat > $@
+
+10.1-stripped: Dockerfile.10.1
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Neon-20140301.tar.gz $(ARGS)
+TARGETS += 10.1-stripped
+
+# Starting from this version, due to the usage of a recent GCC, we need to
+# remove the `-no-pic` flag that was passed when compiling buckx_c.c.
+# Otherwise, we get the dreaded "relocation error".
+Dockerfile.10.1: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+conf-graphviz.0.1 \\\
+ocamlfind.1.8.0 \\\
+why3-base.0.88.3 \\\
+zarith.1.7 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's#@WP_TEST@# ! ( printf "int g;\\n//@assigns g;\\nvoid f(){g = 1;}\\nint main() {f(); return g;}" > /tmp/simple.c; frama-c -wp /tmp/simple.c -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" ); rm -f /tmp/simple.c#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.02|g' | \
+	cat > $@
+
+10.0-stripped: Dockerfile.10.0
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Neon-20140301.tar.gz $(ARGS)
+TARGETS += 10.0-stripped
+
+# Starting from this version, due to the usage of a recent GCC, we need to
+# remove the `-no-pic` flag that was passed when compiling buckx_c.c.
+# Otherwise, we get the dreaded "relocation error".
+Dockerfile.10.0: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+conf-graphviz.0.1 \\\
+ocamlfind.1.8.0 \\\
+why3-base.0.88.3 \\\
+zarith.1.7 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's#@WP_TEST@# ! ( printf "int g;\\n//@assigns g;\\nvoid f(){g = 1;}\\nint main() {f(); return g;}" > /tmp/simple.c; frama-c -wp /tmp/simple.c -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" ); rm -f /tmp/simple.c#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.02|g' | \
+cat > $@
+
+9.2-stripped: Dockerfile.9.2
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Fluorine-20130601.tar.gz $(ARGS)
+TARGETS += 9.2-stripped
+
+# configure.in had a bug detecting Make versions > 4; instead of applying
+# the proper fix (which would be long), we simply "cheat" by replacing '81'
+# (from "make 3.81") with "1".
+Dockerfile.9.2: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|opam switch create 3.12.1|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.01 \\\
+conf-autoconf.0.1 \\\
+conf-graphviz.0.1 \\\
+ocamlfind.1.7.3-1 \\\
+why3-base.0.85 \\\
+zarith.1.7|' | \
+sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile \&\& sed -i "s/ 81/  1/" configure.in|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's#@WP_TEST@# ! ( printf "int g;\\n//@assigns g;\\nvoid f(){g = 1;}\\nint main() {f(); return g;}" > /tmp/simple.c; frama-c -wp /tmp/simple.c -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" ); rm -f /tmp/simple.c#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|3.12.1|g' | \
+cat > $@
+
+8.0-stripped: Dockerfile.8.0
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Oxygen-20120901.tar.gz $(ARGS)
+TARGETS += 8.0-stripped
+
+Dockerfile.8.0: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|opam switch create 3.12.1|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.01 \\\
+conf-autoconf.0.1 \\\
+conf-graphviz.0.1 \\\
+ocamlfind.1.7.3-1 \\\
+why3-base.0.85 \\\
+zarith.1.7|' | \
+sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile \&\& sed -i "s/ 81/  1/" configure.in|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's#@WP_TEST@# ! ( printf "int g;\\n//@assigns g;\\nvoid f(){g = 1;}\\nint main() {f(); return g;}" > /tmp/simple.c; frama-c -wp /tmp/simple.c -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" ); rm -f /tmp/simple.c#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|3.12.1|g' | \
+cat > $@
+
+7.0-stripped: Dockerfile.7.0
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Nitrogen-20111001.tar.gz $(ARGS)
+TARGETS += 7.0-stripped
+
+# For some reason, lablgtk2 files are installed in a directory other than the
+# one where Frama-C's configure expects them; the simplest fix seems to be
+# moving the files to the expected directory.
+Dockerfile.7.0: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|opam switch create 3.12.1|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.01 \\\
+conf-autoconf.0.1 \\\
+conf-graphviz.0.1 \\\
+ocamlfind.1.7.3-1 \\\
+why3-base.0.85 \\\
+zarith.1.7|' | \
+sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile \&\& sed -i "s/ 81/  1/" configure.in|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's#@WP_TEST@# ! ( printf "int g;\\n//@assigns g;\\nvoid f(){g = 1;}\\nint main() {f(); return g;}" > /tmp/simple.c; frama-c -wp /tmp/simple.c -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" ); rm -f /tmp/simple.c#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|lablgtk conf-gnomecanvas conf-gtksourceview \&\& mv /home/opam/.opam/3.12.1/lib/lablgtk2/ /home/opam/.opam/3.12.1/lib/ocaml/|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|3.12.1|g' | \
+cat > $@
+
+6.0-stripped: Dockerfile.6.0
+	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Carbon-20110201.tar.gz $(ARGS)
+TARGETS += 6.0-stripped
+
+# TODO: find out how to make WP installation work; following the instructions, the
+# dynamic version fails during ./configure, with:
+# ./configure: export: line 1666: ENABLE_USAGE:_FRAMA_C_[OPTIONS_AND_FILES...]: bad variable name
+# And the static version (putting in src/wp) fails with:
+# src/wp/Makefile:46: *** recipe commences before first target.  Stop.
+Dockerfile.6.0: Makefile Dockerfile.template env.template
+	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@CVC4@||g' | \
+sed 's|@CVC4_VERSION@||g' | \
+sed 's|@Z3@||g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|opam switch create 3.12.1|g' | \
+sed 's|@OPAM_DEPS@|\\\
+conf-autoconf.0.1 \\\
+conf-graphviz.0.1 \\\
+ocamlfind.1.7.3-1|' | \
+sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile \&\& sed -i "s/ 81/  1/" configure.in|g' | \
+sed 's|@WP_REPORT@||g'| \
+sed 's|@WHY3_CONFIG@|true|g' | \
+sed 's#@WP_TEST@#true#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|lablgtk conf-gnomecanvas conf-gtksourceview \&\& mv /home/opam/.opam/3.12.1/lib/lablgtk2/ /home/opam/.opam/3.12.1/lib/ocaml/|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& autoconf \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|3.12.1|g' | \
+cat > $@
+
+#5.0-stripped: Dockerfile.5.0
+#	docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+#--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Boron-20100401-why-2.24.tar.gz $(ARGS)
+#TARGETS += 5.0-stripped
+#
+# Re-running the makefile for the GUI seems to cause issues,
+# so we restart everything from the archive
+# TODO: fix build and proceed with older Frama-C versions
+# Dockerfile.5.0: Makefile Dockerfile.template env.template
+# 	sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+# sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+# sed 's|@ENV@|$(shell cat env.template)|g' | \
+# sed 's|@CVC4@||g' | \
+# sed 's|@CVC4_VERSION@||g' | \
+# sed 's|@Z3@||g' | \
+# sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+# sed 's|@OPAM_SWITCH@|opam switch create 3.12.1|g' | \
+# sed 's|@OPAM_DEPS@|\\\
+# conf-autoconf.0.1 \\\
+# conf-graphviz.0.1 \\\
+# ocamlfind.1.7.3-1 \\\
+# zarith.1.7|' | \
+# sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile \&\& sed -i "s/ 81/  1/" configure.in|g' | \
+# sed 's|@WP_REPORT@||g'| \
+# sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+# sed 's#@WP_TEST@#true#g' | \
+# sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+# sed 's|@GUI_OPAM_DEPS@|lablgtk conf-gnomecanvas conf-gtksourceview \&\& mv /home/opam/.opam/3.12.1/lib/lablgtk2/ /home/opam/.opam/3.12.1/lib/ocaml/|g'| \
+# sed 's|@GUI_REMAKE@|rm -rf * \&\& wget https://www.frama-c.com/download/frama-c-Boron-20100401-why-2.24.tar.gz \&\& tar xvf frama-c-Boron-20100401-why-2.24.tar.gz --strip 1 \&\& cd /frama-c \&\& sed -i s/-fno-pic// Makefile \&\& sed -i "s/ 81/  1/" configure.in \&\& autoconf \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+# sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+# sed 's|@OCAMLV@|3.12.1|g' | \
+# cat > $@
diff --git a/devel_tools/docker/README.md b/devel_tools/docker/README.md
index 0a1c8e049e40b74e21466ee9b87be75a27475901..e56c8d81b42a389ee8a62c5e772b86ffb3a72c17 100644
--- a/devel_tools/docker/README.md
+++ b/devel_tools/docker/README.md
@@ -1,29 +1,60 @@
-Docker images for Frama-C
-=========================
+# Frama-C Docker images
 
-- To build a new image (slim, without Frama-C sources nor tests):
+Frama-C Docker images are currently based on Alpine Linux,
+using opam's Docker images
+(from https://hub.docker.com/r/ocaml/opam/).
 
-        cd <tag>
-        docker build . --target base -t framac/frama-c:<tag>
+The user is `opam` and it has sudo rights.
+To add packages, run `sudo apk add <package>`.
 
-- To run an interactive shell:
+## Using the Makefile
 
-        docker run -it framac/frama-c:<tag>
+The `Makefile` contains several targets and templates to build most
+Frama-C versions. For each version, there are three images: one
+for the command-line version `frama-c`; a stripped-down version of the former,
+for a slimmer image, but which does not allow recompilation of Frama-C
+or of any external plugin; and a third image including the graphical
+interface (`frama-c-gui`), to be used with Singularity or other tools enabling
+graphical interfaces from within a Docker image.
 
-- To push to Docker Hub (requires access to the `framac/frama-c` repository):
+Run `make` to get a list of targets.
 
-        docker push framac/frama-c:<tag>
+If you have access to the Frama-C Docker Hub, you can also run a
+`push-<version>` target to upload images related to that version to
+the Docker Hub.
 
-- To build an image containing Frama-C sources (downloaded from the .tar.gz, in
-  directory `/root`):
+## Commands to generate images
 
-        cd <tag>
-        docker build . --build-arg with_source=yes \
-          -t framac/frama-c:<tag>-with-source
+Some commands in this section are those used by the above Makefile;
+others allow creating different images (e.g. with the Frama-C sources)
+which are not directly available as Makefile targets.
 
-- To run Frama-C tests (and remove unnecessary image later):
+- Build slim development image (from public Git master branch):
 
-        cd <tag>
-        docker build . --build-arg with_source=yes --build-arg with_test=yes \
-          -t framac/frama-c:<tag>-with-test
-        docker image rm framac/frama-c:<tag>-with-test
+        docker build . -t framac/frama-c:dev --target frama-c-slim
+
+- Build slim development image with GUI:
+
+        docker build . -t framac/frama-c-gui:dev --target frama-c-gui-slim
+
+- Build stripped (minimal) version:
+
+        docker build . -t framac/frama-c:dev-stripped --target frama-c-stripped
+
+- Build image from archive (note: it _must_ be named `frama-c-<something>.tar.gz`, where
+  `<something>` may be a version number, codename, etc:
+
+        docker build . -t framac/frama-c:dev --target frama-c-slim --build-arg=from_archive=frama-c-<version>.tar.gz
+
+- Build image containing Frama-C's source code in `/frama-c` (without and with GUI):
+
+        docker build . -t framac/frama-c-source:dev --target frama-c
+        docker build . -t framac/frama-c-gui-source:dev --target frama-c-gui
+
+- Start Singularity instance
+
+        singularity instance start docker-daemon:framac/frama-c-gui:dev <instance name>
+
+- Run command with Singularity instance
+
+        singularity exec instance://<instance name> <command with args>
diff --git a/devel_tools/docker/cvc4.template b/devel_tools/docker/cvc4.template
new file mode 100644
index 0000000000000000000000000000000000000000..951aa4ea617f12db51d78f5387aadab0b4c824d1
--- /dev/null
+++ b/devel_tools/docker/cvc4.template
@@ -0,0 +1,5 @@
+## CVC4 @CVC4_VERSION@\n
+RUN \\\n
+wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-@CVC4_VERSION@-x86_64-linux-opt -O cvc4-@CVC4_VERSION@ \&\& \\\n
+chmod a+x cvc4-@CVC4_VERSION@ \&\& \\\n
+sudo mv cvc4-@CVC4_VERSION@ /usr/local/bin/
diff --git a/devel_tools/docker/env.template b/devel_tools/docker/env.template
new file mode 100644
index 0000000000000000000000000000000000000000..14b2666ef03ba5ae6f2ce6f8d718eb9e7b6145b6
--- /dev/null
+++ b/devel_tools/docker/env.template
@@ -0,0 +1,11 @@
+ENV OPAM_SWITCH_PREFIX "/home/opam/.opam/@OCAMLV@"\n
+ENV CAML_LD_LIBRARY_PATH "/home/opam/.opam/@OCAMLV@/lib/stublibs:/home/opam/.opam/@OCAMLV@/lib/ocaml/stublibs:/home/opam/.opam/@OCAMLV@/lib/ocaml"\n
+ENV OCAML_TOPLEVEL_PATH "/home/opam/.opam/@OCAMLV@/lib/toplevel"\n
+ENV MANPATH "$MANPATH:/home/opam/.opam/@OCAMLV@/man"\n
+ENV PATH "/home/opam/.opam/@OCAMLV@/bin:$PATH"\n
+\n
+## Avoid prompts for time zone\n
+ENV TZ=Europe/Paris\n
+\n
+## Fix issue with libGL on Windows\n
+ENV LIBGL_ALWAYS_INDIRECT=1\n
diff --git a/devel_tools/docker/frama-c.18.0/Dockerfile b/devel_tools/docker/frama-c.18.0/Dockerfile
deleted file mode 100644
index d3582aa0d4361c90c73a31c39b5023c741386973..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.18.0/Dockerfile
+++ /dev/null
@@ -1,63 +0,0 @@
-FROM debian:buster as base
-
-# Install non-OCaml dependencies + opam
-RUN apt-get update && apt-get install -y \
-    cvc4 \
-    opam \
-    z3 \
-    && rm -rf /var/lib/apt/lists/*
-
-RUN opam init --disable-sandboxing --compiler=ocaml-base-compiler.4.05.0 -y
-
-# "RUN eval $(opam env)" does not work, so we manually set its variables
-ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.05.0"
-ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.05.0/lib/stublibs:/root/.opam/ocaml-base-compiler.4.05.0/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.05.0/lib/ocaml"
-ENV OCAML_TOPLEVEL_PATH "/root/.opam/ocaml-base-compiler.4.05.0/lib/toplevel"
-ENV MANPATH "$MANPATH:/root/.opam/ocaml-base-compiler.4.05.0/man"
-ENV PATH "/root/.opam/ocaml-base-compiler.4.05.0/bin:$PATH"
-
-RUN opam update -y && opam install depext -y
-
-# Install packages from reference configuration
-RUN apt-get update && opam update -y && opam depext --install -y --verbose \
-    alt-ergo.1.30 \
-    apron.20160125 \
-    conf-graphviz.0.1 \
-    mlgmpidl.1.2.7 \
-    ocamlfind.1.8.0 \
-    ocamlgraph.1.8.8 \
-    why3.0.88.3 \
-    yojson.1.4.1 \
-    zarith.1.7 \
-    && rm -rf /var/lib/apt/lists/*
-
-RUN why3 config --detect-provers
-
-# with_source: keep Frama-C sources
-ARG with_source=no
-
-RUN cd /root && \
-    wget http://frama-c.com/download/frama-c-18.0-Argon.tar.gz && \
-    tar xvf frama-c-*.tar.gz && \
-    (cd frama-c-* && \
-        ./configure --disable-gui && \
-        make -j && \
-        make install \
-    ) && \
-    rm -f frama-c-*.tar.gz && \
-    [ "${with_source}" != "no" ] || rm -rf frama-c-*
-
-# with_test: run Frama-C tests; requires "with_source=yes"
-ARG with_test=no
-
-RUN if [ "${with_test}" != "no" ]; then \
-       apt-get update && \
-       opam update -y && opam depext --install -y \
-           conf-python-3.1.0.0 \
-           conf-time.1 \
-           --verbose \
-        && \
-        rm -rf /var/lib/apt/lists/* && \
-        cd /root/frama-c-* && \
-        make tests; \
-    fi
diff --git a/devel_tools/docker/frama-c.19.1/Dockerfile b/devel_tools/docker/frama-c.19.1/Dockerfile
deleted file mode 100644
index b3c7d6d97ece64c7186580f0c5937066179943a8..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.19.1/Dockerfile
+++ /dev/null
@@ -1,63 +0,0 @@
-FROM debian:buster as base
-
-# Install non-OCaml dependencies + opam
-RUN apt-get update && apt-get install -y \
-    cvc4 \
-    opam \
-    z3 \
-    && rm -rf /var/lib/apt/lists/*
-
-RUN opam init --disable-sandboxing --compiler=ocaml-base-compiler.4.05.0 -y
-
-# "RUN eval $(opam env)" does not work, so we manually set its variables
-ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.05.0"
-ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.05.0/lib/stublibs:/root/.opam/ocaml-base-compiler.4.05.0/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.05.0/lib/ocaml"
-ENV OCAML_TOPLEVEL_PATH "/root/.opam/ocaml-base-compiler.4.05.0/lib/toplevel"
-ENV MANPATH "$MANPATH:/root/.opam/ocaml-base-compiler.4.05.0/man"
-ENV PATH "/root/.opam/ocaml-base-compiler.4.05.0/bin:$PATH"
-
-RUN opam update -y && opam install depext -y
-
-# Install packages from reference configuration
-RUN apt-get update && opam update -y && opam depext --install -y --verbose \
-    alt-ergo-free.2.0.0 \
-    apron.20160125 \
-    conf-graphviz.0.1 \
-    mlgmpidl.1.2.9 \
-    ocamlfind.1.8.0 \
-    ocamlgraph.1.8.8 \
-    why3.1.2.0 \
-    yojson.1.4.1 \
-    zarith.1.7 \
-    && rm -rf /var/lib/apt/lists/*
-
-RUN why3 config --detect-provers
-
-# with_source: keep Frama-C sources
-ARG with_source=no
-
-RUN cd /root && \
-    wget http://frama-c.com/download/frama-c-19.1-Potassium.tar.gz && \
-    tar xvf frama-c-*.tar.gz && \
-    (cd frama-c-* && \
-        ./configure --disable-gui && \
-        make -j && \
-        make install \
-    ) && \
-    rm -f frama-c-*.tar.gz && \
-    [ "${with_source}" != "no" ] || rm -rf frama-c-*
-
-# with_test: run Frama-C tests; requires "with_source=yes"
-ARG with_test=no
-
-RUN if [ "${with_test}" != "no" ]; then \
-       apt-get update && \
-       opam update -y && opam depext --install -y \
-           conf-python-3.1.0.0 \
-           conf-time.1 \
-           --verbose \
-        && \
-        rm -rf /var/lib/apt/lists/* && \
-        cd /root/frama-c-* && \
-        make tests; \
-    fi
diff --git a/devel_tools/docker/frama-c.20.0/Dockerfile b/devel_tools/docker/frama-c.20.0/Dockerfile
deleted file mode 100644
index 4f4927b98e810437cfb460d79b96f575775e6a3d..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.20.0/Dockerfile
+++ /dev/null
@@ -1,64 +0,0 @@
-FROM debian:buster as base
-
-# Install non-OCaml dependencies + opam
-RUN apt-get update && apt-get install -y \
-    cvc4 \
-    opam \
-    z3 \
-    && rm -rf /var/lib/apt/lists/*
-
-RUN opam init --disable-sandboxing --compiler=ocaml-base-compiler.4.05.0 -y
-
-# "RUN eval $(opam env)" does not work, so we manually set its variables
-ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.05.0"
-ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.05.0/lib/stublibs:/root/.opam/ocaml-base-compiler.4.05.0/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.05.0/lib/ocaml"
-ENV OCAML_TOPLEVEL_PATH "/root/.opam/ocaml-base-compiler.4.05.0/lib/toplevel"
-ENV MANPATH "$MANPATH:/root/.opam/ocaml-base-compiler.4.05.0/man"
-ENV PATH "/root/.opam/ocaml-base-compiler.4.05.0/bin:$PATH"
-
-RUN opam update -y && opam install depext -y
-
-# Install packages from reference configuration
-RUN apt-get update && opam update -y && opam depext --install -y --verbose \
-    alt-ergo.2.0.0 \
-    apron.20160125 \
-    conf-graphviz.0.1 \
-    mlgmpidl.1.2.11 \
-    ocamlfind.1.8.0 \
-    ocamlgraph.1.8.8 \
-    ppx_deriving_yojson.3.5.2 \
-    why3.1.2.0 \
-    yojson.1.7.0 \
-    zarith.1.9.1 \
-    && rm -rf /var/lib/apt/lists/*
-
-RUN why3 config --detect-provers
-
-# with_source: keep Frama-C sources
-ARG with_source=no
-
-RUN cd /root && \
-    wget http://frama-c.com/download/frama-c-20.0-Calcium.tar.gz && \
-    tar xvf frama-c-*.tar.gz && \
-    (cd frama-c-* && \
-        ./configure --disable-gui && \
-        make -j && \
-        make install \
-    ) && \
-    rm -f frama-c-*.tar.gz && \
-    [ "${with_source}" != "no" ] || rm -rf frama-c-*
-
-# with_test: run Frama-C tests; requires "with_source=yes"
-ARG with_test=no
-
-RUN if [ "${with_test}" != "no" ]; then \
-       apt-get update && \
-       opam update -y && opam depext --install -y \
-           conf-python-3.1.0.0 \
-           conf-time.1 \
-           --verbose \
-        && \
-        rm -rf /var/lib/apt/lists/* && \
-        cd /root/frama-c-* && \
-        make tests; \
-    fi
diff --git a/devel_tools/docker/frama-c.21.0/Dockerfile b/devel_tools/docker/frama-c.21.0/Dockerfile
deleted file mode 100644
index 443601c70b177f1768639d02c9148d8f6a477eab..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.21.0/Dockerfile
+++ /dev/null
@@ -1,65 +0,0 @@
-FROM debian:buster as base
-
-# Install non-OCaml dependencies + opam
-RUN apt-get update && apt-get install -y \
-    cvc4 \
-    opam \
-    z3 \
-    && rm -rf /var/lib/apt/lists/*
-
-RUN opam init --disable-sandboxing --compiler=ocaml-base-compiler.4.07.1 -y
-
-# "RUN eval $(opam env)" does not work, so we manually set its variables
-ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.07.1"
-ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.07.1/lib/stublibs:/root/.opam/ocaml-base-compiler.4.07.1/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.07.1/lib/ocaml"
-ENV OCAML_TOPLEVEL_PATH "/root/.opam/ocaml-base-compiler.4.07.1/lib/toplevel"
-ENV MANPATH "$MANPATH:/root/.opam/ocaml-base-compiler.4.07.1/man"
-ENV PATH "/root/.opam/ocaml-base-compiler.4.07.1/bin:$PATH"
-
-RUN opam update -y && opam install depext -y
-
-# Install packages from reference configuration
-RUN apt-get update && opam update -y && opam depext --install -y --verbose \
-    alt-ergo.2.0.0 \
-    apron.v0.9.12 \
-    conf-graphviz.0.1 \
-    mlgmpidl.1.2.12 \
-    ocamlfind.1.8.0 \
-    ocamlgraph.1.8.8 \
-    ppx_deriving_yojson.3.5.2 \
-    why3.1.3.1 \
-    yojson.1.7.0 \
-    zarith.1.9.1 \
-    zmq.5.1.3 \
-    && rm -rf /var/lib/apt/lists/*
-
-RUN why3 config --full-config
-
-# with_source: keep Frama-C sources
-ARG with_source=no
-
-RUN cd /root && \
-    wget http://frama-c.com/download/frama-c-21.0-Scandium.tar.gz && \
-    tar xvf frama-c-*.tar.gz && \
-    (cd frama-c-* && \
-        ./configure --disable-gui && \
-        make -j && \
-        make install \
-    ) && \
-    rm -f frama-c-*.tar.gz && \
-    [ "${with_source}" != "no" ] || rm -rf frama-c-*
-
-# with_test: run Frama-C tests; requires "with_source=yes"
-ARG with_test=no
-
-RUN if [ "${with_test}" != "no" ]; then \
-       apt-get update && \
-       opam update -y && opam depext --install -y \
-           conf-python-3.1.0.0 \
-           conf-time.1 \
-           --verbose \
-        && \
-        rm -rf /var/lib/apt/lists/* && \
-        cd /root/frama-c-* && \
-        make tests; \
-    fi
diff --git a/devel_tools/docker/frama-c.21.1/Dockerfile b/devel_tools/docker/frama-c.21.1/Dockerfile
deleted file mode 100644
index 90a6e92fe6b801296c1f53d608aac5cd16a4171a..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.21.1/Dockerfile
+++ /dev/null
@@ -1,65 +0,0 @@
-FROM debian:buster as base
-
-# Install non-OCaml dependencies + opam
-RUN apt-get update && apt-get install -y \
-    cvc4 \
-    opam \
-    z3 \
-    && rm -rf /var/lib/apt/lists/*
-
-RUN opam init --disable-sandboxing --compiler=ocaml-base-compiler.4.07.1 -y
-
-# "RUN eval $(opam env)" does not work, so we manually set its variables
-ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.07.1"
-ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.07.1/lib/stublibs:/root/.opam/ocaml-base-compiler.4.07.1/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.07.1/lib/ocaml"
-ENV OCAML_TOPLEVEL_PATH "/root/.opam/ocaml-base-compiler.4.07.1/lib/toplevel"
-ENV MANPATH "$MANPATH:/root/.opam/ocaml-base-compiler.4.07.1/man"
-ENV PATH "/root/.opam/ocaml-base-compiler.4.07.1/bin:$PATH"
-
-RUN opam update -y && opam install depext -y
-
-# Install packages from reference configuration
-RUN apt-get update && opam update -y && opam depext --install -y --verbose \
-    alt-ergo.2.0.0 \
-    apron.v0.9.12 \
-    conf-graphviz.0.1 \
-    mlgmpidl.1.2.12 \
-    ocamlfind.1.8.0 \
-    ocamlgraph.1.8.8 \
-    ppx_deriving_yojson.3.5.2 \
-    why3.1.3.1 \
-    yojson.1.7.0 \
-    zarith.1.9.1 \
-    zmq.5.1.3 \
-    && rm -rf /var/lib/apt/lists/*
-
-RUN why3 config --full-config
-
-# with_source: keep Frama-C sources
-ARG with_source=no
-
-RUN cd /root && \
-    wget http://frama-c.com/download/frama-c-21.1-Scandium.tar.gz && \
-    tar xvf frama-c-*.tar.gz && \
-    (cd frama-c-* && \
-        ./configure --disable-gui && \
-        make -j && \
-        make install \
-    ) && \
-    rm -f frama-c-*.tar.gz && \
-    [ "${with_source}" != "no" ] || rm -rf frama-c-*
-
-# with_test: run Frama-C tests; requires "with_source=yes"
-ARG with_test=no
-
-RUN if [ "${with_test}" != "no" ]; then \
-       apt-get update && \
-       opam update -y && opam depext --install -y \
-           conf-python-3.1.0.0 \
-           conf-time.1 \
-           --verbose \
-        && \
-        rm -rf /var/lib/apt/lists/* && \
-        cd /root/frama-c-* && \
-        make tests; \
-    fi
diff --git a/devel_tools/docker/frama-c.22.0/Dockerfile b/devel_tools/docker/frama-c.22.0/Dockerfile
deleted file mode 100644
index d1e25df7a9d7df30b4b0cba10fccfc169a3dec7f..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.22.0/Dockerfile
+++ /dev/null
@@ -1,66 +0,0 @@
-FROM debian:buster as base
-
-# Install non-OCaml dependencies + opam
-RUN apt-get update && apt-get install -y \
-    cvc4 \
-    opam \
-    z3 \
-    && rm -rf /var/lib/apt/lists/*
-
-RUN opam init --disable-sandboxing --compiler=ocaml-base-compiler.4.08.1 -y
-
-# "RUN eval $(opam env)" does not work, so we manually set its variables
-ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.08.1"
-ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.08.1/lib/stublibs:/root/.opam/ocaml-base-compiler.4.08.1/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.08.1/lib/ocaml"
-ENV OCAML_TOPLEVEL_PATH "/root/.opam/ocaml-base-compiler.4.08.1/lib/toplevel"
-ENV MANPATH "$MANPATH:/root/.opam/ocaml-base-compiler.4.08.1/man"
-ENV PATH "/root/.opam/ocaml-base-compiler.4.08.1/bin:$PATH"
-
-RUN opam update -y && opam install depext -y
-
-# Install packages from reference configuration
-# Note: Python and time packages are only required for tests, but if so,
-# they need to be present before running './configure'
-RUN apt-get update && opam update -y && opam depext --install -y --verbose \
-    alt-ergo.2.2.0 \
-    apron.v0.9.12 \
-    conf-graphviz.0.1 \
-    mlgmpidl.1.2.12 \
-    ocamlfind.1.8.1 \
-    ocamlgraph.1.8.8 \
-    ppx_deriving_yojson.3.5.2 \
-    why3.1.3.3 \
-    yojson.1.7.0 \
-    zarith.1.9.1 \
-    zmq.5.1.3 \
-    conf-python-3.1.0.0 \
-    conf-time.1 \
-    && rm -rf /var/lib/apt/lists/*
-
-RUN why3 config --detect
-
-# with_source: keep Frama-C sources
-ARG with_source=no
-
-RUN cd /root && \
-    wget http://frama-c.com/download/frama-c-22.0-Titanium.tar.gz && \
-    tar xvf frama-c-*.tar.gz && \
-    (cd frama-c-* && \
-        ./configure --disable-gui && \
-        make -j && \
-        make install \
-    ) && \
-    rm -f frama-c-*.tar.gz && \
-    ([ "${with_source}" != "no" ] || rm -rf frama-c-*)
-
-# with_test: run Frama-C tests; requires "with_source=yes"
-ARG with_test=no
-
-# run general tests, then test that WP can see external provers
-RUN if [ "${with_test}" != "no" ]; then \
-        cd /root/frama-c-* && \
-        make tests PTESTS_OPTS=-error-code && \
-        (cd src/plugins/wp/tests/ && \
-         frama-c -wp wp_gallery/binary-multiplication-without-overflow.c \
-         -wp-prover alt-ergo,cvc4); \
-    fi
diff --git a/devel_tools/docker/frama-c.custom/.gitignore b/devel_tools/docker/frama-c.custom/.gitignore
deleted file mode 100644
index 028757c13527bdb23c649f219e11e1a4db317087..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.custom/.gitignore
+++ /dev/null
@@ -1,2 +0,0 @@
-# ignore an eventual frama-c subfolder in this directory
-frama-c
diff --git a/devel_tools/docker/frama-c.custom/Dockerfile b/devel_tools/docker/frama-c.custom/Dockerfile
deleted file mode 100644
index 4eb330c4d69c7dfb1134868b877f2d761193a77c..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.custom/Dockerfile
+++ /dev/null
@@ -1,70 +0,0 @@
-FROM debian:sid as base
-
-# Install non-OCaml dependencies + opam
-RUN apt-get update && apt-get install -y \
-    opam \
-    z3 \
-    && rm -rf /var/lib/apt/lists/*
-
-RUN opam init --disable-sandboxing --compiler=ocaml-base-compiler.4.08.1 -y
-
-# "RUN eval $(opam env)" does not work, so we manually set its variables
-ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.08.1"
-ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.08.1/lib/stublibs:/root/.opam/ocaml-base-compiler.4.08.1/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.08.1/lib/ocaml"
-ENV OCAML_TOPLEVEL_PATH "/root/.opam/ocaml-base-compiler.4.08.1/lib/toplevel"
-ENV MANPATH "$MANPATH:/root/.opam/ocaml-base-compiler.4.08.1/man"
-ENV PATH "/root/.opam/ocaml-base-compiler.4.08.1/bin:$PATH"
-
-RUN opam update -y && opam install depext -y
-
-# Install packages from reference configuration
-# Note: Python and time packages are only required for tests, but if so,
-# they need to be present before running './configure'
-RUN apt-get update && opam update -y && opam depext --install -y --verbose \
-    alt-ergo.2.2.0 \
-    apron.v0.9.12 \
-    conf-graphviz.0.1 \
-    mlgmpidl.1.2.12 \
-    ocamlfind.1.8.1 \
-    ocamlgraph.1.8.8 \
-    ppx_deriving_yojson.3.5.2 \
-    why3.1.3.3 \
-    yojson.1.7.0 \
-    zarith.1.9.1 \
-    zmq.5.1.3 \
-    conf-python-3.1.0.0 \
-    conf-time.1 \
-    && rm -rf /var/lib/apt/lists/*
-
-# Note: Debian's CVC is too recent for Why3, so we do not install the Debian
-# package; instead, we download its binary and add it to a directory in PATH.
-RUN wget https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt -O /usr/local/bin/cvc4
-RUN chmod a+x /usr/local/bin/cvc4
-
-RUN why3 config --detect
-
-# with_source: keep Frama-C sources
-ARG with_source=no
-
-# copies a cloned, non-public Frama-C
-COPY frama-c /root/frama-c
-
-RUN cd /root && \
-    (cd frama-c && \
-        autoconf && ./configure --disable-gui && \
-        make -j && \
-        make install \
-    ) && \
-    ([ "${with_source}" != "no" ] || rm -rf frama-c)
-
-# with_test: run Frama-C tests; requires "with_source=yes"
-ARG with_test=no
-
-# run general tests, then test that WP can see external provers
-RUN if [ "${with_test}" != "no" ]; then \
-        cd /root/frama-c && \
-        make tests PTESTS_OPTS=-error-code && \
-        (cd src/plugins/wp/tests/ && \
-         frama-c -wp wp_gallery/binary-multiplication-without-overflow.c \
-         -wp-prover alt-ergo,cvc4); \
-    fi
diff --git a/devel_tools/docker/frama-c.custom/README.md b/devel_tools/docker/frama-c.custom/README.md
deleted file mode 100644
index 6ce5f94c37e0974215e3678c0512874626431df6..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.custom/README.md
+++ /dev/null
@@ -1,46 +0,0 @@
-Building a Frama-C Docker image with a custom git clone
-=========================================================================
-
-In order to build a Frama-C Docker image with custom plug-ins, or using
-a custom git repository, do the following:
-
-1. Locally clone Frama-C into the `frama-c` directory, e.g. via
-
-        git clone git@frama-c.com:frama-c/frama-c.git
-
-   If needed, modify the clone to add other plug-ins and/or files inside
-   `frama-c`.
-
-2. If needed, add Debian and opam prerequisites to the appropriate lines in the
-   Dockerfile (after `apt update` and before removing the `apt` cache).
-   If you need to change the opam version, also edit the `ENV` lines.
-
-3. For a "minimal" image (with installed Frama-C, but no source code), run:
-
-        docker build . -t fc-custom # or another tag if you prefer
-
-    For an image with the Frama-C source code (in `/root/frama-c`), run:
-
-        docker build . -t fc-custom-with-source --build-arg=with_source=yes
-
-    For an image with source code + tests (e.g. which runs `make tests`), run:
-
-        docker build . -t fc-custom-with-test --build-arg=with_source=yes --build-arg=with_test=yes
-
-4. In all cases, after building the image, run it with:
-
-        docker run -it fc-custom # or another tag
-
-Frama-C will be installed and its sources will be in `/root/frama-c`.
-
-### Notes
-
-1. If you keep the sources, remember that the Docker image may contain
-   non-public code.
-
-2. Using different tags for the `*-with-source` and `*-with-test` images may
-   allow layer reuse by Docker.
-
-3. If you need files outside `/root/frama-c`, add them to the directory
-   containing this README and add a `COPY` instruction to the `Dockerfile`,
-   e.g. `COPY dir /root/dir`.
diff --git a/devel_tools/docker/frama-c.dev/Dockerfile b/devel_tools/docker/frama-c.dev/Dockerfile
deleted file mode 100644
index 0907e4d0438ab1078fee39227f1ed2fb0bba0aa2..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.dev/Dockerfile
+++ /dev/null
@@ -1,68 +0,0 @@
-FROM debian:sid as base
-
-# Install non-OCaml dependencies + opam
-RUN apt-get update && apt-get install -y \
-    opam \
-    z3 \
-    && rm -rf /var/lib/apt/lists/*
-
-RUN opam init --disable-sandboxing --compiler=ocaml-base-compiler.4.08.1 -y
-
-# "RUN eval $(opam env)" does not work, so we manually set its variables
-ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.08.1"
-ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.08.1/lib/stublibs:/root/.opam/ocaml-base-compiler.4.08.1/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.08.1/lib/ocaml"
-ENV OCAML_TOPLEVEL_PATH "/root/.opam/ocaml-base-compiler.4.08.1/lib/toplevel"
-ENV MANPATH "$MANPATH:/root/.opam/ocaml-base-compiler.4.08.1/man"
-ENV PATH "/root/.opam/ocaml-base-compiler.4.08.1/bin:$PATH"
-
-RUN opam update -y && opam install depext -y
-
-# Install packages from reference configuration
-# Note: Python and time packages are only required for tests, but if so,
-# they need to be present before running './configure'
-RUN apt-get update && opam update -y && opam depext --install -y --verbose \
-    alt-ergo.2.2.0 \
-    apron.v0.9.12 \
-    conf-graphviz.0.1 \
-    mlgmpidl.1.2.12 \
-    ocamlfind.1.8.1 \
-    ocamlgraph.1.8.8 \
-    ppx_deriving_yojson.3.5.2 \
-    why3.1.4.0 \
-    yojson.1.7.0 \
-    zarith.1.9.1 \
-    zmq.5.1.3 \
-    conf-python-3.1.0.0 \
-    conf-time.1 \
-    && rm -rf /var/lib/apt/lists/*
-
-# Note: Debian's CVC is too recent for Why3, so we do not install the Debian
-# package; instead, we download its binary and add it to a directory in PATH.
-RUN wget https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt -O /usr/local/bin/cvc4
-RUN chmod a+x /usr/local/bin/cvc4
-
-RUN why3 config detect
-
-# with_source: keep Frama-C sources
-ARG with_source=no
-
-RUN cd /root && \
-    git clone https://git.frama-c.com/pub/frama-c.git && \
-    (cd frama-c && \
-        autoconf && ./configure --disable-gui && \
-        make -j && \
-        make install \
-    ) && \
-    ([ "${with_source}" != "no" ] || rm -rf frama-c)
-
-# with_test: run Frama-C tests; requires "with_source=yes"
-ARG with_test=no
-
-# run general tests, then test that WP can see external provers
-RUN if [ "${with_test}" != "no" ]; then \
-        cd /root/frama-c && \
-        make tests PTESTS_OPTS=-error-code && \
-        (cd src/plugins/wp/tests/ && \
-         frama-c -wp wp_gallery/binary-multiplication-without-overflow.c \
-         -wp-prover alt-ergo,cvc4); \
-    fi
diff --git a/devel_tools/docker/z3.template b/devel_tools/docker/z3.template
new file mode 100644
index 0000000000000000000000000000000000000000..9c4a430e978af90c8d5dc1b30811ddc6e6336f82
--- /dev/null
+++ b/devel_tools/docker/z3.template
@@ -0,0 +1,3 @@
+## Z3: there is no Github release archive with binaries for Alpine (musl), but\n
+##     there is an Alpine package\n
+RUN sudo apk add z3