diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 0a827b81ef53e13958a4c524eb3340285334cec0..f27809a2c512f0e9e41bac352104fd0197a30e0d 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -234,7 +234,7 @@ e-acsl-tests-dev:
ivette:
stage: build
- image: node
+ image: node:lts-gallium
cache:
paths:
- ivette/node_modules/
diff --git a/Changelog b/Changelog
index c46d534ad769b7d9bb0d1fb6c5b9d83edb7a1dc9..e403ba0db675c7de6ea0dfce6ea75a0c50df4d74 100644
--- a/Changelog
+++ b/Changelog
@@ -21,6 +21,23 @@ Open Source Release <next-release>
Open Source Release 24.0 (Chromium)
###################################
+- Eva [2021-10-19] New options to allow states partitioning to survive
+ function returns: -eva-interprocedural-split for disjunctions
+ from split annotations, and -eva-interprocedural-history for
+ disjunctions from the -eva-partition-history option.
+- Eva [2021-10-14] Supports the evaluation of ACSL set comprehension.
+- Eva [2021-10-14] On a SIGINT signal (Ctrl-C), the analysis is stopped
+ but partial results are saved if option -save is set.
+-* Eva [2021-10-12] Always checks the arguments of builtin calls for
+ alarms about initialization, escaping pointers and special
+ floating-point values, unless -eva-warn-copy-indeterminate is set.
+-* Kernel [2021-10-11] Fixes crashes on C integer constants overflowing
+ ocaml integers.
+- Eva [2021-10-06] Improves the precision of the octagon domain on
+ unsigned variables.
+-* Eva [2021-10-06] Fixes a soundness bug in the octagon domain on
+ integer downcasts wrapping around.
+- Eva [2021-09-10] Improves the symbolic-locations domain precision.
- Kernel [2021-09-02] 0-sized flexible array members only available in
gcc_* machdeps, that now also support FAM in nested struct.
- Eva [2021-07-26] Removes the maximum limit of option -eva-ilevel.
diff --git a/devel_tools/docker/.gitignore b/devel_tools/docker/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..7762191a2d2e4e1fcc7889d279426890c04f02ae
--- /dev/null
+++ b/devel_tools/docker/.gitignore
@@ -0,0 +1,10 @@
+Dockerfile.dev*
+Dockerfile.1*
+Dockerfile.2*
+Dockerfile.3*
+Dockerfile.4*
+Dockerfile.5*
+Dockerfile.6*
+Dockerfile.7*
+Dockerfile.8*
+Dockerfile.9*
diff --git a/devel_tools/docker/Dockerfile.template b/devel_tools/docker/Dockerfile.template
new file mode 100644
index 0000000000000000000000000000000000000000..15775528f7f32b98a5fc4c93b71227c943edf8d3
--- /dev/null
+++ b/devel_tools/docker/Dockerfile.template
@@ -0,0 +1,220 @@
+# Inspired by https://github.com/Frederic-Boulanger-UPS/docker-framac and
+# https://gitlab.inria.fr/why3/why3/-/blob/master/misc/Dockerfile.deploy
+
+FROM @ALPINE_OPAM_BASE@ AS base
+
+# Stage 1: switch opam if needed (only for very old versions),
+# then install external provers (see .template files)
+
+FROM base AS frama-c
+
+## 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 \
+@OPAM_CACHE_FIX@ \
+opam update -y && \
+opam install depext -y
+
+RUN @OPAM_SWITCH@
+
+# "RUN eval $(opam env)" does not work, so we manually set its variables
+@ENV@
+
+# Install external provers
+@CVC4@
+@Z3@
+
+RUN opam depext --install -y @OPAM_DEPS@
+
+RUN @WHY3_CONFIG@
+
+# from_archive: if "git", clone from public Git; if prefixed with http,
+# wget it; otherwise, use the given archive name.
+# Note: the archive must contain a root directory
+# starting with 'frama-c'
+ARG from_archive=git
+
+# The following line copies a frama-c archive if it exists, else nothing
+COPY --chown=opam:opam README.md frama-c-*.tar.gz /frama-c/
+
+RUN \
+if [ "${from_archive}" != "git" ]; then \
+ (cd /frama-c && \
+ case "${from_archive}" in \
+ "http"*) wget "${from_archive}" ;; \
+ *) ;; \
+ esac && \
+ tar xvf "${from_archive##*/}" --strip 1 && \
+ rm -f frama-c-*.tar.gz) \
+; else \
+ sudo apk add git && \
+ (cd /frama-c && rm -f * && git clone --depth 1 https://git.frama-c.com/pub/frama-c.git .) \
+; fi
+
+RUN cd /frama-c && @PATCH_FRAMAC@ && autoconf && ./configure --disable-gui
+RUN cd /frama-c && make -j && sudo make install
+
+# Run quick sanity checks
+RUN \
+printf "int g;\n//@assigns g;\nvoid f(){g = 1;}\nint main() {f(); return g;}" > /tmp/simple.c && \
+frama-c -val @WP_REPORT@ /tmp/simple.c && \
+rm -f /tmp/simple.c
+
+## Cleanup
+RUN \
+opam clean --yes --switch-cleanup && \
+rm -rf /home/opam/opam-repository && \
+rm -rf /home/opam/.opam/repo/default/.git*
+
+# Stage 3 (optional): tests
+
+FROM frama-c AS tests
+
+# Run standard Frama-C tests
+RUN @FRAMAC_TESTS@
+
+# Run an extra test for WP with provers
+# Note: we use ';' instead of '&&' because, for older Frama-C's, such directory
+# does not exist.
+RUN cd /frama-c/ && cd src/plugins/wp/tests/; @WP_TEST@
+
+
+# Stage 4 (optional): GUI
+
+FROM frama-c AS frama-c-gui
+
+RUN sudo apk add adwaita-icon-theme font-noto gdk-pixbuf @GUI_ALPINE_DEPS@
+RUN opam depext -y --install @GUI_OPAM_DEPS@
+RUN cd /frama-c && @GUI_REMAKE@
+
+# Stage 5 (to be deployed): 'slim' image
+
+FROM @ALPINE_BASE@ AS frama-c-slim
+
+RUN adduser --disabled-password --gecos '' opam
+
+COPY --from=frama-c /bin /bin/
+COPY --from=frama-c /etc /etc/
+COPY --from=frama-c /lib /lib/
+COPY --from=frama-c /sbin /sbin/
+# RUN true cmds are a workaround against
+# obscure docker bug (https://github.com/moby/moby/issues/37965)
+# manifesting in sequences of COPY
+RUN true
+COPY --from=frama-c /usr /usr/
+RUN true
+COPY --from=frama-c --chown=opam:opam /home/opam/.opam /home/opam/.opam/
+COPY --from=frama-c /home/opam/.profile /home/opam/
+
+RUN apk add sudo
+USER opam
+WORKDIR /home/opam
+@ENV@
+
+RUN @WHY3_CONFIG@
+
+# Stage 6 (optional, to be deployed): 'slim' image with frama-c-gui
+
+FROM @ALPINE_BASE@ AS frama-c-gui-slim
+
+RUN adduser --disabled-password --gecos '' opam
+
+COPY --from=frama-c-gui /bin /bin/
+COPY --from=frama-c-gui /etc /etc/
+COPY --from=frama-c-gui /lib /lib/
+COPY --from=frama-c-gui /sbin /sbin/
+RUN true
+COPY --from=frama-c-gui /usr /usr/
+RUN true
+COPY --from=frama-c-gui --chown=opam:opam /home/opam/.opam /home/opam/.opam/
+COPY --from=frama-c-gui /home/opam/.profile /home/opam/
+
+RUN apk add sudo
+USER opam
+WORKDIR /home/opam
+@ENV@
+
+RUN @WHY3_CONFIG@
+
+# sanity check
+RUN which frama-c-gui
+
+# Stage 7: preparation of 'stripped' image (~200 MB compressed)
+# Note: this image only contains the Frama-C binaries and files closely
+# related to it; most other OCaml tools have been removed.
+# Even recompilation of Frama-C is not guaranteed to work.
+
+FROM frama-c-slim AS frama-c-stripped-prepare
+
+@ENV@
+
+# Remove all non-essential ocaml binaries
+RUN \
+mkdir -p /home/opam/.opam/minimal/bin && \
+(cd /home/opam/.opam/*/bin && \
+ cp -P $(ls -d alt-ergo ocaml ocamlc ocamlc.opt ocamlfind ocamlopt ocamlopt.opt why3 2>/dev/null) /home/opam/.opam/minimal/bin/) && \
+rm -rf /home/opam/.opam/@OCAMLV@/bin && \
+mv /home/opam/.opam/minimal/bin /home/opam/.opam/@OCAMLV@/bin/
+
+# Remove non-essential opam files
+RUN rm -rf /home/opam/.opam/repo/default/packages
+RUN rm -rf /home/opam/.opam/download-cache
+RUN rm -rf /home/opam/.opam/repo/state.cache
+
+# Further stripping: remove non-essential files from tools used by Frama-C
+# (Apron, Alt-Ergo, large OCaml compiler files, etc)
+RUN rm -f /home/opam/.opam/@OCAMLV@/share/apron/lib/*.a
+RUN rm -f /home/opam/.opam/@OCAMLV@/share/apron/lib/*_debug.so
+RUN rm -rf /home/opam/.opam/@OCAMLV@/share/apron/bin
+RUN rm -rf /home/opam/.opam/@OCAMLV@/share/apron/include
+RUN rm -rf /home/opam/.opam/@OCAMLV@/lib/alt-ergo
+RUN rm -rf /home/opam/.opam/@OCAMLV@/lib/lablgtk2
+RUN rm -rf /home/opam/.opam/@OCAMLV@/lib/ppx_tools
+RUN rm -rf /home/opam/.opam/@OCAMLV@/lib/psmt2-frontend
+RUN rm -rf /home/opam/.opam/*/lib/ocaml/expunge
+RUN rm -rf /home/opam/.opam/*/lib/ocaml-migrate-parsetree
+RUN (cd /home/opam/.opam/@OCAMLV@/lib/why3/commands && mv why3config config && rm -f why3* && mv config why3config) || true
+
+# Remove all non-essential OCaml files (everything else other than
+# *.cmxs, *.cmx and *.cmi)
+RUN find /home/opam/.opam \( -name "*.cmt*" -o -name "*.[ao]" -o -name "*.cm[ao]" -o -name "*.cmxa" \) -exec rm {} \;
+
+# Remove non-essential installed files
+RUN sudo rm -f /usr/bin/opam-2.*
+RUN sudo rm /usr/local/bin/frama-c.byte
+RUN sudo find /usr/local/lib/frama-c \( -name "*.[ao]" -o -name "*.cm[ao]" -o -name "*.cmxa" \) -exec rm {} \;
+RUN cd /usr/share && sudo rm -rf gtk-2.0 X11 xml/docbook
+
+# Remove non-essential apk libraries
+RUN sudo apk del libxcb libx11-dev graphviz pango cairo gtk+2.0-dev gtksourceview2-dev pango-dev
+
+# Stage 7 (optional): stripped, slimmest image (running Frama-C works,
+# but almost everything else does not (e.g. recompiling OCaml modules))
+
+FROM @ALPINE_BASE@ AS frama-c-stripped
+
+RUN adduser --disabled-password --gecos '' opam
+
+COPY --from=frama-c-stripped-prepare /bin /bin/
+COPY --from=frama-c-stripped-prepare /etc /etc/
+COPY --from=frama-c-stripped-prepare /lib /lib/
+COPY --from=frama-c-stripped-prepare /sbin /sbin/
+RUN true
+COPY --from=frama-c-stripped-prepare /usr /usr/
+RUN true
+COPY --from=frama-c-stripped-prepare --chown=opam:opam /home/opam/.opam /home/opam/.opam/
+COPY --from=frama-c-stripped-prepare /home/opam/.profile /home/opam/
+
+RUN apk add sudo
+USER opam
+WORKDIR /home/opam
+@ENV@
+
+RUN @WHY3_CONFIG@
+
+# Re-run quick sanity checks
+RUN \
+printf "int g;\n//@assigns g;\nvoid f(){g = 1;}\nint main() {f(); return g;}" > /tmp/simple.c && \
+frama-c -val @WP_REPORT@ /tmp/simple.c && \
+rm -f /tmp/simple.c
diff --git a/devel_tools/docker/Makefile b/devel_tools/docker/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..0c29e493140aa713e4684f32949c2e193ef7a742
--- /dev/null
+++ b/devel_tools/docker/Makefile
@@ -0,0 +1,902 @@
+.PHONY: *-stripped *-gui push-*
+
+help:
+ @echo "Targets: $(TARGETS)"
+
+##########################
+# LIST OF VARIABLES IN TEMPLATE FILES, TO BE REPLACED VIA SED
+# @ALPINE_BASE@
+# @ALPINE_OPAM_BASE@
+# @CVC4@
+# @CVC4_VERSION@
+# @ENV@
+# @FRAMAC_TESTS@
+# @GUI_ALPINE_DEPS@
+# @GUI_OPAM_DEPS@
+# @GUI_REMAKE@
+# @OCAMLV@
+# @OPAM_CACHE_FIX@
+# @OPAM_DEPS@
+# @OPAM_SWITCH@
+# @PATCH_FRAMAC@
+# @TEST_FLAGS@
+# @WHY3_CONFIG@
+# @WP_PROVERS@
+# @WP_REPORT@
+# @WP_TEST@
+# @Z3@
+
+
+## TEST_FLAGS:
+## PTESTS_OPTS=-error-code : if all tests pass
+## (nothing) : if tests compile, but fail
+## || true : if tests fail to compile
+
+push-dev: dev dev-gui dev-stripped
+ docker push framac/frama-c:dev
+ docker push framac/frama-c-gui:dev
+ docker push framac/frama-c:dev-stripped
+
+dev: Dockerfile.dev
+ @echo "For 'dev' builds, consider adding ARGS=--no-cache to force"
+ @echo "Docker to rebuild all layers."
+ docker build . -t framac/frama-c:dev --target frama-c-slim -f $^ $(ARGS)
+
+dev-gui: Dockerfile.dev
+ @echo "For 'dev' builds, consider adding ARGS=--no-cache to force"
+ @echo "Docker to rebuild all layers."
+ docker build . -t framac/frama-c-gui:dev --target frama-c-gui-slim -f $^ $(ARGS)
+TARGETS += dev-gui
+
+dev-stripped: Dockerfile.dev
+ @echo "For 'dev' builds, consider adding ARGS=--no-cache to force"
+ @echo "Docker to rebuild all layers."
+ docker build . -t framac/frama-c:dev-stripped --target frama-c-stripped -f $^ $(ARGS)
+TARGETS += dev-stripped
+
+release: Dockerfile.dev Dockerfile.template
+ @export archive="frama-c-$$(cat ../../VERSION)-$$(cat ../../VERSION_CODENAME).tar.gz"; \
+ if [ ! -e "$$archive" ]; then \
+ echo "error: $$archive not found; run 'make src-distrib' and put the .tar.gz in this directory."; \
+ exit 1; \
+ fi; \
+ docker build . -t framac/frama-c:release --target frama-c-slim --build-arg=from_archive="$$archive" -f $<
+ @echo "Now run: 'docker tag framac/frama-c:release framac/frama-c:<version>'"
+TARGETS += release
+
+release-gui: Dockerfile.dev
+ @echo "For 'dev' builds, consider adding ARGS=--no-cache to force"
+ @echo "Docker to rebuild all layers."
+ docker build . -t framac/frama-c-gui:release --target frama-c-gui-slim -f $^ $(ARGS)
+ @echo "Now run: 'docker tag framac/frama-c-gui:release framac/frama-c-gui:<version>'"
+TARGETS += release-gui
+
+release-stripped: Dockerfile.dev
+ @echo "For 'dev' builds, consider adding ARGS=--no-cache to force"
+ @echo "Docker to rebuild all layers."
+ docker build . -t framac/frama-c:release-stripped --target frama-c-stripped -f $^ $(ARGS)
+ @echo "Now run: 'docker tag framac/frama-c:release-stripped framac/frama-c:<version>-stripped'"
+TARGETS += release-stripped
+
+# Note: alpine-3.14 has Z3 version 4.8.11, which is not supported in some
+# versions of Why3, so we remain with alpine-3.13 for now.
+Dockerfile.dev: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.08|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.7|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|opam repository set-url default https://opam.ocaml.org \&\&|g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+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.4.0 \\\
+yojson.1.7.0 \\\
+zarith.1.9.1 \\\
+zmq.5.1.3 \\\
+conf-python-3.1.0.0 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config detect|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@||g' | \
+sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g' | \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests PTESTS_OPTS=-error-code|g' | \
+sed 's|@OCAMLV@|4.08|g' | \
+cat > $@
+
+23.1-stripped: Dockerfile.23.1
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.1-Vanadium.tar.gz $(ARGS)
+TARGETS += 23.1-stripped
+
+23.1: Dockerfile.23.1
+ docker build . -t framac/frama-c:$@ --target frama-c-slim -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.1-Vanadium.tar.gz $(ARGS)
+TARGETS += 23.1
+
+23.1-gui: Dockerfile.23.1
+ docker build . -t framac/frama-c-gui:23.1 --target frama-c-gui-slim -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.1-Vanadium.tar.gz $(ARGS)
+TARGETS += 23.1-gui
+
+push-23.1: 23.1 23.1-gui 23.1-stripped
+ docker push framac/frama-c:23.1
+ docker push framac/frama-c-gui:23.1
+ docker push framac/frama-c:23.1-stripped
+
+Dockerfile.23.1: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.08|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.7|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@||g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+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.4.0 \\\
+yojson.1.7.0 \\\
+zarith.1.9.1 \\\
+zmq.5.1.3 \\\
+conf-python-3.1.0.0 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config detect|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@||g'| \
+sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests|g' | \
+sed 's|@OCAMLV@|4.08|g' | \
+cat > $@
+
+23.0-stripped: Dockerfile.23.0
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.0-Vanadium.tar.gz $(ARGS)
+TARGETS += 23.0-stripped
+
+23.0: Dockerfile.23.0
+ docker build . -t framac/frama-c:$@ --target frama-c-slim -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.0-Vanadium.tar.gz $(ARGS)
+TARGETS += 23.0
+
+23.0-gui: Dockerfile.23.0
+ docker build . -t framac/frama-c-gui:23.0 --target frama-c-gui-slim -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-23.0-Vanadium.tar.gz $(ARGS)
+TARGETS += 23.0-gui
+
+push-23.0: 23.0 23.0-gui 23.0-stripped
+ docker push framac/frama-c:23.0
+ docker push framac/frama-c-gui:23.0
+ docker push framac/frama-c:23.0-stripped
+
+Dockerfile.23.0: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.08|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.7|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@||g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+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.4.0 \\\
+yojson.1.7.0 \\\
+zarith.1.9.1 \\\
+zmq.5.1.3 \\\
+conf-python-3.1.0.0 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config detect|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@||g'| \
+sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests|g' | \
+sed 's|@OCAMLV@|4.08|g' | \
+cat > $@
+
+22.0-stripped: Dockerfile.22.0
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-22.0-Titanium.tar.gz $(ARGS)
+TARGETS += 22.0-stripped
+
+Dockerfile.22.0: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.08|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.7|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@||g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+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|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@||g'| \
+sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests|g' | \
+sed 's|@OCAMLV@|4.08|g' | \
+cat > $@
+
+21.1-stripped: Dockerfile.21.1
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-21.1-Scandium.tar.gz $(ARGS)
+TARGETS += 21.1-stripped
+
+Dockerfile.21.1: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.13-ocaml-4.07|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.13|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.7|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@||g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.2.0.0 \\\
+apron.v0.9.12 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.12 \\\
+ocamlfind.1.8.0 \\\
+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 \\\
+conf-python-3.1.0.0 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --full-config|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@||g'| \
+sed 's|@GUI_OPAM_DEPS@|lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests|g' | \
+sed 's|@OCAMLV@|4.07|g' | \
+cat > $@
+
+# Note: Frama-C 20.0 and older do not work with GCC >= 10 due to issue with
+# handling of Unicode characters
+20.0-stripped: Dockerfile.20.0
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-20.0-Calcium.tar.gz $(ARGS)
+TARGETS += 20.0-stripped
+
+# Note: cairo2.0.6.1 is used for the GUI because the 0.6.2 requires 'dune-configurator'
+Dockerfile.20.0: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.05|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.6|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.2.0.0 \\\
+apron.20160125 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.11 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+ppx_deriving_yojson.3.5.2 \\\
+why3.1.2.0 \\\
+yojson.1.7.0 \\\
+zarith.1.9.1 \\\
+zmq.5.1.3 \\\
+conf-python-3.1.0.0 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@||g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests \|\| true |g' | \
+sed 's|@OCAMLV@|4.05|g' | \
+cat > $@
+
+19.1-stripped: Dockerfile.19.1
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-19.1-Potassium.tar.gz $(ARGS)
+TARGETS += 19.1-stripped
+
+Dockerfile.19.1: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.05|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.6|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo-free.2.0.0 \\\
+apron.20160125 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.9 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+ppx_deriving_yojson.3.5.2 \\\
+why3.1.2.0 \\\
+yojson.1.7.0 \\\
+zarith.1.7 \\\
+conf-python-3.1.0.0 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@||g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk3 lablgtk3-sourceview3 conf-gtksourceview3|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.05|g' | \
+cat > $@
+
+18.0-stripped: Dockerfile.18.0
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-18.0-Argon.tar.gz $(ARGS)
+TARGETS += 18.0-stripped
+
+Dockerfile.18.0: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.05|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+apron.20160125 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.7 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+why3.0.88.3 \\\
+yojson.1.7.0 \\\
+zarith.1.7 \\\
+conf-python-3.1.0.0 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|sudo apk add ncurses \&\& cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.05|g' | \
+cat > $@
+
+17.1-stripped: Dockerfile.17.1
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Chlorine-20180502.tar.gz $(ARGS)
+TARGETS += 17.1-stripped
+
+# frama-c-script is not shipped from here on, so no need for conf-python
+Dockerfile.17.1: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.05|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+apron.20160125 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.7 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+why3.0.88.3 \\\
+yojson.1.7.0 \\\
+zarith.1.7 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.05|g' | \
+cat > $@
+
+16.0-stripped: Dockerfile.16.0
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Sulfur-20171101.tar.gz $(ARGS)
+TARGETS += 16.0-stripped
+
+# yojson is no longer marked in the opam depends from here on
+Dockerfile.16.0: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.05|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+apron.20160125 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.7 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+why3.0.88.3 \\\
+zarith.1.7 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.05|g' | \
+cat > $@
+
+15.0-stripped: Dockerfile.15.0
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Phosphorus-20170501.tar.gz $(ARGS)
+TARGETS += 15.0-stripped
+
+Dockerfile.15.0: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+apron.20160125 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.7 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+why3.0.88.3 \\\
+zarith.1.7 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's|@WP_TEST@|frama-c -wp wp_gallery/binary-multiplication-without-overflow.c -wp-prover alt-ergo,cvc4,Z3|g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.02|g' | \
+cat > $@
+
+14.0-stripped: Dockerfile.14.0
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Silicon-20161101.tar.gz $(ARGS)
+TARGETS += 14.0-stripped
+
+Dockerfile.14.0: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+apron.20160125 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.7 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+why3.0.88.3 \\\
+zarith.1.7 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's#@WP_TEST@#! ( frama-c -wp wp_usage/reads.i -wp-timeout 1 -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" )#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.02|g' | \
+cat > $@
+
+13.0-stripped: Dockerfile.13.0
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Aluminium-20160502.tar.gz $(ARGS)
+TARGETS += 13.0-stripped
+
+Dockerfile.13.0: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+apron.20160125 \\\
+conf-graphviz.0.1 \\\
+mlgmpidl.1.2.7 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+why3.0.88.3 \\\
+zarith.1.7 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's#@WP_TEST@#! ( frama-c -wp wp_usage/reads.i -wp-timeout 1 -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" )#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.02|g' | \
+cat > $@
+
+12.0-stripped: Dockerfile.12.0
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Magnesium-20151002.tar.gz $(ARGS)
+TARGETS += 12.0-stripped
+
+# apron is not shipped with Frama-C, from here on
+Dockerfile.12.0: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+conf-graphviz.0.1 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+why3.0.88.3 \\\
+zarith.1.7 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's#@WP_TEST@#! ( frama-c -wp wp_usage/reads.i -wp-timeout 1 -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" )#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.02|g' | \
+cat > $@
+
+11.0-stripped: Dockerfile.11.0
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Sodium-20150201.tar.gz $(ARGS)
+TARGETS += 11.0-stripped
+
+Dockerfile.11.0: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+conf-graphviz.0.1 \\\
+ocamlfind.1.8.0 \\\
+ocamlgraph.1.8.8 \\\
+why3.0.88.3 \\\
+zarith.1.7 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|true|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's#@WP_TEST@# ! ( printf "int g;\\n//@assigns g;\\nvoid f(){g = 1;}\\nint main() {f(); return g;}" > /tmp/simple.c; frama-c -wp /tmp/simple.c -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" ); rm -f /tmp/simple.c#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.02|g' | \
+cat > $@
+
+10.1-stripped: Dockerfile.10.1
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Neon-20140301.tar.gz $(ARGS)
+TARGETS += 10.1-stripped
+
+# Starting from this version, due to the usage of a recent GCC, we need to
+# remove the `-no-pic` flag that was passed when compiling buckx_c.c.
+# Otherwise, we get the dreaded "relocation error".
+Dockerfile.10.1: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+conf-graphviz.0.1 \\\
+ocamlfind.1.8.0 \\\
+why3-base.0.88.3 \\\
+zarith.1.7 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's#@WP_TEST@# ! ( printf "int g;\\n//@assigns g;\\nvoid f(){g = 1;}\\nint main() {f(); return g;}" > /tmp/simple.c; frama-c -wp /tmp/simple.c -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" ); rm -f /tmp/simple.c#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.02|g' | \
+ cat > $@
+
+10.0-stripped: Dockerfile.10.0
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Neon-20140301.tar.gz $(ARGS)
+TARGETS += 10.0-stripped
+
+# Starting from this version, due to the usage of a recent GCC, we need to
+# remove the `-no-pic` flag that was passed when compiling buckx_c.c.
+# Otherwise, we get the dreaded "relocation error".
+Dockerfile.10.0: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|true|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.30 \\\
+conf-graphviz.0.1 \\\
+ocamlfind.1.8.0 \\\
+why3-base.0.88.3 \\\
+zarith.1.7 \\\
+conf-time.1|' | \
+sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's#@WP_TEST@# ! ( printf "int g;\\n//@assigns g;\\nvoid f(){g = 1;}\\nint main() {f(); return g;}" > /tmp/simple.c; frama-c -wp /tmp/simple.c -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" ); rm -f /tmp/simple.c#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|cairo2.0.6.1 lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|4.02|g' | \
+cat > $@
+
+9.2-stripped: Dockerfile.9.2
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Fluorine-20130601.tar.gz $(ARGS)
+TARGETS += 9.2-stripped
+
+# configure.in had a bug detecting Make versions > 4; instead of applying
+# the proper fix (which would be long), we simply "cheat" by replacing '81'
+# (from "make 3.81") with "1".
+Dockerfile.9.2: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|opam switch create 3.12.1|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.01 \\\
+conf-autoconf.0.1 \\\
+conf-graphviz.0.1 \\\
+ocamlfind.1.7.3-1 \\\
+why3-base.0.85 \\\
+zarith.1.7|' | \
+sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile \&\& sed -i "s/ 81/ 1/" configure.in|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's#@WP_TEST@# ! ( printf "int g;\\n//@assigns g;\\nvoid f(){g = 1;}\\nint main() {f(); return g;}" > /tmp/simple.c; frama-c -wp /tmp/simple.c -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" ); rm -f /tmp/simple.c#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|3.12.1|g' | \
+cat > $@
+
+8.0-stripped: Dockerfile.8.0
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Oxygen-20120901.tar.gz $(ARGS)
+TARGETS += 8.0-stripped
+
+Dockerfile.8.0: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|opam switch create 3.12.1|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.01 \\\
+conf-autoconf.0.1 \\\
+conf-graphviz.0.1 \\\
+ocamlfind.1.7.3-1 \\\
+why3-base.0.85 \\\
+zarith.1.7|' | \
+sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile \&\& sed -i "s/ 81/ 1/" configure.in|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's#@WP_TEST@# ! ( printf "int g;\\n//@assigns g;\\nvoid f(){g = 1;}\\nint main() {f(); return g;}" > /tmp/simple.c; frama-c -wp /tmp/simple.c -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" ); rm -f /tmp/simple.c#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|lablgtk conf-gnomecanvas conf-gtksourceview|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|3.12.1|g' | \
+cat > $@
+
+7.0-stripped: Dockerfile.7.0
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Nitrogen-20111001.tar.gz $(ARGS)
+TARGETS += 7.0-stripped
+
+# For some reason, lablgtk2 files are installed in a directory other than the
+# one where Frama-C's configure expects them; the simplest fix seems to be
+# moving the files to the expected directory.
+Dockerfile.7.0: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@CVC4@|$(shell cat cvc4.template)|g' | \
+sed 's|@CVC4_VERSION@|1.5|g' | \
+sed 's|@Z3@|$(shell cat z3.template)|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|opam switch create 3.12.1|g' | \
+sed 's|@OPAM_DEPS@|\\\
+alt-ergo.1.01 \\\
+conf-autoconf.0.1 \\\
+conf-graphviz.0.1 \\\
+ocamlfind.1.7.3-1 \\\
+why3-base.0.85 \\\
+zarith.1.7|' | \
+sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile \&\& sed -i "s/ 81/ 1/" configure.in|g' | \
+sed 's|@WP_REPORT@|-wp -report|g'| \
+sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+sed 's#@WP_TEST@# ! ( printf "int g;\\n//@assigns g;\\nvoid f(){g = 1;}\\nint main() {f(); return g;}" > /tmp/simple.c; frama-c -wp /tmp/simple.c -wp-prover alt-ergo,CVC4,Z3 | grep "No prover" ); rm -f /tmp/simple.c#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|lablgtk conf-gnomecanvas conf-gtksourceview \&\& mv /home/opam/.opam/3.12.1/lib/lablgtk2/ /home/opam/.opam/3.12.1/lib/ocaml/|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|3.12.1|g' | \
+cat > $@
+
+6.0-stripped: Dockerfile.6.0
+ docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Carbon-20110201.tar.gz $(ARGS)
+TARGETS += 6.0-stripped
+
+# TODO: find out how to make WP installation work; following the instructions, the
+# dynamic version fails during ./configure, with:
+# ./configure: export: line 1666: ENABLE_USAGE:_FRAMA_C_[OPTIONS_AND_FILES...]: bad variable name
+# And the static version (putting in src/wp) fails with:
+# src/wp/Makefile:46: *** recipe commences before first target. Stop.
+Dockerfile.6.0: Makefile Dockerfile.template env.template
+ sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+sed 's|@ENV@|$(shell cat env.template)|g' | \
+sed 's|@CVC4@||g' | \
+sed 's|@CVC4_VERSION@||g' | \
+sed 's|@Z3@||g' | \
+sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+sed 's|@OPAM_SWITCH@|opam switch create 3.12.1|g' | \
+sed 's|@OPAM_DEPS@|\\\
+conf-autoconf.0.1 \\\
+conf-graphviz.0.1 \\\
+ocamlfind.1.7.3-1|' | \
+sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile \&\& sed -i "s/ 81/ 1/" configure.in|g' | \
+sed 's|@WP_REPORT@||g'| \
+sed 's|@WHY3_CONFIG@|true|g' | \
+sed 's#@WP_TEST@#true#g' | \
+sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+sed 's|@GUI_OPAM_DEPS@|lablgtk conf-gnomecanvas conf-gtksourceview \&\& mv /home/opam/.opam/3.12.1/lib/lablgtk2/ /home/opam/.opam/3.12.1/lib/ocaml/|g'| \
+sed 's|@GUI_REMAKE@|make clean \&\& autoconf \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+sed 's|@OCAMLV@|3.12.1|g' | \
+cat > $@
+
+#5.0-stripped: Dockerfile.5.0
+# docker build . -t framac/frama-c:$@ --target frama-c-stripped -f $^ \
+#--build-arg=from_archive=https://www.frama-c.com/download/frama-c-Boron-20100401-why-2.24.tar.gz $(ARGS)
+#TARGETS += 5.0-stripped
+#
+# Re-running the makefile for the GUI seems to cause issues,
+# so we restart everything from the archive
+# TODO: fix build and proceed with older Frama-C versions
+# Dockerfile.5.0: Makefile Dockerfile.template env.template
+# sed 's|@ALPINE_OPAM_BASE@|ocaml/opam:alpine-3.12-ocaml-4.02|g' Dockerfile.template | \
+# sed 's|@ALPINE_BASE@|alpine:3.12|g' | \
+# sed 's|@ENV@|$(shell cat env.template)|g' | \
+# sed 's|@CVC4@||g' | \
+# sed 's|@CVC4_VERSION@||g' | \
+# sed 's|@Z3@||g' | \
+# sed 's|@OPAM_CACHE_FIX@|git -C /home/opam/opam-repository pull origin master \&\& |g' | \
+# sed 's|@OPAM_SWITCH@|opam switch create 3.12.1|g' | \
+# sed 's|@OPAM_DEPS@|\\\
+# conf-autoconf.0.1 \\\
+# conf-graphviz.0.1 \\\
+# ocamlfind.1.7.3-1 \\\
+# zarith.1.7|' | \
+# sed 's|@PATCH_FRAMAC@|cd /frama-c \&\& sed -i s/-fno-pic// Makefile \&\& sed -i "s/ 81/ 1/" configure.in|g' | \
+# sed 's|@WP_REPORT@||g'| \
+# sed 's|@WHY3_CONFIG@|why3 config --detect-provers|g' | \
+# sed 's#@WP_TEST@#true#g' | \
+# sed 's|@GUI_ALPINE_DEPS@|libart-lgpl-dev|g'| \
+# sed 's|@GUI_OPAM_DEPS@|lablgtk conf-gnomecanvas conf-gtksourceview \&\& mv /home/opam/.opam/3.12.1/lib/lablgtk2/ /home/opam/.opam/3.12.1/lib/ocaml/|g'| \
+# sed 's|@GUI_REMAKE@|rm -rf * \&\& wget https://www.frama-c.com/download/frama-c-Boron-20100401-why-2.24.tar.gz \&\& tar xvf frama-c-Boron-20100401-why-2.24.tar.gz --strip 1 \&\& cd /frama-c \&\& sed -i s/-fno-pic// Makefile \&\& sed -i "s/ 81/ 1/" configure.in \&\& autoconf \&\& ./configure --enable-gui \&\& make -j \&\& sudo make install|g' | \
+# sed 's|@FRAMAC_TESTS@|cd /frama-c \&\& make tests \|\| true|g' | \
+# sed 's|@OCAMLV@|3.12.1|g' | \
+# cat > $@
diff --git a/devel_tools/docker/README.md b/devel_tools/docker/README.md
index 0a1c8e049e40b74e21466ee9b87be75a27475901..e56c8d81b42a389ee8a62c5e772b86ffb3a72c17 100644
--- a/devel_tools/docker/README.md
+++ b/devel_tools/docker/README.md
@@ -1,29 +1,60 @@
-Docker images for Frama-C
-=========================
+# Frama-C Docker images
-- To build a new image (slim, without Frama-C sources nor tests):
+Frama-C Docker images are currently based on Alpine Linux,
+using opam's Docker images
+(from https://hub.docker.com/r/ocaml/opam/).
- cd <tag>
- docker build . --target base -t framac/frama-c:<tag>
+The user is `opam` and it has sudo rights.
+To add packages, run `sudo apk add <package>`.
-- To run an interactive shell:
+## Using the Makefile
- docker run -it framac/frama-c:<tag>
+The `Makefile` contains several targets and templates to build most
+Frama-C versions. For each version, there are three images: one
+for the command-line version `frama-c`; a stripped-down version of the former,
+for a slimmer image, but which does not allow recompilation of Frama-C
+or of any external plugin; and a third image including the graphical
+interface (`frama-c-gui`), to be used with Singularity or other tools enabling
+graphical interfaces from within a Docker image.
-- To push to Docker Hub (requires access to the `framac/frama-c` repository):
+Run `make` to get a list of targets.
- docker push framac/frama-c:<tag>
+If you have access to the Frama-C Docker Hub, you can also run a
+`push-<version>` target to upload images related to that version to
+the Docker Hub.
-- To build an image containing Frama-C sources (downloaded from the .tar.gz, in
- directory `/root`):
+## Commands to generate images
- cd <tag>
- docker build . --build-arg with_source=yes \
- -t framac/frama-c:<tag>-with-source
+Some commands in this section are those used by the above Makefile;
+others allow creating different images (e.g. with the Frama-C sources)
+which are not directly available as Makefile targets.
-- To run Frama-C tests (and remove unnecessary image later):
+- Build slim development image (from public Git master branch):
- cd <tag>
- docker build . --build-arg with_source=yes --build-arg with_test=yes \
- -t framac/frama-c:<tag>-with-test
- docker image rm framac/frama-c:<tag>-with-test
+ docker build . -t framac/frama-c:dev --target frama-c-slim
+
+- Build slim development image with GUI:
+
+ docker build . -t framac/frama-c-gui:dev --target frama-c-gui-slim
+
+- Build stripped (minimal) version:
+
+ docker build . -t framac/frama-c:dev-stripped --target frama-c-stripped
+
+- Build image from archive (note: it _must_ be named `frama-c-<something>.tar.gz`, where
+ `<something>` may be a version number, codename, etc:
+
+ docker build . -t framac/frama-c:dev --target frama-c-slim --build-arg=from_archive=frama-c-<version>.tar.gz
+
+- Build image containing Frama-C's source code in `/frama-c` (without and with GUI):
+
+ docker build . -t framac/frama-c-source:dev --target frama-c
+ docker build . -t framac/frama-c-gui-source:dev --target frama-c-gui
+
+- Start Singularity instance
+
+ singularity instance start docker-daemon:framac/frama-c-gui:dev <instance name>
+
+- Run command with Singularity instance
+
+ singularity exec instance://<instance name> <command with args>
diff --git a/devel_tools/docker/cvc4.template b/devel_tools/docker/cvc4.template
new file mode 100644
index 0000000000000000000000000000000000000000..951aa4ea617f12db51d78f5387aadab0b4c824d1
--- /dev/null
+++ b/devel_tools/docker/cvc4.template
@@ -0,0 +1,5 @@
+## CVC4 @CVC4_VERSION@\n
+RUN \\\n
+wget --quiet http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-@CVC4_VERSION@-x86_64-linux-opt -O cvc4-@CVC4_VERSION@ \&\& \\\n
+chmod a+x cvc4-@CVC4_VERSION@ \&\& \\\n
+sudo mv cvc4-@CVC4_VERSION@ /usr/local/bin/
diff --git a/devel_tools/docker/env.template b/devel_tools/docker/env.template
new file mode 100644
index 0000000000000000000000000000000000000000..14b2666ef03ba5ae6f2ce6f8d718eb9e7b6145b6
--- /dev/null
+++ b/devel_tools/docker/env.template
@@ -0,0 +1,11 @@
+ENV OPAM_SWITCH_PREFIX "/home/opam/.opam/@OCAMLV@"\n
+ENV CAML_LD_LIBRARY_PATH "/home/opam/.opam/@OCAMLV@/lib/stublibs:/home/opam/.opam/@OCAMLV@/lib/ocaml/stublibs:/home/opam/.opam/@OCAMLV@/lib/ocaml"\n
+ENV OCAML_TOPLEVEL_PATH "/home/opam/.opam/@OCAMLV@/lib/toplevel"\n
+ENV MANPATH "$MANPATH:/home/opam/.opam/@OCAMLV@/man"\n
+ENV PATH "/home/opam/.opam/@OCAMLV@/bin:$PATH"\n
+\n
+## Avoid prompts for time zone\n
+ENV TZ=Europe/Paris\n
+\n
+## Fix issue with libGL on Windows\n
+ENV LIBGL_ALWAYS_INDIRECT=1\n
diff --git a/devel_tools/docker/frama-c.18.0/Dockerfile b/devel_tools/docker/frama-c.18.0/Dockerfile
deleted file mode 100644
index d3582aa0d4361c90c73a31c39b5023c741386973..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.18.0/Dockerfile
+++ /dev/null
@@ -1,63 +0,0 @@
-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.05.0 -y
-
-# "RUN eval $(opam env)" does not work, so we manually set its variables
-ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.05.0"
-ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.05.0/lib/stublibs:/root/.opam/ocaml-base-compiler.4.05.0/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.05.0/lib/ocaml"
-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 && opam install depext -y
-
-# Install packages from reference configuration
-RUN apt-get update && opam update -y && opam depext --install -y --verbose \
- alt-ergo.1.30 \
- apron.20160125 \
- conf-graphviz.0.1 \
- mlgmpidl.1.2.7 \
- ocamlfind.1.8.0 \
- ocamlgraph.1.8.8 \
- why3.0.88.3 \
- yojson.1.4.1 \
- zarith.1.7 \
- && rm -rf /var/lib/apt/lists/*
-
-RUN why3 config --detect-provers
-
-# with_source: keep Frama-C sources
-ARG with_source=no
-
-RUN cd /root && \
- wget http://frama-c.com/download/frama-c-18.0-Argon.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 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/devel_tools/docker/frama-c.19.1/Dockerfile b/devel_tools/docker/frama-c.19.1/Dockerfile
deleted file mode 100644
index b3c7d6d97ece64c7186580f0c5937066179943a8..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.19.1/Dockerfile
+++ /dev/null
@@ -1,63 +0,0 @@
-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.05.0 -y
-
-# "RUN eval $(opam env)" does not work, so we manually set its variables
-ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.05.0"
-ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.05.0/lib/stublibs:/root/.opam/ocaml-base-compiler.4.05.0/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.05.0/lib/ocaml"
-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 && opam install depext -y
-
-# Install packages from reference configuration
-RUN apt-get update && opam update -y && opam depext --install -y --verbose \
- alt-ergo-free.2.0.0 \
- apron.20160125 \
- conf-graphviz.0.1 \
- mlgmpidl.1.2.9 \
- ocamlfind.1.8.0 \
- ocamlgraph.1.8.8 \
- why3.1.2.0 \
- yojson.1.4.1 \
- zarith.1.7 \
- && rm -rf /var/lib/apt/lists/*
-
-RUN why3 config --detect-provers
-
-# with_source: keep Frama-C sources
-ARG with_source=no
-
-RUN cd /root && \
- wget http://frama-c.com/download/frama-c-19.1-Potassium.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 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/devel_tools/docker/frama-c.20.0/Dockerfile b/devel_tools/docker/frama-c.20.0/Dockerfile
deleted file mode 100644
index 4f4927b98e810437cfb460d79b96f575775e6a3d..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.20.0/Dockerfile
+++ /dev/null
@@ -1,64 +0,0 @@
-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.05.0 -y
-
-# "RUN eval $(opam env)" does not work, so we manually set its variables
-ENV OPAM_SWITCH_PREFIX "/root/.opam/ocaml-base-compiler.4.05.0"
-ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.05.0/lib/stublibs:/root/.opam/ocaml-base-compiler.4.05.0/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.05.0/lib/ocaml"
-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 && 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.20160125 \
- conf-graphviz.0.1 \
- mlgmpidl.1.2.11 \
- ocamlfind.1.8.0 \
- ocamlgraph.1.8.8 \
- ppx_deriving_yojson.3.5.2 \
- why3.1.2.0 \
- yojson.1.7.0 \
- zarith.1.9.1 \
- && rm -rf /var/lib/apt/lists/*
-
-RUN why3 config --detect-provers
-
-# with_source: keep Frama-C sources
-ARG with_source=no
-
-RUN cd /root && \
- wget http://frama-c.com/download/frama-c-20.0-Calcium.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 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/devel_tools/docker/frama-c.21.0/Dockerfile b/devel_tools/docker/frama-c.21.0/Dockerfile
deleted file mode 100644
index 443601c70b177f1768639d02c9148d8f6a477eab..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.21.0/Dockerfile
+++ /dev/null
@@ -1,65 +0,0 @@
-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.07.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.07.1"
-ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.07.1/lib/stublibs:/root/.opam/ocaml-base-compiler.4.07.1/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.07.1/lib/ocaml"
-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 && 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.0 \
- 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/*
-
-RUN why3 config --full-config
-
-# with_source: keep Frama-C sources
-ARG with_source=no
-
-RUN cd /root && \
- wget http://frama-c.com/download/frama-c-21.0-Scandium.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 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/devel_tools/docker/frama-c.21.1/Dockerfile b/devel_tools/docker/frama-c.21.1/Dockerfile
deleted file mode 100644
index 90a6e92fe6b801296c1f53d608aac5cd16a4171a..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.21.1/Dockerfile
+++ /dev/null
@@ -1,65 +0,0 @@
-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.07.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.07.1"
-ENV CAML_LD_LIBRARY_PATH "/root/.opam/ocaml-base-compiler.4.07.1/lib/stublibs:/root/.opam/ocaml-base-compiler.4.07.1/lib/ocaml/stublibs:/root/.opam/ocaml-base-compiler.4.07.1/lib/ocaml"
-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 && 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.0 \
- 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/*
-
-RUN why3 config --full-config
-
-# with_source: keep Frama-C sources
-ARG with_source=no
-
-RUN cd /root && \
- wget http://frama-c.com/download/frama-c-21.1-Scandium.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 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/devel_tools/docker/frama-c.22.0/Dockerfile b/devel_tools/docker/frama-c.22.0/Dockerfile
deleted file mode 100644
index d1e25df7a9d7df30b4b0cba10fccfc169a3dec7f..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.22.0/Dockerfile
+++ /dev/null
@@ -1,66 +0,0 @@
-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/.gitignore b/devel_tools/docker/frama-c.custom/.gitignore
deleted file mode 100644
index 028757c13527bdb23c649f219e11e1a4db317087..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.custom/.gitignore
+++ /dev/null
@@ -1,2 +0,0 @@
-# ignore an eventual frama-c subfolder in this directory
-frama-c
diff --git a/devel_tools/docker/frama-c.custom/Dockerfile b/devel_tools/docker/frama-c.custom/Dockerfile
deleted file mode 100644
index 4eb330c4d69c7dfb1134868b877f2d761193a77c..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.custom/Dockerfile
+++ /dev/null
@@ -1,70 +0,0 @@
-FROM debian:sid as base
-
-# Install non-OCaml dependencies + opam
-RUN apt-get update && apt-get install -y \
- 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/*
-
-# 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
-ARG with_source=no
-
-# copies a cloned, non-public Frama-C
-COPY frama-c /root/frama-c
-
-RUN cd /root && \
- (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 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/README.md b/devel_tools/docker/frama-c.custom/README.md
deleted file mode 100644
index 6ce5f94c37e0974215e3678c0512874626431df6..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.custom/README.md
+++ /dev/null
@@ -1,46 +0,0 @@
-Building a Frama-C Docker image with a custom git clone
-=========================================================================
-
-In order to build a Frama-C Docker image with custom plug-ins, or using
-a custom git repository, do the following:
-
-1. Locally clone Frama-C into the `frama-c` directory, e.g. via
-
- git clone git@frama-c.com:frama-c/frama-c.git
-
- If needed, modify the clone to add other plug-ins and/or files inside
- `frama-c`.
-
-2. If needed, add Debian and opam prerequisites to the appropriate lines in the
- Dockerfile (after `apt update` and before removing the `apt` cache).
- If you need to change the opam version, also edit the `ENV` lines.
-
-3. For a "minimal" image (with installed Frama-C, but no source code), run:
-
- docker build . -t fc-custom # or another tag if you prefer
-
- For an image with the Frama-C source code (in `/root/frama-c`), run:
-
- docker build . -t fc-custom-with-source --build-arg=with_source=yes
-
- For an image with source code + tests (e.g. which runs `make tests`), run:
-
- docker build . -t fc-custom-with-test --build-arg=with_source=yes --build-arg=with_test=yes
-
-4. In all cases, after building the image, run it with:
-
- docker run -it fc-custom # or another tag
-
-Frama-C will be installed and its sources will be in `/root/frama-c`.
-
-### Notes
-
-1. If you keep the sources, remember that the Docker image may contain
- non-public code.
-
-2. Using different tags for the `*-with-source` and `*-with-test` images may
- allow layer reuse by Docker.
-
-3. If you need files outside `/root/frama-c`, add them to the directory
- containing this README and add a `COPY` instruction to the `Dockerfile`,
- e.g. `COPY dir /root/dir`.
diff --git a/devel_tools/docker/frama-c.dev/Dockerfile b/devel_tools/docker/frama-c.dev/Dockerfile
deleted file mode 100644
index 0907e4d0438ab1078fee39227f1ed2fb0bba0aa2..0000000000000000000000000000000000000000
--- a/devel_tools/docker/frama-c.dev/Dockerfile
+++ /dev/null
@@ -1,68 +0,0 @@
-FROM debian:sid as base
-
-# Install non-OCaml dependencies + opam
-RUN apt-get update && apt-get install -y \
- 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.4.0 \
- 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/*
-
-# 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
-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 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/z3.template b/devel_tools/docker/z3.template
new file mode 100644
index 0000000000000000000000000000000000000000..9c4a430e978af90c8d5dc1b30811ddc6e6336f82
--- /dev/null
+++ b/devel_tools/docker/z3.template
@@ -0,0 +1,3 @@
+## Z3: there is no Github release archive with binaries for Alpine (musl), but\n
+## there is an Alpine package\n
+RUN sudo apk add z3
diff --git a/doc/release/website.tex b/doc/release/website.tex
index 07703879f00911bc5c938ebd7abd477e3d53eab0..075c481f7815f78d499414d9e0c5d9f03fd1f9b6 100644
--- a/doc/release/website.tex
+++ b/doc/release/website.tex
@@ -195,43 +195,44 @@ Just update the \texttt{VERSION} file in \texttt{master}, by adding
\textbf{Note:} you need access to the \texttt{framac} Docker Hub account to be able to upload the image.
-Make sure:
+Make sure that \texttt{devel\_tools/docker/Makefile} is up-to-date:
+
\begin{itemize}
- \item \texttt{devel\_tools/docker/frama-c.dev/Dockerfile}
- \item \texttt{devel\_tools/docker/frama-c.custom/Dockerfile}
+\item changes to \texttt{reference-configuration.md} must have been ported
+ to the corresponding \texttt{Dockerfile.dev} entry inside the
+ \texttt{Makefile}.
\end{itemize}
-are up-to-date; to do so, you can do the following:
-\begin{lstlisting}
-cd devel_tools/docker/frama-c.custom
-<edit Dockerfile to change the base image, from debian:sid (unstable) to the
- latest stable release>
-<copy release .tar.gz to this directory, extract and rename the directory
- `frama-c`>
-docker build . -t fc-with-test --build-arg=with_source=yes\
- --build-arg=with_test=yes
-\end{lstlisting}
+Copy the \texttt{.tar.gz} archive to the \texttt{devel\_tools/docker} directory.
-This should copy the contents of \texttt{frama-c} into the Docker image and try
-to compile Frama-C with it, then run the tests.
+Run \texttt{make release}. It should decompress the archive, build and test
+the Frama-C Docker image.
If the local tests do not work, check that the OCaml version and package
-dependencies are all up-to-date. Remember that there are several differences
-between Debian unstable (`sid`) and stable, which may require changes to the
-\texttt{Dockerfile}.
+dependencies are all up-to-date.
+
+If the image is built succesfully, you can also try building the GUI image
+(\texttt{make release-gui}) and the stripped image
+(\texttt{make release-stripped}).
-If the local tests work, then re-run Docker \textit{without} the source/tests,
-to make the image leaner:
+If you want to upload these images to the Docker Hub, you can re-tag them, e.g.
\begin{lstlisting}
-docker build . -t framac/frama-c:<VERSION>
+docker tag framac/frama-c:release framac/frama-c:<VERSION>
\end{lstlisting}
-Replacing \texttt{<VERSION>} with the release number, e.g. \texttt{23.0}.
+Where \texttt{<VERSION>} is the release number, possibly with a suffix, but
+{\em without} characters such as \texttt{+}. For instance, you can use
+\texttt{23.1-beta} for a beta release.
-After building the image, upload it with \texttt{docker push framac/frama-c:<VERSION>}.
-You will need to have setup your \texttt{framac} Docker Hub account for this to work.
+Then upload the renamed image(s) with:
+\begin{lstlisting}
+docker push framac/frama-c:<VERSION>
+docker push framac/frama-c-gui:<VERSION>
+docker push framac/frama-c:<VERSION>-stripped
+\end{lstlisting}
+You will need to have setup your \texttt{framac} Docker Hub account for this to work.
%%% Local Variables:
%%% mode: latex
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 87f24681b2572e9ab46479914004e7934bc928e5..6c51dff6731f59a3a1f1405b6a9741a2f54a32ab 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -798,6 +798,7 @@ src/plugins/callgraph/Callgraph.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/callgraph_api.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/cg.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/cg.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/callgraph/cg_viewer.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/cg_viewer.yes.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/journalize.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/journalize.mli: CEA_LGPL_OR_PROPRIETARY
diff --git a/share/libc/assert.h b/share/libc/assert.h
index 0886eac92d58bb02635d595448dcc83ba4f914bb..4e7618753ef4fa94d167e7b9e6211a34a5530cbf 100644
--- a/share/libc/assert.h
+++ b/share/libc/assert.h
@@ -34,6 +34,9 @@ __BEGIN_DECLS
*/
extern void __FC_assert(int c, const char* file, int line, const char*expr);
+#define static_assert _Static_assert
+
+
__END_DECLS
__POP_FC_STDLIB
#endif
diff --git a/share/libc/features.h b/share/libc/features.h
index 77ea2e2cac68158bb7c727efe0098ab9ef547fdc..4561934392be974ff1a1fb7e20c0496536cd58f1 100644
--- a/share/libc/features.h
+++ b/share/libc/features.h
@@ -122,5 +122,10 @@
#define __FC_EXTERN extern
#endif
+// C11 §6.10.8.3 Conditional feature macros: Frama-C does not support complex.h
+#ifndef __STDC_NO_COMPLEX__
+#define __STDC_NO_COMPLEX__
+#endif
+
/* end __FC_FEATURES_H */
#endif
diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index 59522610bb16947b1926323abf23c7425917f0d2..42759eb6818675841b52e6064d661aa118df76ad 100644
--- a/src/kernel_internals/parsing/clexer.mll
+++ b/src/kernel_internals/parsing/clexer.mll
@@ -161,6 +161,16 @@ let init_lexicon _ =
"_Noreturn is a C11 keyword, use -c11 option to enable it");
IDENT "_Noreturn"
end);
+ ("_Static_assert",
+ fun loc ->
+ if Kernel.C11.get () then STATIC_ASSERT loc
+ else begin
+ Kernel.(
+ warning
+ ~wkey:wkey_conditional_feature
+ "_Static_assert is a C11 keyword, use -c11 option to enable it");
+ IDENT "_Static_assert"
+ end);
("__attribute__", fun loc -> ATTRIBUTE loc);
("__attribute", fun loc -> ATTRIBUTE loc);
("__blockattribute__", fun _ -> BLOCKATTRIBUTE);
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 11d9ae4dbcd3c6a7af92e7f44b7412d1a2585836..fd98d6e4a86d7443a68f668ad7b5a71766080dc5 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -368,7 +368,7 @@ let in_ghost_block ?(battrs=[]) l =
%token<Cabs.cabsloc> IF TRY EXCEPT FINALLY
%token ELSE
-%token<Cabs.cabsloc> ATTRIBUTE INLINE NORETURN ASM TYPEOF FUNCTION__ PRETTY_FUNCTION__
+%token<Cabs.cabsloc> ATTRIBUTE INLINE NORETURN STATIC_ASSERT ASM TYPEOF FUNCTION__ PRETTY_FUNCTION__
%token LABEL__
%token<Cabs.cabsloc> BUILTIN_VA_ARG
%token BLOCKATTRIBUTE
@@ -1080,6 +1080,20 @@ declaration: /* ISO 6.7.*/
{ doDeclaration (Some $1) ((snd $2)) (fst $2) $3 }
| SPEC decl_spec_list SEMICOLON
{ doDeclaration (Some $1) ((snd $2)) (fst $2) [] }
+| static_assert_declaration
+ { let (e, m, loc) = $1 in STATIC_ASSERT (e, m, loc) }
+;
+
+static_assert_declaration:
+
+| STATIC_ASSERT LPAREN expression RPAREN
+ {
+ ($3, "", $1)
+ }
+| STATIC_ASSERT LPAREN expression COMMA string_constant RPAREN
+ {
+ ($3, fst $5, $1)
+ }
;
init_declarator_list: /* ISO 6.7 */
@@ -1210,6 +1224,17 @@ struct_decl_list: /* (* ISO 6.7.2. Except that we allow empty structs. We
/*(* MSVC allows pragmas in strange places *)*/
| pragma struct_decl_list { $2 }
+/*(* C11 allows static_assert-declaration *)*/
+| static_assert_declaration {
+ let (e, m, loc) = $1 in
+ [ STATIC_ASSERT_FG (e, m, loc) ]
+ }
+
+| static_assert_declaration SEMICOLON struct_decl_list {
+ let (e, m, loc) = $1 in
+ STATIC_ASSERT_FG (e, m, loc) :: $3
+ }
+
;
field_decl_list: /* (* ISO 6.7.2 *) */
field_decl { [$1] }
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 13bf2fc6abd65e107e330649546837b6276740f5..f0ab983e9b53ada76b3011ac0d13267d6b5c1ee5 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -262,9 +262,6 @@ let cabslu s =
* hold the result of function calls *)
let callTempVars: unit IH.t = IH.create 13
-(* Keep a list of functions that were called without a prototype. *)
-let noProtoFunctions : bool IH.t = IH.create 13
-
(* Check that s starts with the prefix p *)
let prefix p s =
let lp = String.length p in
@@ -5603,6 +5600,22 @@ and makeCompType ghost (isstruct: bool)
(* Do regular fields first. *)
let to_field = function
| TYPE_ANNOT _ -> None
+ | STATIC_ASSERT_FG (e, s, loc) ->
+ let (_, _, cond_exp, _) = doExp empty_local_env CConst e ADrop in
+ begin
+ match Cil.constFoldToInt ~machdep:true cond_exp with
+ | Some i ->
+ if Integer.(equal i zero) then
+ Kernel.error ~source:(fst loc) "static assertion failed%s%s@."
+ (if s <> "" then ": " else "") s
+ | None ->
+ Kernel.error ~source:(fst loc)
+ "failed to evaluate constant expression in static assertion:@ \
+ @[%a@]"
+ Cprint.print_expression e
+ end;
+ (* _Static_assert is not stored in the Cil AST *)
+ None
| FIELD (f,g) -> Some (f,g) in
let flds = Extlib.filter_map_opt to_field nglist in
let flds = List.rev (fold addFieldGroup [] flds) in
@@ -6688,7 +6701,6 @@ and doExp local_env
(makeGlobalVar ~temp:false n ftype) in
(* Make it EXTERN *)
proto.vstorage <- Extern;
- IH.add noProtoFunctions proto.vid true;
proto.vdecl <- f.expr_loc;
ImplicitPrototypeHook.apply proto;
(* Add it to the file as well *)
@@ -9195,6 +9207,25 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
| _ -> Kernel.fatal ~current:true "Too many attributes in pragma"
end
+ | Cabs.STATIC_ASSERT (e, s, loc) -> begin
+ CurrentLoc.set (convLoc loc);
+ let (_, _, cond_exp, _) = doExp local_env CConst e ADrop in
+ begin
+ match Cil.constFoldToInt ~machdep:true cond_exp with
+ | Some i ->
+ if Integer.(equal i zero) then
+ Kernel.error ~current:true "static assertion failed%s%s@."
+ (if s <> "" then ": " else "") s
+ | None ->
+ Kernel.error ~current:true
+ "failed to evaluate constant expression in static assertion:@ \
+ @[%a@]"
+ Cprint.print_expression e
+ end;
+ (* _Static_assert is not stored in the Cil AST *)
+ empty
+ end
+
| Cabs.FUNDEF (spec,((specs,(n,dt,a, _)) : Cabs.single_name),
(body : Cabs.block), loc1, loc2) when isglobal ->
begin
@@ -10401,7 +10432,6 @@ let convFile (path, f) =
(* Clean up the global types *)
initGlobals();
startFile ();
- IH.clear noProtoFunctions;
H.clear compInfoNameEnv;
H.clear enumInfoNameEnv;
IH.clear mustTurnIntoDef;
@@ -10432,7 +10462,6 @@ let convFile (path, f) =
let globals = List.rev globals in
List.iter rename_spec globals;
Logic_env.prepare_tables ();
- IH.clear noProtoFunctions;
IH.clear mustTurnIntoDef;
H.clear alreadyDefined;
H.clear compInfoNameEnv;
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index f898d1f50d1ec59321661861cae1f305ff7b1bc2..eb6d64f77d50809496712ae0e5fe13d58d5a1408 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -852,11 +852,10 @@ let removeUnmarked isRoot ast reachable_tbl =
in
let keptGlobals, removedGlobals = List.partition filterGlobal ast.globals in
ast.globals <- keptGlobals;
- if Kernel.is_debug_key_enabled dkey then
+ if Kernel.is_debug_key_enabled dkey then begin
List.iter (fun rg ->
Kernel.debug ~dkey "removing global: %s" (global_type_and_name rg)
) removedGlobals;
- if Kernel.is_debug_key_enabled dkey then
List.iter (fun rg ->
begin
match rg with
@@ -866,12 +865,15 @@ let removeUnmarked isRoot ast reachable_tbl =
let kf = Globals.Functions.get vi in
Kernel.debug ~dkey "GFunDecl: %a@." Kernel_function.pretty_code kf
with Not_found ->
- Kernel.debug ~dkey "GFunDecl: not found for %a@." Printer.pp_varinfo vi;
+ Kernel.debug ~dkey
+ "GFunDecl: %a (no associated kernel function)@."
+ Printer.pp_varinfo vi;
end
| _ -> ()
end;
Kernel.debug ~dkey "kept global %s (%a)" (global_type_and_name rg) Printer.pp_global rg
) keptGlobals;
+ end;
!removedLocals
diff --git a/src/kernel_services/ast_printing/cabs_debug.ml b/src/kernel_services/ast_printing/cabs_debug.ml
index fbcdd4854b795ce496e5ba8bc6a0563d77bb1fa2..3c4fc5fa62e932fb0a647a6559faf055e45e411e 100644
--- a/src/kernel_services/ast_printing/cabs_debug.ml
+++ b/src/kernel_services/ast_printing/cabs_debug.ml
@@ -140,6 +140,8 @@ and pp_field_group fmt = function
l;
fprintf fmt "}@]"
| TYPE_ANNOT _ -> fprintf fmt "TYPE_ANNOT"
+ | STATIC_ASSERT_FG (exp, s, loc) ->
+ fprintf fmt "@[<hov 2>STATIC_ASSERT_FG exp(%a, %s, loc(%a))@]" pp_exp exp s pp_cabsloc loc
and pp_field_groups fmt l =
fprintf fmt "{";
@@ -182,6 +184,8 @@ and pp_def fmt = function
fprintf fmt "@[<hov 2>GLOBASM %s, loc(%a)@]" s pp_cabsloc loc
| PRAGMA (exp, loc) ->
fprintf fmt "@[<hov 2>PRAGMA exp(%a, loc(%a))@]" pp_exp exp pp_cabsloc loc
+ | STATIC_ASSERT (exp, s, loc) ->
+ fprintf fmt "@[<hov 2>STATIC_ASSERT exp(%a, %s, loc(%a))@]" pp_exp exp s pp_cabsloc loc
| LINKAGE (s, loc, defs) ->
fprintf fmt "@[<hov 2>LINKAGE %s, loc(%a), defs(" s pp_cabsloc loc;
List.iter (fun def -> fprintf fmt ",@ def(%a)" pp_def def) defs;
diff --git a/src/kernel_services/ast_printing/cprint.ml b/src/kernel_services/ast_printing/cprint.ml
index 3633b1c43ff50c5db28a42b111ddadfcdb753917..908d9db116e7d766ce5023155baee302e36e0374 100644
--- a/src/kernel_services/ast_printing/cprint.ml
+++ b/src/kernel_services/ast_printing/cprint.ml
@@ -289,6 +289,9 @@ and print_field_group fmt fld = match fld with
| TYPE_ANNOT annot ->
fprintf fmt "@\n/*@@@[@ %a@]@ */@\n"
Logic_print.print_type_annot annot
+ | STATIC_ASSERT_FG (e, s, _) ->
+ fprintf fmt "@[_Static_assert (%a, %s)@]@\n" print_expression e s
+
and print_field fmt (name, widtho) =
match widtho with
@@ -624,6 +627,9 @@ and print_def fmt def =
| PRAGMA (a,_) ->
fprintf fmt "@[#pragma %a@]@\n" print_expression a
+ | STATIC_ASSERT (e, s, _) ->
+ fprintf fmt "@[_Static_assert (%a, %s)@]@\n" print_expression e s
+
| LINKAGE (n, _, dl) ->
fprintf fmt "@[<2>extern@ %s@ {%a@;}@]" n (pp_list print_def) dl
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 2aaec4541364d087d3d0b4ba1a493704d68f6686..397fad3207992d67a177d9b5d0b132bb67e0fbf7 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -525,7 +525,7 @@ module Base_checker = struct
local_vars <- Varinfo.Set.remove v local_vars;
end else begin
check_abort
- "%t is present in a block's blocals but in the function's slocals"
+ "%t is present in a block's blocals but not in the function's slocals"
prefix
end
diff --git a/src/kernel_services/parsetree/cabs.mli b/src/kernel_services/parsetree/cabs.mli
index 9294f5b774a046acd314a3f31fe882fd28e07fb2..4605ae02e5d7596765c9173a0429fc8e9e88878a 100644
--- a/src/kernel_services/parsetree/cabs.mli
+++ b/src/kernel_services/parsetree/cabs.mli
@@ -134,6 +134,7 @@ and name_group = specifier * name list
and field_group =
| FIELD of specifier * (name * expression option) list
| TYPE_ANNOT of Logic_ptree.type_annot
+ | STATIC_ASSERT_FG of expression * string * cabsloc
(* like name_group, except the declared variables are allowed to have initializers *)
(* e.g.: int x=1, y=2; *)
@@ -169,6 +170,7 @@ and definition =
| ONLYTYPEDEF of specifier * cabsloc
| GLOBASM of string * cabsloc
| PRAGMA of expression * cabsloc
+ | STATIC_ASSERT of expression * string * cabsloc
| LINKAGE of string * cabsloc * definition list (* extern "C" { ... } *)
| GLOBANNOT of Logic_ptree.decl list
(** Logical declaration (axiom, logic, etc.)*)
diff --git a/src/kernel_services/parsetree/cabshelper.ml b/src/kernel_services/parsetree/cabshelper.ml
index 6ceeedb4f04e8a71592880ba5ac3cd10a2f01561..14b0e66acbc617f9be372a6d9cc3eeef6287c106 100644
--- a/src/kernel_services/parsetree/cabshelper.ml
+++ b/src/kernel_services/parsetree/cabshelper.ml
@@ -156,6 +156,7 @@ let get_definitionloc (d : definition) : cabsloc =
| ONLYTYPEDEF(_, l) -> l
| GLOBASM(_, l) -> l
| PRAGMA(_, l) -> l
+ | STATIC_ASSERT (_, _, l) -> l
| LINKAGE (_, l, _) -> l
| GLOBANNOT({Logic_ptree.decl_loc = l }::_) -> l
| GLOBANNOT [] -> assert false
diff --git a/src/kernel_services/visitors/cabsvisit.ml b/src/kernel_services/visitors/cabsvisit.ml
index 1783feb0a22c113b7f41dc73a786a520562b507c..ef15f460f554a4082a9dc13498c820159f1f70f6 100644
--- a/src/kernel_services/visitors/cabsvisit.ml
+++ b/src/kernel_services/visitors/cabsvisit.ml
@@ -125,7 +125,7 @@ and childrenTypeSpecifier vis ts =
in
let nel' = mapNoCopy doOneField nel in
if s' != s || nel' != nel then FIELD (s', nel') else input
- | TYPE_ANNOT _ -> input
+ | TYPE_ANNOT _ | STATIC_ASSERT_FG _ -> input
in
match ts with
Tstruct (n, Some fg, extraAttrs) ->
@@ -257,6 +257,9 @@ and childrenDefinition vis d =
| PRAGMA (e, l) ->
let e' = visitCabsExpression vis e in
if e' != e then PRAGMA (e', l) else d
+ | STATIC_ASSERT (e, s, l) ->
+ let e' = visitCabsExpression vis e in
+ if e' != e then STATIC_ASSERT (e', s, l) else d
| LINKAGE (n, l, dl) ->
let dl' = mapNoCopyList (visitCabsDefinition vis) dl in
if dl' != dl then LINKAGE (n, l, dl') else d
diff --git a/src/plugins/callgraph/cg_viewer.mli b/src/plugins/callgraph/cg_viewer.mli
new file mode 100644
index 0000000000000000000000000000000000000000..74f71e807575328df490c96638838ea7007ad21c
--- /dev/null
+++ b/src/plugins/callgraph/cg_viewer.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Extension of the Frama-C GUI for the plugin. Nothing is exported. *)
diff --git a/src/plugins/callgraph/cg_viewer.yes.ml b/src/plugins/callgraph/cg_viewer.yes.ml
index dfbff693bae3e58a0b86c34e8058541648c5df43..4aabc903f4432765f0d8e9fbe542de03118c8c90 100644
--- a/src/plugins/callgraph/cg_viewer.yes.ml
+++ b/src/plugins/callgraph/cg_viewer.yes.ml
@@ -181,8 +181,6 @@ let warn_degrade reason =
View degraded to non-service graph.\n\
(use -cg-no-services to avoid this warning)")
-exception Found_vertex of bool
-
let main (window: Design.main_window_extension_points) =
ignore
((window#menu_manager ())#add_plugin
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index c3e5537eff57f24539cc3172f30f939f1fb41ff3..93fe3e1be9eef035a663acb0c1366e666c03b693 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -59,6 +59,7 @@ SRC_PROJECT_INITIALIZER:=\
SRC_ANALYSES:= \
rte \
lscope \
+ e_acsl_visitor \
logic_normalizer \
bound_variables \
interval \
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index b6729b91e48eab50f97bc67615a78bfc01ee7664..77c47d3113ad4339362f25fbe8573ea54adb43ef 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -73,6 +73,8 @@ share/e-acsl/e_acsl.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
share/e-acsl/e_acsl_rtl.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/bound_variables.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/bound_variables.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/e_acsl_visitor.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/e_acsl_visitor.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/exit_points.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/exit_points.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/interval.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data_api.c b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data_api.c
index 9be8e0f579f111122cc5a1210ad0c5b719f3a0f7..3f72b11861dd2694d59e859dd3b86b6ba41e7169 100644
--- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data_api.c
+++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert_data_api.c
@@ -309,15 +309,16 @@ void eacsl_assert_register_mpq(eacsl_assert_data_t *data, const char *name,
void eacsl_assert_register_ptr(eacsl_assert_data_t *data, const char *name,
void *ptr) {
- eacsl_assert_register_data(data, name, E_ACSL_PTR,
- (eacsl_assert_data_content_t){.value_ptr = ptr});
+ eacsl_assert_register_data(
+ data, name, E_ACSL_PTR,
+ (eacsl_assert_data_content_t){.value_ptr = (uintptr_t)ptr});
}
void eacsl_assert_register_array(eacsl_assert_data_t *data, const char *name,
void *array) {
eacsl_assert_register_data(
data, name, E_ACSL_ARRAY,
- (eacsl_assert_data_content_t){.value_array = array});
+ (eacsl_assert_data_content_t){.value_array = (uintptr_t)array});
}
void eacsl_assert_register_fun(eacsl_assert_data_t *data, const char *name) {
@@ -395,12 +396,13 @@ void eacsl_assert_copy_value(eacsl_assert_data_t *dest,
break;
}
case E_ACSL_PTR: {
- eacsl_assert_register_ptr(dest, value->name, value->content.value_ptr);
+ eacsl_assert_register_ptr(dest, value->name,
+ (void *)value->content.value_ptr);
break;
}
case E_ACSL_ARRAY: {
eacsl_assert_register_array(dest, value->name,
- value->content.value_array);
+ (void *)value->content.value_array);
break;
}
case E_ACSL_FUN: {
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 9ca2a162568d089f09e9f94cbfc5eab49fd7eeaf..28581fd29080aeaa60b201349e649738441220b9 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -33,7 +33,6 @@
intersect the first guard with the provided type for the variable v
*)
open Cil_types
-open Cil
open Cil_datatype
(** [error_msg quantif msg pp x] creates an error message from the string [msg]
@@ -80,8 +79,13 @@ module Quantified_predicate =
(* Memoization module to store the preprocessed form of a quantified predicate
*)
module Quantifier: sig
- val add: predicate -> (term * logic_var * term) list -> predicate -> unit
- val get: predicate -> ((term * logic_var * term) list * predicate) option
+ val add:
+ predicate ->
+ ((term * logic_var * term) list * predicate) Error.or_error ->
+ unit
+ val get:
+ predicate ->
+ ((term * logic_var * term) list * predicate) Error.or_error
(** getter and setter for the additional guard that intersects with the type
of the variable *)
val get_guard_for_small_type : logic_var -> predicate option
@@ -95,10 +99,11 @@ end = struct
let guard_tbl = Cil_datatype.Logic_var.Hashtbl.create 97
let get p =
- Quantified_predicate.Hashtbl.find_opt tbl p
+ try Quantified_predicate.Hashtbl.find tbl p
+ with Not_found -> Error.not_memoized ()
- let add p guarded_vars goal =
- Quantified_predicate.Hashtbl.add tbl p (guarded_vars, goal)
+ let add p res_or_error =
+ Quantified_predicate.Hashtbl.add tbl p res_or_error
let get_guard_for_small_type x =
try Some (Cil_datatype.Logic_var.Hashtbl.find guard_tbl x)
@@ -108,7 +113,7 @@ end = struct
Cil_datatype.Logic_var.Hashtbl.add guard_tbl lv p
let replace p guarded_vars goal =
- Quantified_predicate.Hashtbl.replace tbl p (guarded_vars, goal)
+ Quantified_predicate.Hashtbl.replace tbl p (Error.Res (guarded_vars, goal))
let clear () =
Cil_datatype.Logic_var.Hashtbl.clear guard_tbl;
@@ -212,7 +217,7 @@ end = struct
(fun s v ->
let v =
match v.lv_type with
- | Ctype ty when isIntegralType ty -> v
+ | Ctype ty when Cil.isIntegralType ty -> v
| Linteger -> v
| Ltype _ as ty when Logic_const.is_boolean_type ty -> v
| Ctype _ | Ltype _ | Lvar _ | Lreal | Larrow _ ->
@@ -657,10 +662,13 @@ let normalize_guard ~loc (t1, rel1, lv, rel2, t2) =
let compute_guards loc ~is_forall p bounded_vars hyps =
- let guards,goal = compute_quantif_guards p ~is_forall bounded_vars hyps in
- (* transform [guards] into [lscope_var list] *)
- let normalized_guards = List.map (normalize_guard ~loc) guards
- in Quantifier.add p normalized_guards goal
+ try
+ let guards,goal = compute_quantif_guards p ~is_forall bounded_vars hyps in
+ (* transform [guards] into [lscope_var list] *)
+ let normalized_guards = List.map (normalize_guard ~loc) guards
+ in Quantifier.add p (Res (normalized_guards,goal))
+ with exn ->
+ Quantifier.add p (Err exn)
module Preprocessor : sig
val compute : file -> unit
@@ -681,7 +689,7 @@ end
| _ -> ()
let preprocessor = object
- inherit Visitor.frama_c_inplace
+ inherit E_acsl_visitor.visitor
(* Only logic functions and logic predicates are handled.
E-acsl simply ignores all the other global annotations *)
@@ -690,62 +698,31 @@ end
| Dfun_or_pred _ -> Cil.DoChildren
| _ -> Cil.SkipChildren
- (* Ignore the annotations attached to statements from the RTL *)
- method !vglob_aux =
- function
- (* library functions and built-ins *)
- | GVarDecl(vi, _) | GVar(vi, _, _)
- | GFunDecl(_, vi, _)
- | GFun({ svar = vi }, _) when Builtins.mem vi.vname ->
- Cil.SkipChildren
-
- | GVarDecl(vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _)
- when Misc.is_fc_or_compiler_builtin vi ->
- Cil.SkipChildren
- | g when Rtl.Symbols.mem_global g ->
- Cil.SkipChildren
-
- (* generated function declaration: nothing to do *)
- | GFunDecl(_, vi, _) when Misc.is_fc_stdlib_generated vi ->
- Cil.SkipChildren
-
- | GFun({svar = vi}, _) ->
- let kf = try Globals.Functions.get vi with Not_found -> assert false in
- if Functions.check kf then Cil.DoChildren else Cil.SkipChildren
-
- | GAnnot _ -> Cil.DoChildren
-
- (* other globals: nothing to do *)
- | GFunDecl _
- | GVarDecl _
- | GVar _
- | GType _
- | GCompTag _
- | GCompTagDecl _
- | GEnumTag _
- | GEnumTagDecl _
- | GAsm _
- | GPragma _
- | GText _
- -> Cil.SkipChildren
-
method !vpredicate p =
let loc = p.pred_loc in
match Logic_normalizer.get_pred p with
- | PoT_pred p -> Error.generic_handle (process_quantif ~loc) () p;
+ | PoT_pred p -> process_quantif ~loc p;
Cil.DoChildren
| PoT_term _ -> Cil.DoChildren
end
let compute ast =
- Visitor.visitFramacFileSameGlobals preprocessor ast
+ Visitor.visitFramacFileSameGlobals
+ (preprocessor :> Visitor.frama_c_inplace)
+ ast
let compute_annot annot =
- ignore (Visitor.visitFramacCodeAnnotation preprocessor annot)
+ ignore
+ (Visitor.visitFramacCodeAnnotation
+ (preprocessor :> Visitor.frama_c_inplace)
+ annot)
let compute_predicate p =
- ignore (Visitor.visitFramacPredicate preprocessor p)
+ ignore
+ (Visitor.visitFramacPredicate
+ (preprocessor :> Visitor.frama_c_inplace)
+ p)
end
let preprocess = Preprocessor.compute
diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.mli b/src/plugins/e-acsl/src/analyses/bound_variables.mli
index fd76f29dbe0e102dbadc6fdebb772911ddac93ff..fed7065c6f3a0e165e005394fb31fa26c0e60232 100644
Binary files a/src/plugins/e-acsl/src/analyses/bound_variables.mli and b/src/plugins/e-acsl/src/analyses/bound_variables.mli differ
diff --git a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml
new file mode 100644
index 0000000000000000000000000000000000000000..6a4e932f2fdbc81dbb072dee04740169913f0ec6
--- /dev/null
+++ b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.ml
@@ -0,0 +1,124 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+let case_globals
+ ~default
+ ?(builtin = fun _ -> default ())
+ ?(fc_compiler_builtin = fun _ -> default ())
+ ?(rtl_symbol = fun _ -> default ())
+ ?(fc_stdlib_generated = fun _ -> default ())
+ ?(var_fun_decl = fun _ -> default ())
+ ?(var_init = fun _ -> default ())
+ ?(var_def = fun _ _ -> default ())
+ ~fun_def
+ = function
+ (* library functions and built-ins *)
+ | GVarDecl(vi, _) | GVar(vi, _, _)
+ | GFunDecl(_, vi, _) | GFun({ svar = vi }, _) when Builtins.mem vi.vname ->
+ builtin vi
+
+ (* Cil built-ins and other library globals*)
+ | GVarDecl(vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _)
+ when Misc.is_fc_or_compiler_builtin vi ->
+ fc_compiler_builtin vi
+
+ | g when Rtl.Symbols.mem_global g ->
+ rtl_symbol g
+
+ (* generated function declaration *)
+ | GFunDecl(_, vi, _) when Misc.is_fc_stdlib_generated vi ->
+ fc_stdlib_generated vi
+
+ (* variable declarations *)
+ | GVarDecl(vi, _) | GFunDecl(_, vi, _) ->
+ var_fun_decl vi
+
+ (* variable definition *)
+ | GVar(vi, { init = None }, _) ->
+ var_init vi
+
+ | GVar(vi, { init = Some init }, _) ->
+ var_def vi init
+
+ (* function definition *)
+ | GFun(fundec, _) ->
+ fun_def fundec
+
+ (* other globals: nothing to do *)
+ | GType _
+ | GCompTag _
+ | GCompTagDecl _
+ | GEnumTag _
+ | GEnumTagDecl _
+ | GAsm _
+ | GPragma _
+ | GText _
+ | GAnnot _ (* do never read annotation from sources *)
+ ->
+ default ()
+
+class visitor
+ = object(self)
+ inherit Visitor.frama_c_inplace
+
+ method private default : unit -> global list Cil.visitAction =
+ fun _ -> Cil.SkipChildren
+
+ method builtin : varinfo -> global list Cil.visitAction =
+ fun _ -> self#default ()
+
+ method fc_compiler_builtin : varinfo -> global list Cil.visitAction =
+ fun _ -> self#default ()
+
+ method rtl_symbol : global -> global list Cil.visitAction =
+ fun _ -> self#default ()
+
+ method fc_stdlib_generated : varinfo -> global list Cil.visitAction =
+ fun _ -> self#default ()
+
+ method var_fun_decl : varinfo -> global list Cil.visitAction =
+ fun _ -> self#default ()
+
+ method var_init : varinfo -> global list Cil.visitAction =
+ fun _ -> self#default ()
+
+ method var_def : varinfo -> init -> global list Cil.visitAction =
+ fun _ _ -> self#default ()
+
+ method fun_def ({svar = vi}) =
+ let kf = try Globals.Functions.get vi with Not_found -> assert false in
+ if Functions.check kf then Cil.DoChildren else Cil.SkipChildren
+
+ method !vglob_aux =
+ case_globals
+ ~default:self#default
+ ~builtin:self#builtin
+ ~fc_compiler_builtin:self#fc_compiler_builtin
+ ~rtl_symbol:self#rtl_symbol
+ ~fc_stdlib_generated:self#fc_stdlib_generated
+ ~var_fun_decl:self#var_fun_decl
+ ~var_init:self#var_init
+ ~var_def:self#var_def
+ ~fun_def:self#fun_def
+ end
diff --git a/src/plugins/e-acsl/src/analyses/e_acsl_visitor.mli b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.mli
new file mode 100644
index 0000000000000000000000000000000000000000..7b1fc2e7f9d2dcbb5d87d5891c9a0376e25dde40
--- /dev/null
+++ b/src/plugins/e-acsl/src/analyses/e_acsl_visitor.mli
@@ -0,0 +1,68 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+val case_globals :
+ default:(unit -> 'a) ->
+ ?builtin:(varinfo -> 'a) ->
+ ?fc_compiler_builtin:(varinfo -> 'a) ->
+ ?rtl_symbol:(global -> 'a) ->
+ ?fc_stdlib_generated:(varinfo -> 'a) ->
+ ?var_fun_decl:(varinfo -> 'a) ->
+ ?var_init:(varinfo -> 'a) ->
+ ?var_def:(varinfo -> init -> 'a) ->
+ fun_def:(fundec -> 'a) ->
+ global -> 'a
+(** Function to descend into the root of the ast according to the various cases
+ relevant for E-ACSL. Each of the named argument corresponds to the function
+ to be applied in the corresponding case. The [default] case is used if any
+ optional argument is not given
+ - [builtin] is the case for C builtins
+ - [fc_builtin_compiler] is the case for frama-c or compiler builtins
+ - [rtl_symbol] is the case for any global coming from the runtime library
+ - [fc_stdlib_generated] is the case for frama-c or standard library
+ generated functions
+ - [var_fun_decl] is the case for variables or functions declarations
+ - [var_init] is the case for variable definition wihtout an initialization
+ value
+ - [var_def] is the case for variable definitions with an initialization
+ value
+ - [fun_def] is the case for function definition. *)
+
+(** Visitor for managing the root of the AST, on the globals level, with the
+ cases that are relevant to E-ACSL. Each case is handled by a method of
+ the visitor. The cases are similar, and similarly named as the ones of
+ the function [case_globals]. *)
+class visitor :
+ object
+ inherit Visitor.frama_c_inplace
+ method private default: unit -> global list Cil.visitAction
+ method builtin: varinfo -> global list Cil.visitAction
+ method fc_compiler_builtin: varinfo -> global list Cil.visitAction
+ method rtl_symbol: global -> global list Cil.visitAction
+ method fc_stdlib_generated: varinfo -> global list Cil.visitAction
+ method var_fun_decl: varinfo -> global list Cil.visitAction
+ method var_init: varinfo -> global list Cil.visitAction
+ method var_def: varinfo -> init -> global list Cil.visitAction
+ method fun_def: fundec -> global list Cil.visitAction
+ end
diff --git a/src/plugins/e-acsl/src/analyses/logic_normalizer.ml b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
index 46efb9de68cdb81c771a2c1b7cf55d77754be37c..f98b3485092d29c6659b6a6a989cfe64ffb99acc 100644
--- a/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
+++ b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
@@ -135,7 +135,7 @@ let preprocess_term ~loc t =
| _ -> None
let preprocessor = object
- inherit Visitor.frama_c_inplace
+ inherit E_acsl_visitor.visitor
(* Only logic functions and logic predicates are handled.
E-acsl simply ignores all the other global annotations *)
@@ -144,40 +144,7 @@ let preprocessor = object
| Dfun_or_pred _ -> Cil.DoChildren
| _ -> Cil.SkipChildren
- (* Ignore the annotations attached to statements from the RTL *)
- method !vglob_aux =
- function
- | g when Rtl.Symbols.mem_global g ->
- Cil.SkipChildren
-
- | GFun({ svar = vi }, _) when Builtins.mem vi.vname ->
- Cil.SkipChildren
-
- | GFun({ svar = vi }, _)
- when Misc.is_fc_or_compiler_builtin vi ->
- Cil.SkipChildren
-
- | GFun({svar = vi}, _) ->
- let kf = try Globals.Functions.get vi with Not_found -> assert false in
- if Functions.check kf then Cil.DoChildren else Cil.SkipChildren
-
- | GAnnot _ -> Cil.DoChildren
-
- (* other globals: nothing to do *)
- | GFunDecl _
- | GVarDecl _
- | GVar _
- | GType _
- | GCompTag _
- | GCompTagDecl _
- | GEnumTag _
- | GEnumTagDecl _
- | GAsm _
- | GPragma _
- | GText _
- -> Cil.SkipChildren
-
- method !vpredicate p =
+ method !vpredicate p =
let loc = p.pred_loc in
Memo.memo_pred (preprocess_pred ~loc) p;
Cil.DoChildren
@@ -189,13 +156,19 @@ let preprocessor = object
end
let preprocess ast =
- Visitor.visitFramacFileSameGlobals preprocessor ast
+ Visitor.visitFramacFileSameGlobals
+ (preprocessor :> Visitor.frama_c_inplace)
+ ast
let preprocess_annot annot =
- ignore (Visitor.visitFramacCodeAnnotation preprocessor annot)
+ ignore
+ (Visitor.visitFramacCodeAnnotation
+ (preprocessor :> Visitor.frama_c_inplace)
+ annot)
let preprocess_predicate p =
- ignore (Visitor.visitFramacPredicate preprocessor p)
+ ignore
+ (Visitor.visitFramacPredicate (preprocessor :> Visitor.frama_c_inplace) p)
let get_pred = Memo.get_pred
let get_term = Memo.get_term
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 456f0e7d5234d24526ba4f326876639ec1f52e32..f993c860397bc69cf7ef77d50598983fa2487be1 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -197,8 +197,9 @@ module Memo: sig
?lenv:Function_params_ty.t ->
(term -> computed_info) ->
term ->
- computed_info
- val get: ?lenv:Function_params_ty.t -> term -> computed_info
+ computed_info Error.or_error
+ val get: ?lenv:Function_params_ty.t -> term ->
+ computed_info Error.or_error
val clear: unit -> unit
end = struct
@@ -216,7 +217,8 @@ end = struct
the guard and once for encoding [x+1] when incrementing it. The
memoization is only useful here and indeed prevent the generation of one
extra variable in some cases. *)
- let tbl = Misc.Id_term.Hashtbl.create 97
+ let tbl : computed_info Error.or_error Misc.Id_term.Hashtbl.t =
+ Misc.Id_term.Hashtbl.create 97
(* The type of the logic function
\\@ logic integer f (integer x) = x + 1;
@@ -228,23 +230,16 @@ end = struct
We distinguish the calls to the function by storing the type of the
arguments corresponding to each call, and we weaken the typing so that it
is invariant when the arguments have the same type. *)
- let dep_tbl : computed_info Id_term_with_lenv.Hashtbl.t
+ let dep_tbl : computed_info Error.or_error Id_term_with_lenv.Hashtbl.t
= Id_term_with_lenv.Hashtbl.create 97
let get_dep lenv t =
- try
- Id_term_with_lenv.Hashtbl.find dep_tbl (t,lenv)
- with Not_found ->
- Options.fatal
- "[typing] type of term '%a' was never computed with arguments '%a'."
- Printer.pp_term t Function_params_ty.pretty lenv
+ try Id_term_with_lenv.Hashtbl.find dep_tbl (t,lenv)
+ with Not_found -> Error.not_memoized ()
let get_nondep t =
try Misc.Id_term.Hashtbl.find tbl t
- with Not_found ->
- Options.fatal
- "[typing] type of term '%a' was never computed."
- Printer.pp_term t
+ with Not_found -> Error.not_memoized ()
let get ?(lenv=[]) t =
match lenv with
@@ -254,7 +249,10 @@ end = struct
let memo_nondep f t =
try Misc.Id_term.Hashtbl.find tbl t
with Not_found ->
- let x = f t in
+ let x =
+ try Error.Res (f t)
+ with Error.Not_yet _ | Error.Typing_error _ as exn -> Error.Err exn
+ in
Misc.Id_term.Hashtbl.add tbl t x;
x
@@ -262,9 +260,12 @@ end = struct
try
Id_term_with_lenv.Hashtbl.find dep_tbl (t, lenv)
with Not_found ->
- let ty = f t in
- Id_term_with_lenv.Hashtbl.add dep_tbl (t, lenv) ty;
- ty
+ let x =
+ try Error.Res (f t)
+ with Error.Not_yet _ | Error.Typing_error _ as exn -> Error.Err exn
+ in
+ Id_term_with_lenv.Hashtbl.add dep_tbl (t, lenv) x;
+ x
let memo ?(lenv=[]) f t =
match lenv with
@@ -678,13 +679,17 @@ let rec type_term
| Tempty_set -> dup Nan
in
let t = Logic_normalizer.get_term t in
- Memo.memo ~lenv
- (fun t ->
- let ty, op = infer t in
- match ctx with
- | None -> { ty; op; cast = None }
- | Some ctx -> coerce ~arith_operand ~ctx ~op ty)
- t
+ match
+ Memo.memo ~lenv
+ (fun t ->
+ let ty, op = infer t in
+ match ctx with
+ | None -> { ty; op; cast = None }
+ | Some ctx -> coerce ~arith_operand ~ctx ~op ty)
+ t
+ with
+ | Res res -> res
+ | Err exn -> raise exn
and type_term_lval ~lenv (host, offset) =
type_term_lhost ~lenv host;
@@ -870,22 +875,21 @@ and type_predicate ?(lenv=[]) p =
ignore (type_term ~use_gmp_opt:true ~lenv li_t);
(type_predicate ~lenv p).ty
| Pforall _
- | Pexists _ -> begin
- match Bound_variables.get_preprocessed_quantifier p with
- (* If there is no preprocessed form for the quantifier, it means that
- the preprocessing phase raised an error. It is costly to analyze
- again and determine what was the error, so instead we raise the
- exception [Ignored] which signifies that no error message should
- be displayed *)
- | None -> Error.ignored ()
- | Some (guards, goal) ->
- let guards =
- List.map
- (fun (t1, x, t2) ->
- type_bound_variables ~loc:p.pred_loc ~lenv (t1, x, t2))
- guards
- in Bound_variables.replace p guards goal;
- (type_predicate ~lenv goal).ty
+ | Pexists _ ->
+ begin
+ let guards, goal =
+ Error.retrieve_preprocessing
+ "quantified predicate"
+ Bound_variables.get_preprocessed_quantifier
+ p
+ in
+ let guards =
+ List.map
+ (fun (t1, x, t2) ->
+ type_bound_variables ~loc:p.pred_loc ~lenv (t1, x, t2))
+ guards
+ in Bound_variables.replace p guards goal;
+ (type_predicate ~lenv goal).ty
end
| Pseparated tlist ->
List.iter
@@ -931,8 +935,10 @@ let unsafe_set t ?ctx ty =
(** {2 Getters} *)
(******************************************************************************)
-let get_number_ty ~lenv t = (Memo.get ~lenv t).ty
-let get_integer_op ~lenv t = (Memo.get ~lenv t).op
+let get_number_ty ~lenv t =
+ (Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t).ty
+let get_integer_op ~lenv t =
+ (Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t).op
let get_integer_op_of_predicate ~lenv p = (type_predicate ~lenv p).op
(* {!typ_of_integer}, but handle the not-integer cases. *)
@@ -948,15 +954,15 @@ let extract_typ t ty =
| Larrow _ -> Error.not_yet "unsupported logic type: type arrow"
let get_typ ~lenv t =
- let info = Memo.get ~lenv t in
+ let info = Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t in
extract_typ t info.ty
let get_op ~lenv t =
- let info = Memo.get ~lenv t in
+ let info = Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t in
extract_typ t info.op
let get_cast ~lenv t =
- let info = Memo.get ~lenv t in
+ let info = Error.retrieve_preprocessing "typing" (Memo.get ~lenv) t in
try Option.map typ_of_number_ty info.cast
with Not_a_number -> None
@@ -967,58 +973,37 @@ let get_cast_of_predicate ~lenv p =
let clear = Memo.clear
-open Cil_types
-
let typer_visitor lenv = object
- inherit Visitor.frama_c_inplace
-
- method !vglob_aux =
- function
- (* library functions and built-ins *)
- | GFun({ svar = vi }, _) when Builtins.mem vi.vname ->
- Cil.SkipChildren
-
- | GFun({ svar = vi }, _)
- when Misc.is_fc_or_compiler_builtin vi ->
- Cil.SkipChildren
-
- | g when Rtl.Symbols.mem_global g ->
- Cil.SkipChildren
-
- | GFun({svar = vi}, _) ->
- let kf = try Globals.Functions.get vi with Not_found -> assert false in
- if Functions.check kf then Cil.DoChildren else Cil.SkipChildren
-
- (* other globals: nothing to do *)
- | GFunDecl _
- | GVarDecl _
- | GVar _
- | GType _
- | GCompTag _
- | GCompTagDecl _
- | GEnumTag _
- | GEnumTagDecl _
- | GAsm _
- | GPragma _
- | GText _
- | GAnnot _
- -> Cil.SkipChildren
+ inherit E_acsl_visitor.visitor
method !vpredicate p =
- Error.generic_handle (type_named_predicate ~lenv) () p;
+ (* Do not raise a warning for e-acsl errors at preprocessing time,
+ those errrors are stored in the table and warnings are raised at
+ translation time*)
+ let _ = try type_named_predicate ~lenv p
+ with Error.Not_yet _ | Error.Typing_error _ -> ()
+ in
Cil.SkipChildren
end
let type_program ast =
- Visitor.visitFramacFileSameGlobals (typer_visitor []) ast
+ Visitor.visitFramacFileSameGlobals
+ (typer_visitor [] :> Visitor.frama_c_inplace)
+ ast
let type_code_annot lenv annot =
- ignore (Visitor.visitFramacCodeAnnotation (typer_visitor lenv) annot)
+ ignore
+ (Visitor.visitFramacCodeAnnotation
+ (typer_visitor lenv :> Visitor.frama_c_inplace)
+ annot)
let preprocess_predicate lenv p =
Logic_normalizer.preprocess_predicate p;
Bound_variables.preprocess_predicate p;
- ignore (Visitor.visitFramacPredicate (typer_visitor lenv) p)
+ ignore
+ (Visitor.visitFramacPredicate
+ (typer_visitor lenv :> Visitor.frama_c_inplace)
+ p)
let preprocess_rte ~lenv rte =
Logic_normalizer.preprocess_annot rte;
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index f4686759f3d9cdde894266b34ed634e2080a6f93..f035c49cccbf839490a74834949484e17de2a47a 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -621,61 +621,32 @@ let unghost_vi vi =
| _ ->
()
-let inject_in_global (env, main) = function
- (* library functions and built-ins *)
- | GVarDecl(vi, _) | GVar(vi, _, _)
- | GFunDecl(_, vi, _) | GFun({ svar = vi }, _) when Builtins.mem vi.vname ->
- Builtins.update vi.vname vi;
- env, main
-
- (* Cil built-ins and other library globals: nothing to do *)
- | GVarDecl(vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _)
- when Misc.is_fc_or_compiler_builtin vi ->
- env, main
- | g when Rtl.Symbols.mem_global g ->
- env, main
- (* generated function declaration: nothing to do *)
- | GFunDecl(_, vi, _) when Misc.is_fc_stdlib_generated vi ->
- env, main
-
- (* variable declarations *)
- | GVarDecl(vi, _) | GFunDecl(_, vi, _) ->
- unghost_vi vi;
- Global_observer.add vi;
- env, main
-
- (* variable definition *)
- | GVar(vi, { init = None }, _) ->
- Global_observer.add vi;
- unghost_vi vi;
- env, main
-
- | GVar(vi, { init = Some init }, _) ->
+let inject_in_global (env, main) global =
+ let update_builtin vi = Builtins.update vi.vname vi; env, main in
+ let observe_and_unghost vi =
+ unghost_vi vi; Global_observer.add vi; env, main
+ in
+ let var_def vi init =
Global_observer.add vi;
unghost_vi vi;
let _init, env = inject_in_init env None vi NoOffset init in
- (* ignore the new initializer that handles literal strings since they are
- not substituted in global initializers (see
- [replace_literal_string_in_exp]) *)
+ (* ignore the new initializer that handles literal strings
+ since they are not substituted in global initializers
+ (see [replace_literal_string_in_exp]) *)
env, main
-
- (* function definition *)
- | GFun({ svar = vi } as fundec, _) ->
+ in
+ let fun_def ({svar = vi} as fundec) =
unghost_vi vi;
inject_in_fundec main fundec
-
- (* other globals: nothing to do *)
- | GType _
- | GCompTag _
- | GCompTagDecl _
- | GEnumTag _
- | GEnumTagDecl _
- | GAsm _
- | GPragma _
- | GText _
- | GAnnot _ (* do never read annotation from sources *)
- ->
- env, main
+ in
+ E_acsl_visitor.case_globals
+ ~default:(fun () -> env, main)
+ ~builtin:update_builtin
+ ~var_fun_decl:observe_and_unghost
+ ~var_init:observe_and_unghost
+ ~var_def
+ ~fun_def
+ global
(* Insert [stmt_begin] as the first statement of [fundec] and insert [stmt_end] as
the last before [return] *)
diff --git a/src/plugins/e-acsl/src/code_generator/quantif.ml b/src/plugins/e-acsl/src/code_generator/quantif.ml
index be2f7f342069e7b048c43038f8c3f3b7a77dbed1..d569c5df9ee9c84e8e3a789109d9c7231926d57e 100644
--- a/src/plugins/e-acsl/src/code_generator/quantif.ml
+++ b/src/plugins/e-acsl/src/code_generator/quantif.ml
@@ -66,88 +66,91 @@ module Label_ids =
let convert kf env loc ~is_forall quantif =
(* guarded quantification over integers (or a subtype of integer) *)
- match Bound_variables.get_preprocessed_quantifier quantif with
- | None -> Error.ignored ()
- | Some (bound_vars, goal) ->
- match has_empty_quantif_with_false_negative bound_vars, is_forall with
- | true, true ->
- Cil.one ~loc, env
- | true, false ->
- Cil.zero ~loc, env
- | false, _ ->
- begin
- (* create different "initial value", "found value" and guard expression
- for the predicate depending on the type of quantification *)
- let init_val, found_val, mk_guard =
- let z = zero ~loc in
- let o = one ~loc in
- if is_forall then o, z, fun x -> x
- else z, o, fun e -> Smart_exp.lnot ~loc:e.eloc e
- in
- (* transform [bound_vars] into [lscope_var list],
- and update logic scope in the process *)
- let lvs_guards, env = List.fold_right
- (fun (t1, lv, t2) (lvs_guards, env) ->
- let lvs = Lscope.Lvs_quantif (t1, Rle, lv, Rlt, t2) in
- let env = Env.Logic_scope.extend env lvs in
- lvs :: lvs_guards, env)
- bound_vars
- ([], env)
+ let bound_vars, goal =
+ Error.retrieve_preprocessing
+ "quantified predicate"
+ Bound_variables.get_preprocessed_quantifier
+ quantif
+ in
+ match has_empty_quantif_with_false_negative bound_vars, is_forall with
+ | true, true ->
+ Cil.one ~loc, env
+ | true, false ->
+ Cil.zero ~loc, env
+ | false, _ ->
+ begin
+ (* create different "initial value", "found value" and guard expression
+ for the predicate depending on the type of quantification *)
+ let init_val, found_val, mk_guard =
+ let z = zero ~loc in
+ let o = one ~loc in
+ if is_forall then o, z, fun x -> x
+ else z, o, fun e -> Smart_exp.lnot ~loc:e.eloc e
+ in
+ (* transform [bound_vars] into [lscope_var list],
+ and update logic scope in the process *)
+ let lvs_guards, env = List.fold_right
+ (fun (t1, lv, t2) (lvs_guards, env) ->
+ let lvs = Lscope.Lvs_quantif (t1, Rle, lv, Rlt, t2) in
+ let env = Env.Logic_scope.extend env lvs in
+ lvs :: lvs_guards, env)
+ bound_vars
+ ([], env)
+ in
+ let var_res, res, env =
+ (* variable storing the result of the quantifier *)
+ let name = if is_forall then "forall" else "exists" in
+ Env.new_var
+ ~loc
+ ~name
+ env
+ kf
+ None
+ intType
+ (fun v _ ->
+ let lv = var v in
+ [ Smart_stmt.assigns ~loc ~result:lv init_val ])
+ in
+ let end_loop_ref = ref dummyStmt in
+ (* innermost block *)
+ let mk_innermost_block env =
+ (* innermost loop body: store the result in [res] and go out according
+ to evaluation of the goal *)
+ let predicate_to_exp = !predicate_to_exp_ref ~adata:Assert.no_data in
+ let test, _, env = predicate_to_exp kf (Env.push env) goal in
+ let then_blk = mkBlock [ mkEmptyStmt ~loc () ] in
+ let else_blk =
+ (* use a 'goto', not a simple 'break' in order to handle 'forall' with
+ multiple binders (leading to imbricated loops) *)
+ mkBlock
+ [ Smart_stmt.assigns ~loc ~result:(var var_res) found_val;
+ mkStmt ~valid_sid:true (Goto(end_loop_ref, loc)) ]
in
- let var_res, res, env =
- (* variable storing the result of the quantifier *)
- let name = if is_forall then "forall" else "exists" in
- Env.new_var
- ~loc
- ~name
+ let blk, env =
+ Env.pop_and_get
env
- kf
- None
- intType
- (fun v _ ->
- let lv = var v in
- [ Smart_stmt.assigns ~loc ~result:lv init_val ])
- in
- let end_loop_ref = ref dummyStmt in
- (* innermost block *)
- let mk_innermost_block env =
- (* innermost loop body: store the result in [res] and go out according
- to evaluation of the goal *)
- let predicate_to_exp = !predicate_to_exp_ref ~adata:Assert.no_data in
- let test, _, env = predicate_to_exp kf (Env.push env) goal in
- let then_blk = mkBlock [ mkEmptyStmt ~loc () ] in
- let else_blk =
- (* use a 'goto', not a simple 'break' in order to handle 'forall' with
- multiple binders (leading to imbricated loops) *)
- mkBlock
- [ Smart_stmt.assigns ~loc ~result:(var var_res) found_val;
- mkStmt ~valid_sid:true (Goto(end_loop_ref, loc)) ]
- in
- let blk, env =
- Env.pop_and_get
- env
- (Smart_stmt.if_stmt ~loc ~cond:(mk_guard test) then_blk ~else_blk)
- ~global_clear:false
- Env.After
- in
- let blk = Cil.flatten_transient_sub_blocks blk in
- [ Smart_stmt.block_stmt blk ], env
+ (Smart_stmt.if_stmt ~loc ~cond:(mk_guard test) then_blk ~else_blk)
+ ~global_clear:false
+ Env.After
in
- let stmts, env =
- Loops.mk_nested_loops ~loc mk_innermost_block kf env lvs_guards
- in
- let env =
- Env.add_stmt env kf (Smart_stmt.block_stmt (mkBlock stmts))
- in
- (* where to jump to go out of the loop *)
- let end_loop = mkEmptyStmt ~loc () in
- let label_name = "e_acsl_end_loop" ^ string_of_int (Label_ids.next ()) in
- let label = Label(label_name, loc, false) in
- end_loop.labels <- label :: end_loop.labels;
- end_loop_ref := end_loop;
- let env = Env.add_stmt env kf end_loop in
- res, env
- end
+ let blk = Cil.flatten_transient_sub_blocks blk in
+ [ Smart_stmt.block_stmt blk ], env
+ in
+ let stmts, env =
+ Loops.mk_nested_loops ~loc mk_innermost_block kf env lvs_guards
+ in
+ let env =
+ Env.add_stmt env kf (Smart_stmt.block_stmt (mkBlock stmts))
+ in
+ (* where to jump to go out of the loop *)
+ let end_loop = mkEmptyStmt ~loc () in
+ let label_name = "e_acsl_end_loop" ^ string_of_int (Label_ids.next ()) in
+ let label = Label(label_name, loc, false) in
+ end_loop.labels <- label :: end_loop.labels;
+ end_loop_ref := end_loop;
+ let env = Env.add_stmt env kf end_loop in
+ res, env
+ end
let quantif_to_exp kf env p =
let loc = p.pred_loc in
diff --git a/src/plugins/e-acsl/src/libraries/error.ml b/src/plugins/e-acsl/src/libraries/error.ml
index ad46049b2928299d1f4c2329ab5518a7793aba09..202366afded83098265d405b7f26a48dad720d33 100644
--- a/src/plugins/e-acsl/src/libraries/error.ml
+++ b/src/plugins/e-acsl/src/libraries/error.ml
@@ -29,6 +29,9 @@ let untypable s = raise (Typing_error s)
exception Not_yet of string
let not_yet s = raise (Not_yet s)
+exception Not_memoized
+let not_memoized () = raise Not_memoized
+
module Nb_typing =
State_builder.Ref
(Datatype.Int)
@@ -74,6 +77,16 @@ let generic_handle f res x =
let handle f x = generic_handle f x x
+type 'a or_error = Res of 'a | Err of exn
+
+let retrieve_preprocessing analyse_name getter parameter =
+ try
+ match getter parameter with
+ | Res res -> res
+ | Err exn -> raise exn
+ with Not_memoized ->
+ Options.fatal "%s was not performed on construct" analyse_name
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/src/libraries/error.mli b/src/plugins/e-acsl/src/libraries/error.mli
index bfde94f602c323ae8f4aab177bfc801168185c3d..be38598dd1b71ae8c3f1b432dcd12cbfa1e5f5f9 100644
--- a/src/plugins/e-acsl/src/libraries/error.mli
+++ b/src/plugins/e-acsl/src/libraries/error.mli
@@ -25,6 +25,9 @@
exception Ignored
exception Typing_error of string
exception Not_yet of string
+exception Not_memoized
+
+type 'a or_error = Res of 'a | Err of exn
val untypable: string -> 'a
(** Type error built from the given argument. *)
@@ -35,6 +38,10 @@ val not_yet: string -> 'a
val ignored: unit -> 'a
(** Statement already signaled and marked as ignored *)
+val not_memoized : unit -> 'a
+(** @raise Not_memoized when asking the preprocessed form of something that
+ was not preprocessed *)
+
val handle: ('a -> 'a) -> 'a -> 'a
(** Run the closure with the given argument and handle potential errors.
Return the provide argument in case of errors. *)
@@ -52,6 +59,11 @@ val nb_not_yet: unit -> int
val print_not_yet: string -> unit
(** Print the "not yet" message without raising an exception. *)
+val retrieve_preprocessing: string -> ('a -> 'b or_error) -> 'a -> 'b
+(** Retrieve the result of a preprocessing phase, which possibly failed.
+ The [string] argument is used to display a message in case the preprocessing
+ phase did not compute the required result. *)
+
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
index abb0a4b867b9cc06cf9b53f3ce515b1cf529eb7c..6aebd3583d94ca969621b0130e324f1f8aec2d6b 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
@@ -1,34 +1,30 @@
[e-acsl] beginning translation.
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
+[e-acsl] FRAMAC_SHARE/libc/string.h:379: Warning:
+ E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:388: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:389: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:391: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:392: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:379: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:378: Warning:
Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations.
[e-acsl] FRAMAC_SHARE/libc/string.h:378: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:389: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:392: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/bts/bts2252.c:17: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle
index 99eb8b87048de208995e26ad5544d36eb211a1d7..785bb4d1a1e21157ee06063aaaac742b0d19d976 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-40.res.oracle
@@ -2,15 +2,6 @@
[e-acsl] Warning: annotating undefined function `fopen':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdio.h:155: Warning:
- E-ACSL construct
- `logic functions or predicates with no definition nor reads clause'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:350: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
index 0f0aa26e6d14542c8f36a0b17799cea189aee69e..fcc76624c98e753c5e2bd700d0f26ffcc45bcf4b 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
@@ -116,7 +116,7 @@ char *__gen_e_acsl_strdup(char const *s);
__inline static void fail_ncomp(int cond, char *fmt, int l, int r)
{
if (cond) {
- fprintf(stderr,(char const *)fmt,l,r); /* fprintf_fallback_1 */
+ fprintf(stderr,(char const *)fmt,l,r); /* fprintf_va_6 */
__gen_e_acsl_abort();
}
return;
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
index 62a192f51bb497bafc4593371ad9b0a29aa1e3ef..3367e2acfe62389f490071eedf4a433b181cc886 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
@@ -1,6 +1,5 @@
[variadic] tests/builtin/strcmp.c:11: Warning:
- Call to function fprintf with non-static format argument:
- no specification will be generated.
+ Call to function fprintf with non-static format argument: assuming that parameters are coherent with the format, and that no %n specifiers are present in the actual string.
[e-acsl] beginning translation.
[e-acsl] Warning: annotating undefined function `abort':
the generated program may miss memory instrumentation
@@ -17,28 +16,6 @@
[e-acsl] Warning: annotating undefined function `strdup':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:488: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:491: Warning:
- E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:495: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:278: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
@@ -59,6 +36,8 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:491: Warning:
+ E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
index 6d74b78c4afc235b980f246374e40a7ed1a19c5c..3e8329fdab9843ee60527c5553ba99d3fd33d7d0 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
@@ -11,28 +11,6 @@
[e-acsl] Warning: annotating undefined function `strdup':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:488: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:491: Warning:
- E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:495: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:278: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
@@ -53,6 +31,8 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:491: Warning:
+ E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
index 2a293aeb5a71df9b7843ceaf791a0bc6ab4ed61f..63fa3d663a20e3ea37390b3ff59807ccabe20f05 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
+++ b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
@@ -14,28 +14,6 @@
[e-acsl] Warning: annotating undefined function `strdup':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:488: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:491: Warning:
- E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:495: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:278: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
@@ -56,6 +34,8 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:484: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:491: Warning:
+ E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:493: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
diff --git a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
index 7802760e7ec64d97faa5d42c9ccb54934ce27c63..28f90799844b6840f81cc10717ea7f2075b735fb 100644
--- a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
@@ -14,11 +14,6 @@
[e-acsl] Warning: annotating undefined function `fork':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/stdio.h:97: Warning:
- E-ACSL construct
- `logic functions or predicates with no definition nor reads clause'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
index 7e89d6bf65fb59bc622fec23ce63f326b7028103..2b791e3541a23ef13830317b9ea07bbe17a1835d 100644
--- a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
@@ -20,15 +20,8 @@
[e-acsl] Warning: annotating undefined function `strchr':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/string.h:181: Warning:
- E-ACSL construct
- `non integer variable p in quantification
- result_first_occur:
- \forall char *p; \old(s) <= p < \result ==> *p != (char)\old(c)'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
+[e-acsl] FRAMAC_SHARE/libc/string.h:367: Warning:
+ E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:368: Warning:
@@ -39,45 +32,33 @@
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:367: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:373: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:173: Warning:
+ E-ACSL construct `logic functions or predicates with labels'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:176: Warning:
E-ACSL construct `user-defined logic type' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:179: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:183: Warning:
E-ACSL construct `user-defined logic type' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:143: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:367: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:370: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:367: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:173: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:173: Warning:
Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations.
[e-acsl] FRAMAC_SHARE/libc/string.h:173: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:179: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
@@ -96,6 +77,10 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:141: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:143: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/unistd.h:843: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
index 1df935d00f5814645015d240d06a8c182774bd74..e66ace13b42b0c23943de0125ef7c106870e94e9 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/file.res.oracle
@@ -2,15 +2,6 @@
[e-acsl] Warning: annotating undefined function `fopen':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdio.h:155: Warning:
- E-ACSL construct
- `logic functions or predicates with no definition nor reads clause'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdio.h:350: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
index 063513be8b69a14d5df4c5e2f38ba83debea7ce5..234a0c3eb0ee7ec3bb6181e7a8d94a4d3878cbc0 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/mem.res.oracle
@@ -1,15 +1,4 @@
[e-acsl] beginning translation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:134: Warning:
- E-ACSL construct `user-defined logic type' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:124: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:101: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:131: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
@@ -17,6 +6,9 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:131: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:134: Warning:
+ E-ACSL construct `user-defined logic type' is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:120: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
@@ -28,6 +20,10 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:120: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:124: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
@@ -39,6 +35,10 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:101: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] FRAMAC_SHARE/libc/string.h:135: Warning:
function __e_acsl_assert_register_ptr: precondition data->values == \null ||
diff --git a/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle b/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
index 2e04b464ae0b12258d1104ea66575204cfff0230..92c864736fb000c03417c43e377e3d1ef73988b7 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
+++ b/src/plugins/e-acsl/tests/libc/oracle/str.res.oracle
@@ -1,25 +1,21 @@
[e-acsl] beginning translation.
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
+[e-acsl] FRAMAC_SHARE/libc/string.h:439: Warning:
+ E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:278: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
+[e-acsl] FRAMAC_SHARE/libc/string.h:440: Warning:
+ E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:445: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:446: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
+ E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:450: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
+[e-acsl] FRAMAC_SHARE/libc/string.h:453: Warning:
+ E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:453: Warning:
+[e-acsl] FRAMAC_SHARE/libc/string.h:446: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
@@ -27,105 +23,85 @@
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:458: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
+[e-acsl] FRAMAC_SHARE/libc/string.h:438: Warning:
+ Some assumes clauses could not be translated.
+ Ignoring complete and disjoint behaviors annotations.
+[e-acsl] FRAMAC_SHARE/libc/string.h:438: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:426: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
+[e-acsl] FRAMAC_SHARE/libc/string.h:443: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:429: Warning:
+[e-acsl] FRAMAC_SHARE/libc/string.h:450: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:432: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
+[e-acsl] FRAMAC_SHARE/libc/string.h:450: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:433: Warning:
+[e-acsl] FRAMAC_SHARE/libc/string.h:458: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:388: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
+[e-acsl] FRAMAC_SHARE/libc/string.h:424: Warning:
+ E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:389: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
+[e-acsl] FRAMAC_SHARE/libc/string.h:425: Warning:
+ E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:391: Warning:
+[e-acsl] FRAMAC_SHARE/libc/string.h:426: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:392: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
+[e-acsl] FRAMAC_SHARE/libc/string.h:423: Warning:
+ E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:368: Warning:
+[e-acsl] FRAMAC_SHARE/libc/string.h:429: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:370: Warning:
+[e-acsl] FRAMAC_SHARE/libc/string.h:432: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:373: Warning:
+[e-acsl] FRAMAC_SHARE/libc/string.h:433: Warning:
E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:439: Warning:
- E-ACSL construct `logic functions or predicates with labels'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:440: Warning:
+[e-acsl] FRAMAC_SHARE/libc/string.h:379: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:445: Warning:
- E-ACSL construct `logic functions or predicates with labels'
+[e-acsl] FRAMAC_SHARE/libc/string.h:388: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:453: Warning:
- E-ACSL construct `logic functions or predicates with labels'
+[e-acsl] FRAMAC_SHARE/libc/string.h:391: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:438: Warning:
+[e-acsl] FRAMAC_SHARE/libc/string.h:378: Warning:
Some assumes clauses could not be translated.
Ignoring complete and disjoint behaviors annotations.
-[e-acsl] FRAMAC_SHARE/libc/string.h:438: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:443: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:450: Warning:
+[e-acsl] FRAMAC_SHARE/libc/string.h:378: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:424: Warning:
- E-ACSL construct `logic functions or predicates with labels'
+[e-acsl] FRAMAC_SHARE/libc/string.h:389: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:425: Warning:
- E-ACSL construct `logic functions or predicates with labels'
+[e-acsl] FRAMAC_SHARE/libc/string.h:392: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:423: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:379: Warning:
+[e-acsl] FRAMAC_SHARE/libc/string.h:367: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:378: Warning:
- Some assumes clauses could not be translated.
- Ignoring complete and disjoint behaviors annotations.
-[e-acsl] FRAMAC_SHARE/libc/string.h:378: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:367: Warning:
- E-ACSL construct `logic functions or predicates with labels'
+[e-acsl] FRAMAC_SHARE/libc/string.h:368: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:370: Warning:
@@ -135,6 +111,10 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:367: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:373: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/libc/str.c:12: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
diff --git a/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle
index 201473ea00c1c7cd15e8baf4f3b9b973bcf2fe0f..cf4f531b3ee983c209330fb353666577caa839c6 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle
@@ -2,14 +2,6 @@
[e-acsl] Warning: annotating undefined function `strlen':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:143: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:141: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
@@ -17,6 +9,10 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:141: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:143: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/memory/mainargs.c:7: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
diff --git a/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
index 476e946ba75399bcc809e56f6827a993e559e38e..362b90a9aa1066abdeab79981edb2bd136cff44a 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
@@ -2,16 +2,6 @@
[e-acsl] Warning: annotating undefined function `posix_memalign':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:675: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:679: Warning:
- E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdlib.h:682: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning:
E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:675: Warning:
@@ -28,6 +18,8 @@
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:665: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/stdlib.h:679: Warning:
+ E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:680: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
index 23536de8173f67a8dc6af747788123c5fe67b928..7936c2eba8e8ddf4880fffdd44b734ce70929b3d 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
@@ -2,10 +2,6 @@
[e-acsl] Warning: annotating undefined function `getenv':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] FRAMAC_SHARE/libc/__fc_string_axiomatic.h:281: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/stdlib.h:486: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
index 712744e8ddd0287b1c780b0f1c256ce1177e266d..322634c9ecbdd994890c2c5dc7be36316aa80871 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
@@ -1,11 +1,4 @@
[e-acsl] beginning translation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:134: Warning:
- E-ACSL construct `user-defined logic type' is not yet supported.
- Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/string.h:101: Warning:
- E-ACSL construct `logic functions or predicates performing read accesses'
- is not yet supported.
- Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:131: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
@@ -13,6 +6,9 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:131: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:134: Warning:
+ E-ACSL construct `user-defined logic type' is not yet supported.
+ Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning:
E-ACSL construct `logic functions or predicates with labels'
is not yet supported.
@@ -24,6 +20,10 @@
[e-acsl] FRAMAC_SHARE/libc/string.h:95: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
+[e-acsl] FRAMAC_SHARE/libc/string.h:101: Warning:
+ E-ACSL construct `logic functions or predicates performing read accesses'
+ is not yet supported.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/temporal/t_memcpy.c:20: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
diff --git a/src/plugins/metrics/metrics_cabs.ml b/src/plugins/metrics/metrics_cabs.ml
index 5f7929d605735f42fd156d47c60b687ab3f8e295..315698ea973cbc168f0fd59e634f9b33257602a9 100644
--- a/src/plugins/metrics/metrics_cabs.ml
+++ b/src/plugins/metrics/metrics_cabs.ml
@@ -114,6 +114,7 @@ class metricsCabsVisitor = object(self)
| ONLYTYPEDEF _
| GLOBASM _
| PRAGMA _
+ | STATIC_ASSERT _
| LINKAGE _
| CUSTOM _
| GLOBANNOT _ -> Cil.DoChildren;
diff --git a/src/plugins/variadic/standard.ml b/src/plugins/variadic/standard.ml
index 7b7deeeaf33514d0aa63683d05db7801e0063fe5..9e927870b2a0d3cfb34ee59fd980823934618ba4 100644
--- a/src/plugins/variadic/standard.ml
+++ b/src/plugins/variadic/standard.ml
@@ -618,6 +618,108 @@ let build_specialized_fun env vf format_fun tvparams =
(* --- Call translation --- *)
+let format_of_ikind = function
+ | IBool -> Some `hh, `u
+ | IChar -> None, `c
+ | ISChar -> Some `hh, `d
+ | IUChar -> Some `hh, `u
+ | IInt -> None, `d
+ | IUInt -> None, `u
+ | IShort -> Some `h, `d
+ | IUShort -> Some `h, `u
+ | ILong -> Some `l, `d
+ | IULong -> Some `l, `u
+ | ILongLong -> Some `ll, `d
+ | IULongLong -> Some `ll, `u
+
+let format_of_fkind k = function
+ | FFloat -> None, `f
+ | FDouble ->
+ (match k with
+ | Format_types.PrintfLike -> None, `f
+ | ScanfLike -> Some `l, `f)
+ | FLongDouble -> Some `L, `f
+
+let rec format_of_type vf k t =
+ match t with
+ | TInt (ikind,_) | TEnum ({ekind = ikind},_) -> format_of_ikind ikind
+ | TFloat (fkind,_) -> format_of_fkind k fkind
+ | TPtr(_,_) ->
+ (* technically, we might still want to write/read the actual pointer,
+ but this is not the most likely possibility. *)
+ if Cil.isCharPtrType t then
+ None, `s
+ else
+ None, `p
+ | TNamed ({tname;ttype},_) ->
+ (match tname with
+ | "size_t" -> Some `z, `u
+ | "ptrdiff_t" -> Some `t, `d
+ | "intmax_t" -> Some `j, `d
+ | "uintmax_t" -> Some `j, `u
+ (* not really standard, but that's what glibc does. *)
+ | "ssize_t" -> Some `z, `d
+ | _ -> format_of_type vf k ttype
+ )
+ (* in the case of a scanf-like function, it might happen
+ that we pass a void* whose actual type is coherent with
+ the format string itself, but this can't really be checked
+ here.
+ *)
+ | TVoid _ -> raise (Translate_call_exn vf.vf_decl)
+
+ (* these cases should not happen anyway *)
+ | TComp _
+ | TFun _
+ | TArray _
+ | TBuiltin_va_list _ -> raise (Translate_call_exn vf.vf_decl)
+
+let infer_format_from_args vf format_fun args =
+ let args = List.drop (format_fun.f_format_pos + 1) args in
+ let f_format (l,s) =
+ Format_types.(
+ Specification
+ { f_flags = [];
+ f_field_width = None;
+ f_precision = None;
+ f_length_modifier = l;
+ f_conversion_specifier = s;
+ f_capitalize = false;
+ })
+ in
+ let s_format (l,s) =
+ Format_types.(
+ Specification
+ { s_assignment_suppression = false;
+ s_field_width = None;
+ s_length_modifier = l;
+ s_conversion_specifier = s;
+ }
+ )
+ in
+ let treat_one_arg arg =
+ let t = Cil.typeOf arg in
+ let t =
+ match format_fun.f_kind with
+ | PrintfLike -> t
+ | ScanfLike ->
+ if not (Cil.isPointerType t) then begin
+ let source = fst arg.eloc in
+ Self.warning ~source
+ "Expecting pointer as parameter of scanf function. \
+ Argument %a has type %a"
+ Printer.pp_exp arg Printer.pp_typ t;
+ raise (Translate_call_exn vf.vf_decl);
+ end;
+ Cil.typeOf_pointed t
+ in
+ format_of_type vf format_fun.f_kind t
+ in
+ let format = List.map treat_one_arg args in
+ match format_fun.f_kind with
+ | PrintfLike -> Format_types.FFormat (List.map f_format format)
+ | ScanfLike -> Format_types.SFormat (List.map s_format format)
+
let format_fun_call ~fundec env format_fun scope loc mk_call vf args =
(* Extract the format if possible *)
let format =
@@ -626,9 +728,11 @@ let format_fun_call ~fundec env format_fun scope loc mk_call vf args =
match static_string format_arg with
| None ->
Self.warning ~current:true
- "Call to function %s with non-static format argument:@ \
- no specification will be generated." vf.vf_decl.vorig_name;
- raise (Translate_call_exn vf.vf_decl) (* No syntactic hint *)
+ "Call to function %s with non-static format argument: \
+ assuming that parameters are coherent with the format, and that \
+ no %%n specifiers are present in the actual string."
+ vf.vf_decl.vorig_name;
+ infer_format_from_args vf format_fun args
| Some s -> Format_parser.parse_format format_fun.f_kind s
with
| Format_parser.Invalid_format -> raise (Translate_call_exn vf.vf_decl)
diff --git a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
index 5cded5c9814f6a691f524589f3da627d5cb8992c..0a72e68f29843f25f4a08f83fdfb8f738707856b 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_print.res.oracle
@@ -17,40 +17,35 @@
[variadic] FRAMAC_SHARE/libc/stdio.h:590:
Declaration of variadic function asprintf.
[variadic] tests/known/stdio_print.c:9: Warning:
- Call to function fprintf with non-static format argument:
- no specification will be generated.
+ Call to function fprintf with non-static format argument: assuming that parameters are coherent with the format, and that no %n specifiers are present in the actual string.
[variadic] tests/known/stdio_print.c:9:
- Fallback translation of call fprintf to a call to the specialized version fprintf_fallback_1.
+ Translating call to fprintf to a call to the specialized version fprintf_va_1.
[variadic] tests/known/stdio_print.c:10: Warning:
- Call to function printf with non-static format argument:
- no specification will be generated.
+ Call to function printf with non-static format argument: assuming that parameters are coherent with the format, and that no %n specifiers are present in the actual string.
[variadic] tests/known/stdio_print.c:10:
- Fallback translation of call printf to a call to the specialized version printf_fallback_1.
+ Translating call to printf to a call to the specialized version printf_va_1.
[variadic] tests/known/stdio_print.c:11: Warning:
- Call to function snprintf with non-static format argument:
- no specification will be generated.
+ Call to function snprintf with non-static format argument: assuming that parameters are coherent with the format, and that no %n specifiers are present in the actual string.
[variadic] tests/known/stdio_print.c:11:
- Fallback translation of call snprintf to a call to the specialized version snprintf_fallback_1.
+ Translating call to snprintf to a call to the specialized version snprintf_va_1.
[variadic] tests/known/stdio_print.c:12: Warning:
- Call to function sprintf with non-static format argument:
- no specification will be generated.
+ Call to function sprintf with non-static format argument: assuming that parameters are coherent with the format, and that no %n specifiers are present in the actual string.
[variadic] tests/known/stdio_print.c:12:
- Fallback translation of call sprintf to a call to the specialized version sprintf_fallback_1.
+ Translating call to sprintf to a call to the specialized version sprintf_va_1.
[variadic] tests/known/stdio_print.c:13: Warning:
- Call to function dprintf with non-static format argument:
- no specification will be generated.
+ Call to function dprintf with non-static format argument: assuming that parameters are coherent with the format, and that no %n specifiers are present in the actual string.
[variadic] tests/known/stdio_print.c:13:
- Fallback translation of call dprintf to a call to the specialized version dprintf_fallback_1.
+ Translating call to dprintf to a call to the specialized version dprintf_va_1.
[variadic] tests/known/stdio_print.c:15:
- Translating call to fprintf to a call to the specialized version fprintf_va_1.
+ Translating call to fprintf to a call to the specialized version fprintf_va_2.
[variadic] tests/known/stdio_print.c:16:
- Translating call to printf to a call to the specialized version printf_va_1.
+ Translating call to printf to a call to the specialized version printf_va_2.
[variadic] tests/known/stdio_print.c:17:
- Translating call to snprintf to a call to the specialized version snprintf_va_1.
+ Translating call to snprintf to a call to the specialized version snprintf_va_2.
[variadic] tests/known/stdio_print.c:18:
- Translating call to sprintf to a call to the specialized version sprintf_va_1.
+ Translating call to sprintf to a call to the specialized version sprintf_va_2.
[variadic] tests/known/stdio_print.c:19:
- Translating call to dprintf to a call to the specialized version dprintf_va_1.
+ Translating call to dprintf to a call to the specialized version dprintf_va_2.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -59,8 +54,6 @@
[eva] done for function main
[eva] tests/known/stdio_print.c:9:
assertion 'Eva,initialization' got final status invalid.
-[kernel:annot:missing-spec] tests/known/stdio_print.c:9: Warning:
- Neither code nor specification for function fprintf_fallback_1, generating default assigns from the prototype
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
NON TERMINATING FUNCTION
@@ -69,27 +62,79 @@
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
-/*@ assigns \result, *stream;
+/*@ requires valid_read_string(param1);
+ requires valid_read_string(format);
+ assigns \result, stream->__fc_FILE_data;
assigns \result
- \from *stream, *(format + (0 ..)), *(param1 + (0 ..)), param0, param2;
- assigns *stream
- \from *stream, *(format + (0 ..)), *(param1 + (0 ..)), param0, param2;
+ \from (indirect: stream->__fc_FILE_id),
+ (indirect: stream->__fc_FILE_data),
+ (indirect: *(format + (0 ..))), (indirect: param2),
+ (indirect: *(param1 + (0 ..))), (indirect: param0);
+ assigns stream->__fc_FILE_data
+ \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+ (indirect: *(format + (0 ..))), param2, *(param1 + (0 ..)),
+ param0;
*/
-int fprintf_fallback_1(FILE * restrict stream, char const * restrict format,
- int param0, char const *param1, int param2);
+int fprintf_va_1(FILE * restrict stream, char const * restrict format,
+ int param0, char *param1, int param2);
-int printf_fallback_1(char const * restrict format, int param0,
- char const *param1, int param2);
+/*@ requires valid_read_string(param1);
+ requires valid_read_string(format);
+ assigns \result, __fc_stdout->__fc_FILE_data;
+ assigns \result
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ (indirect: __fc_stdout->__fc_FILE_data),
+ (indirect: *(format + (0 ..))), (indirect: param2),
+ (indirect: *(param1 + (0 ..))), (indirect: param0);
+ assigns __fc_stdout->__fc_FILE_data
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+ param2, *(param1 + (0 ..)), param0;
+ */
+int printf_va_1(char const * restrict format, int param0, char *param1,
+ int param2);
-int snprintf_fallback_1(char * restrict s, size_t n,
- char const * restrict format, int param0,
- char const *param1, int param2);
+/*@ requires valid_read_string(param1);
+ requires valid_read_string(format);
+ requires
+ \valid(s + (0 .. n - 1)) ∨
+ \valid(s + (0 .. format_length(format) - 1));
+ assigns \result, *(s + (0 ..));
+ assigns \result
+ \from (indirect: n), (indirect: *(format + (0 ..))),
+ (indirect: param2), (indirect: *(param1 + (0 ..))),
+ (indirect: param0);
+ assigns *(s + (0 ..))
+ \from (indirect: n), (indirect: *(format + (0 ..))), param2,
+ *(param1 + (0 ..)), param0;
+ */
+int snprintf_va_1(char * restrict s, size_t n, char const * restrict format,
+ int param0, char *param1, int param2);
-int sprintf_fallback_1(char * restrict s, char const * restrict format,
- int param0, char const *param1, int param2);
+/*@ requires valid_read_string(param1);
+ requires valid_read_string(format);
+ assigns \result, *(s + (0 ..));
+ assigns \result
+ \from (indirect: *(format + (0 ..))), (indirect: param2),
+ (indirect: *(param1 + (0 ..))), (indirect: param0);
+ assigns *(s + (0 ..))
+ \from (indirect: *(format + (0 ..))), param2, *(param1 + (0 ..)),
+ param0;
+ */
+int sprintf_va_1(char * restrict s, char const * restrict format, int param0,
+ char *param1, int param2);
-int dprintf_fallback_1(int fd, char const * restrict format, int param0,
- char const *param1, char const *param2);
+/*@ requires valid_read_string(param1);
+ requires valid_read_string(param2);
+ requires valid_read_string(format);
+ assigns \result;
+ assigns \result
+ \from (indirect: fd), (indirect: *(format + (0 ..))),
+ (indirect: *(param2 + (0 ..))), (indirect: *(param1 + (0 ..))),
+ (indirect: param0);
+ */
+int dprintf_va_1(int fd, char const * restrict format, int param0,
+ char *param1, char *param2);
/*@ requires valid_read_string(param1);
requires valid_read_string(format);
@@ -104,7 +149,7 @@ int dprintf_fallback_1(int fd, char const * restrict format, int param0,
(indirect: *(format + (0 ..))), param2, *(param1 + (0 ..)),
param0;
*/
-int fprintf_va_1(FILE * restrict stream, char const * restrict format,
+int fprintf_va_2(FILE * restrict stream, char const * restrict format,
int param0, char *param1, int param2);
/*@ requires valid_read_string(param1);
@@ -120,7 +165,7 @@ int fprintf_va_1(FILE * restrict stream, char const * restrict format,
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param2, *(param1 + (0 ..)), param0;
*/
-int printf_va_1(char const * restrict format, int param0, char *param1,
+int printf_va_2(char const * restrict format, int param0, char *param1,
int param2);
/*@ requires valid_read_string(param1);
@@ -137,7 +182,7 @@ int printf_va_1(char const * restrict format, int param0, char *param1,
\from (indirect: n), (indirect: *(format + (0 ..))), param2,
*(param1 + (0 ..)), param0;
*/
-int snprintf_va_1(char * restrict s, size_t n, char const * restrict format,
+int snprintf_va_2(char * restrict s, size_t n, char const * restrict format,
int param0, char *param1, int param2);
/*@ requires valid_read_string(param1);
@@ -150,7 +195,7 @@ int snprintf_va_1(char * restrict s, size_t n, char const * restrict format,
\from (indirect: *(format + (0 ..))), param2, *(param1 + (0 ..)),
param0;
*/
-int sprintf_va_1(char * restrict s, char const * restrict format, int param0,
+int sprintf_va_2(char * restrict s, char const * restrict format, int param0,
char *param1, int param2);
/*@ requires valid_read_string(param1);
@@ -162,7 +207,7 @@ int sprintf_va_1(char * restrict s, char const * restrict format, int param0,
(indirect: *(param2 + (0 ..))), (indirect: *(param1 + (0 ..))),
(indirect: param0);
*/
-int dprintf_va_1(int fd, char const * restrict format, int param0,
+int dprintf_va_2(int fd, char const * restrict format, int param0,
char *param1, char *param2);
int main(void)
@@ -173,16 +218,16 @@ int main(void)
char *str;
size_t size;
/*@ assert Eva: initialization: \initialized(&format); */
- fprintf(stream,(char const *)format,1,"2",3); /* fprintf_fallback_1 */
- printf((char const *)format,1,"2",3); /* printf_fallback_1 */
- snprintf(str,size,(char const *)format,1,"2",3); /* snprintf_fallback_1 */
- sprintf(str,(char const *)format,1,"2",3); /* sprintf_fallback_1 */
- dprintf(1,(char const *)format,1,"3","4"); /* dprintf_fallback_1 */
- fprintf(stream,"%d %s %d",1,(char *)"2",3); /* fprintf_va_1 */
- printf("%d %s %d",1,(char *)"2",3); /* printf_va_1 */
- snprintf(str,size,"%d %s %d",1,(char *)"2",3); /* snprintf_va_1 */
- sprintf(str,"%d %s %d",1,(char *)"2",3); /* sprintf_va_1 */
- dprintf(1,"%d %s %s",1,(char *)"3",(char *)"4"); /* dprintf_va_1 */
+ fprintf(stream,(char const *)format,1,(char *)"2",3); /* fprintf_va_1 */
+ printf((char const *)format,1,(char *)"2",3); /* printf_va_1 */
+ snprintf(str,size,(char const *)format,1,(char *)"2",3); /* snprintf_va_1 */
+ sprintf(str,(char const *)format,1,(char *)"2",3); /* sprintf_va_1 */
+ dprintf(1,(char const *)format,1,(char *)"3",(char *)"4"); /* dprintf_va_1 */
+ fprintf(stream,"%d %s %d",1,(char *)"2",3); /* fprintf_va_2 */
+ printf("%d %s %d",1,(char *)"2",3); /* printf_va_2 */
+ snprintf(str,size,"%d %s %d",1,(char *)"2",3); /* snprintf_va_2 */
+ sprintf(str,"%d %s %d",1,(char *)"2",3); /* sprintf_va_2 */
+ dprintf(1,"%d %s %s",1,(char *)"3",(char *)"4"); /* dprintf_va_2 */
__retres = 0;
return __retres;
}
diff --git a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
index 933132b068079dfb5faef71a4bd04a21f96f2acb..83103e4ba9a423384d500ad5bdbac32a33889ec5 100644
--- a/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/stdio_scan.res.oracle
@@ -17,26 +17,23 @@
[variadic] FRAMAC_SHARE/libc/stdio.h:590:
Declaration of variadic function asprintf.
[variadic] tests/known/stdio_scan.c:10: Warning:
- Call to function fscanf with non-static format argument:
- no specification will be generated.
+ Call to function fscanf with non-static format argument: assuming that parameters are coherent with the format, and that no %n specifiers are present in the actual string.
[variadic] tests/known/stdio_scan.c:10:
- Fallback translation of call fscanf to a call to the specialized version fscanf_fallback_1.
+ Translating call to fscanf to a call to the specialized version fscanf_va_1.
[variadic] tests/known/stdio_scan.c:11: Warning:
- Call to function scanf with non-static format argument:
- no specification will be generated.
+ Call to function scanf with non-static format argument: assuming that parameters are coherent with the format, and that no %n specifiers are present in the actual string.
[variadic] tests/known/stdio_scan.c:11:
- Fallback translation of call scanf to a call to the specialized version scanf_fallback_1.
+ Translating call to scanf to a call to the specialized version scanf_va_1.
[variadic] tests/known/stdio_scan.c:12: Warning:
- Call to function sscanf with non-static format argument:
- no specification will be generated.
+ Call to function sscanf with non-static format argument: assuming that parameters are coherent with the format, and that no %n specifiers are present in the actual string.
[variadic] tests/known/stdio_scan.c:12:
- Fallback translation of call sscanf to a call to the specialized version sscanf_fallback_1.
+ Translating call to sscanf to a call to the specialized version sscanf_va_1.
[variadic] tests/known/stdio_scan.c:14:
- Translating call to fscanf to a call to the specialized version fscanf_va_1.
+ Translating call to fscanf to a call to the specialized version fscanf_va_2.
[variadic] tests/known/stdio_scan.c:15:
- Translating call to scanf to a call to the specialized version scanf_va_1.
+ Translating call to scanf to a call to the specialized version scanf_va_2.
[variadic] tests/known/stdio_scan.c:16:
- Translating call to sscanf to a call to the specialized version sscanf_va_1.
+ Translating call to sscanf to a call to the specialized version sscanf_va_2.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -45,8 +42,6 @@
[eva] done for function main
[eva] tests/known/stdio_scan.c:10:
assertion 'Eva,initialization' got final status invalid.
-[kernel:annot:missing-spec] tests/known/stdio_scan.c:10: Warning:
- Neither code nor specification for function fscanf_fallback_1, generating default assigns from the prototype
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
NON TERMINATING FUNCTION
@@ -55,26 +50,82 @@
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
-/*@ assigns \result, *stream, *param0, *(param1 + (0 ..)), *param2;
+/*@ requires \valid(param0);
+ requires \valid(param1);
+ requires \valid(param2);
+ requires valid_read_string(format);
+ ensures \initialized(param0);
+ ensures \initialized(param1);
+ ensures \initialized(param2);
+ assigns \result, stream->__fc_FILE_data, *param2, *param1, *param0;
assigns \result
- \from *stream, *(format + (0 ..)), *param0, *(param1 + (0 ..)), *param2;
- assigns *stream
- \from *stream, *(format + (0 ..)), *param0, *(param1 + (0 ..)), *param2;
- assigns *param0
- \from *stream, *(format + (0 ..)), *param0, *(param1 + (0 ..)), *param2;
- assigns *(param1 + (0 ..))
- \from *stream, *(format + (0 ..)), *param0, *(param1 + (0 ..)), *param2;
+ \from (indirect: stream->__fc_FILE_id),
+ (indirect: stream->__fc_FILE_data),
+ (indirect: *(format + (0 ..)));
+ assigns stream->__fc_FILE_data
+ \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
assigns *param2
- \from *stream, *(format + (0 ..)), *param0, *(param1 + (0 ..)), *param2;
+ \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
+ assigns *param1
+ \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
+ assigns *param0
+ \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
*/
-int fscanf_fallback_1(FILE * restrict stream, char const * restrict format,
- int *param0, char *param1, int *param2);
+int fscanf_va_1(FILE * restrict stream, char const * restrict format,
+ int *param0, char *param1, int *param2);
-int scanf_fallback_1(char const * restrict format, int *param0, char *param1,
- int *param2);
+/*@ requires \valid(param0);
+ requires \valid(param1);
+ requires \valid(param2);
+ requires valid_read_string(format);
+ ensures \initialized(param0);
+ ensures \initialized(param1);
+ ensures \initialized(param2);
+ assigns \result, __fc_stdin->__fc_FILE_data, *param2, *param1, *param0;
+ assigns \result
+ \from (indirect: __fc_stdin->__fc_FILE_id),
+ (indirect: __fc_stdin->__fc_FILE_data),
+ (indirect: *(format + (0 ..)));
+ assigns __fc_stdin->__fc_FILE_data
+ \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
+ assigns *param2
+ \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
+ assigns *param1
+ \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
+ assigns *param0
+ \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
+ */
+int scanf_va_1(char const * restrict format, int *param0, char *param1,
+ int *param2);
-int sscanf_fallback_1(char const * restrict s, char const * restrict format,
- int *param0, char *param1, int *param2);
+/*@ requires \valid(param0);
+ requires \valid(param1);
+ requires \valid(param2);
+ requires valid_read_string(format);
+ requires valid_read_string(s);
+ ensures \initialized(param0);
+ ensures \initialized(param1);
+ ensures \initialized(param2);
+ assigns \result, *param2, *param1, *param0;
+ assigns \result
+ \from (indirect: *(s + (0 ..))), (indirect: *(format + (0 ..)));
+ assigns *param2
+ \from (indirect: *(s + (0 ..))), (indirect: *(format + (0 ..)));
+ assigns *param1
+ \from (indirect: *(s + (0 ..))), (indirect: *(format + (0 ..)));
+ assigns *param0
+ \from (indirect: *(s + (0 ..))), (indirect: *(format + (0 ..)));
+ */
+int sscanf_va_1(char const * restrict s, char const * restrict format,
+ int *param0, char *param1, int *param2);
/*@ requires \valid(param0);
requires \valid(param2);
@@ -100,7 +151,7 @@ int sscanf_fallback_1(char const * restrict s, char const * restrict format,
\from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int fscanf_va_1(FILE * restrict stream, char const * restrict format,
+int fscanf_va_2(FILE * restrict stream, char const * restrict format,
int *param0, char *param1, int *param2);
/*@ requires \valid(param0);
@@ -127,7 +178,7 @@ int fscanf_va_1(FILE * restrict stream, char const * restrict format,
\from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
(indirect: *(format + (0 ..)));
*/
-int scanf_va_1(char const * restrict format, int *param0, char *param1,
+int scanf_va_2(char const * restrict format, int *param0, char *param1,
int *param2);
/*@ requires \valid(param0);
@@ -146,7 +197,7 @@ int scanf_va_1(char const * restrict format, int *param0, char *param1,
assigns *param0
\from (indirect: *(s + (0 ..))), (indirect: *(format + (0 ..)));
*/
-int sscanf_va_1(char const * restrict s, char const * restrict format,
+int sscanf_va_2(char const * restrict s, char const * restrict format,
int *param0, char *param1, int *param2);
int main(void)
@@ -159,12 +210,12 @@ int main(void)
int j;
char *s;
/*@ assert Eva: initialization: \initialized(&s); */
- fscanf(stream,(char const *)format,& i,s,& j); /* fscanf_fallback_1 */
- scanf((char const *)format,& i,s,& j); /* scanf_fallback_1 */
- sscanf((char const *)str,(char const *)format,& i,s,& j); /* sscanf_fallback_1 */
- fscanf(stream,"%d %s %d",& i,s,& j); /* fscanf_va_1 */
- scanf("%d %s %d",& i,s,& j); /* scanf_va_1 */
- sscanf((char const *)str,"%d %s %d",& i,s,& j); /* sscanf_va_1 */
+ fscanf(stream,(char const *)format,& i,s,& j); /* fscanf_va_1 */
+ scanf((char const *)format,& i,s,& j); /* scanf_va_1 */
+ sscanf((char const *)str,(char const *)format,& i,s,& j); /* sscanf_va_1 */
+ fscanf(stream,"%d %s %d",& i,s,& j); /* fscanf_va_2 */
+ scanf("%d %s %d",& i,s,& j); /* scanf_va_2 */
+ sscanf((char const *)str,"%d %s %d",& i,s,& j); /* sscanf_va_2 */
__retres = 0;
return __retres;
}
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 63e68dd7fbced0a26bd0e134462ecd42329e2c4d..7c0fa5e2fee5169f4987a60e46cd19f1fd243733 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,7 @@
Plugin WP <next-release>
#########################
+- WP [2021-10-25] Removes -wp-overflows option (unsound)
- WP [2021-06-11] Adds an experimental support of "terminates" clauses.
Adds the options -wp-declaration-terminate and
-wp-frama-c-stdlib to claims that external functions
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index f658fb960d3d81374da97757d420fa320f02a569..3ec3b7227a1b0744cae8d2817be3cd31ce299614 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -426,10 +426,7 @@ let range i a =
let ensures warn i a =
if warn i
- then
- (if Lang.has_gamma () && Wp_parameters.get_overflows ()
- then Lang.assume (range i a) ;
- a)
+ then a
else e_fun (f_to_int i) [a]
let downcast = ensures is_downcast_an_error
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 7031a0f45b54619cce68c9a24ef6ef1e562fbe77..937fcb63221b3deac4e2cec20d30eb37727a3547 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -895,11 +895,6 @@ The available \textsf{WP} command-line options related to model selection are:
used by the (default) arithmetic model \texttt{-wp-model +int} to interpret integer
arithmetic. See section~\ref{wp-model-arith} for details.
-\item[\tt -wp-(no)-overflows] explicitly add to proof context the assumptions related
- to overflows and downcasts selected. This is especially useful when casts are inserted
- in \textsf{ACSL} contracts to ensure type-checking but are related to identity-casts
- from the code. The option is \texttt{off} by default.
-
\item[\tt -wp-literals] exports the contents of string literals
to provers (default: \texttt{no}).
\item[\tt -wp-extern-arrays] gives an arbitrary large size to arrays
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 042f73ad14869b3a275bf69fb951b86f49ba131d..528a9b251ff910b2b78a1cf4303b73e8259e9718 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -259,14 +259,6 @@ module ExternArrays =
let help = "Put some default size for extern arrays."
end)
-let () = Parameter_customize.set_group wp_model
-module Overflows =
- False(struct
- let option_name = "-wp-overflows"
- let help = "Collect hypotheses for absence of overflow and downcast\n\
- (incompatible with RTE generator plug-in)"
- end)
-
let () = Parameter_customize.set_group wp_model
module WeakIntModel =
False(struct
@@ -1135,19 +1127,6 @@ module OutputDir =
Defaults to some temporary directory."
end)
-(* -------------------------------------------------------------------------- *)
-(* --- Overflows --- *)
-(* -------------------------------------------------------------------------- *)
-
-let active_unless_rte option =
- if RTE.get () || Dynamic.Parameter.Bool.get "-rte" () then
- ( warning ~once:true
- "Option %s incompatiable with RTE (ignored)" option ;
- false )
- else true
-
-let get_overflows () = Overflows.get () && active_unless_rte "-wp-overflows"
-
(* -------------------------------------------------------------------------- *)
(* --- Output Dir --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 84df958fcca466a64fbd97f64878b4bae00b0e41..bcd61322625875596952fe032fdd4899c4000e4e 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -171,7 +171,6 @@ val get_session_dir : force:bool -> string -> Datatype.Filepath.t
val get_output : unit -> Datatype.Filepath.t
val get_output_dir : string -> Datatype.Filepath.t
val make_output_dir : string -> unit
-val get_overflows : unit -> bool
(** {2 Debugging Categories} *)
val has_print_generated: unit -> bool
diff --git a/tests/syntax/oracle/static_assert.0.res.oracle b/tests/syntax/oracle/static_assert.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1a9b662e55791706fe688dba778443ab94804f6f
--- /dev/null
+++ b/tests/syntax/oracle/static_assert.0.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing tests/syntax/static_assert.c (with preprocessing)
+/* Generated by Frama-C */
+#include "assert.h"
+int main(void)
+{
+ int ret = 42;
+ return ret;
+}
+
+
diff --git a/tests/syntax/oracle/static_assert.1.res.oracle b/tests/syntax/oracle/static_assert.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..241aa7a05b62b5cd6b27fdd463f43f9d57f72757
--- /dev/null
+++ b/tests/syntax/oracle/static_assert.1.res.oracle
@@ -0,0 +1,12 @@
+[kernel] Parsing tests/syntax/static_assert.c (with preprocessing)
+[kernel] tests/syntax/static_assert.c:12: User Error:
+ static assertion failed: fail
+[kernel] tests/syntax/static_assert.c:26: User Error:
+ failed to evaluate constant expression in static assertion:
+ a == 42
+[kernel] tests/syntax/static_assert.c:37: User Error: static assertion failed
+[kernel] tests/syntax/static_assert.c:38: User Error:
+ static assertion failed: failure inside struct
+[kernel] User Error: stopping on file "tests/syntax/static_assert.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/static_assert.c b/tests/syntax/static_assert.c
new file mode 100644
index 0000000000000000000000000000000000000000..93ca57c958c5e284805fa5172a85fa675c5bc359
--- /dev/null
+++ b/tests/syntax/static_assert.c
@@ -0,0 +1,39 @@
+/* run.config
+ STDOPT: #"-c11"
+ EXIT: 1
+ STDOPT: #"-c11 -cpp-extra-args=-DFAIL"
+*/
+
+_Static_assert(1, "string");
+
+#include <assert.h>
+
+#ifdef FAIL
+static_assert(0, "fail");
+#endif
+
+_Static_assert(2); // without message string; this is not C11-compliant, but
+ // a C++17 extension. GCC/Clang allow it.
+
+// _Static_assert can also appear inside struct declarations
+struct st { _Static_assert (sizeof(char) == 1, "inside struct"); int a; };
+
+int main() {
+ static_assert(sizeof(int) > sizeof(char), "int must be greater than char");
+
+#ifdef FAIL
+ int a = 42;
+ static_assert(a == 42, "non-static condition");
+#endif
+
+ int ret = 42;
+
+ static_assert(3); // between statements
+
+ return ret;
+}
+
+#ifdef FAIL
+static_assert(0); // fail without message string
+struct st2 { _Static_assert (sizeof(char) > 1, "failure inside struct"); int a; };
+#endif