Skip to content
Snippets Groups Projects
Commit 1c6b1a4e authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] added test for docker

parent ca93e2f0
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
devel_tools/docker/frama-c.dev/Dockerfile
+ 5
− 1
View file @ 1c6b1a4e
...@@ -50,6 +50,7 @@ RUN cd /root && \ ...@@ -50,6 +50,7 @@ RUN cd /root && \
# with_test: run Frama-C tests; requires "with_source=yes" # with_test: run Frama-C tests; requires "with_source=yes"
ARG with_test=no ARG with_test=no
# run general tests, then test that WP can see external provers
RUN if [ "${with_test}" != "no" ]; then \ RUN if [ "${with_test}" != "no" ]; then \
apt-get update && \ apt-get update && \
opam update -y && opam depext --install -y \ opam update -y && opam depext --install -y \
...@@ -59,5 +60,8 @@ RUN if [ "${with_test}" != "no" ]; then \ ...@@ -59,5 +60,8 @@ RUN if [ "${with_test}" != "no" ]; then \
&& \ && \
rm -rf /var/lib/apt/lists/* && \ rm -rf /var/lib/apt/lists/* && \
cd /root/frama-c && \ 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 fi
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment