Merge branch 'fix/andre/dockerfiles-dev-custom' into 'stable/titanium'

[Dev] update opam dependencies; fix Python for tests

See merge request frama-c/frama-c!2912

devel_tools/docker/frama-c.custom/Dockerfile

@@ -19,21 +19,25 @@ 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.0.0 \
+    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.1 \
+    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 --full-config
+RUN why3 config --detect
 
 # with_source: keep Frama-C sources
 ARG with_source=no
@@ -52,14 +56,11 @@ RUN cd /root && \
 # 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 \
-       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; \
+        make tests && \
+        (cd src/plugins/wp/tests/ && \
+         frama-c -wp wp_gallery/binary-multiplication-without-overflow.c \
+         -wp-prover alt-ergo,cvc4); \
     fi

devel_tools/docker/frama-c.dev/Dockerfile

@@ -19,6 +19,8 @@ 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 \
@@ -31,6 +33,8 @@ RUN apt-get update && opam update -y && opam depext --install -y --verbose \
     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
@@ -52,13 +56,6 @@ ARG with_test=no
 
 # run general tests, then test that WP can see external provers
 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 && \
         (cd src/plugins/wp/tests/ && \