From 0e9c499648bda88a22f292ec4a98eb1dd1e395cf Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 22 Oct 2020 22:47:35 +0200
Subject: [PATCH] [Dev] update opam dependencies; fix Python for tests
---
devel_tools/docker/frama-c.custom/Dockerfile | 23 ++++++++++----------
devel_tools/docker/frama-c.dev/Dockerfile | 11 ++++------
2 files changed, 16 insertions(+), 18 deletions(-)
diff --git a/devel_tools/docker/frama-c.custom/Dockerfile b/devel_tools/docker/frama-c.custom/Dockerfile
index c742082bbd4..0d93e4f5b41 100644
--- a/devel_tools/docker/frama-c.custom/Dockerfile
+++ b/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
diff --git a/devel_tools/docker/frama-c.dev/Dockerfile b/devel_tools/docker/frama-c.dev/Dockerfile
index 67acc324b14..ff51e8094c9 100644
--- a/devel_tools/docker/frama-c.dev/Dockerfile
+++ b/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/ && \
--
GitLab