diff --git a/devel_tools/docker/frama-c.22.0/Dockerfile b/devel_tools/docker/frama-c.22.0/Dockerfile new file mode 100644 index 0000000000000000000000000000000000000000..d1e25df7a9d7df30b4b0cba10fccfc169a3dec7f --- /dev/null +++ b/devel_tools/docker/frama-c.22.0/Dockerfile @@ -0,0 +1,66 @@ +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/Dockerfile b/devel_tools/docker/frama-c.custom/Dockerfile index 0d93e4f5b41b8b06faa056db6d05c0cc5351d613..4eb330c4d69c7dfb1134868b877f2d761193a77c 100644 --- a/devel_tools/docker/frama-c.custom/Dockerfile +++ b/devel_tools/docker/frama-c.custom/Dockerfile @@ -2,7 +2,6 @@ FROM debian:sid as base # Install non-OCaml dependencies + opam RUN apt-get update && apt-get install -y \ - cvc4 \ opam \ z3 \ && rm -rf /var/lib/apt/lists/* @@ -37,6 +36,11 @@ RUN apt-get update && opam update -y && opam depext --install -y --verbose \ 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 @@ -59,7 +63,7 @@ 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 && \ + 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); \ diff --git a/devel_tools/docker/frama-c.dev/Dockerfile b/devel_tools/docker/frama-c.dev/Dockerfile index ff51e8094c952ebdf3254a7b0ece8d5b37843218..bdd95a3d5de09857476f68b4fd01def1cdc6b9a2 100644 --- a/devel_tools/docker/frama-c.dev/Dockerfile +++ b/devel_tools/docker/frama-c.dev/Dockerfile @@ -2,7 +2,6 @@ FROM debian:sid as base # Install non-OCaml dependencies + opam RUN apt-get update && apt-get install -y \ - cvc4 \ opam \ z3 \ && rm -rf /var/lib/apt/lists/* @@ -37,6 +36,11 @@ RUN apt-get update && opam update -y && opam depext --install -y --verbose \ 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 @@ -49,7 +53,7 @@ RUN cd /root && \ make -j && \ make install \ ) && \ - [ "${with_source}" != "no" ] || rm -rf frama-c + ([ "${with_source}" != "no" ] || rm -rf frama-c) # with_test: run Frama-C tests; requires "with_source=yes" ARG with_test=no @@ -57,7 +61,7 @@ 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 && \ + 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); \