diff --git a/devel_tools/docker/frama-c.20.0/Dockerfile b/devel_tools/docker/frama-c.20.0/Dockerfile
index d73738fb95080d205a3c8a6668c246dbd41ca1a7..66dcd40c0252c89768cc13ce42210595823e1f79 100644
--- a/devel_tools/docker/frama-c.20.0/Dockerfile
+++ b/devel_tools/docker/frama-c.20.0/Dockerfile
@@ -1,7 +1,11 @@
FROM debian:sid as base
-RUN apt update
-RUN apt install opam -y
+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
@@ -11,11 +15,10 @@ 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
-RUN opam install depext -y
+RUN opam update -y && opam install depext -y
# Install packages from reference configuration
-RUN opam depext --install -y \
+RUN apt-get update && opam update -y && opam depext --install -y --verbose \
alt-ergo.2.0.0 \
apron.20160125 \
conf-graphviz.0.1 \
@@ -26,7 +29,8 @@ RUN opam depext --install -y \
why3.1.2.0 \
yojson.1.7.0 \
zarith.1.9.1 \
- --verbose # intentionally left as last line in this RUN command
+ && rm -rf /var/lib/apt/lists/*
+
RUN why3 config --detect-provers
# with_source: keep Frama-C sources
@@ -47,12 +51,14 @@ RUN cd /root && \
ARG with_test=no
RUN if [ "${with_test}" != "no" ]; then \
- opam depext --install -y \
+ apt-get update && \
+ opam update -y && opam depext --install -y \
conf-python-3.1.0.0 \
conf-time.1 \
--verbose \
&& \
- apt install python -y && \
+ apt-get install python -y && \
+ 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
index 3a615a7bf0f9d87ec211b428dd12891c3ea4c57d..472d6dce9eb0e3f5fc718bc80fee0dba5bb0421c 100644
--- a/devel_tools/docker/frama-c.21.0/Dockerfile
+++ b/devel_tools/docker/frama-c.21.0/Dockerfile
@@ -1,7 +1,11 @@
FROM debian:sid as base
-RUN apt update
-RUN apt install opam -y
+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
@@ -11,11 +15,10 @@ 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
-RUN opam install depext -y
+RUN opam update -y && opam install depext -y
# Install packages from reference configuration
-RUN opam depext --install -y \
+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 \
@@ -27,7 +30,11 @@ RUN opam depext --install -y \
yojson.1.7.0 \
zarith.1.9.1 \
zmq.5.1.3 \
- --verbose # intentionally left as last line in this RUN command
+ && rm -rf /var/lib/apt/lists/*
+
+# Install non-OCaml solvers
+RUN apt install z3 cvc4 -y
+
RUN why3 config --full-config
# with_source: keep Frama-C sources
@@ -48,11 +55,13 @@ RUN cd /root && \
ARG with_test=no
RUN if [ "${with_test}" != "no" ]; then \
- opam depext --install -y \
+ 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
index 8852ac14805bad7b5862b8b1205a5e667ab8ca8c..c37b6441aa885a8e2bdee5acb507b95443c04338 100644
--- a/devel_tools/docker/frama-c.21.1/Dockerfile
+++ b/devel_tools/docker/frama-c.21.1/Dockerfile
@@ -1,7 +1,11 @@
FROM debian:sid as base
-RUN apt update
-RUN apt install opam -y
+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
@@ -11,11 +15,10 @@ 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
-RUN opam install depext -y
+RUN opam update -y && opam install depext -y
# Install packages from reference configuration
-RUN opam depext --install -y \
+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 \
@@ -27,7 +30,11 @@ RUN opam depext --install -y \
yojson.1.7.0 \
zarith.1.9.1 \
zmq.5.1.3 \
- --verbose # intentionally left as last line in this RUN command
+ && rm -rf /var/lib/apt/lists/*
+
+# Install non-OCaml solvers
+RUN apt install z3 cvc4 -y
+
RUN why3 config --full-config
# with_source: keep Frama-C sources
@@ -48,11 +55,13 @@ RUN cd /root && \
ARG with_test=no
RUN if [ "${with_test}" != "no" ]; then \
- opam depext --install -y \
+ 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.dev/Dockerfile b/devel_tools/docker/frama-c.dev/Dockerfile
new file mode 100644
index 0000000000000000000000000000000000000000..aa819b0a6617f4d3396392fcb00153e7327d5d52
--- /dev/null
+++ b/devel_tools/docker/frama-c.dev/Dockerfile
@@ -0,0 +1,65 @@
+FROM debian:sid as base
+
+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
+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.1 \
+ 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/*
+
+# Install non-OCaml solvers
+RUN apt install z3 cvc4 -y
+
+RUN why3 config --full-config
+
+# 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 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/nix/frama-ci.nix b/nix/frama-ci.nix
index ce0e87a5dff5d1d6eb098b7e2461311249bdaf3d..7939e05dd1161d65a13c6d4093cfff78d3f3fe81 100644
--- a/nix/frama-ci.nix
+++ b/nix/frama-ci.nix
@@ -5,7 +5,7 @@ let
src = builtins.fetchGit {
"url" = "https://bobot:${password}@git.frama-c.com/frama-c/Frama-CI.git";
"name" = "Frama-CI";
- "rev" = "36e99854d59cda2c97d0b52f1f098f6beb3baf04";
+ "rev" = "3e8a67b19d5923c651509070eec5db646b80ec32";
"ref" = "master";
};
in