diff --git a/.Makefile.lint b/.Makefile.lint
index c2648ca66aafcbf1311b68871dfb983d47a9fbd4..80fb691a8370490eea2a7db9b60c1fae64ab498a 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -52,7 +52,6 @@ ML_LINT_KO+=src/kernel_services/analysis/dataflow2.mli
ML_LINT_KO+=src/kernel_services/analysis/dataflows.ml
ML_LINT_KO+=src/kernel_services/analysis/dataflows.mli
ML_LINT_KO+=src/kernel_services/analysis/dominators.ml
-ML_LINT_KO+=src/kernel_services/analysis/exn_flow.ml
ML_LINT_KO+=src/kernel_services/analysis/interpreted_automata.ml
ML_LINT_KO+=src/kernel_services/analysis/interpreted_automata.mli
ML_LINT_KO+=src/kernel_services/analysis/logic_interp.ml
diff --git a/.gitignore b/.gitignore
index 1280fb74b6358d88d5bc8c8d488d981b1569472f..c4204e5ff6e7981f0a1fa70898438580dd785939 100644
--- a/.gitignore
+++ b/.gitignore
@@ -55,6 +55,7 @@ autom4te.cache
/tests/journal/intra.byte
/tests/misc/my_visitor_plugin/my_visitor.opt
/tests/misc/my_visitor.sav
+/tests/spec/preprocess_dos.c
/tests/*/*.opt
/tests/pdg/*.dot
@@ -92,6 +93,8 @@ autom4te.cache
/doc/acsl/
+/doc/aorai/aorai-example.tgz
+/doc/aorai/aorai-example/
/doc/aorai/frama-c-aorai-example.tgz
/doc/aorai/frama-c-aorai-example
/doc/aorai/main.pdf
diff --git a/ALL_VERSIONS b/ALL_VERSIONS
index 30537788bc31ee6d08b604c796fc9793aa7f0312..6f60aa58c52031931854e1eac39f5c8ed2b9f840 100644
--- a/ALL_VERSIONS
+++ b/ALL_VERSIONS
@@ -1,5 +1,6 @@
Version number Date of release Notes
============== =============== =====
+21.1 (Scandium) 2020, June 25 Bugs fixed
21.0 (Scandium) 2020, June 11
20.0 (Calcium) 2019, December 4
19.1 (Potassium) 2019, September 18 OCaml 4.08 compatibility
diff --git a/Changelog b/Changelog
index 2350706750699c5dd5119f88187c08b334db2fe5..3cd809c4cb31f6030fbea1adc5a62e71fcb9bc55 100644
--- a/Changelog
+++ b/Changelog
@@ -30,6 +30,10 @@ Open Source Release <next-release>
- Eva [2020-05-20] Supports the ACSL mathematical operator \abs
- Kernel [2020-05-18] Support for C11's _Noreturn function specifier
+###################################
+Open Source Release 21.1 (Scandium)
+###################################
+
###################################
Open Source Release 21.0 (Scandium)
###################################
@@ -3517,11 +3521,11 @@ Open Source Release 4.1 (Beryllium-20090901)
-! Syntactic_callgraph [2009-08-27] New design of the callgraph in the GUI.
Frama-C now requires ocamlgraph 1.2.
-- Logic "reads" clauses on logic functions and predicates, which
- disappeared with the introduction of axiomatic blocks, have been
- resurected. Beware that the semantics is slightly different
- from before: see ACSL document for details. It is used to
- automatically generate footprint axioms.
+- Logic [2009-08-25]"reads" clauses on logic functions and predicates,
+ which disappeared with the introduction of axiomatic blocks,
+ have been ressurrected. Beware that the semantics is slightly
+ different from before: see ACSL document for details. It is used
+ to automatically generate footprint axioms.
- GUI [2009-08-18] Improved display of summary information when
selecting a file.
- Kernel [2009-08-05] New options -kernel-help, -kernel-verbose and
@@ -3980,7 +3984,7 @@ Binary Release 1.0 (Hydrogen-20080302)
Open Source Release 1.0 (Hydrogen-20080301)
###########################################
-- First release
+- Kernel [2008-03-01] First release.
diff --git a/Makefile b/Makefile
index d6d044aebe2a88c183a3477078b4574087e5699d..9c91110466759f5eb47597511f8bf3d340c9addb 100644
--- a/Makefile
+++ b/Makefile
@@ -910,6 +910,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
partitioning/partitioning_index partitioning/trace_partitioning \
engine/mem_exec engine/iterator engine/initialization \
engine/compute_functions engine/analysis register \
+ utils/unit_tests \
$(APRON_CMO) $(NUMERORS_CMO)
PLUGIN_CMI:= values/abstract_value values/abstract_location \
domains/abstract_domain domains/simpler_domains
@@ -2338,7 +2339,29 @@ PTESTS_SRC=ptests/ptests_config.ml ptests/ptests.ml
# that does not contain a 'tests' dir
PTESTS_CONFIG:= $(shell if test -d tests; then echo tests/ptests_config; fi)
-ptests: bin/ptests.$(OCAMLBEST)$(EXE) $(PTESTS_CONFIG)
+ifneq ("$(PTESTS_CONFIG)","")
+GENERATED_TESTS:=tests/spec/preprocess_dos.c
+else
+GENERATED_TESTS:=
+endif
+
+tests/spec/preprocess_dos.c: tests/spec/preprocess_dos.c.in \
+ Makefile share/Makefile.config
+ $(RM) $@
+ $(SED) -e "s|@UNIX2DOS@|$(PP_DOS_UNIX2DOS)|g" \
+ -e "s|@DONTRUN@|$(PP_DOS_DONTRUN)|g" \
+ $< > $@
+ $(CHMOD_RO) $@
+
+ifneq ("$(HAS_UNIX2DOS)","no")
+tests/spec/preprocess_dos.c: PP_DOS_UNIX2DOS=$(UNIX2DOS)
+tests/spec/preprocess_dos.c: PP_DOS_DONTRUN=
+else
+tests/spec/preprocess_dos.c: PP_DOS_UNIX2DOS=unix2dos
+tests/spec/preprocess_dos.c: PP_DOS_DONTRUN=DONTRUN: no unix2dos found
+endif
+
+ptests: bin/ptests.$(OCAMLBEST)$(EXE) $(PTESTS_CONFIG) $(GENERATED_TESTS)
bin/ptests.byte$(EXE): $(PTESTS_SRC)
$(PRINT_LINKING) $@
@@ -2350,7 +2373,7 @@ bin/ptests.opt$(EXE): $(PTESTS_SRC)
$(OCAMLOPT) -I ptests -dtypes -thread -o $@ \
unix.cmxa threads.cmxa str.cmxa dynlink.cmxa $^
-GENERATED+=ptests/ptests_config.ml tests/ptests_config
+GENERATED+=ptests/ptests_config.ml tests/ptests_config $(GENERATED_TESTS)
#######################
# Source distribution #
diff --git a/VERSION b/VERSION
index 4d9c5c492ab8d7bb65127c811de9553e31e9916f..d22a678d5a1453d0dea85f01e751014c8a59254b 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-21.0+dev
+21.1+dev
diff --git a/bin/build-src-distrib.sh b/bin/build-src-distrib.sh
index e48857d7e715b96357cdeb2e275bea9dcabe659d..272eb1caf79a83e93b09e0c8e75e8cf9559839bc 100755
--- a/bin/build-src-distrib.sh
+++ b/bin/build-src-distrib.sh
@@ -228,6 +228,8 @@ case "${STEP}" in
run "cp Changelog $WEBSITE_DIR/src/last-release/Changelog"
run "cp src/plugins/wp/Changelog $WEBSITE_DIR/src/wpChangelog"
run "cp src/plugins/wp/Changelog $WEBSITE_DIR/src/last-release/wpChangelog"
+ run "cp src/plugins/e-acsl/doc/Changelog $WEBSITE_DIR/src/eacslChangelog"
+ run "cp src/plugins/e-acsl/doc/Changelog $WEBSITE_DIR/src/last-release/eacslChangelog"
fi
;&
3)
diff --git a/bin/wp-qualif.sh b/bin/wp-qualif.sh
new file mode 100644
index 0000000000000000000000000000000000000000..26d743608360c8676a6801e0b70459332e64caea
--- /dev/null
+++ b/bin/wp-qualif.sh
@@ -0,0 +1,2 @@
+export FRAMAC_WP_CACHE=update
+export FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE)
diff --git a/configure.in b/configure.in
index 284e9f5cea3280ba307aa6962ea4ad07f207f5ca..364940906cb9c955115ee9d81cca18b36168df30 100644
--- a/configure.in
+++ b/configure.in
@@ -657,14 +657,6 @@ REQUIRE_LABLGTK=
USE_LABLGTK=
HAS_LABLGTK=
-# Tool declarations
-####################
-
-DOT=
-REQUIRE_DOT=
-USE_DOT=
-HAS_DOT=
-
### Now plugin declarations
PLUGINS_FORCE_LIST=
@@ -957,6 +949,11 @@ configure_library([LABLGTK],
configure_tool([DOT],[dot],[dot not found: you should install GraphViz],no)
+configure_tool([UNIX2DOS],[unix2dos],
+ [unix2dos not found: you should install tofrodos],no)
+
+plugin_use_external(tests,unix2dos)
+
########################
# Plug-in dependencies #
########################
@@ -974,8 +971,6 @@ EXTERNAL_PLUGINS="${EXTERNAL_PLUGINS} ${EXTRA_EXTERNAL_PLUGINS}"
AC_SUBST(PLATFORM)
AC_SUBST(VERBOSEMAKE)
AC_SUBST(DEVELOPMENT)
-AC_SUBST(DOT)
-AC_SUBST(HAS_DOT)
AC_SUBST(HAS_APRON)
AC_SUBST(HAS_MPFR)
AC_SUBST(HAS_LANDMARKS)
diff --git a/devel_tools/docker/README.md b/devel_tools/docker/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..0a1c8e049e40b74e21466ee9b87be75a27475901
--- /dev/null
+++ b/devel_tools/docker/README.md
@@ -0,0 +1,29 @@
+Docker images for Frama-C
+=========================
+
+- To build a new image (slim, without Frama-C sources nor tests):
+
+ cd <tag>
+ docker build . --target base -t framac/frama-c:<tag>
+
+- To run an interactive shell:
+
+ docker run -it framac/frama-c:<tag>
+
+- To push to Docker Hub (requires access to the `framac/frama-c` repository):
+
+ docker push framac/frama-c:<tag>
+
+- To build an image containing Frama-C sources (downloaded from the .tar.gz, in
+ directory `/root`):
+
+ cd <tag>
+ docker build . --build-arg with_source=yes \
+ -t framac/frama-c:<tag>-with-source
+
+- To run Frama-C tests (and remove unnecessary image later):
+
+ 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
diff --git a/devel_tools/docker/frama-c.21.0/Dockerfile b/devel_tools/docker/frama-c.21.0/Dockerfile
new file mode 100644
index 0000000000000000000000000000000000000000..3a615a7bf0f9d87ec211b428dd12891c3ea4c57d
--- /dev/null
+++ b/devel_tools/docker/frama-c.21.0/Dockerfile
@@ -0,0 +1,58 @@
+FROM debian:sid as base
+
+RUN apt update
+RUN apt install opam -y
+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
+RUN opam install depext -y
+
+# Install packages from reference configuration
+RUN opam depext --install -y \
+ 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 \
+ --verbose # intentionally left as last line in this RUN command
+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 \
+ opam depext --install -y \
+ conf-python-3.1.0.0 \
+ conf-time.1 \
+ --verbose \
+ && \
+ 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
new file mode 100644
index 0000000000000000000000000000000000000000..8852ac14805bad7b5862b8b1205a5e667ab8ca8c
--- /dev/null
+++ b/devel_tools/docker/frama-c.21.1/Dockerfile
@@ -0,0 +1,58 @@
+FROM debian:sid as base
+
+RUN apt update
+RUN apt install opam -y
+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
+RUN opam install depext -y
+
+# Install packages from reference configuration
+RUN opam depext --install -y \
+ 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 \
+ --verbose # intentionally left as last line in this RUN command
+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 \
+ opam depext --install -y \
+ conf-python-3.1.0.0 \
+ conf-time.1 \
+ --verbose \
+ && \
+ cd /root/frama-c-* && \
+ make tests; \
+ fi
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 956eda16413b10e71b1d45b1882db9669098ee23..91c8e28c36120e62de749eac8174f2c34f15399a 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -1020,9 +1020,7 @@ directory of directory \texttt{tests}\codeidx{tests}. The
\texttt{DONTRUN} directive does not need to have any content, but it
is useful to provide an explanation of why the test should not be run
({\it e.g} test of a feature that is currently developed and not fully
-operational yet). If a test file is explicitly given on the command
-line of \ptests, it is always executed, regardless of the presence of
-a \texttt{DONTRUN} directive.
+operational yet).
As said in Section~\ref{ptests:configuration}, these directives can be
found in different places:
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 7e490058938700555937492f2f5c734a796673f5..a8437b5bd42c4ad9d51a59deff3c1dbac6e31fa2 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1367,6 +1367,8 @@ src/plugins/value/utils/state_import.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/state_import.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/structure.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/structure.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/unit_tests.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/unit_tests.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/value_perf.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/value_perf.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/value_results.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/ivette/src/dome/src/main/dome.js b/ivette/src/dome/src/main/dome.js
index 07d0d620e051c9fd3021cf5fd67f4122c71951ad..cd01363afb0b82961da1f77f1baed2b3865e5b7c 100644
--- a/ivette/src/dome/src/main/dome.js
+++ b/ivette/src/dome/src/main/dome.js
@@ -57,7 +57,7 @@ function loadSettings( file ) {
const text = fs.readFileSync(file, { encoding: 'utf8' } );
return Object.assign({}, JSON.parse(text));
} catch(err) {
- console.error("[Dome] Can not load settings", file, err);
+ console.error("[Dome] Unable to load settings", file, err);
return {};
}
}
@@ -67,7 +67,7 @@ function saveSettings( file, data={} ) {
const text = JSON.stringify( data, undefined, DEVEL ? 2 : 0 );
fs.writeFileSync( file, text, { encoding: 'utf8' }, (err) => { throw(err); } );
} catch(err) {
- console.error("[Dome] Can not save settings", file, err);
+ console.error("[Dome] Unable to save settings", file, err);
}
}
@@ -86,7 +86,7 @@ function saveGlobalSettings() {
if (!fstat( APP_DIR )) fs.mkdirSync( APP_DIR );
saveSettings( PATH_GLOBAL_SETTINGS, GlobalSettings );
} catch(err) {
- console.error("[Dome] Can not save global settings", err);
+ console.error("[Dome] Unable to save global settings", err);
}
}
diff --git a/ivette/src/dome/src/misc/plugins.js b/ivette/src/dome/src/misc/plugins.js
index 5d468d4017a308f65f0dfad93f3ef2dcc6c17aea..87a08c0c836e960d70158825db1a98a685f2282c 100644
--- a/ivette/src/dome/src/misc/plugins.js
+++ b/ivette/src/dome/src/misc/plugins.js
@@ -34,7 +34,7 @@ export function install( name )
let config ;
try { config = JSON.pargse(fs.readFileSync( pkg , 'UTF-8' )); }
catch(err) {
- console.error( `[Dome] reading '${pkg}':\n`, err );
+ console.error( `[Dome] Reading '${pkg}':\n`, err );
throw `Plugin '${name}' has invalid 'package.json' file` ;
}
@@ -49,7 +49,7 @@ export function install( name )
let bundle ;
try { bundle = fs.readFileSync( bundlejs , 'UTF-8' ); }
catch(err) {
- console.error( `[Dome] loading '${bundlejs}':\n`, err );
+ console.error( `[Dome] Loading '${bundlejs}':\n`, err );
throw `Plugin '${name}' can not load its entry point` ;
}
@@ -63,7 +63,7 @@ export function install( name )
let module = { id, exports };
compiled( module, require, static_d );
} catch(err) {
- console.error( `[Dome] running '${bundlejs}':\n`, err );
+ console.error( `[Dome] Running '${bundlejs}':\n`, err );
throw `Plugin '${name}' can not install bundle` ;
}
register( id, exports ); // final exports
diff --git a/ivette/src/dome/src/misc/system.js b/ivette/src/dome/src/misc/system.js
index 48808f72562593c59043fcd977d147a4f5abee93..3a4deac841f74817b387562192b72de5108edd91 100644
--- a/ivette/src/dome/src/misc/system.js
+++ b/ivette/src/dome/src/misc/system.js
@@ -593,7 +593,7 @@ export function spawn(command,args,options) {
}
if ( !process ) {
- throw "[Dome] Can not create process ('"+command+"')";
+ throw `[Dome] Unable to create process ('${command}')`;
return;
}
diff --git a/ivette/src/dome/src/renderer/data/json.ts b/ivette/src/dome/src/renderer/data/json.ts
index 145e4220ff79cf0b058347855e9d8223f9786658..018fe14b19477769249dd41d4e2b24d0cb0bf870 100644
--- a/ivette/src/dome/src/renderer/data/json.ts
+++ b/ivette/src/dome/src/renderer/data/json.ts
@@ -5,7 +5,7 @@
/**
Safe JSON utilities.
@packageDocumentation
- @package dome/data/json
+ @module dome/data/json
*/
import { DEVEL } from 'dome/system';
@@ -25,7 +25,7 @@ export function parse(text: string, noError = false): json {
try {
return JSON.parse(text);
} catch (err) {
- if (DEVEL) console.error('[Dome.json] invalid format:', err);
+ if (DEVEL) console.error('[Dome.json] Invalid format:', err);
return undefined;
}
} else
@@ -141,12 +141,13 @@ export function jDefault<A>(
fn: Loose<A>,
defaultValue: A,
): Safe<A> {
- return (js: json) => js === undefined ? defaultValue : (fn(js) ?? defaultValue);
+ return (js: json) =>
+ js === undefined ? defaultValue : (fn(js) ?? defaultValue);
}
/**
Force returning `undefined` or a default value for `undefined` _or_ `null` JSON input.
- Typically usefull to leverage an existing `Safe<A>` decoder.
+ Typically useful to leverage an existing `Safe<A>` decoder.
*/
export function jOption<A>(fn: Safe<A>, defaultValue?: A): Loose<A> {
return (js: json) => (js === undefined || js === null ? defaultValue : fn(js));
@@ -194,7 +195,7 @@ export function jTry<A>(fn: Loose<A>, defaultValue?: A): Loose<A> {
}
/**
- Converts maps to dictionnaries.
+ Converts maps to dictionaries.
*/
export function jMap<A>(fn: Loose<A>): Safe<Map<string, A>> {
return (js: json) => {
@@ -210,7 +211,7 @@ export function jMap<A>(fn: Loose<A>): Safe<Map<string, A>> {
}
/**
- Converts dictionnaries to maps.
+ Converts dictionaries to maps.
*/
export function eMap<A>(fn: Encoder<A>): Encoder<Map<string, undefined | A>> {
return m => {
@@ -226,10 +227,10 @@ export function eMap<A>(fn: Encoder<A>): Encoder<Map<string, undefined | A>> {
}
/**
- Apply the decoder on each item of a JSON array, or return `[]` otherwize.
+ Apply the decoder on each item of a JSON array, or return `[]` otherwise.
Can be also applied on a _loose_ decoder, but you will get
an array with possibly `undefined` elements. Use [[jList]]
- to discard undefined elements, or use a true « safe » decoder.
+ to discard undefined elements, or use a true _safe_ decoder.
*/
export function jArray<A>(fn: Safe<A>): Safe<A[]> {
return (js: json) => Array.isArray(js) ? js.map(fn) : [];
@@ -237,7 +238,7 @@ export function jArray<A>(fn: Safe<A>): Safe<A[]> {
/**
Apply the loose decoder on each item of a JSON array, discarding
- all `undefined` elements. To keep all, possibly undefined array entries,
+ all `undefined` elements. To keep the all possibly undefined array entries,
use [[jArray]] instead.
*/
export function jList<A>(fn: Loose<A>): Safe<A[]> {
@@ -443,7 +444,7 @@ export function index<K, A>(d: dict<K, A>, key: key<K>, value: A) {
}
/**
- Decode a JSON dictionary, dicarding all inconsistent entries.
+ Decode a JSON dictionary, discarding all inconsistent entries.
If the JSON contains no valid entry, still returns `{}`.
*/
export function jDictionary<K, A>(kd: K, fn: Loose<A>): Safe<dict<K, A>> {
@@ -463,7 +464,7 @@ export function jDictionary<K, A>(kd: K, fn: Loose<A>): Safe<dict<K, A>> {
}
/**
- Encode a dictionary into JSON, dicarding all inconsistent entries.
+ Encode a dictionary into JSON, discarding all inconsistent entries.
If the dictionary contains no valid entry, still returns `{}`.
*/
export function eDictionary<K, A>(fn: Encoder<A>): Encoder<dict<K, A>> {
diff --git a/ivette/src/dome/src/renderer/data/states.ts b/ivette/src/dome/src/renderer/data/states.ts
index e614ab0309c0adaa8c4293f47f42a62a67fbcbc3..c19b5fa9a9427339ba696d66571b4a71af84bf2e 100644
--- a/ivette/src/dome/src/renderer/data/states.ts
+++ b/ivette/src/dome/src/renderer/data/states.ts
@@ -5,7 +5,7 @@
/**
Typed States & Settings
@packageDocumentation
- @package dome/data/states
+ @module dome/data/states
*/
import React from 'react';
@@ -17,17 +17,23 @@ import * as JSON from './json';
const UPDATE = 'dome.states.update';
-/** Base state interface. */
+/** Cross-component State. */
export class State<A> {
+
private value: A;
private emitter: Emitter;
+
constructor(initValue: A) {
this.value = initValue;
this.emitter = new Emitter;
this.getValue = this.getValue.bind(this);
this.setValue = this.setValue.bind(this);
}
+
+ /** Current state value. */
getValue() { return this.value; }
+
+ /** Notify callbacks on change, using _deep_ structural comparison. */
setValue(value: A) {
if (!isEqual(value, this.value)) {
this.value = value;
@@ -35,10 +41,12 @@ export class State<A> {
}
}
+ /** Callback Emitter. */
on(callback: (value: A) => void) {
this.emitter.on(UPDATE, callback);
}
+ /** Callback Emitter. */
off(callback: (value: A) => void) {
this.emitter.off(UPDATE, callback);
}
@@ -73,18 +81,19 @@ export function useState<A>(s: State<A>): [A, (update: A) => void] {
When several components share the same setting `dataKey` the behavior will be
different depending on the situation:
- for Window Settings, each component in each window retains its own
- setting value, although the last modified value from _any_ of them will be saved
- and used for any further initial value;
+ setting value, although the last modified value from _any_ of them will be
+ saved and used for any further initial value;
- for Global Settings, all components synchronize to the last modified value
from any component of any window.
Type safety is ensured by safe JSON encoders and decoders, however, they
might fail at runtime, causing settings value to be initialized to their
- fallback and not to be saved or synchronized. This is not harmfull but annoying.
+ fallback and not to be saved nor synchronized.
+ This is not harmful but annoying.
To mitigate this effect, each instance of a Settings class has its
own, private, unique symbol that we call its « role ». A given `dataKey`
- shall always be used with the same « role » otherwized it is discarded,
+ shall always be used with the same « role » otherwise it is discarded,
and an error message is logged when in DEVEL mode.
*/
abstract class Settings<A> {
@@ -99,11 +108,12 @@ abstract class Settings<A> {
Encoders shall be protected against exception.
Use [[JSON.jTry]] and [[JSON.jCatch]] in case of uncertainty.
Decoders are automatically protected internally to the Settings class.
- @param role - Debugging name of instance roles (each instance has its unique role, though)
- @param decoder - JSON decoder for the setting values
- @param encoder - JSON encoder for the setting values
- @param fallback -
- If provided, used to automatically protect your encoders against exceptions.
+ @param role Debugging name of instance roles (each instance has its unique
+ role, though)
+ @param decoder JSON decoder for the setting values
+ @param encoder JSON encoder for the setting values
+ @param fallback If provided, used to automatically protect your encoders
+ against exceptions.
*/
constructor(
role: string,
@@ -131,7 +141,7 @@ abstract class Settings<A> {
} else {
if (rk !== rq) {
if (DEVEL) console.error(
- `[Dome.settings] key ${dataKey} used with incompatible roles`, rk, rq,
+ `[Dome.settings] Key ${dataKey} used with incompatible roles`, rk, rq,
);
return undefined;
}
@@ -155,13 +165,13 @@ abstract class Settings<A> {
}
/** Push the new setting value for the provided data key.
- You only use validated keys otherwise further loads
+ You shall only use validated keys otherwise further loads
might fail and fallback to defaults. */
saveValue(dataKey: string, value: A) {
try { this.saveData(dataKey, this.encoder(value)); }
catch (err) {
if (DEVEL) console.error(
- '[Dome.settings] error while encoding value',
+ '[Dome.settings] Error while encoding value',
dataKey, value, err,
);
}
@@ -174,8 +184,8 @@ abstract class Settings<A> {
You may share `dataKey` between components, or change it dynamically.
However, a given data key shall always be used for the same Setting instance.
See [[Settings]] documentation for details.
- @param S - the instance settings to be used
- @param dataKey - identifies which value in the settings to be used
+ @param S The instance settings to be used.
+ @param dataKey Identifies which value in the settings to be used.
*/
export function useSettings<A>(
S: Settings<A>,
diff --git a/ivette/src/dome/src/renderer/dome.js b/ivette/src/dome/src/renderer/dome.js
index 89205b050f9e26d1c2f5a52320ddc52da8b021ae..322a76d8bc3242c7d2631da72db37257d2602649 100644
--- a/ivette/src/dome/src/renderer/dome.js
+++ b/ivette/src/dome/src/renderer/dome.js
@@ -424,7 +424,7 @@ const writeSetting = ( local, key, value ) => {
patches.set(key,value);
}
if (local) {
- if (DEVEL) fireSaveSettings();
+ fireSaveSettings();
} else {
emitter.emit('dome.settings');
fireSaveGlobals();
diff --git a/ivette/src/dome/src/renderer/table/views.tsx b/ivette/src/dome/src/renderer/table/views.tsx
index 1729d9549b0f5b3df14b27085a08ab6ab9ef1102..5e7888b7c89035af4b1b8de6cfa738f47a075fdd 100644
--- a/ivette/src/dome/src/renderer/table/views.tsx
+++ b/ivette/src/dome/src/renderer/table/views.tsx
@@ -212,7 +212,7 @@ function makeDataGetter(
if (rowData !== undefined) return getter(rowData, dataKey);
} catch (err) {
console.error(
- '[Dome.table] custom getter error',
+ '[Dome.table] Custom getter error',
'rowData:', rowData,
'dataKey:', dataKey,
err,
@@ -240,7 +240,7 @@ function makeDataRenderer(
return contents;
} catch (err) {
console.error(
- '[Dome.table] custom renderer error',
+ '[Dome.table] Custom renderer error',
'dataKey:', props.dataKey,
'cellData:', cellData,
err,
diff --git a/nix/default.nix b/nix/default.nix
index 5b892f99684c6fbc9350df9a936c175b73a09bdd..c8e4966f3f26110ec5cfa96fd6629275292a6864 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -2,7 +2,7 @@
{ pkgs, stdenv, src ? ../., opam2nix, ocaml_version ? "ocaml-ng.ocamlPackages_4_05.ocaml", plugins ? { } }:
let mk_buildInputs = { opamPackages ? [], nixPackages ? [] } :
- [ pkgs.gnugrep pkgs.gnused pkgs.autoconf pkgs.gnumake pkgs.gcc pkgs.ncurses pkgs.time pkgs.python3 pkgs.perl pkgs.file pkgs.which] ++ nixPackages ++ opam2nix.build {
+ [ pkgs.gnugrep pkgs.gnused pkgs.autoconf pkgs.gnumake pkgs.gcc pkgs.ncurses pkgs.time pkgs.python3 pkgs.perl pkgs.file pkgs.which pkgs.dos2unix] ++ nixPackages ++ opam2nix.build {
specs = opam2nix.toSpecs ([ "ocamlfind" "zarith" "ocamlgraph" "yojson"
{ name = "coq"; constraint = "=8.11.1"; }
{ name = "why3" ; constraint = "=1.3.1"; }
diff --git a/opam/opam b/opam/opam
index 7a9cf964ddc104a6fed5641840c9ad527dc55d3f..9f715d2b74b753268a2849ab0b69103582117e28 100644
--- a/opam/opam
+++ b/opam/opam
@@ -1,7 +1,7 @@
opam-version: "2.0"
name: "frama-c"
synopsis: "Platform dedicated to the analysis of source code written in C"
-version: "21.0+dev"
+version: "21.1+dev"
description:"""
Frama-C gathers several analysis techniques in a single collaborative
framework, based on analyzers (called "plug-ins") that can build upon the
@@ -65,7 +65,7 @@ authors: [
homepage: "http://frama-c.com/"
license: "GNU Lesser General Public License version 2.1"
dev-repo: "git+https://git.frama-c.com/pub/frama-c.git"
-doc: "http://frama-c.com/download/user-manual-21.0-Scandium.pdf"
+doc: "http://frama-c.com/download/user-manual-21.1-Scandium.pdf"
bug-reports: "https://bts.frama-c.com/"
tags: [
"deductive"
diff --git a/ptests/ptests.ml b/ptests/ptests.ml
index 6b316854a46960544bb38a7812c206217cb4304b..3202933a25a1a124dc0eda2ae77bae5763a43943 100644
--- a/ptests/ptests.ml
+++ b/ptests/ptests.ml
@@ -819,13 +819,16 @@ let scan_options dir scan_buffer default =
r := (List.assoc name config_options) dir opt !r
with Not_found ->
lock_eprintf "@[unknown configuration option: %s@\n%!@]" name)
- with Scanf.Scan_failure _ ->
+ with
+ | Scanf.Scan_failure _ ->
if str_string_match end_comment s 0
then raise End_of_file
else ()
+ | End_of_file -> (* ignore blank lines. *) ()
in
try
while true do
+ if Scanf.Scanning.end_of_input scan_buffer then raise End_of_file;
Scanf.bscanf scan_buffer "%s@\n" treat_line
done;
assert false
diff --git a/reference-configuration.md b/reference-configuration.md
index 4924e5ebc07ff2fce10e9a8b86ceedf958fdee05..67657200acdd65fd4798d090e3865c5e88fb7d3d 100644
--- a/reference-configuration.md
+++ b/reference-configuration.md
@@ -1,14 +1,15 @@
The following set of packages is known to be a working configuration for
-compiling Frama-C 21 (Scandium), on a machine with gcc <= 9[^gcc-10]
+compiling Frama-C+dev, on a machine with gcc <= 9[^gcc-10]
-- OCaml 4.07.1
-- ocamlfind.1.8.0
-- apron.v0.9.12 (optional)
-- lablgtk.2.18.10 | lablgtk3.3.0.beta6 + lablgtk3-sourceview3.3.0.beta6
-- mlgmpidl.1.2.12 (optional)
+- OCaml 4.08.1
+- alt-ergo.2.0.0 (for wp, optional)
+- apron.v0.9.12 (for eva, optional)
+- lablgtk.2.18.11 | lablgtk3.3.1.1 + lablgtk3-sourceview3.3.1.1
+- mlgmpidl.1.2.12 (for eva, optional)
+- ocamlfind.1.8.1
- ocamlgraph.1.8.8
+- ppx_deriving_yojson.3.5.2 (for mdr, optional)
- why3.1.3.1
-- alt-ergo.2.0.0 (for wp, optional)
- yojson.1.7.0
- zarith.1.9.1
- zmq.5.1.3 (for server, optional)
@@ -16,5 +17,4 @@ compiling Frama-C 21 (Scandium), on a machine with gcc <= 9[^gcc-10]
[^gcc-10]: As mentioned in this [OCaml PR](https://github.com/ocaml/ocaml/issues/9144)
gcc 10 changed its default linking conventions to make them more stringent,
resulting in various linking issues. In particular, only OCaml 4.10 can be
-linked against gcc-10. With respect to the list above, this also means using
-ocamlfind.1.8.1 and the development version of lablgtk (https://github.com/garrigue/lablgtk)
\ No newline at end of file
+linked against gcc-10.
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index 5b485c09b90a8ca699170b6a3e6f649d48946a9a..653d91fad5e4696a2cb7398993aad983048684d5 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -138,6 +138,9 @@ HAS_DOT ?=@HAS_DOT@
HEADACHE ?= headache -c $(FRAMAC_SRC)/headers/headache_config.txt
+UNIX2DOS ?= @UNIX2DOS@
+HAS_UNIX2DOS ?= @HAS_UNIX2DOS@
+
###########################
# Miscellaneous variables #
###########################
diff --git a/src/kernel_internals/parsing/logic_preprocess.mll b/src/kernel_internals/parsing/logic_preprocess.mll
index ff9d1acb52dd5ff53b0f2045c5f11ade20418656..34ea01b4d6bda1c8a16eb82d54425fc1b82b90ef 100644
--- a/src/kernel_internals/parsing/logic_preprocess.mll
+++ b/src/kernel_internals/parsing/logic_preprocess.mll
@@ -94,13 +94,14 @@
let content = Buffer.create 80 in
let rec ignore_content () =
let s = input_line file in
- if s <> annot_beg then ignore_content ()
+ if not (Extlib.string_prefix annot_beg s) then ignore_content ()
in
let rec get_annot first =
let s = input_line file in
- if s = annot_end then false, Buffer.contents content
- else if s = annot_end_nl then true, Buffer.contents content
- else if s = annot_end_comment then begin
+ if Extlib.string_prefix annot_end s then false, Buffer.contents content
+ else if Extlib.string_prefix annot_end_nl s then
+ true, Buffer.contents content
+ else if Extlib.string_prefix annot_end_comment s then begin
Buffer.add_char content '\n';
false, Buffer.contents content
end else begin
diff --git a/src/kernel_internals/runtime/frama_c_config.ml.in b/src/kernel_internals/runtime/frama_c_config.ml.in
index f9488a16dcccdbdd2a8d3dc5d70d52fdcefc0640..6b0e200a724380edfba96d88e2aaa62243da89fb 100644
--- a/src/kernel_internals/runtime/frama_c_config.ml.in
+++ b/src/kernel_internals/runtime/frama_c_config.ml.in
@@ -53,7 +53,7 @@ let options = Arg.([
"-scripts",
Unit (fun _ -> Format.printf "%s%!"
- (Filename.concat Fc_config.datadir "analyis-scripts"); exit 0),
+ (Filename.concat Fc_config.datadir "analysis-scripts"); exit 0),
" Print the path of Frama-C analysis-scripts directory";
"-print-libpath",
diff --git a/src/kernel_internals/typing/allocates.ml b/src/kernel_internals/typing/allocates.ml
index 7b732f4edf83cefc6aa9e672b86c541c014648b6..21d04239663de36f3e20c3b6e81bc6a4e9a292be 100644
--- a/src/kernel_internals/typing/allocates.ml
+++ b/src/kernel_internals/typing/allocates.ml
@@ -35,7 +35,7 @@ let add_allocates_loop stmt =
let all_default = Annotations.fold_code_annot all_default stmt true in
if all_default then
let ca = AAllocation ([], FreeAlloc ([], [])) in
- Annotations.add_code_annot Emitter.kernel stmt
+ Annotations.add_code_annot ~keep_empty:false Emitter.kernel stmt
(Logic_const.new_code_annotation ca)
let add_allocates_nothing_funspec kf =
diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml
index d87771d648f135516e46dbb69a3eb2c97856afb8..b61d0d1c2b343fee034e3bf7e7c162d7affd86e3 100644
--- a/src/kernel_internals/typing/asm_contracts.ml
+++ b/src/kernel_internals/typing/asm_contracts.ml
@@ -184,7 +184,7 @@ class visit_assembly =
let ca =
Logic_const.new_code_annotation (AStmtSpec ([],spec))
in
- Annotations.add_code_annot emitter ~kf stmt ca;
+ Annotations.add_code_annot ~keep_empty:false emitter ~kf stmt ca;
if not mem_clobbered && Kernel.AsmContractsAutoValidate.get()
then begin
let active = [] in
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 2b0157f69b5bb35fd22301b642da63030e968430..17cf66913b9a127047fe7e66bbaf98ad4e871dfb 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -448,6 +448,19 @@ let process_pack_pragma name args =
current_packing_pragma:= new_pragma; None
end else
Some (Attr (name, args))
+ | ACons ("push",[]) :: args (* unknown push directive *) ->
+ Kernel.warning ~current:true
+ "Unsupported argument for pragma pack push directive: `%a'."
+ Format.(
+ pp_print_list
+ ~pp_sep:(fun fmt ()->pp_print_string fmt ", ")
+ Cil_printer.pp_attrparam)
+ args;
+ (* We don't change the current packing directive, but
+ nevertheless push it on the stack, to avoid a mismatched
+ pop somewhere later. *)
+ Stack.push !current_packing_pragma packing_pragma_stack;
+ None
| [ACons ("pop",[])] (* #pragma pack(pop) *) ->
begin try
current_packing_pragma := Stack.pop packing_pragma_stack;
diff --git a/src/kernel_services/abstract_interp/bottom.mli b/src/kernel_services/abstract_interp/bottom.mli
index 799ccedfc3f67f9507b9bcb5b89893eeb0bb109a..0af283e70bf755cd874fc5ea3bc51725fd8007d6 100644
--- a/src/kernel_services/abstract_interp/bottom.mli
+++ b/src/kernel_services/abstract_interp/bottom.mli
@@ -42,7 +42,7 @@ val non_bottom: 'a or_bottom -> 'a
val equal: ('a -> 'a -> bool) -> 'a or_bottom -> 'a or_bottom -> bool
val compare: ('a -> 'a -> int) -> 'a or_bottom -> 'a or_bottom -> int
-val is_included: ('a -> 'a -> bool) -> 'a or_bottom -> 'a or_bottom -> bool
+val is_included: ('a -> 'b -> bool) -> 'a or_bottom -> 'b or_bottom -> bool
val join: ('a -> 'a -> 'a) -> 'a or_bottom -> 'a or_bottom -> 'a or_bottom
val join_list: ('a -> 'a -> 'a) -> 'a or_bottom list -> 'a or_bottom
val narrow: ('a -> 'a -> 'a or_bottom) -> 'a or_bottom -> 'a or_bottom -> 'a or_bottom
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index 6af4807ad9b794215796de279d6fd12c749bf790..64b75c8765fc4219d2c831d6d1f165cd59197ca2 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -286,41 +286,6 @@ module Location_Bytes = struct
| Base.Variable { Base.weak } -> not weak
with Not_found -> false
- let iter_on_strings =
- let z = "\000" in
- fun ~skip f l ->
- match l with
- | Top _ ->
- assert false
- | Map m ->
- M.iter
- (fun base offs ->
- match skip with
- Some base_to_skip when Base.equal base base_to_skip -> ()
- | _ ->
- match base with
- Base.String (_, strid) ->
- let str =
- match strid with
- | Base.CSString s -> s
- | Base.CSWstring _ ->
- failwith "Unimplemented: wide strings"
- in
- let strz = str ^ z in
- let len = String.length str in
- let range =
- Ival.inject_range
- (Some Int.zero)
- (Some (Int.of_int len))
- in
- let roffs = Ival.narrow range offs in
- Ival.fold_int
- (fun i () -> f base strz (Int.to_int i) len)
- roffs
- ()
- | _ -> ())
- m
-
let topify_merge_origin v =
topify_with_origin_kind Origin.K_Merge v
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index f96d8f6bccf067d275003dec375f9f13a8bb9d5d..b8de6dce344930a6d04a3a1b97088f0a966d7976 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -194,9 +194,6 @@ module Location_Bytes : sig
(** {2 Misc} *)
- val iter_on_strings :
- skip:Base.t option -> (Base.t -> string -> int -> int -> unit) -> t -> unit
-
(** [is_relationable loc] returns [true] iff [loc] represents a single
memory location. *)
val is_relationable: t -> bool
diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml
index a75151352f640348731a343532d6cfa4da1a5646..f31a727c80275794f9265fc86312e1fd673e7dbf 100644
--- a/src/kernel_services/analysis/exn_flow.ml
+++ b/src/kernel_services/analysis/exn_flow.ml
@@ -23,20 +23,20 @@
open Cil
open Cil_types
-(* all exceptions that can be raised somewhere in the AST.
+(* all exceptions that can be raised somewhere in the AST.
Used to handle function pointers without exn specification
- *)
+*)
module All_exn =
State_builder.Option_ref(Cil_datatype.Typ.Set)
(struct let name = "Exn_flow.All_exn" let dependencies = [Ast.self] end)
-
+
module Exns =
State_builder.Hashtbl(Kernel_function.Hashtbl)(Cil_datatype.Typ.Set)
(struct
- let name = "Exn_flow.Exns"
- let dependencies = [Ast.self; All_exn.self]
- let size = 47
- end)
+ let name = "Exn_flow.Exns"
+ let dependencies = [Ast.self; All_exn.self]
+ let size = 47
+ end)
module ExnsStmt =
State_builder.Hashtbl(Cil_datatype.Stmt.Hashtbl)(Cil_datatype.Typ.Set)
@@ -61,10 +61,10 @@ class all_exn =
method get_exn = all_exn
method! vstmt_aux s =
match s.skind with
- | Throw (Some (_,t),_) ->
- all_exn <- Cil_datatype.Typ.Set.add (purify t) all_exn;
- SkipChildren
- | _ -> DoChildren
+ | Throw (Some (_,t),_) ->
+ all_exn <- Cil_datatype.Typ.Set.add (purify t) all_exn;
+ SkipChildren
+ | _ -> DoChildren
end
let compute_all_exn () =
@@ -82,41 +82,41 @@ let add_exn_var exns v =
let add_exn_clause exns (v,_) = add_exn_var exns v
(* We're not really interested by intra-procedural Dataflow here: all the
- interesting stuff happens at inter-procedural level (except for Throw
+ interesting stuff happens at inter-procedural level (except for Throw
encapsulated directly in a TryCatch, but even then it is easily captured
- at syntactical level). Therefore, we can as well use a syntactic pass
+ at syntactical level). Therefore, we can as well use a syntactic pass
at intra-procedural level
- *)
+*)
class exn_visit =
-object (self)
- inherit Visitor.frama_c_inplace
- val stack = Stack.create ()
- val possible_exn = Stack.create ()
- (* current set of exn included in a catch-all clause. Used to
- handle Throw None;
- *)
- val current_exn = Stack.create ()
-
- method private recursive_call kf =
- try
- Stack.iter
- (fun (kf',_) -> if Kernel_function.equal kf kf' then raise Exit) stack;
- false
- with Exit -> true
-
- method private add_exn t =
- let current_uncaught = Stack.top possible_exn in
- current_uncaught:= Cil_datatype.Typ.Set.add t !current_uncaught
-
- method private union_exn s =
- let current_uncaught = Stack.top possible_exn in
- current_uncaught := Cil_datatype.Typ.Set.union s !current_uncaught
-
- method! vstmt_aux s =
- match s.skind with
+ object (self)
+ inherit Visitor.frama_c_inplace
+ val stack = Stack.create ()
+ val possible_exn = Stack.create ()
+ (* current set of exn included in a catch-all clause. Used to
+ handle Throw None;
+ *)
+ val current_exn = Stack.create ()
+
+ method private recursive_call kf =
+ try
+ Stack.iter
+ (fun (kf',_) -> if Kernel_function.equal kf kf' then raise Exit) stack;
+ false
+ with Exit -> true
+
+ method private add_exn t =
+ let current_uncaught = Stack.top possible_exn in
+ current_uncaught:= Cil_datatype.Typ.Set.add t !current_uncaught
+
+ method private union_exn s =
+ let current_uncaught = Stack.top possible_exn in
+ current_uncaught := Cil_datatype.Typ.Set.union s !current_uncaught
+
+ method! vstmt_aux s =
+ match s.skind with
| Throw (None,_) ->
- let my_exn = Stack.top current_exn in
- self#union_exn my_exn; ExnsStmt.replace s my_exn; SkipChildren
+ let my_exn = Stack.top current_exn in
+ self#union_exn my_exn; ExnsStmt.replace s my_exn; SkipChildren
| Throw(Some (_,t),_) ->
let t = Cil.unrollTypeDeep t in
let t = Cil.type_remove_qualifier_attributes t in
@@ -127,14 +127,14 @@ object (self)
let catch, catch_all =
List.fold_left
(fun (catch, catch_all) ->
- function
- | (Catch_all,_) -> catch, true
- | (Catch_exn(v,[]),_) ->
- let catch = add_exn_var catch v in
- catch, catch_all
- | (Catch_exn(_,aux), _) ->
- let catch = List.fold_left add_exn_clause catch aux in
- catch, catch_all)
+ function
+ | (Catch_all,_) -> catch, true
+ | (Catch_exn(v,[]),_) ->
+ let catch = add_exn_var catch v in
+ catch, catch_all
+ | (Catch_exn(_,aux), _) ->
+ let catch = List.fold_left add_exn_clause catch aux in
+ catch, catch_all)
(Cil_datatype.Typ.Set.empty,false) c
in
Stack.push (ref Cil_datatype.Typ.Set.empty) possible_exn;
@@ -147,7 +147,7 @@ object (self)
if not catch_all then self#union_exn uncaught;
List.iter
(fun (v,b) ->
- (match v with
+ (match v with
| Catch_all ->
(* catch_all will catch all exceptions that are not
already handled by a previous clause. It must be the
@@ -164,9 +164,9 @@ object (self)
add_exn_clause Cil_datatype.Typ.Set.empty aux
in
Stack.push catch current_exn);
- ignore
- (Visitor.visitFramacBlock (self:>Visitor.frama_c_inplace) b);
- ignore (Stack.pop current_exn))
+ ignore
+ (Visitor.visitFramacBlock (self:>Visitor.frama_c_inplace) b);
+ ignore (Stack.pop current_exn))
c;
let my_exn = !(Stack.pop possible_exn) in
ExnsStmt.replace s my_exn;
@@ -175,34 +175,34 @@ object (self)
| If _ | Switch _ | Loop _ | Block _ | UnspecifiedSequence _
| TryFinally _ | TryExcept _
| Instr _ -> (* must take into account exceptions thrown by a fun call*)
- Stack.push (ref Cil_datatype.Typ.Set.empty) possible_exn;
- DoChildrenPost
- (fun s ->
+ Stack.push (ref Cil_datatype.Typ.Set.empty) possible_exn;
+ DoChildrenPost
+ (fun s ->
let my_exn = !(Stack.pop possible_exn) in
ExnsStmt.replace s my_exn;
self#union_exn my_exn;
s)
(* No exception can be thrown here. *)
| Return _ | Goto _ | Break _ | Continue _ ->
- ExnsStmt.replace s Cil_datatype.Typ.Set.empty;
- SkipChildren
+ ExnsStmt.replace s Cil_datatype.Typ.Set.empty;
+ SkipChildren
- method! vinst =
- function
+ method! vinst =
+ function
| Call(_,{ enode = Lval(Var f,NoOffset) },_,_)
| Local_init(_, ConsInit(f, _, _), _) ->
let kf = Globals.Functions.get f in
if self#recursive_call kf then begin
let module Found =
- struct
- exception F of Cil_datatype.Typ.Set.t
- end
+ struct
+ exception F of Cil_datatype.Typ.Set.t
+ end
in
let computed_exn =
try
Stack.iter
(fun (kf', exns) ->
- if Kernel_function.equal kf kf' then raise (Found.F !exns))
+ if Kernel_function.equal kf kf' then raise (Found.F !exns))
stack;
Kernel.fatal "No cycle found!"
with Found.F exns -> exns
@@ -220,7 +220,7 @@ object (self)
let kf_exn = Cil_datatype.Typ.Set.union computed_exn known_exn in
Exns.replace kf kf_exn;
ignore
- (Visitor.visitFramacFunction
+ (Visitor.visitFramacFunction
(self:>Visitor.frama_c_visitor)
(Kernel_function.get_definition kf));
let callee_exn = Exns.find kf in
@@ -236,9 +236,9 @@ object (self)
self#union_exn callee_exn
end else begin (* TODO: introduce extension to declare
exceptions that can be thrown by prototypes. *)
- Kernel.warning
- "Assuming declared function %a can't throw any exception"
- Kernel_function.pretty kf
+ Kernel.warning
+ "Assuming declared function %a can't throw any exception"
+ Kernel_function.pretty kf
end;
SkipChildren
| Call _ ->
@@ -247,60 +247,60 @@ object (self)
self#union_exn (all_exn()); SkipChildren
| _ -> SkipChildren
- method! vfunc f =
- let my_exns = ref Cil_datatype.Typ.Set.empty in
- let kf = Globals.Functions.get f.svar in
- Stack.push (kf,my_exns) stack;
- Stack.push my_exns possible_exn;
- let after_visit f =
- let callee_exn = Stack.pop possible_exn in
- Exns.add kf !callee_exn;
- ignore (Stack.pop stack); f
- in
- DoChildrenPost after_visit
+ method! vfunc f =
+ let my_exns = ref Cil_datatype.Typ.Set.empty in
+ let kf = Globals.Functions.get f.svar in
+ Stack.push (kf,my_exns) stack;
+ Stack.push my_exns possible_exn;
+ let after_visit f =
+ let callee_exn = Stack.pop possible_exn in
+ Exns.add kf !callee_exn;
+ ignore (Stack.pop stack); f
+ in
+ DoChildrenPost after_visit
-end
+ end
let compute_kf kf =
if Kernel_function.is_definition kf then
ignore
(Visitor.visitFramacFunction (new exn_visit)
(Kernel_function.get_definition kf))
- (* just ignore prototypes. *)
+(* just ignore prototypes. *)
let compute () = Globals.Functions.iter compute_kf
let get_type_tag t =
let rec aux t =
match t with
- | TVoid _ -> "v"
- | TInt (IBool,_) -> "B"
- | TInt (IChar,_) -> "c"
- | TInt (ISChar,_) -> "sc"
- | TInt (IUChar,_) -> "uc"
- | TInt (IInt,_) -> "i"
- | TInt (IUInt,_) -> "ui"
- | TInt (IShort,_) -> "s"
- | TInt (IUShort,_) -> "us"
- | TInt (ILong,_) -> "l"
- | TInt (IULong,_) -> "ul"
- | TInt (ILongLong,_) -> "ll"
- | TInt (IULongLong,_) -> "ull"
- | TFloat(FFloat,_) -> "f"
- | TFloat(FDouble,_) -> "d"
- | TFloat (FLongDouble,_) -> "ld"
- | TPtr(t,_) -> "p" ^ aux t
- | TArray(t,_,_,_) -> "a" ^ aux t
- | TFun(rt,l,_,_) ->
- let base = "fun" ^ aux rt in
- (match l with
- | None -> base
- | Some l ->
- List.fold_left (fun acc (_,t,_) -> acc ^ aux t) base l)
- | TNamed _ -> Kernel.fatal "named type not correctly unrolled"
- | TComp (s,_,_) -> (if s.cstruct then "S" else "U") ^ s.cname
- | TEnum (e,_) -> "E" ^ e.ename
- | TBuiltin_va_list _ -> "va"
+ | TVoid _ -> "v"
+ | TInt (IBool,_) -> "B"
+ | TInt (IChar,_) -> "c"
+ | TInt (ISChar,_) -> "sc"
+ | TInt (IUChar,_) -> "uc"
+ | TInt (IInt,_) -> "i"
+ | TInt (IUInt,_) -> "ui"
+ | TInt (IShort,_) -> "s"
+ | TInt (IUShort,_) -> "us"
+ | TInt (ILong,_) -> "l"
+ | TInt (IULong,_) -> "ul"
+ | TInt (ILongLong,_) -> "ll"
+ | TInt (IULongLong,_) -> "ull"
+ | TFloat(FFloat,_) -> "f"
+ | TFloat(FDouble,_) -> "d"
+ | TFloat (FLongDouble,_) -> "ld"
+ | TPtr(t,_) -> "p" ^ aux t
+ | TArray(t,_,_,_) -> "a" ^ aux t
+ | TFun(rt,l,_,_) ->
+ let base = "fun" ^ aux rt in
+ (match l with
+ | None -> base
+ | Some l ->
+ List.fold_left (fun acc (_,t,_) -> acc ^ aux t) base l)
+ | TNamed _ -> Kernel.fatal "named type not correctly unrolled"
+ | TComp (s,_,_) -> (if s.cstruct then "S" else "U") ^ s.cname
+ | TEnum (e,_) -> "E" ^ e.ename
+ | TBuiltin_va_list _ -> "va"
in "__fc_" ^ aux t
let get_type_enum t = "__fc_exn_kind_" ^ (get_type_tag t)
@@ -372,9 +372,9 @@ let generate_exn_union e exns =
let add_types_and_globals typs globs f =
let iter_globs (acc,added) g =
match g with
- | GVarDecl _ | GVar _ | GFun _ as g when not added ->
- (g :: List.rev_append globs (List.rev_append typs acc), true)
- | _ -> g :: acc, added
+ | GVarDecl _ | GVar _ | GFun _ as g when not added ->
+ (g :: List.rev_append globs (List.rev_append typs acc), true)
+ | _ -> g :: acc, added
in
let globs, added = List.fold_left iter_globs ([],false) f.globals in
let globs =
@@ -399,130 +399,130 @@ let find_exns_func v =
let find_exns e =
match e.enode with
- | Lval(Var v, NoOffset) -> find_exns_func v
- | _ -> all_exn ()
+ | Lval(Var v, NoOffset) -> find_exns_func v
+ | _ -> all_exn ()
class erase_exn =
-object(self)
- inherit Visitor.frama_c_inplace
- (* reverse before filling. *)
- val mutable new_types = []
-
- val exn_enum = Cil_datatype.Typ.Hashtbl.create 7
+ object(self)
+ inherit Visitor.frama_c_inplace
+ (* reverse before filling. *)
+ val mutable new_types = []
- val exn_union = Cil_datatype.Typ.Hashtbl.create 7
+ val exn_enum = Cil_datatype.Typ.Hashtbl.create 7
- val mutable modified_funcs = Cil_datatype.Fundec.Set.empty
+ val exn_union = Cil_datatype.Typ.Hashtbl.create 7
- val mutable exn_struct = None
+ val mutable modified_funcs = Cil_datatype.Fundec.Set.empty
- val mutable exn_var = None
+ val mutable exn_struct = None
- val mutable can_throw = false
+ val mutable exn_var = None
- val mutable fct_can_throw = false
+ val mutable can_throw = false
- val mutable catched_var = None
+ val mutable fct_can_throw = false
- val mutable label_counter = 0
+ val mutable catched_var = None
- val exn_labels = Cil_datatype.Typ.Hashtbl.create 7
- val catch_all_label = Stack.create ()
+ val mutable label_counter = 0
- method modified_funcs = modified_funcs
+ val exn_labels = Cil_datatype.Typ.Hashtbl.create 7
+ val catch_all_label = Stack.create ()
- method private update_enum_bindings enum exns =
- let update_one_binding t =
- let s = get_type_enum t in
- let ei = List.find (fun ei -> ei.einame = s) enum.eitems in
- Cil_datatype.Typ.Hashtbl.add exn_enum t ei
- in
- Cil_datatype.Typ.Set.iter update_one_binding exns
+ method modified_funcs = modified_funcs
- method private update_union_bindings union exns =
- let update_one_binding t =
- let s = get_type_tag t in
- Kernel.debug ~dkey:Kernel.dkey_exn_flow
- "Registering %a as possible exn type" Cil_datatype.Typ.pretty t;
- let fi = List.find (fun fi -> fi.fname = s) union.cfields in
- Cil_datatype.Typ.Hashtbl.add exn_union t fi
- in
- Cil_datatype.Typ.Set.iter update_one_binding exns
-
- method private exn_kind t = Cil_datatype.Typ.Hashtbl.find exn_enum t
-
- method private is_thrown t = Cil_datatype.Typ.Hashtbl.mem exn_enum t
+ method private update_enum_bindings enum exns =
+ let update_one_binding t =
+ let s = get_type_enum t in
+ let ei = List.find (fun ei -> ei.einame = s) enum.eitems in
+ Cil_datatype.Typ.Hashtbl.add exn_enum t ei
+ in
+ Cil_datatype.Typ.Set.iter update_one_binding exns
+
+ method private update_union_bindings union exns =
+ let update_one_binding t =
+ let s = get_type_tag t in
+ Kernel.debug ~dkey:Kernel.dkey_exn_flow
+ "Registering %a as possible exn type" Cil_datatype.Typ.pretty t;
+ let fi = List.find (fun fi -> fi.fname = s) union.cfields in
+ Cil_datatype.Typ.Hashtbl.add exn_union t fi
+ in
+ Cil_datatype.Typ.Set.iter update_one_binding exns
- method private exn_field_off name =
- List.find (fun fi -> fi.fname = name) (Extlib.the exn_struct).cfields
+ method private exn_kind t = Cil_datatype.Typ.Hashtbl.find exn_enum t
- method private exn_field name =
- Var (Extlib.the exn_var), Field(self#exn_field_off name, NoOffset)
+ method private is_thrown t = Cil_datatype.Typ.Hashtbl.mem exn_enum t
- method private exn_field_term name =
- TVar(Cil.cvar_to_lvar (Extlib.the exn_var)),
- TField(self#exn_field_off name, TNoOffset)
+ method private exn_field_off name =
+ List.find (fun fi -> fi.fname = name) (Extlib.the exn_struct).cfields
- method private exn_obj_field = self#exn_field exn_obj_name
+ method private exn_field name =
+ Var (Extlib.the exn_var), Field(self#exn_field_off name, NoOffset)
- method private exn_obj_field_term = self#exn_field_term exn_obj_name
+ method private exn_field_term name =
+ TVar(Cil.cvar_to_lvar (Extlib.the exn_var)),
+ TField(self#exn_field_off name, TNoOffset)
- method private exn_kind_field = self#exn_field exn_kind_name
+ method private exn_obj_field = self#exn_field exn_obj_name
- method private exn_kind_field_term = self#exn_field_term exn_kind_name
+ method private exn_obj_field_term = self#exn_field_term exn_obj_name
- method private uncaught_flag_field = self#exn_field exn_uncaught_name
+ method private exn_kind_field = self#exn_field exn_kind_name
- method private uncaught_flag_field_term =
- self#exn_field_term exn_uncaught_name
+ method private exn_kind_field_term = self#exn_field_term exn_kind_name
- method private exn_obj_kind_field t =
- Kernel.debug ~dkey:Kernel.dkey_exn_flow
- "Searching for %a as possible exn type" Cil_datatype.Typ.pretty t;
- Cil_datatype.Typ.Hashtbl.find exn_union t
+ method private uncaught_flag_field = self#exn_field exn_uncaught_name
- method private test_uncaught_flag loc b =
- let e1 = Cil.new_exp ~loc (Lval self#uncaught_flag_field) in
- let e2 = if b then Cil.one ~loc else Cil.zero ~loc in
- Cil.new_exp ~loc (BinOp(Eq,e1,e2,Cil.intType))
+ method private uncaught_flag_field_term =
+ self#exn_field_term exn_uncaught_name
- method private pred_uncaught_flag loc b =
- let e1 =
- Logic_const.term
- ~loc (TLval self#uncaught_flag_field_term) Linteger
- in
- let e2 =
- if b then Logic_const.tinteger ~loc 1
- else Logic_const.tinteger ~loc 0
- in
- Logic_const.prel ~loc (Req,e1,e2)
-
- method private set_uncaught_flag loc b =
- let e = if b then Cil.one ~loc else Cil.zero ~loc in
- Cil.mkStmtOneInstr (Set(self#uncaught_flag_field,e,loc))
-
- method private set_exn_kind loc t =
- let e = self#exn_kind (purify t) in
- let e = Cil.new_exp ~loc (Const (CEnum e)) in
- Cil.mkStmtOneInstr(Set(self#exn_kind_field,e,loc))
-
- method private set_exn_value loc t e =
- let lv = self#exn_obj_field in
- let union_field = self#exn_obj_kind_field (purify t) in
- let lv = Cil.addOffsetLval (Field (union_field, NoOffset)) lv in
- Cil.mkStmtOneInstr (Set(lv,e,loc))
-
- method private jumps_to_default_handler loc =
- if Stack.is_empty catch_all_label then begin
- (* no catch-all clause in the function: just go up in the stack. *)
- fct_can_throw <- true;
- let kf = Extlib.the self#current_kf in
- let ret = Kernel_function.find_return kf in
- let rtyp = Kernel_function.get_return_type kf in
- if ret.labels = [] then
- ret.labels <- [Label("__ret_label",Cil_datatype.Stmt.loc ret,false)];
- let goto = mkStmt (Goto (ref ret,loc)) in
- match ret.skind with
+ method private exn_obj_kind_field t =
+ Kernel.debug ~dkey:Kernel.dkey_exn_flow
+ "Searching for %a as possible exn type" Cil_datatype.Typ.pretty t;
+ Cil_datatype.Typ.Hashtbl.find exn_union t
+
+ method private test_uncaught_flag loc b =
+ let e1 = Cil.new_exp ~loc (Lval self#uncaught_flag_field) in
+ let e2 = if b then Cil.one ~loc else Cil.zero ~loc in
+ Cil.new_exp ~loc (BinOp(Eq,e1,e2,Cil.intType))
+
+ method private pred_uncaught_flag loc b =
+ let e1 =
+ Logic_const.term
+ ~loc (TLval self#uncaught_flag_field_term) Linteger
+ in
+ let e2 =
+ if b then Logic_const.tinteger ~loc 1
+ else Logic_const.tinteger ~loc 0
+ in
+ Logic_const.prel ~loc (Req,e1,e2)
+
+ method private set_uncaught_flag loc b =
+ let e = if b then Cil.one ~loc else Cil.zero ~loc in
+ Cil.mkStmtOneInstr (Set(self#uncaught_flag_field,e,loc))
+
+ method private set_exn_kind loc t =
+ let e = self#exn_kind (purify t) in
+ let e = Cil.new_exp ~loc (Const (CEnum e)) in
+ Cil.mkStmtOneInstr(Set(self#exn_kind_field,e,loc))
+
+ method private set_exn_value loc t e =
+ let lv = self#exn_obj_field in
+ let union_field = self#exn_obj_kind_field (purify t) in
+ let lv = Cil.addOffsetLval (Field (union_field, NoOffset)) lv in
+ Cil.mkStmtOneInstr (Set(lv,e,loc))
+
+ method private jumps_to_default_handler loc =
+ if Stack.is_empty catch_all_label then begin
+ (* no catch-all clause in the function: just go up in the stack. *)
+ fct_can_throw <- true;
+ let kf = Extlib.the self#current_kf in
+ let ret = Kernel_function.find_return kf in
+ let rtyp = Kernel_function.get_return_type kf in
+ if ret.labels = [] then
+ ret.labels <- [Label("__ret_label",Cil_datatype.Stmt.loc ret,false)];
+ let goto = mkStmt (Goto (ref ret,loc)) in
+ match ret.skind with
| Return (None,_) -> [goto]
(* rt is void: do not need to create a dummy return value *)
| Return (Some { enode = Lval(Var rv, NoOffset) },_) ->
@@ -532,232 +532,232 @@ object(self)
Kernel.fatal "exception removal should be used after oneRet"
| _ ->
Kernel.fatal "find_return did not give a Return statement"
- end else begin
- let stmt = Stack.top catch_all_label in
- [mkStmt (Goto (ref stmt, loc))]
- end
-
- method private jumps_to_handler loc t =
- let t = purify t in
- try
- let stmt = Cil_datatype.Typ.Hashtbl.find exn_labels t in
- [mkStmt (Goto (ref stmt, loc))]
- with
+ end else begin
+ let stmt = Stack.top catch_all_label in
+ [mkStmt (Goto (ref stmt, loc))]
+ end
+
+ method private jumps_to_handler loc t =
+ let t = purify t in
+ try
+ let stmt = Cil_datatype.Typ.Hashtbl.find exn_labels t in
+ [mkStmt (Goto (ref stmt, loc))]
+ with
| Not_found -> self#jumps_to_default_handler loc
- method! vfile f =
- let exns = all_exn () in
- if not (Cil_datatype.Typ.Set.is_empty exns) then begin
- let loc = Cil_datatype.Location.unknown in
- let e = generate_exn_enum exns in
- let u,s = generate_exn_union e exns in
- let exn =
- Cil.makeGlobalVar "__fc_exn" (TComp (s,{scache = Not_Computed},[]))
- in
- self#update_enum_bindings e exns;
- self#update_union_bindings u exns;
- exn_struct <- Some s;
- can_throw <- true;
- new_types <-
- GCompTag (s,loc) ::
- GCompTag (u,loc) ::
- GEnumTag (e,loc) :: new_types;
- exn_var <- Some exn;
- let exn_init = Cil.makeZeroInit ~loc (TComp(s,{scache=Not_Computed},[]))
- in
- let gexn_var = GVar(exn, { init = Some exn_init }, loc) in
- ChangeDoChildrenPost(
- f,add_types_and_globals (List.rev new_types) [gexn_var])
- end else (* nothing can be thrown in the first place, but we still have
- to get rid of (useless) try/catch blocks if any. *)
+ method! vfile f =
+ let exns = all_exn () in
+ if not (Cil_datatype.Typ.Set.is_empty exns) then begin
+ let loc = Cil_datatype.Location.unknown in
+ let e = generate_exn_enum exns in
+ let u,s = generate_exn_union e exns in
+ let exn =
+ Cil.makeGlobalVar "__fc_exn" (TComp (s,{scache = Not_Computed},[]))
+ in
+ self#update_enum_bindings e exns;
+ self#update_union_bindings u exns;
+ exn_struct <- Some s;
+ can_throw <- true;
+ new_types <-
+ GCompTag (s,loc) ::
+ GCompTag (u,loc) ::
+ GEnumTag (e,loc) :: new_types;
+ exn_var <- Some exn;
+ let exn_init = Cil.makeZeroInit ~loc (TComp(s,{scache=Not_Computed},[]))
+ in
+ let gexn_var = GVar(exn, { init = Some exn_init }, loc) in
+ ChangeDoChildrenPost(
+ f,add_types_and_globals (List.rev new_types) [gexn_var])
+ end else (* nothing can be thrown in the first place, but we still have
+ to get rid of (useless) try/catch blocks if any. *)
DoChildren
- method private visit_catch_clause loc (v,b) =
- let loc =
- match b.bstmts with
+ method private visit_catch_clause loc (v,b) =
+ let loc =
+ match b.bstmts with
| [] -> loc
| [x] -> Cil_datatype.Stmt.loc x
| x::tl ->
fst (Cil_datatype.Stmt.loc x),
snd (Cil_datatype.Stmt.loc (Extlib.last tl))
- in
- let add_unreachable_block b =
- Cil.mkStmt (If(Cil.zero ~loc, b, Cil.mkBlock [], loc))
- in
- let assign_catched_obj v b =
- let exn_obj = self#exn_obj_field in
- let kind_field = self#exn_obj_kind_field (purify v.vtype) in
- let lv = Cil.addOffsetLval (Field (kind_field,NoOffset)) exn_obj in
- let s =
- Cil.mkStmtOneInstr
- (Set ((Var v, NoOffset), Cil.new_exp ~loc (Lval lv), loc))
in
- b.bstmts <- s :: b.bstmts
- in
- let f = Extlib.the self#current_func in
- let update_locals v b =
- if not (List.memq v b.blocals) then b.blocals <- v::b.blocals;
- if not (List.memq v f.slocals) then f.slocals <- v::f.slocals
- in
- let b =
- (match v with
- | Catch_all -> b
- | Catch_exn (v,[]) ->
- Cil.update_var_type v (purify v.vtype);
- update_locals v b;
- assign_catched_obj v b; b
- | Catch_exn(v,aux) ->
- let add_one_aux stmts (v,b) =
- Cil.update_var_type v (purify v.vtype);
- update_locals v b;
- assign_catched_obj v b;
- add_unreachable_block b :: stmts
- in
- b.blocals <- List.filter (fun v' -> v!=v') b.blocals;
- let aux_blocks =
- List.fold_left add_one_aux [Cil.mkStmt (Block b)] aux
- in
- let main_block = Cil.mkBlock aux_blocks in
- Cil.update_var_type v (purify v.vtype);
- update_locals v main_block;
- main_block)
- in
- ignore (Visitor.visitFramacBlock (self :> Visitor.frama_c_visitor) b);
- add_unreachable_block b
-
- method! vfunc _ =
- label_counter <- 0;
- fct_can_throw <- false;
- let update_body f =
- if fct_can_throw then begin
- Oneret.encapsulate_local_vars f
- end;
- f
- in
- DoChildrenPost update_body
+ let add_unreachable_block b =
+ Cil.mkStmt (If(Cil.zero ~loc, b, Cil.mkBlock [], loc))
+ in
+ let assign_catched_obj v b =
+ let exn_obj = self#exn_obj_field in
+ let kind_field = self#exn_obj_kind_field (purify v.vtype) in
+ let lv = Cil.addOffsetLval (Field (kind_field,NoOffset)) exn_obj in
+ let s =
+ Cil.mkStmtOneInstr
+ (Set ((Var v, NoOffset), Cil.new_exp ~loc (Lval lv), loc))
+ in
+ b.bstmts <- s :: b.bstmts
+ in
+ let f = Extlib.the self#current_func in
+ let update_locals v b =
+ if not (List.memq v b.blocals) then b.blocals <- v::b.blocals;
+ if not (List.memq v f.slocals) then f.slocals <- v::f.slocals
+ in
+ let b =
+ (match v with
+ | Catch_all -> b
+ | Catch_exn (v,[]) ->
+ Cil.update_var_type v (purify v.vtype);
+ update_locals v b;
+ assign_catched_obj v b; b
+ | Catch_exn(v,aux) ->
+ let add_one_aux stmts (v,b) =
+ Cil.update_var_type v (purify v.vtype);
+ update_locals v b;
+ assign_catched_obj v b;
+ add_unreachable_block b :: stmts
+ in
+ b.blocals <- List.filter (fun v' -> v!=v') b.blocals;
+ let aux_blocks =
+ List.fold_left add_one_aux [Cil.mkStmt (Block b)] aux
+ in
+ let main_block = Cil.mkBlock aux_blocks in
+ Cil.update_var_type v (purify v.vtype);
+ update_locals v main_block;
+ main_block)
+ in
+ ignore (Visitor.visitFramacBlock (self :> Visitor.frama_c_visitor) b);
+ add_unreachable_block b
+
+ method! vfunc _ =
+ label_counter <- 0;
+ fct_can_throw <- false;
+ let update_body f =
+ if fct_can_throw then begin
+ Oneret.encapsulate_local_vars f
+ end;
+ f
+ in
+ DoChildrenPost update_body
- method private modify_current () =
- modified_funcs <-
- Cil_datatype.Fundec.Set.add (Extlib.the self#current_func) modified_funcs;
+ method private modify_current () =
+ modified_funcs <-
+ Cil_datatype.Fundec.Set.add (Extlib.the self#current_func) modified_funcs;
- method private aux_handler_goto target (v,b) =
- let loc = v.vdecl in
- let goto_main_handler = Cil.mkStmt (Goto (ref target,loc)) in
- let suf =
- if label_counter = 0 then "" else "_" ^ (string_of_int label_counter)
- in
- let lab = (get_type_tag (purify v.vtype)) ^ suf in
- label_counter <- label_counter + 1;
- b.bstmts <- b.bstmts @ [goto_main_handler];
- (* we have at least the goto statement in the block *)
- let s = List.hd b.bstmts in
- s.labels <- (Label(lab,loc,false)::s.labels);
- Cil_datatype.Typ.Hashtbl.add exn_labels (purify v.vtype) s
-
- method private guard_post_cond (kind,pred as orig) =
- match kind with
- (* If we exit explicitly with exit,
- we haven't seen an uncaught exception anyway. *)
+ method private aux_handler_goto target (v,b) =
+ let loc = v.vdecl in
+ let goto_main_handler = Cil.mkStmt (Goto (ref target,loc)) in
+ let suf =
+ if label_counter = 0 then "" else "_" ^ (string_of_int label_counter)
+ in
+ let lab = (get_type_tag (purify v.vtype)) ^ suf in
+ label_counter <- label_counter + 1;
+ b.bstmts <- b.bstmts @ [goto_main_handler];
+ (* we have at least the goto statement in the block *)
+ let s = List.hd b.bstmts in
+ s.labels <- (Label(lab,loc,false)::s.labels);
+ Cil_datatype.Typ.Hashtbl.add exn_labels (purify v.vtype) s
+
+ method private guard_post_cond (kind,pred as orig) =
+ match kind with
+ (* If we exit explicitly with exit,
+ we haven't seen an uncaught exception anyway. *)
| Exits | Breaks | Continues -> orig
| Returns | Normal ->
- let loc = pred.ip_content.pred_loc in
- let p = self#pred_uncaught_flag loc false in
- let pred' = Logic_const.pred_of_id_pred pred in
- (kind,
- (Logic_const.new_predicate
- (Logic_const.pimplies ~loc (p,pred'))))
-
- method! vbehavior b =
- match self#current_kf, self#current_stmt with
+ let loc = pred.ip_content.pred_loc in
+ let p = self#pred_uncaught_flag loc false in
+ let pred' = Logic_const.pred_of_id_pred pred in
+ (kind,
+ (Logic_const.new_predicate
+ (Logic_const.pimplies ~loc (p,pred'))))
+
+ method! vbehavior b =
+ match self#current_kf, self#current_stmt with
| None, None -> SkipChildren
- (* Prototype is assumed to not throw any exception. *)
+ (* Prototype is assumed to not throw any exception. *)
| None, Some _ ->
- Kernel.fatal
- "Inconsistent visitor state: visiting a statement \
- outside of any function."
- | Some f, None when not (Kernel_function.is_definition f) ->
- (* By hypothesis, prototypes do not throw anything. *)
- SkipChildren
+ Kernel.fatal
+ "Inconsistent visitor state: visiting a statement \
+ outside of any function."
+ | Some f, None when not (Kernel_function.is_definition f) ->
+ (* By hypothesis, prototypes do not throw anything. *)
+ SkipChildren
| Some f, None -> (* function contract *)
- let exns = Exns.find f in
- if Cil_datatype.Typ.Set.is_empty exns then SkipChildren
- else begin
- b.b_post_cond <- List.map self#guard_post_cond b.b_post_cond;
- ChangeTo b (* need to register the new clauses. *)
- end
+ let exns = Exns.find f in
+ if Cil_datatype.Typ.Set.is_empty exns then SkipChildren
+ else begin
+ b.b_post_cond <- List.map self#guard_post_cond b.b_post_cond;
+ ChangeTo b (* need to register the new clauses. *)
+ end
| Some _, Some s -> (* statement contract *)
- let exns = ExnsStmt.find s in
- if Cil_datatype.Typ.Set.is_empty exns then SkipChildren
- else begin
- b.b_post_cond <- List.map self#guard_post_cond b.b_post_cond;
- ChangeTo b
- end
-
- method private clean_catch_clause (bind,b as handler) acc =
- let remove_local v =
- let f =
- Visitor_behavior.Get.fundec self#behavior (Extlib.the self#current_func)
- in
- let v = Visitor_behavior.Get.varinfo self#behavior v in
- f.slocals <- List.filter (fun v' -> v!=v') f.slocals;
- in
- match bind with
- | Catch_all -> handler :: acc
- | Catch_exn (v, []) ->
- if self#is_thrown (purify v.vtype) then handler :: acc
- else begin remove_local v; acc end
- | Catch_exn (v, l) ->
- let caught, remove =
- List.partition (fun (v,_) -> self#is_thrown (purify v.vtype)) l
- in
- List.iter (fun (v,_) -> remove_local v) remove;
- if caught = [] then begin remove_local v; acc end
- else (Catch_exn (v,caught), b) :: acc
-
- method! vstmt_aux s =
- let generate_jumps instr exns loc =
- if Cil_datatype.Typ.Set.is_empty exns then SkipChildren
- else begin
- self#modify_current ();
- let make_jump t (stmts, uncaught) =
- let t = purify t in
- if Cil_datatype.Typ.Hashtbl.mem exn_labels t then begin
- let e = self#exn_kind t in
- let e = Cil.new_exp ~loc (Const (CEnum e)) in
- let b = self#jumps_to_handler loc t in
- let s = Cil.mkStmt (Block (Cil.mkBlock b)) in
- s.labels <- [Case (e,loc)];
- s::stmts, uncaught
- end else stmts, true
+ let exns = ExnsStmt.find s in
+ if Cil_datatype.Typ.Set.is_empty exns then SkipChildren
+ else begin
+ b.b_post_cond <- List.map self#guard_post_cond b.b_post_cond;
+ ChangeTo b
+ end
+
+ method private clean_catch_clause (bind,b as handler) acc =
+ let remove_local v =
+ let f =
+ Visitor_behavior.Get.fundec self#behavior (Extlib.the self#current_func)
in
- let stmts, uncaught =
- Cil_datatype.Typ.Set.fold make_jump exns ([],false)
+ let v = Visitor_behavior.Get.varinfo self#behavior v in
+ f.slocals <- List.filter (fun v' -> v!=v') f.slocals;
+ in
+ match bind with
+ | Catch_all -> handler :: acc
+ | Catch_exn (v, []) ->
+ if self#is_thrown (purify v.vtype) then handler :: acc
+ else begin remove_local v; acc end
+ | Catch_exn (v, l) ->
+ let caught, remove =
+ List.partition (fun (v,_) -> self#is_thrown (purify v.vtype)) l
in
- let stmts =
- if uncaught then begin
- let default =
+ List.iter (fun (v,_) -> remove_local v) remove;
+ if caught = [] then begin remove_local v; acc end
+ else (Catch_exn (v,caught), b) :: acc
+
+ method! vstmt_aux s =
+ let generate_jumps instr exns loc =
+ if Cil_datatype.Typ.Set.is_empty exns then SkipChildren
+ else begin
+ self#modify_current ();
+ let make_jump t (stmts, uncaught) =
+ let t = purify t in
+ if Cil_datatype.Typ.Hashtbl.mem exn_labels t then begin
+ let e = self#exn_kind t in
+ let e = Cil.new_exp ~loc (Const (CEnum e)) in
+ let b = self#jumps_to_handler loc t in
+ let s = Cil.mkStmt (Block (Cil.mkBlock b)) in
+ s.labels <- [Case (e,loc)];
+ s::stmts, uncaught
+ end else stmts, true
+ in
+ let stmts, uncaught =
+ Cil_datatype.Typ.Set.fold make_jump exns ([],false)
+ in
+ let stmts =
+ if uncaught then begin
+ let default =
Cil.mkStmt (
Block (Cil.mkBlock (self#jumps_to_default_handler loc)))
- in
- default.labels <- [Default loc];
- List.rev_append stmts [default]
- end else List.rev stmts
- in
- let test = self#test_uncaught_flag loc true in
- let cases = Cil.new_exp ~loc (Lval self#exn_kind_field) in
- let switch = Cil.mkStmt (Switch(cases,Cil.mkBlock stmts,stmts,loc)) in
- let handler =
- Cil.mkStmt (If(test,Cil.mkBlock [switch],Cil.mkBlock [],loc))
- in
- let instr =
- Visitor.visitFramacInstr (self:>Visitor.frama_c_visitor) instr
- in
- let call = Cil.mkStmtOneInstr (List.hd instr) in
- s.skind <- Block (Cil.mkBlockNonScoping [call;handler]);
- SkipChildren
- end
- in
- match s.skind with
+ in
+ default.labels <- [Default loc];
+ List.rev_append stmts [default]
+ end else List.rev stmts
+ in
+ let test = self#test_uncaught_flag loc true in
+ let cases = Cil.new_exp ~loc (Lval self#exn_kind_field) in
+ let switch = Cil.mkStmt (Switch(cases,Cil.mkBlock stmts,stmts,loc)) in
+ let handler =
+ Cil.mkStmt (If(test,Cil.mkBlock [switch],Cil.mkBlock [],loc))
+ in
+ let instr =
+ Visitor.visitFramacInstr (self:>Visitor.frama_c_visitor) instr
+ in
+ let call = Cil.mkStmtOneInstr (List.hd instr) in
+ s.skind <- Block (Cil.mkBlockNonScoping [call;handler]);
+ SkipChildren
+ end
+ in
+ match s.skind with
| Instr (Call (_,f,_,loc) as instr) ->
generate_jumps instr (find_exns f) loc
| Instr (Local_init(_, ConsInit(f,_,_), loc) as instr) ->
@@ -795,7 +795,7 @@ object(self)
than the current block. As we are adding statements in the
auxiliary blocks, we need to do that before adding labels to the
entry points of these blocks.
- *)
+ *)
let stmts = List.map (self#visit_catch_clause loc) c in
let suf =
if label_counter = 0 then "" else "_" ^ (string_of_int label_counter)
@@ -812,10 +812,10 @@ object(self)
stmt.labels <- [Label (label,v.vdecl,false)];
b.bstmts <- stmt :: b.bstmts;
(match aux with
- | [] ->
- Cil_datatype.Typ.Hashtbl.add exn_labels (purify v.vtype) stmt
- | _ :: _ ->
- List.iter (self#aux_handler_goto stmt) aux)
+ | [] ->
+ Cil_datatype.Typ.Hashtbl.add exn_labels (purify v.vtype) stmt
+ | _ :: _ ->
+ List.iter (self#aux_handler_goto stmt) aux)
| (Catch_all, b) ->
let loc =
match b.bstmts with [] -> loc | s::_ -> Cil_datatype.Stmt.loc s
@@ -837,7 +837,7 @@ object(self)
| Catch_exn(_,l), _ ->
List.iter
(fun (v,_) ->
- Cil_datatype.Typ.Hashtbl.remove exn_labels (purify v.vtype))
+ Cil_datatype.Typ.Hashtbl.remove exn_labels (purify v.vtype))
l
| Catch_all,_ -> ignore (Stack.pop catch_all_label))
c; (* we remove bindings in the reverse order as we added them,
@@ -846,8 +846,8 @@ object(self)
s.skind <- Block t;
SkipChildren
| _ -> DoChildren
-
-end
+
+ end
let prepare_file f =
if Kernel.SimplifyCfg.get () then begin
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 9152b5e455fd39d1c64ef5e1836b8beb0872b28a..7f6f2802239ca20044ef97d8dbd18fd2146d74a1 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -290,85 +290,64 @@ module Behavior_set_map = Transitioning.Stdlib.Map.Make(Datatype.String.Set)
let is_same_behavior_set l1 l2 =
Datatype.String.Set.(equal (of_list l1) (of_list l2))
-let merge_stmt_contracts_emitters contracts =
- let add_one acc (c,e) =
- match c.annot_content with
- | AStmtSpec(bhvs, spec) ->
- let bhvs = Datatype.String.Set.of_list bhvs in
- (match Behavior_set_map.find_opt bhvs acc with
- | Some (spec', e') ->
- merge_funspec spec' spec;
- if Emitter.equal e e' then acc
- else
- Behavior_set_map.add bhvs (spec', Emitter.kernel) acc
- | None ->
- let spec' = Cil.empty_funspec () in
- merge_funspec spec' spec;
- Behavior_set_map.add bhvs (spec',e) acc
- (* avoid sharing directly the spec,
- as merge_funspec will modify it in place*))
- | _ -> acc
- in
- let merged_contracts =
- List.fold_left add_one Behavior_set_map.empty contracts
- in
- Behavior_set_map.fold
- (fun bhvs (spec,e) acc ->
- (Logic_const.new_code_annotation
- (AStmtSpec (Datatype.String.Set.elements bhvs, spec)),e)
- :: acc)
- merged_contracts []
-
-let merge_loop_assigns_emitters annots =
- let merge_assigns bhvs (a,e) acc =
+let merge_annots_emitters extract merge make annots =
+ let merge_same_bhvs bhvs (ca,a,e) acc =
let elt =
match Behavior_set_map.find_opt bhvs acc with
- | Some (a',e') ->
- let a' = merge_assigns ~keep_empty:false a a' in
+ | Some (ca', a',e') ->
+ let a' = merge a a' in
let e' = if Emitter.equal e e' then e else Emitter.kernel in
- a', e'
- | None -> a,e
+ let ca' =
+ if Cil_datatype.Code_annotation.compare ca' ca < 0 then ca' else ca
+ in
+ let annot_content = make (Datatype.String.Set.elements bhvs) a' in
+ let ca' = { ca' with annot_content } in
+ ca', a', e'
+ | None -> ca,a,e
in
Behavior_set_map.add bhvs elt acc
in
let treat_code_annot acc (ca,e) =
- match ca.annot_content with
- | AAssigns(bhvs,a) ->
- merge_assigns (Datatype.String.Set.of_list bhvs) (a,e) acc
- | _ -> acc
+ match extract ca with
+ | Some(bhvs,a) ->
+ merge_same_bhvs (Datatype.String.Set.of_list bhvs) (ca,a,e) acc
+ | None -> acc
in
let bhvs = List.fold_left treat_code_annot Behavior_set_map.empty annots in
- Behavior_set_map.fold
- (fun bhvs (a,e) acc ->
- (Logic_const.new_code_annotation
- (AAssigns (Datatype.String.Set.elements bhvs, a)),e)
- :: acc)
- bhvs []
-
-let merge_loop_allocation annots =
- let merge_allocates bhvs (a,e) acc =
- let elt =
- match Behavior_set_map.find_opt bhvs acc with
- | Some (a', e') ->
- let a' = merge_allocation ~keep_empty:false a a' in
- let e' = if Emitter.equal e e' then e else Emitter.kernel in
- a', e'
- | None -> a,e
- in Behavior_set_map.add bhvs elt acc
+ Behavior_set_map.fold (fun _ (ca,_,e) acc -> (ca,e) :: acc) bhvs []
+
+let merge_stmt_contracts_emitters =
+ let extract ca =
+ match ca.annot_content with
+ | AStmtSpec(bhvs, spec) -> Some (bhvs,spec)
+ | _ -> None
in
- let treat_code_annot acc (ca, e) =
+ let merge s s' =
+ let e = Cil.empty_funspec() in
+ merge_funspec e s;
+ merge_funspec e s';
+ e
+ in
+ let make bhvs s = AStmtSpec(bhvs,s) in
+ merge_annots_emitters extract merge make
+
+let merge_loop_assigns_emitter =
+ let extract ca =
match ca.annot_content with
- | AAllocation(bhvs,a) ->
- merge_allocates (Datatype.String.Set.of_list bhvs) (a,e) acc
- | _ -> acc
+ | AAssigns(bhvs,a) -> Some(bhvs,a)
+ | _ -> None
in
- let bhvs = List.fold_left treat_code_annot Behavior_set_map.empty annots in
- Behavior_set_map.fold
- (fun bhvs (a,e) acc ->
- (Logic_const.new_code_annotation
- (AAllocation (Datatype.String.Set.elements bhvs, a)),e)
- ::acc)
- bhvs []
+ let merge a a' = merge_assigns ~keep_empty:false a a' in
+ let make bhvs a = AAssigns(bhvs,a) in
+ merge_annots_emitters extract merge make
+
+let merge_loop_allocation_emitter =
+ let extract ca =
+ match ca.annot_content with AAllocation(bhvs,a) -> Some (bhvs,a) | _ -> None
+ in
+ let merge a a' = merge_allocation ~keep_empty:false a a' in
+ let make bhvs a = AAllocation(bhvs,a) in
+ merge_annots_emitters extract merge make
let partition_code_annot_emitter l =
let add_one_ca (contracts, assigns, alloc, others) (ca,_ as v) =
@@ -410,8 +389,8 @@ let code_annot_emitter ?filter stmt =
in
let contracts,assigns,allocation,others = partition_code_annot_emitter l in
merge_stmt_contracts_emitters contracts @
- merge_loop_assigns_emitters assigns @
- merge_loop_allocation allocation @
+ merge_loop_assigns_emitter assigns @
+ merge_loop_allocation_emitter allocation @
others
with Not_found ->
[]
@@ -541,25 +520,12 @@ let model_fields ?emitter t =
(**************************************************************************)
let iter_code_annot f stmt =
- try
- let tbl = Code_annots.find stmt in
- Emitter.Usable_emitter.Hashtbl.iter
- (fun e l -> List.iter (f (Emitter.Usable_emitter.get e)) !l)
- tbl
- with Not_found ->
- ()
+ let l = code_annot_emitter stmt in
+ List.iter (fun (a,e) -> f e a) l
let fold_code_annot f stmt acc =
- try
- let tbl = Code_annots.find stmt in
- Emitter.Usable_emitter.Hashtbl.fold
- (fun e l acc ->
- let e = Emitter.Usable_emitter.get e in
- List.fold_left (fun acc x -> f e x acc) acc !l)
- tbl
- acc
- with Not_found ->
- acc
+ let l = code_annot_emitter stmt in
+ List.fold_left (fun acc (a,e) -> f e a acc) acc l
let iter_all_code_annot ?(sorted=true) f =
let cmp s1 s2 =
@@ -1071,6 +1037,25 @@ let add_ensures e kf ?stmt ?active ?behavior l =
in
extend_behavior e kf ?stmt ?active ?behavior set_bhv
+let get_full_spec kf ?stmt ?(behavior=[]) () =
+ match stmt with
+ | None ->
+ (try funspec ~populate:false kf with Not_found -> Cil.empty_funspec())
+ | Some stmt ->
+ let filter a =
+ match a.annot_content with
+ | AStmtSpec(bhvs,_) when is_same_behavior_set bhvs behavior -> true
+ | _ -> false
+ in
+ (match code_annot ~filter stmt with
+ | [] -> Cil.empty_funspec ()
+ | [ { annot_content = AStmtSpec(_,s)} ] -> s
+ | _ -> Kernel.fatal "More than one contract associated to a statement")
+
+let get_spec_behavior s = function
+ | None -> Cil.find_default_behavior s
+ | Some name -> List.find_opt (fun { b_name } -> b_name = name) s.spec_behavior
+
let add_assigns ~keep_empty e kf ?stmt ?active ?behavior a =
let set_bhv full_bhv e_bhv =
let keep_empty = keep_empty && full_bhv.b_assigns = WritesAny in
@@ -1093,7 +1078,15 @@ let add_assigns ~keep_empty e kf ?stmt ?active ?behavior a =
(Property.ip_from_of_behavior kf ki active full_bhv);
)
in
- extend_behavior e kf ?stmt ?active ?behavior set_bhv
+ let old_spec = get_full_spec kf ?stmt ?behavior:active () in
+ let bhv = get_spec_behavior old_spec behavior in
+ let is_empty =
+ match bhv with
+ | None -> true
+ | Some b -> b.b_assigns = WritesAny
+ in
+ if not (keep_empty && is_empty) then
+ extend_behavior e kf ?stmt ?active ?behavior set_bhv
let add_allocates ~keep_empty e kf ?stmt ?active ?behavior a =
let ki = kinstr stmt in
@@ -1109,7 +1102,15 @@ let add_allocates ~keep_empty e kf ?stmt ?active ?behavior a =
Extlib.may Property_status.register
(Property.ip_allocation_of_behavior kf ki active full_bhv);
in
- extend_behavior e kf ?stmt ?active ?behavior set_bhv
+ let old_spec = get_full_spec kf ?stmt ?behavior:active () in
+ let bhv = get_spec_behavior old_spec behavior in
+ let is_empty =
+ match bhv with
+ | None -> true
+ | Some b -> b.b_allocation = FreeAllocAny
+ in
+ if not (keep_empty && is_empty) then
+ extend_behavior e kf ?stmt ?active ?behavior set_bhv
let add_extended e kf ?stmt ?active ?behavior ext =
let set_bhv _ e_bhv =
@@ -1121,212 +1122,165 @@ let add_extended e kf ?stmt ?active ?behavior ext =
(** {3 Adding code annotations} *)
-let add_code_annot emitter ?kf stmt ca =
+let add_code_annot ?(keep_empty=true) emitter ?kf stmt ca =
(* Kernel.feedback "%a: adding code annot %a with stmt %a (%d)"
Project.pretty (Project.current ())
Code_annotation.pretty ca
Stmt.pretty stmt
stmt.sid;*)
let kf = find_englobing_kf ?kf stmt in
- let convert a =
- match a.annot_content with
- | AAssert(l, kind, p) ->
- let a = { a with annot_content=AAssert(l,kind,extend_name emitter p) } in
- a, Property.ip_of_code_annot kf stmt a
- | AInvariant(l, b, p) ->
- let a={a with annot_content=AInvariant(l,b,extend_name emitter p)} in
- a, Property.ip_of_code_annot kf stmt a
- | AStmtSpec (bhvs, spec) ->
- let filter ca =
- match ca.annot_content with
- | AStmtSpec(bhvs',_) -> is_same_behavior_set bhvs bhvs'
- | _ -> false
- in
- let contract = code_annot ~filter stmt in
- (match contract with
- | [] -> a, Property.ip_of_code_annot kf stmt a
- | [ { annot_content = AStmtSpec _ } ] ->
- let register_children = true in
- let active = bhvs in
- add_behaviors
- ~register_children emitter kf ~stmt ~active spec.spec_behavior;
- if spec.spec_variant <> None then
- Kernel.fatal
- "statement contract cannot have a decrease clause";
- Extlib.may
- (add_terminates emitter kf ~stmt ~active) spec.spec_terminates;
- List.iter
- (add_complete emitter kf ~stmt ~active)
- spec.spec_complete_behaviors;
- List.iter
- (add_disjoint emitter kf ~stmt ~active)
- spec.spec_disjoint_behaviors;
- (* By construction, we have exactly one contract
- corresponding to our criterion and emitter. *)
- let ca = List.hd (code_annot ~emitter ~filter stmt) in
- (* remove the previous binding in order to replace it
- with the updated one. Statuses being attached to sub-elements
- of the contract, they do not need any update here.
- *)
- remove_code_annot_internal emitter ~remove_statuses:false ~kf stmt ca;
- { a with annot_content = ca.annot_content }, []
- | _ ->
- Kernel.fatal
- "more than one contract attached to a given statement for \
- emitter %a. Invariant of annotations management broken."
- Emitter.pretty emitter)
- | AVariant _ ->
- let v = code_annot ~filter:Logic_utils.is_variant stmt in
- (match v with
- | [] -> a, Property.ip_of_code_annot kf stmt a
- | _ ->
- let source = fst (Cil_datatype.Stmt.loc stmt) in
- Kernel.fatal ~source
- "trying to register a second variant for statement %a"
- Stmt.pretty stmt)
- | AAssigns (bhvs, assigns) ->
- let filter ca =
- match ca.annot_content with
- | AAssigns (bhvs', _) -> is_same_behavior_set bhvs bhvs'
- | _ -> false
- in
- let assigns' = code_annot ~filter stmt in
- (match assigns' with
- | [] -> a, Property.ip_of_code_annot kf stmt a
- | l ->
- let merge_assigns_ca acc ca =
- match ca.annot_content with
- | AAssigns(_,assigns') ->
- merge_assigns ~keep_empty:false assigns' acc
- | _ -> acc
- in
- let assigns' = List.fold_left merge_assigns_ca WritesAny l in
- let merged_ca = { a with annot_content = AAssigns(bhvs,assigns') }
- in
- let ip =
- Property.(
- ip_of_assigns
- kf (Kstmt stmt) (Id_loop merged_ca) assigns')
- in
- Extlib.may Property_status.remove ip;
- (match assigns' with
- | WritesAny -> ()
- | Writes l ->
- List.iter
- (fun from ->
- let ip =
- Property.(
- ip_of_from kf (Kstmt stmt)
- (Id_loop merged_ca) from)
- in
- Extlib.may Property_status.remove ip)
- l);
- let new_assigns =
- merge_assigns ~keep_empty:false assigns' assigns
- in
- let new_ca = { a with annot_content = AAssigns(bhvs,new_assigns) }
- in
- let ips =
- Extlib.list_of_opt
- Property.(
- ip_of_assigns
- kf (Kstmt stmt) (Id_loop new_ca) new_assigns)
- in
- let ips =
- match new_assigns with
- | WritesAny -> ips
- | Writes l ->
- List.fold_left
- (fun acc f ->
- Extlib.opt_fold
- (fun x y -> x::y)
- Property.(
- ip_of_from kf (Kstmt stmt)
- (Id_loop new_ca) f)
- acc)
- ips l
- in
- let ca' = code_annot ~filter stmt in
- let new_a =
- match ca' with
- | [] -> a
- | [ { annot_content = AAssigns(_, assigns') } as ca ] ->
- remove_code_annot_internal emitter ~kf stmt ca;
- let merged =
- merge_assigns ~keep_empty:false assigns' assigns
- in
- { a with annot_content = AAssigns (bhvs, merged) }
- | _ ->
- Kernel.fatal
- "More than one loop assigns clause for a statement. \
- Annotations internal state broken."
- in
- new_a, ips)
- | AAllocation (bhvs, alloc) ->
- let filter ca =
- match ca.annot_content with
- | AAllocation(bhvs',_) -> is_same_behavior_set bhvs bhvs'
- | _ -> false
- in
- (match code_annot ~filter stmt with
- | [] -> a, Property.ip_of_code_annot kf stmt a
- | l ->
- let merge_alloc_ca acc alloc =
- match alloc.annot_content with
- | AAllocation(_,a) -> merge_allocation ~keep_empty:false acc a
- | _ -> acc
- in
- let alloc' = List.fold_left merge_alloc_ca FreeAllocAny l in
- let merged_a =
- { a with annot_content = AAllocation(bhvs,alloc') }
- in
- let ip =
- Property.(
- ip_of_allocation kf (Kstmt stmt)
- (Id_loop merged_a) alloc')
- in
- Extlib.may Property_status.remove ip;
- let new_alloc = merge_allocation ~keep_empty:false alloc' alloc in
- let new_a =
- { a with annot_content = AAllocation(bhvs,new_alloc) }
- in
- let ip =
- Property.(
- ip_of_allocation
- kf (Kstmt stmt) (Id_loop new_a) new_alloc)
- in
- let emit_a =
- match code_annot ~emitter ~filter stmt with
- | [] -> a
- | [ { annot_content = AAllocation(_,alloc') } as ca ] ->
- remove_code_annot_internal emitter ~kf stmt ca;
- { a with annot_content =
- AAllocation(
- bhvs,
- merge_allocation ~keep_empty:false alloc' alloc) }
- | _ ->
- Kernel.fatal
- "More than one allocation clause for a statement. \
- Annotations internal state broken"
- in
- emit_a, Extlib.list_of_opt ip)
- | APragma _ | AExtended _ -> a, Property.ip_of_code_annot kf stmt a
- in
- let ca, ppts = convert ca in
- let e = Emitter.get emitter in
- List.iter Property_status.register ppts;
- let add_emitter tbl = Emitter.Usable_emitter.Hashtbl.add tbl e (ref [ ca ]) in
- try
- let tbl = Code_annots.find stmt in
+ let fill_tables ca ppts =
+ let e = Emitter.get emitter in
+ List.iter Property_status.register ppts;
+ let add_emitter tbl =
+ Emitter.Usable_emitter.Hashtbl.add tbl e (ref [ ca ]) in
try
- let l = Emitter.Usable_emitter.Hashtbl.find tbl e in
- l := ca :: !l;
+ let tbl = Code_annots.find stmt in
+ try
+ let l = Emitter.Usable_emitter.Hashtbl.find tbl e in
+ l := ca :: !l;
+ with Not_found ->
+ add_emitter tbl
with Not_found ->
- add_emitter tbl
- with Not_found ->
- let tbl = Emitter.Usable_emitter.Hashtbl.create 7 in
- add_emitter tbl;
- Code_annots.add stmt tbl
+ let tbl = Emitter.Usable_emitter.Hashtbl.create 7 in
+ add_emitter tbl;
+ Code_annots.add stmt tbl
+ in
+ match ca.annot_content with
+ | AAssert(l, kind, p) ->
+ let a = { ca with annot_content=AAssert(l,kind,extend_name emitter p) } in
+ fill_tables a (Property.ip_of_code_annot kf stmt a)
+ | AInvariant(l, b, p) ->
+ let a={ca with annot_content=AInvariant(l,b,extend_name emitter p)} in
+ fill_tables a (Property.ip_of_code_annot kf stmt a)
+ | AStmtSpec (bhvs, spec) ->
+ let filter ca =
+ match ca.annot_content with
+ | AStmtSpec(bhvs',_) -> is_same_behavior_set bhvs bhvs'
+ | _ -> false
+ in
+ let contract = code_annot ~filter stmt in
+ (match contract with
+ | [] ->
+ if not (keep_empty && Logic_utils.funspec_has_only_assigns spec) then
+ fill_tables ca (Property.ip_of_code_annot kf stmt ca)
+ | [ { annot_content = AStmtSpec _ } ] ->
+ let register_children = true in
+ let active = bhvs in
+ add_behaviors
+ ~register_children emitter kf ~stmt ~active spec.spec_behavior;
+ if spec.spec_variant <> None then
+ Kernel.fatal
+ "statement contract cannot have a decrease clause";
+ Extlib.may
+ (add_terminates emitter kf ~stmt ~active) spec.spec_terminates;
+ List.iter
+ (add_complete emitter kf ~stmt ~active)
+ spec.spec_complete_behaviors;
+ List.iter
+ (add_disjoint emitter kf ~stmt ~active)
+ spec.spec_disjoint_behaviors;
+ (* By construction, we have exactly one contract
+ corresponding to our criterion and emitter. *)
+ let ca' = List.hd (code_annot ~emitter ~filter stmt) in
+ (* remove the previous binding in order to replace it
+ with the updated one. Statuses being attached to sub-elements
+ of the contract, they do not need any update here.
+ *)
+ remove_code_annot_internal emitter ~remove_statuses:false ~kf stmt ca';
+ fill_tables ca' []
+ | _ ->
+ Kernel.fatal
+ "more than one contract attached to a given statement for \
+ emitter %a. Invariant of annotations management broken."
+ Emitter.pretty emitter)
+ | AVariant _ ->
+ let v = code_annot ~filter:Logic_utils.is_variant stmt in
+ (match v with
+ | [] -> fill_tables ca (Property.ip_of_code_annot kf stmt ca)
+ | _ ->
+ let source = fst (Cil_datatype.Stmt.loc stmt) in
+ Kernel.fatal ~source
+ "trying to register a second variant for statement %a"
+ Stmt.pretty stmt)
+ | AAssigns (bhvs, assigns) ->
+ let filter_ca ca =
+ match ca.annot_content with
+ | AAssigns (bhvs', _) -> is_same_behavior_set bhvs bhvs'
+ | _ -> false
+ in
+ let filter e ca = Emitter.equal e emitter && filter_ca ca in
+ let ca_e = code_annot_emitter ~filter stmt in
+ let ca_total = code_annot ~filter:filter_ca stmt in
+ (match ca_total with
+ | [] when keep_empty -> ()
+ | [] -> fill_tables ca (Property.ip_of_code_annot kf stmt ca)
+ | [{ annot_content = AAssigns(_,assigns_total)}] ->
+ let assigns_e =
+ match ca_e with
+ | [] -> WritesAny
+ | [ { annot_content = AAssigns(_, assigns') } as ca,_ ] ->
+ remove_code_annot_internal emitter ~kf stmt ca;
+ assigns'
+ | _ ->
+ Kernel.fatal
+ "More than one loop assigns clause for a statement. \
+ Annotations internal state broken."
+ in
+ (* we have assigns at statement level, just not from this
+ emitter yet, hence merge at emitter level regardless of keep_empty *)
+ let merged_e = merge_assigns ~keep_empty:false assigns_e assigns in
+ let new_a = { ca with annot_content = AAssigns(bhvs,merged_e) } in
+ let merged_total = merge_assigns ~keep_empty assigns_total assigns in
+ let ips =
+ Property.ip_of_code_annot kf stmt
+ { ca with annot_content = AAssigns(bhvs,merged_total) }
+ in
+ fill_tables new_a ips
+ | _ ->
+ Kernel.fatal
+ "More than one loop assigns clause for a statement. \
+ Annotations internal state broken.")
+ | AAllocation (bhvs, alloc) ->
+ let filter_ca ca =
+ match ca.annot_content with
+ | AAllocation(bhvs',_) -> is_same_behavior_set bhvs bhvs'
+ | _ -> false
+ in
+ let filter e ca = Emitter.equal e emitter && filter_ca ca in
+ let ca_e = code_annot_emitter ~filter stmt in
+ let ca_total = code_annot ~filter:filter_ca stmt in
+ (match ca_total with
+ | [] when keep_empty -> ()
+ | [] -> fill_tables ca (Property.ip_of_code_annot kf stmt ca)
+ | [{ annot_content = AAllocation(_,alloc_total)}] ->
+ let alloc_e =
+ match ca_e with
+ | [] -> FreeAllocAny
+ | [ { annot_content = AAllocation(_, alloc') } as ca,_ ] ->
+ remove_code_annot_internal emitter ~kf stmt ca;
+ alloc'
+ | _ ->
+ Kernel.fatal
+ "More than one loop assigns clause for a statement. \
+ Annotations internal state broken."
+ in
+ (* we have assigns at statement level, just not from this
+ emitter yet, hence merge at emitter level regardless of keep_empty *)
+ let merged_e = merge_allocation ~keep_empty:false alloc_e alloc in
+ let new_a = { ca with annot_content = AAllocation(bhvs,merged_e) } in
+ let merged_total = merge_allocation ~keep_empty alloc_total alloc in
+ let ips =
+ Property.ip_of_code_annot kf stmt
+ { ca with annot_content = AAllocation(bhvs,merged_total) }
+ in
+ fill_tables new_a ips
+ | _ ->
+ Kernel.fatal
+ "More than one loop assigns clause for a statement. \
+ Annotations internal state broken.")
+ | APragma _ | AExtended _ ->
+ fill_tables ca (Property.ip_of_code_annot kf stmt ca)
let add_assert e ?kf stmt a =
let a = Logic_const.new_code_annotation (AAssert ([],Assert,a)) in
diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli
index 1b65f10d2efddf9672f05edb67d95f407c459c3c..4bc65d57621c0a9b55781d84375b210e71206629 100644
--- a/src/kernel_services/ast_data/annotations.mli
+++ b/src/kernel_services/ast_data/annotations.mli
@@ -261,6 +261,7 @@ val fold_decreases:
(**************************************************************************)
val add_code_annot:
+ ?keep_empty:bool ->
Emitter.t -> ?kf:kernel_function -> stmt -> code_annotation -> unit
(** Add a new code annotation attached to the given statement. If [kf] is
provided, the function runs faster.
@@ -270,9 +271,16 @@ val add_code_annot:
Trying to associate more than one will result in a merge of the contracts.
The same things happens with loop assigns and allocates/frees.
+ The [keep_empty] argument is only used for loop assigns
+ and loop allocates, where it is used to decide whether to add the given
+ code annot in case the corresponding category was empty. It defaults to
+ [true], which is sound wrt ACSL semantics of equating an absence of
+ annotation with assigns/allocates \everything.
There can be at most one loop variant registered per statement.
Attempting to register a second one will result in a fatal error.
+
+ @modify Frama-C+dev: add keep_empty argument
*)
val add_assert:
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 676c7dbcf56e4c289c1ed465dc7d0b46cebce977..6deba7d75d1e529660d1516ff905088ba8af6f8d 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -533,11 +533,31 @@ let parse_cabs = function
let cpp_command = build_cpp_cmd cmdl supp_args (f:>string) (ppf:>string) in
if Sys.command cpp_command <> 0 then begin
safe_remove_file ppf;
+ let possible_cause =
+ if Kernel.JsonCompilationDatabase.is_set () then
+ if not (Json_compilation_database.has_entry f) then
+ Format.asprintf "note: %s is set but \
+ contains no entries for '%a'.@ "
+ Kernel.JsonCompilationDatabase.option_name
+ Datatype.Filepath.pretty f
+ else ""
+ else
+ if not (Kernel.CppExtraArgs.is_set ()) &&
+ not (Kernel.CppExtraArgsPerFile.is_set ()) &&
+ not (Kernel.CppCommand.is_set ()) then
+ Format.asprintf
+ "this is possibly due to missing preprocessor flags;@ \
+ consider options %s, %s or %s.@ "
+ Kernel.CppExtraArgs.option_name
+ Kernel.JsonCompilationDatabase.option_name
+ Kernel.CppCommand.option_name
+ else ""
+ in
Kernel.abort
"failed to run: %s@\n\
- you may set the CPP environment variable to select the proper \
- preprocessor command or use the option \"-cpp-command\"."
- cpp_command
+ %sSee chapter \"Preparing the Sources\" in the Frama-C user manual \
+ for more details."
+ cpp_command possible_cause
end;
let ppf =
if Kernel.ReadAnnot.get() &&
@@ -701,7 +721,7 @@ let emit_all_statuses _ =
let () = Ast.apply_after_computed emit_all_statuses
let add_annotation kf st a =
- Annotations.add_code_annot Emitter.end_user ~kf st a;
+ Annotations.add_code_annot ~keep_empty:false Emitter.end_user ~kf st a;
(* Now check if the annotation is valid by construction
(provided normalization is correct). *)
match a.annot_content with
@@ -741,7 +761,7 @@ let synchronize_source_annot has_new_stmt kf =
st_ann.skind <- (Block (Cil.mkBlockNonScoping [st]));
has_new_stmt := true;
Annotations.add_code_annot
- Emitter.end_user ~kf st_ann annot;
+ ~keep_empty:false Emitter.end_user ~kf st_ann annot;
(true, st_ann)
end else begin
add_annotation kf st annot;
diff --git a/src/kernel_services/ast_queries/json_compilation_database.ml b/src/kernel_services/ast_queries/json_compilation_database.ml
index 091216de519479409665cb4a4cb5bf1f27a94a8d..5e0124ac2b1d59fb49d71896598f905243a8cec7 100644
--- a/src/kernel_services/ast_queries/json_compilation_database.ml
+++ b/src/kernel_services/ast_queries/json_compilation_database.ml
@@ -239,32 +239,33 @@ let parse_entry jcdb_dir r =
| Not_found ->
Flags.add path flags
+let compute_flags_from_file () =
+ let database = Kernel.JsonCompilationDatabase.get () in
+ let jcdb_dir, jcdb_path =
+ if Sys.is_directory database then
+ database, Filename.concat database "compile_commands.json"
+ else Filename.dirname database, database
+ in
+ Kernel.feedback ~dkey:Kernel.dkey_compilation_db
+ "using compilation database: %s" jcdb_path;
+ begin
+ try
+ let r_list =
+ Yojson.Basic.from_file jcdb_path |> Yojson.Basic.Util.to_list
+ in
+ List.iter (parse_entry jcdb_dir) r_list;
+ with
+ | Sys_error msg
+ | Yojson.Json_error msg
+ | Yojson.Basic.Util.Type_error (msg, _) ->
+ Kernel.abort "could not parse compilation database: %s@ %s"
+ database msg
+ end;
+ Flags.mark_as_computed ()
+
let get_flags f =
if Kernel.JsonCompilationDatabase.get () <> "" then begin
- if not (Flags.is_computed ()) then begin
- let database = Kernel.JsonCompilationDatabase.get () in
- let jcdb_dir, jcdb_path =
- if Sys.is_directory database then
- database, Filename.concat database "compile_commands.json"
- else Filename.dirname database, database
- in
- Kernel.feedback ~dkey:Kernel.dkey_compilation_db
- "using compilation database: %s" jcdb_path;
- begin
- try
- let r_list =
- Yojson.Basic.from_file jcdb_path |> Yojson.Basic.Util.to_list
- in
- List.iter (parse_entry jcdb_dir) r_list;
- with
- | Sys_error msg
- | Yojson.Json_error msg
- | Yojson.Basic.Util.Type_error (msg, _) ->
- Kernel.abort "could not parse compilation database: %s@ %s"
- database msg
- end;
- Flags.mark_as_computed ()
- end;
+ if not (Flags.is_computed ()) then compute_flags_from_file ();
try
let flags = Flags.find f in
Kernel.feedback ~dkey:Kernel.dkey_compilation_db
@@ -276,3 +277,7 @@ let get_flags f =
[]
end
else []
+
+let has_entry f =
+ if not (Flags.is_computed ()) then compute_flags_from_file ();
+ Flags.mem f
diff --git a/src/kernel_services/ast_queries/json_compilation_database.mli b/src/kernel_services/ast_queries/json_compilation_database.mli
index 9e3101b1d8a2ead1ee26330ee039c88749c0dbee..5b9f18f1b087c5dc1b185eb10404de4584f0f49d 100644
--- a/src/kernel_services/ast_queries/json_compilation_database.mli
+++ b/src/kernel_services/ast_queries/json_compilation_database.mli
@@ -24,3 +24,9 @@
in the JSON compilation database (when enabled), or the empty string
otherwise. If not empty, the flags always start with a space. *)
val get_flags : Datatype.Filepath.t -> string list
+
+(** [has_entry f] returns true iff [f] has an entry in the JSON compilation
+ database. Must only be called if a JCDB file has been specified.
+ @since Frama-C+dev
+*)
+val has_entry : Datatype.Filepath.t -> bool
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 242feb6c6a054e09f4016d0168be57a3e4a9c38f..bf0b1e828dbf5c66679c255ebaf1c2e306b066c2 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -676,6 +676,18 @@ let rec add_attribute_glob_annot a g =
| Dcustom_annot(c,n,al,l) -> Dcustom_annot(c,n,Cil.addAttribute a al, l)
| Dextended (e,al,l) -> Dextended(e,Cil.addAttribute a al,l)
+let behavior_has_only_assigns bhvs =
+ bhvs.b_requires = [] && bhvs.b_assumes = [] &&
+ bhvs.b_post_cond = [] && bhvs.b_allocation = FreeAllocAny &&
+ bhvs.b_extended = []
+
+let funspec_has_only_assigns spec =
+ List.for_all behavior_has_only_assigns spec.spec_behavior &&
+ spec.spec_variant = None &&
+ spec.spec_terminates = None &&
+ spec.spec_complete_behaviors = [] &&
+ spec.spec_disjoint_behaviors = []
+
let is_same_list f l1 l2 =
try List.for_all2 f l1 l2 with Invalid_argument _ -> false
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 1394e8408fbb3f58bf5200c5413f5dd934ca236c..b1e4074364ff4216e5558b9c7b449678405f7df5 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -312,6 +312,18 @@ val is_annot_next_stmt: code_annotation -> bool
val add_attribute_glob_annot:
attribute -> global_annotation -> global_annotation
+(** {2 Contracts } *)
+
+(** [true] if the behavior has only an assigns clause.
+ @since Frama-C+dev
+*)
+val behavior_has_only_assigns: behavior -> bool
+
+(** [true] if the only non-empty fields of the contract are assigns clauses
+ @since Frama-C+dev
+*)
+val funspec_has_only_assigns: funspec -> bool
+
(** {2 Structural equality between annotations} *)
val is_same_list: ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml
index 36adae8427fe37790298e9a576b3e4847eaba0a6..b50798b0e70b5fa79be73f4ff36a9cd19e35fbc3 100644
--- a/src/kernel_services/ast_transformations/inline.ml
+++ b/src/kernel_services/ast_transformations/inline.ml
@@ -123,7 +123,7 @@ let inline_call loc caller callee return args =
fd.sbody.bstmts <- inits @ fd.sbody.bstmts;
end else begin
(* put a statement contract on top of the function's body,
- but only after we have assigned the formals. Not that there
+ but only after we have assigned the formals. Note that there
is no need to rename behaviors: they will only shadow behaviors
of the caller within callee's body, just as we need.
*)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 47c5174627a24ad9e96c2092ceaea97ea0840caf..0d5cfc8f14bd3213c0d186142b7ed97f41605dd9 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -592,6 +592,7 @@ module Time =
end)
let () = Parameter_customize.set_group messages
+let () = Parameter_customize.do_not_projectify ()
module SymbolicPath =
String_set (* TODO: to be replaced by an hashtbl *)
(struct
diff --git a/src/kernel_services/visitors/visitor.ml b/src/kernel_services/visitors/visitor.ml
index ce00bb69329b5755fcc162379f73ecaa3ce86d8e..cc918e122f511db3fe8acf500aaaa9c701204b9f 100644
--- a/src/kernel_services/visitors/visitor.ml
+++ b/src/kernel_services/visitors/visitor.ml
@@ -124,7 +124,8 @@ object(self)
remove;
List.iter
(fun (e, a) ->
- Annotations.add_code_annot e ~kf:new_kf stmt a)
+ Annotations.add_code_annot
+ ~keep_empty:false e ~kf:new_kf stmt a)
add)
self#get_filling_actions
end
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index 004941db6742cd482c8910fc0e7a1d3f3d0f197a..7ce63778b530c98bf41e20013662ec11946bf0c9 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -272,7 +272,10 @@ let update_loop_assigns kf stmt state vi code_annot =
(AAssigns (bhvs, Logic_utils.concat_assigns old_assigns assigns))
| _ -> Aorai_option.fatal "Expecting an assigns clause here"
in
- Annotations.add_code_annot Aorai_option.emitter ~kf stmt new_assigns
+ (* we're putting the annotation on a new statement, with an empty
+ loop assigns by construction. Don't keep_empty *)
+ Annotations.add_code_annot
+ ~keep_empty:false Aorai_option.emitter ~kf stmt new_assigns
let get_action_post_cond kf ?init_trans return_states =
let to_consider pre_state int_states =
diff --git a/src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle b/src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle
index 6c66a3027f5e460bd9c2f940af4e5161e5b44de4..ef6224bb447e03550381c8c205c6feb41da0f37e 100644
--- a/src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle
@@ -275,8 +275,8 @@ int main(void)
/*@ ghost main_pre_func(); */
/*@ assigns X; */
X ++;
- /*@ assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
- in_main, X;
+ /*@ assigns X, aorai_CurOpStatus, aorai_CurOperation, S1, S2, S_in_f, Sf,
+ in_main;
*/
f();
/*@ ghost main_post_func(X); */
diff --git a/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle b/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle
index 2434556b05d580bac96d12dfa195f2e84cc9ee09..7e00479c453e3e785b4726a59de9906430c04c39 100644
--- a/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle
@@ -213,7 +213,7 @@ int main(void)
/*@ ghost main_pre_func(); */
/*@ assigns X; */
X ++;
- /*@ assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates, X; */
+ /*@ assigns X, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates; */
f();
/*@ ghost main_post_func(X); */
return X;
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 8e00ca6887362ed044ee2bbef2ff73042b7292fa..88e8b8893d14a439fefe504bf97a9e6ab47903c4 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -49,7 +49,6 @@ Plugin E-ACSL 21.0 (Scandium)
model analysis is running.
-* E-ACSL [2020-03-10] Fix frama-c/e-acsl#105 about misplaced
`__e_acsl_delete_block` in presence of gotos to return statements.
-- E-ACSL [2020-03-09] Improve verdict messages emitted by e_acsl_assert.
-* E-ACSL [2020-03-16] Fix #?1386 and frama-c/e-acsl#91 about the tracking
of variables declared inside the body of switches.
- E-ACSL [2020-02-09] Improve verdict messages emitted by e_acsl_assert.
@@ -157,7 +156,7 @@ Plugin E-ACSL 16.0 (Sulfur-20171101)
respective shadow spaces.
########################################
-Plugin E-ACSL 15.0 (Phosphorus-20170515)
+Plugin E-ACSL 15.0 (Phosphorus-20170501)
########################################
- runtime [2017-03-29] The (much more efficient) shadow memory model is
@@ -184,9 +183,9 @@ Plugin E-ACSL 15.0 (Phosphorus-20170515)
operations in a few cases: the generated code might have
overflowed.
-###########################
-Plugin E-ACSL 0.8 (Silicon)
-###########################
+####################################
+Plugin E-ACSL 0.8 (Silicon-20161101)
+####################################
-* e-acsl-gcc [2016-11-07] Added --rte-select feature to e-acsl-gcc.sh.
-* e-acsl-gcc [2016-08-02] Added --rt-debug feature to e-acsl-gcc.sh.
@@ -222,9 +221,9 @@ Plugin E-ACSL 0.8 (Silicon)
initialization of tracked memory blocks in the E-ACSL
memory model library.
-#############################
-Plugin E-ACSL 0.6 (Magnesium)
-#############################
+######################################
+Plugin E-ACSL 0.6 (Magnesium_20151002)
+######################################
-* e-acsl-gcc [2016-01-22] Add an e-acsl-gcc.sh option allowing to skip
compilation of original sources.
@@ -238,9 +237,9 @@ Plugin E-ACSL 0.6 (Magnesium)
-* runtime [2015-11-06] Fix a crash occuring when using a recent libc
while GMP headers provided by E-ACSL are used.
-##########################
-Plugin E-ACSL 0.5 (Sodium)
-##########################
+###################################
+Plugin E-ACSL 0.5 (Sodium_20150201)
+###################################
- E-ACSL [2015-06-01] Support of \freeable. Thus illegal calls to
free (e.g. double free) are detected.
@@ -256,9 +255,9 @@ o E-ACSL [2014-12-17] Export a minimal API for other plug-ins.
-* E-ACSL [2014-10-27] Add a missing cast when translating an integral
type used in a floating point/real context in an annotation.
-##########################
-Plugin E-ACSL 0.4.1 (Neon)
-##########################
+###################################
+Plugin E-ACSL 0.4.1 (Neon_20140301)
+###################################
-* E-ACSL [2014-08-05] Fix bug #1838 about memset.
-* E-ACSL [2014-08-05] Fix bug #1818 about initialization of globals.
diff --git a/src/plugins/e-acsl/src/code_generator/label.ml b/src/plugins/e-acsl/src/code_generator/label.ml
index 9225fdb571810e50ef40d96f5953ffa23cf573aa..f06c2232dfc45e230fda88c989d10349a949426d 100644
--- a/src/plugins/e-acsl/src/code_generator/label.ml
+++ b/src/plugins/e-acsl/src/code_generator/label.ml
@@ -48,7 +48,7 @@ let move kf ~old new_stmt =
List.iter
(fun (e, ca) ->
Annotations.remove_code_annot ~kf e old ca;
- Annotations.add_code_annot ~kf e new_stmt ca)
+ Annotations.add_code_annot ~keep_empty:false ~kf e new_stmt ca)
l;
(* update the gotos of the function jumping to one of the labels *)
let f =
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 4de6198ed1a43b3c1d4a9c2d0a344b378eee5dc6..a11a0dca9aa2bab2ab56cfc918b2dbb915cd0c8e 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -60,3 +60,9 @@ module Eval_terms: sig
@return None on either an evaluation error or on unsupported construct. *)
val predicate_deps: eval_env -> Cil_types.predicate -> logic_deps option
end
+
+
+module Unit_tests: sig
+ (** Runs the unit tests of Eva. *)
+ val run: unit -> unit
+end
diff --git a/src/plugins/value/utils/unit_tests.ml b/src/plugins/value/utils/unit_tests.ml
new file mode 100644
index 0000000000000000000000000000000000000000..043a2a726fa93a52dba15278fa6a4ca2881935e0
--- /dev/null
+++ b/src/plugins/value/utils/unit_tests.ml
@@ -0,0 +1,135 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-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
+
+(* If true, prints each operation performed for the tests. Otherwise, only
+ prints wrong operations. *)
+let print = false
+
+let report bug format =
+ if print || bug
+ then Value_parameters.result ("%s" ^^ format) (if bug then "BUG " else "")
+ else Format.ifprintf Format.std_formatter format
+
+
+(* Tests the semantics of sign values, by comparison with the Ival semantics. *)
+module Sign = struct
+
+ module Sign = struct
+ include Sign_value
+ let zero = zero
+ let pos = one
+ let neg = inject_int Cil.uintType Integer.minus_one
+ let pos_or_zero = join zero pos
+ let neg_or_zero = join zero neg
+ let pos_neg = join pos neg
+ end
+
+ module Ival = struct
+ include Ival
+ let positive = inject_range (Some Integer.one) None
+ let negative = inject_range None (Some Integer.minus_one)
+ let pos irange =
+ let max = Eval_typ.range_upper_bound irange in
+ inject_range (Some Integer.one) (Some max)
+ let neg irange =
+ let min = Eval_typ.range_lower_bound irange in
+ inject_range (Some min) (Some Integer.minus_one)
+ end
+
+ module Cval = Main_values.CVal
+
+ (* List of pairs (ival, sign) such that γ(ival) ⊆ γ(sign) and all values in
+ γ(sign) are in the range of [ikind]. *)
+ let test_values ikind =
+ let irange = Eval_typ.ik_range ikind in
+ let list =
+ [ Ival.zero, Sign.zero;
+ Ival.pos irange, Sign.pos;
+ Ival.zero, Sign.pos_or_zero;
+ Ival.pos irange, Sign.pos_or_zero; ]
+ in
+ if not irange.Eval_typ.i_signed
+ then list
+ else
+ list @
+ [ Ival.neg irange, Sign.neg;
+ Ival.zero, Sign.neg_or_zero;
+ Ival.neg irange, Sign.neg_or_zero;
+ Ival.pos irange, Sign.pos_neg;
+ Ival.neg irange, Sign.pos_neg; ]
+
+ let make_cvalue values =
+ List.map (fun (ival, sign) -> Cvalue.V.inject_ival ival, sign) values
+
+ (* Checks whether γ(ival) ⊆ γ(sign). *)
+ let is_included cvalue sign =
+ try
+ let ival = Cvalue.V.project_ival cvalue in
+ (not (Ival.contains_zero ival) || sign.Sign.zero) &&
+ (Ival.(is_bottom (narrow ival positive)) || sign.Sign.pos) &&
+ (Ival.(is_bottom (narrow ival negative)) || sign.Sign.neg)
+ with Cvalue.V.Not_based_on_null -> Sign.(equal sign top)
+
+ let test_unop unop typ values =
+ let test (cval, sign) =
+ let cval_res = Cval.forward_unop typ unop cval in
+ let sign_res = Sign.forward_unop typ unop sign in
+ let bug = not (Bottom.is_included is_included cval_res sign_res) in
+ report bug "%a %a = %a while %a %a = %a"
+ Printer.pp_unop unop Cval.pretty cval (Bottom.pretty Cval.pretty) cval_res
+ Printer.pp_unop unop Sign.pretty sign (Bottom.pretty Sign.pretty) sign_res
+ in
+ List.iter test values
+
+ let test_binop binop typ values =
+ let test (cval1, sign1) (cval2, sign2) =
+ let cval_res = Cval.forward_binop typ binop cval1 cval2 in
+ let sign_res = Sign.forward_binop typ binop sign1 sign2 in
+ let bug = not (Bottom.is_included is_included cval_res sign_res) in
+ report bug "%a %a %a = %a while %a %a %a = %a"
+ Cval.pretty cval1 Printer.pp_binop binop Cval.pretty cval2
+ (Bottom.pretty Cval.pretty) cval_res
+ Sign.pretty sign1 Printer.pp_binop binop Sign.pretty sign2
+ (Bottom.pretty Sign.pretty) sign_res
+ in
+ List.iter (fun x -> List.iter (test x) values) values
+
+ let test_typ ikind =
+ let typ = TInt (ikind, [])
+ and values = make_cvalue (test_values ikind) in
+ let apply f op = f op typ values in
+ List.iter (apply test_unop) [Neg; BNot; LNot];
+ List.iter (apply test_binop)
+ [PlusA; MinusA; Mult; Div; BAnd; BOr; BXor; LAnd; LOr]
+
+ let test () = List.iter test_typ [IInt; IUInt]
+end
+
+(** Runs all tests. *)
+let run () =
+ Value_parameters.result "Runs unit tests: %s."
+ (if print
+ then "all operations will be printed"
+ else "only faulty operations will be printed");
+ Sign.test ()
diff --git a/src/plugins/value/utils/unit_tests.mli b/src/plugins/value/utils/unit_tests.mli
new file mode 100644
index 0000000000000000000000000000000000000000..8783260b33accee3d55c8edf0a5002e41d3ed89b
--- /dev/null
+++ b/src/plugins/value/utils/unit_tests.mli
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-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). *)
+(* *)
+(**************************************************************************)
+
+(** Currently tested by this file:
+ - semantics of sign values. *)
+
+(** Runs some programmatic tests on Eva. *)
+val run: unit -> unit
diff --git a/src/plugins/value/values/cvalue_forward.ml b/src/plugins/value/values/cvalue_forward.ml
index 6822e5f5a5c0218144b3776f9d489431f8c63b9e..91263cb385821059a3a9b72b50ad514a788a35f0 100644
--- a/src/plugins/value/values/cvalue_forward.ml
+++ b/src/plugins/value/values/cvalue_forward.ml
@@ -28,28 +28,54 @@ open Abstract_value
Comparison
-------------------------------------------------------------------------- *)
+(* Representation of a pointer value to a literal string, with the string
+ itself, its length and the offsets pointed to in the string. *)
+type str = { string: string; offset: Ival.t; length: int; }
+
+(* Returns true if one string is a suffix of the other, and if there are offsets
+ pointing to the same point in this suffix. *)
+let may_be_suffix s1 s2 =
+ (* Requires [s1.length] <= [s2.length]. *)
+ let is_suffix s1 s2 =
+ let sub2 = String.sub s2.string (s2.length - s1.length) s1.length in
+ String.equal s1.string sub2 &&
+ let delta = Integer.of_int (s1.length - s2.length) in
+ let off2 = Ival.add_singleton_int delta s2.offset in
+ not (Ival.is_bottom (Ival.narrow s1.offset off2))
+ in
+ if s1.length <= s2.length then is_suffix s1 s2 else is_suffix s2 s1
+
+(* Returns true if [s1] may be shared with [s2] or a substring of [s2]. *)
+let rec may_be_shared_within s1 s2 =
+ may_be_suffix s1 s2 ||
+ match String.rindex_opt s2.string '\x00' with
+ | None -> false
+ | Some i ->
+ let s2 = { s2 with string = String.sub s2.string 0 i; length = i } in
+ may_be_shared_within s1 s2
+
+(* Returns true if [s1] and [s2] might point to the same literal string. *)
+let may_be_shared str1 off1 str2 off2 =
+ let s1 = { string = str1; offset = off1; length = String.length str1 }
+ and s2 = { string = str2; offset = off2; length = String.length str2 } in
+ may_be_shared_within s1 s2 || may_be_shared_within s2 s1
+
+(* Checks if all string bases of [v] satisfy [f]. *)
+let for_all_string v f =
+ Locations.Location_Bytes.for_all
+ (fun base off -> match base with
+ | Base.String (_, Base.CSString str) -> f base str off
+ | Base.String (_, Base.CSWstring _ ) -> false (* Not implemented yet *)
+ | _ -> true)
+ v
+
(* Literal strings can only be compared if their contents are recognizably
different (or the strings are physically the same). *)
-let are_comparable_string pointer1 pointer2 =
- try
- Locations.Location_Bytes.iter_on_strings ~skip:None
- (fun base1 s1 offs1 len1 ->
- Locations.Location_Bytes.iter_on_strings ~skip:(Some base1)
- (fun _ s2 offs2 len2 ->
- let delta = offs1 - offs2 in
- let start = if delta <= 0 then -delta else 0
- and max = min len2 (len1 - delta) in
- let length = max - start + 1 in
- let sub1 = String.sub s1 (start + delta) length
- and sub2 = String.sub s2 start length in
- if String.compare sub1 sub2 = 0
- then raise Not_found)
- pointer1)
- pointer2;
- true
- with
- | Not_found -> false
- | Invalid_argument _s -> assert false
+let are_comparable_string v1 v2 =
+ for_all_string v1 (fun base1 str1 off1 ->
+ for_all_string v2 (fun base2 str2 off2 ->
+ Base.equal base1 base2 ||
+ not (may_be_shared str1 off1 str2 off2)))
(* Under-approximation of the fact that a pointer is actually correct w.r.t.
what can be created through pointer arithmetics. See C99 6.5.6 and 6.5.8
diff --git a/src/plugins/value/values/sign_value.ml b/src/plugins/value/values/sign_value.ml
index 74c45a2c26862947e8909f5d0997dbf695722b5a..93051f60d086a6613c33d8327a049d52343fb9f8 100644
--- a/src/plugins/value/values/sign_value.ml
+++ b/src/plugins/value/values/sign_value.ml
@@ -125,17 +125,28 @@ let assume_comparable _ v1 v2 = `Unknown (v1, v2)
(** {2 Forward transfer functions} *)
-(* The three functions below are forward transformers for the mathematical
- operations +, *, /, and the unary negation -. The potential overflows for the
- operations on machine integers are taken into account by the functions
- [truncate_integer] and [rewrap_integer]. *)
+(* Functions [neg_unop], [plus], [mul] and [div] below are forward transformers
+ for the mathematical operations -, +, *, /. The potential overflows and
+ wrappings for the operations on machine integers are taken into account by
+ the functions [truncate_integer] and [rewrap_integer]. *)
let neg_unop v = { v with neg = v.pos; pos = v.neg }
-let forward_unop _ op v =
+let bitwise_not typ v =
+ match Cil.unrollType typ with
+ | TInt (ikind, _) | TEnum ({ekind=ikind}, _) ->
+ if Cil.isSigned ikind
+ then { pos = v.neg; neg = v.pos || v.zero; zero = v.neg }
+ else { pos = v.pos || v.zero; neg = false; zero = v.pos }
+ | _ -> top
+
+let logical_not v = { pos = v.zero; neg = false; zero = v.pos || v.neg }
+
+let forward_unop typ op v =
match op with
| Neg -> `Value (neg_unop v)
- | _ -> `Value top
+ | BNot -> `Value (bitwise_not typ v)
+ | LNot -> `Value (logical_not v)
let plus v1 v2 =
let neg = v1.neg || v2.neg in
@@ -158,12 +169,69 @@ let div v1 v2 =
let zero = true in (* zero can appear with large enough v2 *)
{ neg; pos; zero }
+(* The implementation of the bitwise operators below relies on this table
+ giving the sign of the result according to the sign of both operands.
+
+ v1 v2 v1&v2 v1|v2 v1^v2
+ -----------------------------------
+ | + + +0 + +0
+ | + 0 0 + +
+ | + - +0 - -
+ | 0 + 0 + +
+ | 0 0 0 0 0
+ | 0 - 0 - -
+ | - + +0 - -
+ | - 0 0 - -
+ | - - - - +0
+*)
+
+let bitwise_and v1 v2 =
+ let pos = (v1.pos && (v2.pos || v2.neg)) || (v2.pos && v1.neg) in
+ let neg = v1.neg && v2.neg in
+ let zero = v1.zero || v1.pos || v2.zero || v2.pos in
+ { neg; pos; zero }
+
+let bitwise_or v1 v2 =
+ let pos = (v1.pos && (v2.pos || v2.zero)) || (v1.zero && v2.pos) in
+ let neg = v1.neg || v2.neg in
+ let zero = v1.zero && v2.zero in
+ { neg; pos; zero }
+
+let bitwise_xor v1 v2 =
+ let pos =
+ (v1.pos && v2.pos) || (v1.pos && v2.zero) || (v1.zero && v2.pos)
+ || (v1.neg && v2.neg)
+ in
+ let neg =
+ (v1.neg && (v2.pos || v2.zero)) ||
+ (v2.neg && (v1.pos || v1.zero))
+ in
+ let zero = (v1.zero && v2.zero) || (v1.pos && v2.pos) || (v1.neg && v2.neg) in
+ { neg; pos; zero }
+
+let logical_and v1 v2 =
+ let pos = (v1.pos || v1.neg) && (v2.pos || v2.neg) in
+ let neg = false in
+ let zero = v1.zero || v2.zero in
+ { pos; neg; zero }
+
+let logical_or v1 v2 =
+ let pos = v1.pos || v1.neg || v2.pos || v2.neg in
+ let neg = false in
+ let zero = v1.zero && v2.zero in
+ { pos; neg; zero }
+
let forward_binop _ op v1 v2 =
match op with
| PlusA -> `Value (plus v1 v2)
| MinusA -> `Value (plus v1 (neg_unop v2))
| Mult -> `Value (mul v1 v2)
| Div -> if equal zero v2 then `Bottom else `Value (div v1 v2)
+ | BAnd -> `Value (bitwise_and v1 v2)
+ | BOr -> `Value (bitwise_or v1 v2)
+ | BXor -> `Value (bitwise_xor v1 v2)
+ | LAnd -> `Value (logical_and v1 v2)
+ | LOr -> `Value (logical_or v1 v2)
| _ -> `Value top
let rewrap_integer range v =
diff --git a/src/plugins/value/values/sign_value.mli b/src/plugins/value/values/sign_value.mli
index 055794019f7c3ace0d52ffd9652037f60c978d4e..94dd0faa8383c843fc97a7e8093f992c51f74bd5 100644
--- a/src/plugins/value/values/sign_value.mli
+++ b/src/plugins/value/values/sign_value.mli
@@ -22,6 +22,12 @@
(** Sign domain: abstraction of integer numerical values by their signs. *)
-include Abstract_value.Leaf
+type signs = {
+ pos: bool; (** true: maybe positive, false: never positive *)
+ zero: bool; (** true: maybe zero, false: never zero *)
+ neg: bool; (** true: maybe negative, false: never negative *)
+}
+
+include Abstract_value.Leaf with type t = signs
val pretty_debug: t Pretty_utils.formatter
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 2157ff0e014ed5bb8f107f89e420728f698a76ae..33d00e5c2bc3331d2648273f5dd6979ecebd4099 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -26,12 +26,19 @@ Plugin WP <next-release>
- WP [2020-06-12] Supports the \initialized ACSL predicate
+#########################
+Plugin WP 21.1 (Scandium)
+#########################
+
+-* WP [2020-06-23] Fixes Coq region function
+-* WP [2020-06-23] Fixes MemTyped structure loader for wp-rte
+
#########################
Plugin WP 21.0 (Scandium)
#########################
- WP [2020-04-10] Full support for Why3 IEEE float library
-- WP [2020-04-10] Removed option-wp-check
+- WP [2020-04-10] Removed option -wp-check
- WP [2020-04-09] Added smoke tests for dead call (-wp-smoke-dead-call)
- WP [2020-03-23] Added smoke tests for dead code (-wp-smoke-dead-code)
- WP [2020-03-23] Added smoke tests for dead loop (-wp-smoke-dead-loop)
@@ -41,16 +48,16 @@ Plugin WP 21.0 (Scandium)
- WP [2020-02-21] Why3 prover full-names use ':' instead of ','
- WP [2020-02-20] Fixes handling of LoopCurrent in loop invariants
- WP [2020-02-10] Specify cache mode with FRAMAC_WP_CACHE=<mode> (-wp-cache-env)
-- WP [2020-02-10] Update scripts with FRAMAC_WP_SCRIPT=update and-wp-prover script
+- WP [2020-02-10] Update scripts with FRAMAC_WP_SCRIPT=update and -wp-prover script
- WP [2020-02-10] Move frame conditions to Type section for better filtering
- WP [2020-02-10] Extended frame conditions to pointers inside compound
- WP [2020-02-10] Extended frame conditions with global C-types
-- WP [2019-17-04] Control splitting with-wp-max-split <n>
+- WP [2019-17-04] Control splitting with -wp-max-split <n>
- WP [2019-12-19] Fix drivers in different projects
-- WP [2019-12-04] Added option-wp-run-all-provers
+- WP [2019-12-04] Added option -wp-run-all-provers
- WP [2019-06-04] Checks for inconsistent requires (-wp-smoke-tests)
- WP [2019-01-29] Emit a warning when no goal is generated
-- WP [2018-04-17] Limit the number of splits (see-wp-max-split)
+- WP [2018-04-17] Limit the number of splits (see -wp-max-split)
- TIP [2018-04-03] Create session directory only on demand
- TIP [2018-03-19] Specification of JSON script format
- WP [2018-03-18] Additional lemma about remainder (mod)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index d8bbb4231bb2d648c5a755474fc69a7bcd01fc35..43f7709a6ac2a16f7bc8a6fb93d99c01970566d4 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -165,8 +165,8 @@ let ext_compare a b = Datatype.Int.compare a.ext_id b.ext_id
let sort_of_object = function
| C_int _ -> Logic.Sint
- | C_float _ -> Logic.Sreal
| C_pointer _ | C_comp _ | C_array _ -> Logic.Sdata
+ | C_float f -> Qed.Kind.of_tau (Context.get floats f)
let init_sort_of_object = function
| C_int _ | C_float _ | C_pointer _ -> Logic.Sbool
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 05e547e21821031a3d31d0ae3c9b57739f3ebc3e..c16073091edcdfc27feac50c7b1d236f141e9f46 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -174,10 +174,6 @@ wp-qualif: ./bin/toplevel.opt ./bin/ptests.opt $(WP_QUALIF_CACHE)
FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE) \
./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code
-wp-qualif-env:
- echo "FRAMAC_WP_CACHE=update"
- echo "FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE)"
-
wp-qualif-update: ./bin/toplevel.opt ./bin/ptests.opt $(WP_QUALIF_CACHE)
@echo "[CACHE] pull cache"
@echo "[CACHE] $(WP_QUALIF_CACHE)"
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index 801cb06218e395c5c75e9183f25528acab36c680..33815ea85957317b24de5f143b300f918bb56049 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -131,8 +131,8 @@ struct
begin
let prefix = Fun.debug phi in
let sigma = Sigma.create () in
- List.iter
- (fun chunk ->
+ List.iteri
+ (fun i chunk ->
List.iter
(fun (name,triggers,conditions,m1,m2) ->
let mem1 = assigned sigma chunk m1 chunks in
@@ -151,8 +151,8 @@ struct
[ (Trigger.of_term value1 :: triggers );
(Trigger.of_term value2 :: triggers ) ]
in
- let l_name = Pretty_utils.sfprintf "%s_%s_%a"
- prefix name Chunk.pretty chunk in
+ let l_name = Pretty_utils.sfprintf "%s_%s_%a%d"
+ prefix name Chunk.pretty chunk i in
let l_lemma = F.p_hyps conditions (p_equal value1 value2) in
Definitions.define_lemma {
l_assumed = true ;
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index f09f8b9249f5618566c9472f4dc088010ede14b3..90311c627cfb9ae4ae5c87405d93f58aea8179c5 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -160,6 +160,9 @@ struct
let compare a b = rank a - rank b
let equal = (=)
let pretty fmt c = Format.pp_print_string fmt (name c)
+ let detailed_pretty fmt = function
+ | M_int i -> Format.fprintf fmt "M%a" Ctypes.pp_int i
+ | m -> Format.pp_print_string fmt (name m)
let val_of_chunk = function
| M_int _ | M_char -> L.Int
| M_f32 -> Cfloat.tau_of_float Ctypes.Float32
@@ -1150,7 +1153,7 @@ and lookup_lv e = try lookup_a e with Not_found -> Sigs.(Mmem e,[])
let mchunk c =
match c with
| T_init -> Sigs.Mchunk (Pretty_utils.to_string Chunk.pretty c, KInit)
- | _ -> Sigs.Mchunk (Pretty_utils.to_string Chunk.pretty c, KValue)
+ | _ -> Sigs.Mchunk (Pretty_utils.to_string Chunk.detailed_pretty c, KValue)
let lookup s e =
try mchunk (Tmap.find e s)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 403ea107b96337b5c46d3afccdb86b38b8d04426..c8b8b89130d3bc301d2b89a9aa88880de8598c85 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -34,7 +34,7 @@ The recommended versions for external provers are:
\begin{tabular}{crlc}
Prover & Versions & Download &\\
\hline
- \textsf{Why3} & \verb|1.2.0| &
+ \textsf{Why3} & \verb|1.3.1| &
\url{http://why3.lri.fr} & \cite{Why3}\\
\textsf{Alt-Ergo} & \verb|2.0.0| &
\url{http://alt-ergo.ocamlpro.com} & \cite{AltErgo2006}\\
@@ -48,7 +48,7 @@ Other versions might be supported as well, typically, as far as we know:
\begin{itemize}
\item \textsf{Alt-Ergo} \verb+2.2.0+ and \verb+2.3.0+, although distributed under a non-commercial licence.
% \item \textsf{Coq} \verb+8.7.2+ and \verb+8.8.2+, although proof scripts compatibility can be an issue.
-\item \textsf{Why3} \verb+1.0.0+ and \verb+1.1.1+, although only \verb+1.2.0+ is provided with Coq support.
+\item \textsf{Why3} \verb+1.3.1+.
\end{itemize}
Other provers, like \textsf{Coq}, \textsf{Gappa}, \textsf{Z3}, \textsf{CVC3},
diff --git a/src/plugins/wp/share/coqwp/Memory.v b/src/plugins/wp/share/coqwp/Memory.v
index 474c1ca7f927453e6e8c9c8e36e7cf040562038d..de9c9ff58517407ea2b35069c94958a574edcb7d 100644
--- a/src/plugins/wp/share/coqwp/Memory.v
+++ b/src/plugins/wp/share/coqwp/Memory.v
@@ -249,7 +249,7 @@ Lemma separated_1 :
Admitted.
(* Why3 goal *)
-Definition region : array Z.
+Definition region : Z -> Z.
Admitted.
(* Why3 goal *)
@@ -262,7 +262,7 @@ Admitted.
(* Why3 assumption *)
Definition framed (m: farray addr addr) : Prop :=
- forall (p:addr), ((region .[ (base (m .[ p ]))] ) <= 0%Z)%Z.
+ forall (p:addr), ((region (base (m .[ p ])) ) <= 0%Z)%Z.
(* Why3 goal *)
Lemma separated_included :
diff --git a/src/plugins/wp/tests/README.md b/src/plugins/wp/tests/README.md
index 22304d9713e6856ad19c3ba07aa90da92aa43df5..2eb7d3d587b555af4b14c9f791c20376a97d2b5c 100644
--- a/src/plugins/wp/tests/README.md
+++ b/src/plugins/wp/tests/README.md
@@ -105,11 +105,10 @@ environment. To run individual tests, you may now use:
$ export FRAMAC_WP_CACHEDIR=$WP_QUALIF_CACHE
$ ./bin/ptests.opt src/plugins/wp/tests/xxx/yyy.i -config qualif [-show|-update]
-The necessary environment variables can also be displayed by the makefile:
+An utility script is provided to export the necessary environment variables
+(dont forget the `.` to execute the script in the current shell environment):
- $ make wp-qualif-env
- FRAMAC_WP_CACHE=update
- FRAMAC_WP_CACHEDIR=$WP_QUALIF_CACHE
+ $ . bin/wp_qualif.sh
As mentionned above, it is _not_ recommanded to globally set the
`FRAMAC_WP_XXX` variables in your default shell environment, because WP will
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..671f41e12dab20cba05bfa5d58879b49162d44be
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
@@ -0,0 +1,286 @@
+# frama-c -wp -wp-rte -wp-no-let [...]
+[kernel] Parsing tests/wp_acsl/struct_fields.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[rte] annotating function foo
+[wp] 2 goals scheduled
+---------------------------------------------
+--- Context 'typed_foo' Cluster 'Chunk'
+---------------------------------------------
+theory Chunk
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use frama_c_wp.memory.Memory *)
+
+ (* use frama_c_wp.cint.Cint *)
+
+ predicate is_sint8_chunk (m:addr -> int) =
+ forall a:addr. is_sint8 (get m a)
+
+ predicate is_sint16_chunk (m:addr -> int) =
+ forall a:addr. is_sint16 (get m a)
+
+ predicate is_sint32_chunk (m:addr -> int) =
+ forall a:addr. is_sint32 (get m a)
+end
+---------------------------------------------
+--- Context 'typed_foo' Cluster 'S1_X'
+---------------------------------------------
+theory S1_X
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ type S1_X =
+ | S1_X1 (F1_X_a:int) (F1_X_b:int) (F1_X_c:int)
+
+ (* use frama_c_wp.cint.Cint *)
+
+ predicate IsS1_X (s:S1_X) =
+ (is_sint8 (F1_X_a s) /\ is_sint16 (F1_X_b s)) /\ is_sint32 (F1_X_c s)
+end
+---------------------------------------------
+--- Context 'typed_foo' Cluster 'Compound'
+---------------------------------------------
+theory Compound
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use frama_c_wp.memory.Memory *)
+
+ function shiftfield_F1_X_a (p:addr) : addr = shift p 0
+
+ function shiftfield_F1_X_b (p:addr) : addr = shift p 1
+
+ function shiftfield_F1_X_c (p:addr) : addr = shift p 2
+
+ (* use S1_X *)
+
+ function Load_S1_X (p:addr) (mchar:addr -> int) (mint:addr -> int) (mint1:
+ addr -> int) : S1_X =
+ S1_X1 (get mchar (shiftfield_F1_X_a p)) (get mint (shiftfield_F1_X_b p))
+ (get mint1 (shiftfield_F1_X_c p))
+
+ Q_Load_S1_X_update_Mchar0 :
+ forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
+ addr, v:int [Load_S1_X p (set mchar q v) mint mint1].
+ separated p 3 q 1 ->
+ Load_S1_X p (set mchar q v) mint mint1 = Load_S1_X p mchar mint mint1
+
+ Q_Load_S1_X_eqmem_Mchar0 :
+ forall mchar:addr -> int, mchar1:addr -> int, mint:addr -> int, mint1:
+ addr -> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint mint1,
+ eqmem mchar mchar1 q n| Load_S1_X p mchar1 mint mint1,
+ eqmem mchar mchar1 q n].
+ included p 3 q n ->
+ eqmem mchar mchar1 q n ->
+ Load_S1_X p mchar1 mint mint1 = Load_S1_X p mchar mint mint1
+
+ Q_Load_S1_X_havoc_Mchar0 :
+ forall mchar:addr -> int, mchar1:addr -> int, mint:addr -> int, mint1:
+ addr -> int, n:int, p:addr, q:addr
+ [Load_S1_X p (havoc mchar1 mchar q n) mint mint1].
+ separated p 3 q n ->
+ Load_S1_X p (havoc mchar1 mchar q n) mint mint1
+ = Load_S1_X p mchar mint mint1
+
+ Q_Load_S1_X_update_Mint1 :
+ forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
+ addr, v:int [Load_S1_X p mchar (set mint1 q v) mint].
+ separated p 3 q 1 ->
+ Load_S1_X p mchar (set mint1 q v) mint = Load_S1_X p mchar mint1 mint
+
+ Q_Load_S1_X_eqmem_Mint1 :
+ forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
+ -> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint1 mint,
+ eqmem mint1 mint2 q n| Load_S1_X p mchar mint2 mint,
+ eqmem mint1 mint2 q n].
+ included p 3 q n ->
+ eqmem mint1 mint2 q n ->
+ Load_S1_X p mchar mint2 mint = Load_S1_X p mchar mint1 mint
+
+ Q_Load_S1_X_havoc_Mint1 :
+ forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
+ -> int, n:int, p:addr, q:addr
+ [Load_S1_X p mchar (havoc mint2 mint1 q n) mint].
+ separated p 3 q n ->
+ Load_S1_X p mchar (havoc mint2 mint1 q n) mint
+ = Load_S1_X p mchar mint1 mint
+
+ Q_Load_S1_X_update_Mint2 :
+ forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
+ addr, v:int [Load_S1_X p mchar mint (set mint1 q v)].
+ separated p 3 q 1 ->
+ Load_S1_X p mchar mint (set mint1 q v) = Load_S1_X p mchar mint mint1
+
+ Q_Load_S1_X_eqmem_Mint2 :
+ forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
+ -> int, n:int, p:addr, q:addr [Load_S1_X p mchar mint mint1,
+ eqmem mint1 mint2 q n| Load_S1_X p mchar mint mint2,
+ eqmem mint1 mint2 q n].
+ included p 3 q n ->
+ eqmem mint1 mint2 q n ->
+ Load_S1_X p mchar mint mint2 = Load_S1_X p mchar mint mint1
+
+ Q_Load_S1_X_havoc_Mint2 :
+ forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, mint2:addr
+ -> int, n:int, p:addr, q:addr
+ [Load_S1_X p mchar mint (havoc mint2 mint1 q n)].
+ separated p 3 q n ->
+ Load_S1_X p mchar mint (havoc mint2 mint1 q n)
+ = Load_S1_X p mchar mint mint1
+end
+[wp:print-generated]
+ theory WP
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use frama_c_wp.memory.Memory *)
+
+ (* use Chunk *)
+
+ (* use S1_X *)
+
+ (* use Compound *)
+
+ goal wp_goal :
+ forall t:addr -> bool, t1:int -> int, t2:addr -> int, t3:addr -> int, t4:
+ addr -> int, a:addr.
+ region (base a) <= 0 ->
+ is_sint16_chunk t3 ->
+ is_sint32_chunk t4 ->
+ is_sint8_chunk t2 ->
+ linked t1 ->
+ sconst t2 ->
+ cinits t ->
+ valid_rd t1 a 3 -> IsS1_X (Load_S1_X a t2 t3 t4) -> valid_rw t1 a 3
+ end
+[wp:print-generated]
+ theory WP1
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use frama_c_wp.memory.Memory *)
+
+ (* use Chunk *)
+
+ (* use S1_X *)
+
+ (* use Compound *)
+
+ goal wp_goal :
+ forall t:addr -> bool, t1:int -> int, t2:addr -> int, t3:addr -> int, t4:
+ addr -> int, a:addr.
+ region (base a) <= 0 ->
+ is_sint16_chunk t3 ->
+ is_sint32_chunk t4 ->
+ is_sint8_chunk t2 ->
+ linked t1 ->
+ sconst t2 ->
+ cinits t -> IsS1_X (Load_S1_X a t2 t3 t4) -> valid_rd t1 a 3
+ end
+[wp] 2 goals generated
+------------------------------------------------------------
+ Function foo
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/struct_fields.i, line 15):
+Assume {
+ Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+ is_sint8_chunk(Mchar_0) /\
+ IsS1_X(Load_S1_X(p, Mchar_0, Mint_0, Mint_1)).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0) /\
+ cinits(Init_0).
+ Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+ is_sint8_chunk(Mchar_0).
+ Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+ is_sint8_chunk(Mchar_0).
+ (* Block In *)
+ Have: ({ Init_F1_X_a = false ; Init_F1_X_b = false ; Init_F1_X_c = false }) =
+ Init_r_0.
+}
+Prove: valid_rd(Malloc_0, p, 3).
+
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/struct_fields.i, line 16):
+Let a = Load_S1_X(p, Mchar_0, Mint_0, Mint_1).
+Assume {
+ Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+ is_sint8_chunk(Mchar_0) /\ IsS1_X(a).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0) /\
+ cinits(Init_0).
+ Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+ is_sint8_chunk(Mchar_0).
+ Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+ is_sint8_chunk(Mchar_0).
+ Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
+ is_sint8_chunk(Mchar_0).
+ (* Block In *)
+ Have: ({ Init_F1_X_a = false ; Init_F1_X_b = false ; Init_F1_X_c = false }) =
+ Init_r_0.
+ (* Assertion 'rte,mem_access' *)
+ Have: valid_rd(Malloc_0, p, 3).
+ (* Initializer *)
+ Init: a = r.
+}
+Prove: valid_rw(Malloc_0, p, 3).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/struct_fields.i b/src/plugins/wp/tests/wp_acsl/struct_fields.i
new file mode 100644
index 0000000000000000000000000000000000000000..93b9c90858aaca1db67542015efe50acabd61703
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/struct_fields.i
@@ -0,0 +1,17 @@
+/* run.config
+ OPT:-wp-rte -wp-no-let -wp-gen -wp-prover why3 -wp-msg-key print-generated
+*/
+/* run.config_qualif
+ DONTRUN:
+*/
+
+struct X {
+ char a ;
+ short b ;
+ int c ;
+};
+
+void foo(struct X* p){
+ struct X r = *p ;
+ *p = r ;
+}
\ No newline at end of file
diff --git a/src/plugins/wp/tests/wp_bts/issue_898.i b/src/plugins/wp/tests/wp_bts/issue_898.i
new file mode 100644
index 0000000000000000000000000000000000000000..76c3fa6d43e8ccb9c7aa6fb68859a691ad83ea51
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/issue_898.i
@@ -0,0 +1,14 @@
+struct S {
+ int valid;
+ double value;
+};
+
+/*@
+ requires \is_finite(val);
+ ensures \eq_double(\result.value,val);
+ assigns \nothing;
+*/
+struct S job(double val) {
+ struct S result = { 0, val };
+ return result;
+}
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
index 2842dc0b66878ac96c03c3ff2756011a1b9d2ecf..b1af7c7da5cf23d35ee6e70c4dbfdb89fb3af036 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
@@ -60,19 +60,19 @@ theory Compound
function Load_S2_A (p:addr) (mint:addr -> int) : S2_A =
S2_A1 (get mint (shiftfield_F2_A_dummy p))
- Q_Load_S2_A_update_Mint :
+ Q_Load_S2_A_update_Mint0 :
forall mint:addr -> int, p:addr, q:addr, v:int
[Load_S2_A p (set mint q v)].
not q = p -> Load_S2_A p (set mint q v) = Load_S2_A p mint
- Q_Load_S2_A_eqmem_Mint :
+ Q_Load_S2_A_eqmem_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
[Load_S2_A p mint, eqmem mint mint1 q n| Load_S2_A p mint1,
eqmem mint mint1 q n].
included p 1 q n ->
eqmem mint mint1 q n -> Load_S2_A p mint1 = Load_S2_A p mint
- Q_Load_S2_A_havoc_Mint :
+ Q_Load_S2_A_havoc_Mint0 :
forall mint:addr -> int, mint1:addr -> int, n:int, p:addr, q:addr
[Load_S2_A p (havoc mint1 mint q n)].
separated p 1 q n ->
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_898.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_898.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f3dbc6f8d161250a1dab323a3012745b1929ae9c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_898.res.oracle
@@ -0,0 +1,20 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_898.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function job
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_bts/issue_898.i, line 8) in 'job':
+Let a = job_0.F1_S_value.
+Assume { (* Pre-condition *) Have: is_finite_f64(a). }
+Prove: eq_f64(a, a).
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'job':
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_898.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_898.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7d9049804fb645d575944e4ce403903b3c3e6b8c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_898.res.oracle
@@ -0,0 +1,15 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_898.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 2 goals scheduled
+[wp] [Alt-Ergo] Goal typed_job_ensures : Valid
+[wp] [Qed] Goal typed_job_assigns : Valid
+[wp] Proved goals: 2 / 2
+ Qed: 1
+ Alt-Ergo: 1
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ job 1 1 2 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/region_to_coq.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/region_to_coq.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e9138f7b492a1b4692401846228aec556b99e6b1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/region_to_coq.res.oracle
@@ -0,0 +1,21 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/region_to_coq.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] Warning: native support for coq is deprecated, use tip instead
+[wp] 4 goals scheduled
+[wp] [Coq] Goal typed_copy_loop_invariant_preserved : Saved script
+[wp] [Coq (native)] Goal typed_copy_loop_invariant_preserved : Valid
+[wp] [Coq] Goal typed_copy_loop_invariant_established : Saved script
+[wp] [Coq (native)] Goal typed_copy_loop_invariant_established : Valid
+[wp] [Qed] Goal typed_copy_loop_assigns_part1 : Valid
+[wp] [Coq] Goal typed_copy_loop_assigns_part2 : Saved script
+[wp] [Coq (native)] Goal typed_copy_loop_assigns_part2 : Valid
+[wp] Proved goals: 4 / 4
+ Qed: 1
+ Coq (native): 3
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ copy 1 - 4 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/region_to_coq.i b/src/plugins/wp/tests/wp_plugin/region_to_coq.i
new file mode 100644
index 0000000000000000000000000000000000000000..181b5891315053a6b1757046fec83385a9a6d3ac
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/region_to_coq.i
@@ -0,0 +1,14 @@
+/* run.config
+ DONTRUN:
+*/
+/* run.config_qualif
+ OPT: -wp-prover native:coq -wp-coq-script tests/wp_plugin/region_to_coq.script
+*/
+
+void copy(int* a, unsigned int n, int* b)
+{
+ /*@ loop invariant 0 <= i <= n ;
+ loop assigns i, b[0..n-1]; */
+ for(unsigned int i = 0; i < n; ++i)
+ b[i] = a[i];
+}
diff --git a/src/plugins/wp/tests/wp_plugin/region_to_coq.script b/src/plugins/wp/tests/wp_plugin/region_to_coq.script
new file mode 100644
index 0000000000000000000000000000000000000000..975ea9f72afde75a92fee1218e0788e4e3c6c0cc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/region_to_coq.script
@@ -0,0 +1,36 @@
+(* Generated by Frama-C WP *)
+
+Goal typed_copy_loop_assigns_part2.
+Hint *,b,copy,i,loop-assigns,part-1.
+Proof.
+ intros.
+ unfold included, shift_sint32.
+ unfold base, offset, shift ; simpl.
+ omega.
+Qed.
+
+Goal typed_copy_loop_invariant_established.
+Hint copy,established.
+Proof.
+ unfold is_uint32 ; intros ; omega.
+Qed.
+
+Goal typed_copy_loop_invariant_preserved.
+Hint copy,preserved.
+Proof.
+ intros.
+ assert (Hi_1: (1+i_1 <= i)%Z) by omega.
+ unfold is_uint32, to_uint32.
+ unfold to_range.
+ intros.
+ rewrite Z.add_0_l.
+ repeat rewrite Z.sub_0_r.
+ unfold is_uint32 in H2.
+ assert (Bs: (1 + i_1 = 4294967296)%Z \/ (1 + i_1 < 4294967296)%Z) by omega.
+ inversion Bs.
+ - rewrite <- H4.
+ rewrite Z_mod_same ; omega.
+ - rewrite Z.mod_small ; omega.
+Qed.
+
+
diff --git a/src/plugins/wp/tests/wp_tip/chunk_printing.i b/src/plugins/wp/tests/wp_tip/chunk_printing.i
new file mode 100644
index 0000000000000000000000000000000000000000..d4259c4eae03c0578c556b08fa4fa496605055e7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/chunk_printing.i
@@ -0,0 +1,33 @@
+/* run.config
+ OPT: -wp-rte -wp-msg-key state
+*/
+/* run.config_qualif
+ DONTRUN:
+*/
+
+struct V {
+ int* a ;
+ unsigned* b ;
+};
+
+struct V* y ;
+
+/*@
+ assigns \nothing;
+ ensures \result == v->a || \result == y->a;
+*/
+int* get_int(struct V* v);
+
+/*@
+ assigns \nothing;
+ ensures \result == v->b || \result == y->b;
+*/
+unsigned* get_uint(struct V* v);
+
+int main(void){
+ struct V x ;
+ x.a = get_int(&x);
+ x.b = get_uint(&x);
+
+ //@ assert *(x.a) == *(x.b);
+}
diff --git a/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e6de0501d53a2b2f1a10599ec0affcfe32491e76
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
@@ -0,0 +1,28 @@
+# frama-c -wp -wp-rte [...]
+[kernel] Parsing tests/wp_tip/chunk_printing.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[rte] annotating function main
+------------------------------------------------------------
+ Function main
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp_tip/chunk_printing.i, line 32):
+Let x_1 = « *`v_1 »@L1.
+Let x_2 = « *`v »@L1.
+Assume {
+ Type: is_sint32_chunk(µ:Msint32@L1) /\ is_uint32_chunk(µ:Muint32@L1) /\
+ is_uint32(`x_1) /\ is_sint32(`x_2).
+ (* Heap *)
+ Type: framed(µ:Mptr@L1).
+ Stmt { L1: }
+ Stmt { x.a = `v; }
+ (* Call 'get_int' *)
+ Have: ((x@L1.F1_V_a) = `v) \/ (« y->a »@L1 = `v).
+ Stmt { x.b = `v_1; }
+ (* Call 'get_uint' *)
+ Have: ((x@L1.F1_V_b) = `v_1) \/ (« y->b »@L1 = `v_1).
+}
+Prove: `x_2 = `x_1.
+
+------------------------------------------------------------
diff --git a/tests/float/fval_test.i b/tests/float/fval_test.i
index cabb28768924493f9964d6329934d0356b2e5143..f480093ba099eda06a2fdca943402b02945c5cce 100644
--- a/tests/float/fval_test.i
+++ b/tests/float/fval_test.i
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
- OPT: -load-module @PTEST_DIR@/@PTEST_NAME@
+ MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT:
*/
/* run.config*
DONTRUN:
diff --git a/tests/spec/loop_assigns_generated.i b/tests/spec/loop_assigns_generated.i
index 79fba31ec9f994b9302948f03a58372f3ec0ab71..f85c8c5a1ccec3e842a459fe4f1df20aee349285 100644
--- a/tests/spec/loop_assigns_generated.i
+++ b/tests/spec/loop_assigns_generated.i
@@ -7,4 +7,6 @@ void f() {
int i = 0;
/*@ loop assigns i; */
while (i< 10) { i++; }
+
+ while (i>0) { i--; }
}
diff --git a/tests/spec/loop_assigns_generated.ml b/tests/spec/loop_assigns_generated.ml
index 30d64b3ffebd318e7ce1585b73f21428fc2e389e..7e9340737ab5ed66e19981bec6e1ba8d3d2b5de8 100644
--- a/tests/spec/loop_assigns_generated.ml
+++ b/tests/spec/loop_assigns_generated.ml
@@ -3,7 +3,7 @@ open Cil_types
let e1 = Emitter.(create "emitter1" [ Code_annot ] [] [])
let e2 = Emitter.(create "emitter2" [ Code_annot ] [] [])
-let add_assigns e kf stmt v =
+let mk_assigns e v =
let lv = Cil.cvar_to_lvar v in
let term_v = Logic_const.tvar lv in
let named_term_v =
@@ -11,12 +11,15 @@ let add_assigns e kf stmt v =
term_name = ("added_by_"^(Emitter.get_name e))::term_v.term_name }
in
let id_v = Logic_const.new_identified_term named_term_v in
- Annotations.add_code_annot e ~kf stmt
+ Writes[id_v,FromAny]
+
+let add_assigns ?(keep_empty=false) e kf stmt v =
+ Annotations.add_code_annot ~keep_empty e ~kf stmt
(Logic_const.new_code_annotation
- (AAssigns ([], Writes [id_v, FromAny])));
+ (AAssigns ([], mk_assigns e v)));
Filecheck.check_ast ("after insertion of loop assigns " ^ v.vname)
-let add_allocates e kf stmt v =
+let mk_allocates e v =
let lv = Cil.cvar_to_lvar v in
let term_v = Logic_const.tvar lv in
let named_term_v =
@@ -24,11 +27,23 @@ let add_allocates e kf stmt v =
term_name = ("added_by_"^(Emitter.get_name e))::term_v.term_name }
in
let id_v = Logic_const.new_identified_term named_term_v in
- Annotations.add_code_annot e ~kf stmt
- (Logic_const.new_code_annotation
- (AAllocation([],FreeAlloc ([],[id_v]))));
+ FreeAlloc ([],[id_v])
+
+let add_allocates ?(keep_empty=false) e kf stmt v =
+ Annotations.add_code_annot ~keep_empty e ~kf stmt
+ (Logic_const.new_code_annotation (AAllocation([],mk_allocates e v)));
Filecheck.check_ast ("after insertion of loop allocates " ^ v.vname )
+let check_only_one f =
+ let seen = ref false in
+ fun _ a ->
+ if f a then begin
+ assert (not !seen);
+ seen := true
+ end
+
+let filter_category f _ a acc = if f a then a :: acc else acc
+
let main () =
Ast.compute();
let kf = Globals.Functions.find_by_name "f" in
@@ -37,14 +52,44 @@ let main () =
List.find
(fun s -> match s.skind with Loop _ -> true | _ -> false) def.sallstmts
in
+ let s2 =
+ List.find
+ (fun s' -> s!=s' && (match s'.skind with Loop _ -> true | _ -> false))
+ def.sallstmts
+ in
+ let s3 = Kernel_function.find_return kf in
let j = Cil.makeLocalVar def ~insert:true "j" Cil.intType in
let k = Cil.makeLocalVar def ~insert:true "k" Cil.intType in
+ let l = Cil.makeLocalVar def ~insert:true "l" Cil.intType in
let p = Cil.makeLocalVar def ~insert:true "p" Cil.intPtrType in
let q = Cil.makeLocalVar def ~insert:true "q" Cil.intPtrType in
+ let r = Cil.makeLocalVar def ~insert:true "r" Cil.intPtrType in
add_assigns e1 kf s j;
add_assigns e2 kf s k;
+ add_assigns e1 kf s l;
+ add_assigns ~keep_empty:true e2 kf s2 j;
+ Annotations.add_assigns ~keep_empty:true e1 kf ~stmt:s3 (mk_assigns e1 k);
add_allocates e1 kf s p;
add_allocates e2 kf s q;
+ add_allocates e1 kf s r;
+ add_allocates ~keep_empty:true e2 kf s2 p;
+ Annotations.add_allocates ~keep_empty:true e1 kf ~stmt:s3 (mk_allocates e1 k);
+ Annotations.iter_code_annot (check_only_one Logic_utils.is_assigns) s;
+ Annotations.iter_code_annot (check_only_one Logic_utils.is_allocation) s;
+ let lassigns =
+ Annotations.fold_code_annot (filter_category Logic_utils.is_assigns) s []
+ in
+ assert (List.length lassigns = 1);
+ let lalloc =
+ Annotations.fold_code_annot (filter_category Logic_utils.is_allocation) s []
+ in
+ assert (List.length lalloc = 1);
+ ignore
+ (Property_status.get
+ (Property.ip_of_code_annot_single kf s (List.hd lassigns)));
+ ignore
+ (Property_status.get
+ (Property.ip_of_code_annot_single kf s (List.hd lalloc)));
File.pretty_ast ()
let () = Db.Main.extend main
diff --git a/tests/spec/oracle/assigns_array.res.oracle b/tests/spec/oracle/assigns_array.res.oracle
index 778268bcc22bfd3fab2ede1fbea4c8539be364f5..6e4846e218d9c35e30edec7a74b34aa5e7f1492c 100644
--- a/tests/spec/oracle/assigns_array.res.oracle
+++ b/tests/spec/oracle/assigns_array.res.oracle
@@ -36,8 +36,8 @@ int h(int reset, int n)
int i;
int r = 0;
i = 0;
- /*@ for bar: loop assigns \nothing;
- for foo: loop assigns Tab[0 .. i]; */
+ /*@ for foo: loop assigns Tab[0 .. i];
+ for bar: loop assigns \nothing; */
while (i < n) {
r += Tab[i];
if (reset) Tab[i] = 0;
diff --git a/tests/spec/oracle/bts0578.res.oracle b/tests/spec/oracle/bts0578.res.oracle
index f25516888c6bafe4e5e1910dfa516174a2f9c2d2..7c6d8517d86a1a289b4f02db5da2cf00e985955e 100644
--- a/tests/spec/oracle/bts0578.res.oracle
+++ b/tests/spec/oracle/bts0578.res.oracle
@@ -7,11 +7,11 @@ void main(void)
int i;
int t[10];
i = 0;
- /*@ loop invariant \true;
- loop assigns t[0 .. i];
+ /*@ loop assigns t[0 .. i];
+ loop invariant \true;
+ for foo: loop assigns t[0 .. i];
for foo: loop invariant \true;
for foo: loop invariant \true;
- for foo: loop assigns t[0 .. i];
loop variant 0;
*/
while (i < 10) {
diff --git a/tests/spec/oracle/loop_assigns_generated.res.oracle b/tests/spec/oracle/loop_assigns_generated.res.oracle
index a30771642fda30636515438444f889311c81bf84..64f6610b539d47a1612fa69853c4760b6970cae5 100644
--- a/tests/spec/oracle/loop_assigns_generated.res.oracle
+++ b/tests/spec/oracle/loop_assigns_generated.res.oracle
@@ -2,15 +2,20 @@
/* Generated by Frama-C */
void f(void)
{
+ int *r;
int *q;
int *p;
+ int l;
int k;
int j;
int i = 0;
- /*@ loop allocates (added_by_emitter1: p), (added_by_emitter2: q);
- loop assigns i, (added_by_emitter1: j), (added_by_emitter2: k);
+ /*@ loop assigns i, (added_by_emitter1: j), (added_by_emitter1: l),
+ (added_by_emitter2: k);
+ loop allocates
+ (added_by_emitter1: p), (added_by_emitter1: r), (added_by_emitter2: q);
*/
while (i < 10) i ++;
+ while (i > 0) i --;
return;
}
diff --git a/tests/spec/oracle/preprocess_dos.res.oracle b/tests/spec/oracle/preprocess_dos.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..875a7eae29550f7c2bc14248aa39a15614d7216a
--- /dev/null
+++ b/tests/spec/oracle/preprocess_dos.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing tests/spec/preprocess_dos.c (with preprocessing)
+/* Generated by Frama-C */
+int main(void)
+{
+ int a = 0;
+ /*@ assert a ≡ 0; */ ;
+ return a;
+}
+
+
diff --git a/tests/spec/preprocess_dos.c.in b/tests/spec/preprocess_dos.c.in
new file mode 100644
index 0000000000000000000000000000000000000000..abae8ad374b159cd60043731308ac57df1f96498
--- /dev/null
+++ b/tests/spec/preprocess_dos.c.in
@@ -0,0 +1,13 @@
+/* run.config*
+COMMENT: Don't edit directly preprocess_dos.c, but preprocess_dos.c.in
+@DONTRUN@
+OPT: -cpp-command="@PTEST_DIR@/@PTEST_NAME@.sh @UNIX2DOS@ %i %o" -cpp-frama-c-compliant -print
+*/
+
+int main() {
+ int a = 0;
+ /*@
+ assert a == 0;
+ */
+ return a;
+}
diff --git a/tests/spec/preprocess_dos.sh b/tests/spec/preprocess_dos.sh
new file mode 100755
index 0000000000000000000000000000000000000000..a63a982d043b5847b333d4e556892393f97c8a7d
--- /dev/null
+++ b/tests/spec/preprocess_dos.sh
@@ -0,0 +1,3 @@
+#!/bin/sh
+gcc -C -E -I. -o $3 $2
+$1 -q $3
diff --git a/tests/syntax/oracle/asm_with_contracts.res.oracle b/tests/syntax/oracle/asm_with_contracts.res.oracle
index de45604755bf733ffeb4e6885baede947f7b9fb3..aab309b2eeb8fce6f14a24fcacbb3bd5d283cdc1 100644
--- a/tests/syntax/oracle/asm_with_contracts.res.oracle
+++ b/tests/syntax/oracle/asm_with_contracts.res.oracle
@@ -9,9 +9,9 @@ int f(int z)
int y = 2;
/*@ assigns y; */
__asm__ ("mov %1, %0\n\t" : "=r" (y) : "r" (x));
+ /*@ for b: assigns x, y; */
/*@ assigns x;
assigns x \from y; */
- /*@ for b: assigns x, y; */
__asm__ ("mov %1, %0\n\t" : "=r" (x) : "r" (y));
/*@ assigns x, y;
diff --git a/tests/syntax/oracle/pragma.res.oracle b/tests/syntax/oracle/pragma.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1a8c485d86b2bf01d6e9983907bd8509e92f82fe
--- /dev/null
+++ b/tests/syntax/oracle/pragma.res.oracle
@@ -0,0 +1,12 @@
+[kernel] Parsing tests/syntax/pragma.i (no preprocessing)
+[kernel] tests/syntax/pragma.i:1: Warning:
+ Unsupported argument for pragma pack push directive: `_CRT_PACKING'.
+/* Generated by Frama-C */
+int main(void)
+{
+ int __retres;
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/pragma.i b/tests/syntax/pragma.i
new file mode 100644
index 0000000000000000000000000000000000000000..c8dc1b09b1865c15352e9e78f8f5ed3a6ddfee49
--- /dev/null
+++ b/tests/syntax/pragma.i
@@ -0,0 +1,5 @@
+#pragma pack(push, _CRT_PACKING)
+#pragma pack(pop)
+int main() {
+ return 0;
+}
diff --git a/tests/value/oracle/strings.0.res.oracle b/tests/value/oracle/strings.0.res.oracle
deleted file mode 100644
index f82b23c4a9e97d73b6db8238c657b9fee2c9bc52..0000000000000000000000000000000000000000
--- a/tests/value/oracle/strings.0.res.oracle
+++ /dev/null
@@ -1,152 +0,0 @@
-[kernel] Parsing tests/value/strings.i (no preprocessing)
-[eva] Analyzing a complete application starting at main1
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- s1[0] ∈ {104}
- [1] ∈ {101}
- [2..3] ∈ {108}
- [4] ∈ {111}
- [5] ∈ {0}
- [6] ∈ {32}
- [7] ∈ {119}
- [8] ∈ {111}
- [9] ∈ {114}
- [10] ∈ {108}
- [11] ∈ {100}
- [12] ∈ {0}
- s2[0] ∈ {104}
- [1] ∈ {101}
- [2..3] ∈ {108}
- [4] ∈ {111}
- [5] ∈ {0}
- s5 ∈ {0}
- s6 ∈ {0}
- cc ∈ {97}
- Q ∈ {0}
- R ∈ {0}
- S ∈ {0}
- T ∈ {0}
- U ∈ {0}
- V ∈ {0}
- W ∈ {0}
- X ∈ {0}
- Y ∈ {0}
- Z ∈ {0}
- s3 ∈ {{ "tutu" }}
- s4 ∈ {{ "tutu" }}
- s7 ∈ {{ "hello\000 world" }}
- s8 ∈ {{ "hello" }}
-[eva] computing for function u <- main1.
- Called from tests/value/strings.i:39.
-[kernel:annot:missing-spec] tests/value/strings.i:39: Warning:
- Neither code nor specification for function u, generating default assigns from the prototype
-[eva] using specification for function u
-[eva] Done for function u
-[eva:alarm] tests/value/strings.i:39: Warning:
- out of bounds read. assert \valid_read(p - 4);
-[eva] computing for function u <- main1.
- Called from tests/value/strings.i:42.
-[eva] Done for function u
-[eva:alarm] tests/value/strings.i:42: Warning:
- out of bounds read. assert \valid_read(p + 12);
-[eva] computing for function u <- main1.
- Called from tests/value/strings.i:44.
-[eva] Done for function u
-[eva] computing for function u <- main1.
- Called from tests/value/strings.i:48.
-[eva] Done for function u
-[eva:alarm] tests/value/strings.i:48: Warning:
- out of bounds read. assert \valid_read(p - 4);
-[eva] computing for function u <- main1.
- Called from tests/value/strings.i:53.
-[eva] Done for function u
-[eva] computing for function strcpy <- main1.
- Called from tests/value/strings.i:53.
-[eva:alarm] tests/value/strings.i:21: Warning:
- out of bounds write.
- assert \valid(tmp_unroll_46);
- (tmp_unroll_46 from ldst++)
-[kernel] tests/value/strings.i:21: Warning:
- all target addresses were invalid. This path is assumed to be dead.
-[eva] Recording results for strcpy
-[eva] Done for function strcpy
-[eva] computing for function strlen <- main1.
- Called from tests/value/strings.i:58.
-[eva] Recording results for strlen
-[eva] Done for function strlen
-[eva] Recording results for main1
-[eva] done for function main1
-[eva] tests/value/strings.i:21:
- assertion 'Eva,mem_access' got final status invalid.
-[eva] tests/value/strings.i:39:
- assertion 'Eva,mem_access' got final status invalid.
-[eva] tests/value/strings.i:42:
- assertion 'Eva,mem_access' got final status invalid.
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function strcpy:
- NON TERMINATING FUNCTION
-[eva:final-states] Values at end of function strlen:
- s ∈ {{ &s1[6] }}
- l ∈ {5}
-[eva:final-states] Values at end of function main1:
- s1[0] ∈ {104}
- [1] ∈ {101}
- [2] ∈ {108}
- [3] ∈ {97}
- [4] ∈ {111}
- [5] ∈ {0}
- [6] ∈ {97}
- [7] ∈ {119}
- [8] ∈ {111}
- [9] ∈ {114}
- [10] ∈ {108}
- [11] ∈ {100}
- [12] ∈ {0}
- R ∈ {0}
- S ∈ {0}
- T ∈ {0; 101}
- p ∈ {{ &s1[5] ; &s2[3] }}
- __retres ∈ {5}
-[from] Computing for function strcpy
-[from] Non-terminating function strcpy (no dependencies)
-[from] Done for function strcpy
-[from] Computing for function strlen
-[from] Done for function strlen
-[from] Computing for function main1
-[from] Computing for function u <-main1
-[from] Done for function u
-[from] Done for function main1
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function strcpy:
- NON TERMINATING - NO EFFECTS
-[from] Function strlen:
- \result FROM s1[0..4]; s
-[from] Function u:
- \result FROM \nothing
-[from] Function main1:
- s1{[3]; [6]} FROM cc
- R FROM \nothing (and SELF)
- S FROM \nothing (and SELF)
- T FROM s1[1] (and SELF)
- \result FROM s1{[0..2]; [4]}; cc
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function strcpy:
- src; ldst; b[0..4]; tmp_unroll_46; tmp_1_unroll_46; tmp_0_unroll_46;
- tmp_unroll_49; tmp_1_unroll_49; tmp_0_unroll_49; tmp_unroll_52;
- tmp_1_unroll_52; tmp_0_unroll_52; tmp_unroll_55; tmp_1_unroll_55;
- tmp_0_unroll_55; tmp_unroll_58; tmp_1_unroll_58; tmp_0_unroll_58;
- tmp_unroll_61; tmp_1_unroll_61; tmp_0_unroll_61
-[inout] Inputs for function strcpy:
- a[0..5]
-[inout] Out (internal) for function strlen:
- s; l; tmp_unroll_106; tmp_unroll_109; tmp_unroll_112; tmp_unroll_115;
- tmp_unroll_118; tmp_unroll_121
-[inout] Inputs for function strlen:
- s1[0..5]
-[inout] Out (internal) for function main1:
- s1{[3]; [6]}; R; S; T; p; tmp; tmp_0; tmp_1; tmp_2; a[0..9]; b[0..4];
- tmp_3; tmp_4; __retres
-[inout] Inputs for function main1:
- s1[0..5]; cc
diff --git a/tests/value/oracle/strings.1.res.oracle b/tests/value/oracle/strings.1.res.oracle
deleted file mode 100644
index cf5a4433579e96602d54f51e4a713f7e1c7fe4d9..0000000000000000000000000000000000000000
--- a/tests/value/oracle/strings.1.res.oracle
+++ /dev/null
@@ -1,145 +0,0 @@
-[kernel] Parsing tests/value/strings.i (no preprocessing)
-[eva] Analyzing a complete application starting at main6
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- s1[0] ∈ {104}
- [1] ∈ {101}
- [2..3] ∈ {108}
- [4] ∈ {111}
- [5] ∈ {0}
- [6] ∈ {32}
- [7] ∈ {119}
- [8] ∈ {111}
- [9] ∈ {114}
- [10] ∈ {108}
- [11] ∈ {100}
- [12] ∈ {0}
- s2[0] ∈ {104}
- [1] ∈ {101}
- [2..3] ∈ {108}
- [4] ∈ {111}
- [5] ∈ {0}
- s5 ∈ {0}
- s6 ∈ {0}
- cc ∈ {97}
- Q ∈ {0}
- R ∈ {0}
- S ∈ {0}
- T ∈ {0}
- U ∈ {0}
- V ∈ {0}
- W ∈ {0}
- X ∈ {0}
- Y ∈ {0}
- Z ∈ {0}
- s3 ∈ {{ "tutu" }}
- s4 ∈ {{ "tutu" }}
- s7 ∈ {{ "hello\000 world" }}
- s8 ∈ {{ "hello" }}
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:72.
-[kernel:annot:missing-spec] tests/value/strings.i:72: Warning:
- Neither code nor specification for function u, generating default assigns from the prototype
-[eva] using specification for function u
-[eva] Done for function u
-[eva:alarm] tests/value/strings.i:73: Warning:
- pointer comparison. assert \pointer_comparable((void *)s3, (void *)s4);
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:74.
-[eva] Done for function u
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:76.
-[eva] Done for function u
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:78.
-[eva] Done for function u
-[eva:alarm] tests/value/strings.i:79: Warning:
- pointer comparison. assert \pointer_comparable((void *)s7, (void *)s8);
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:80.
-[eva] Done for function u
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:82.
-[eva] Done for function u
-[eva:alarm] tests/value/strings.i:83: Warning:
- pointer comparison.
- assert \pointer_comparable((void *)(s7 + 1), (void *)(s8 + 1));
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:84.
-[eva] Done for function u
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:86.
-[eva] Done for function u
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:87.
-[eva] Done for function u
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:88.
-[eva] Done for function u
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:89.
-[eva] Done for function u
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:89.
-[eva] Done for function u
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:90.
-[eva] Done for function u
-[eva:alarm] tests/value/strings.i:91: Warning:
- pointer comparison. assert \pointer_comparable((void *)s5, (void *)s6);
-[eva] computing for function u <- main6.
- Called from tests/value/strings.i:92.
-[eva] Done for function u
-[eva:alarm] tests/value/strings.i:93: Warning:
- pointer comparison.
- assert \pointer_comparable((void *)("oh, hello" + 4), (void *)s7);
-[eva] Recording results for main6
-[eva] done for function main6
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main6:
- s5 ∈ {{ "tutu" ; "hello" }}
- s6 ∈ {{ "tutu" ; "tutu" ; "hello" }}
- cc ∈ {116}
- Q ∈ {0}
- R ∈ {0}
- S ∈ {0}
- T ∈ {0}
- U ∈ {0}
- V ∈ {0}
- W ∈ {0}
- X ∈ {0; 1}
- Y ∈ {0; 1}
- Z ∈ {0; 1}
- s ∈ {{ "toto" }}
- __retres ∈ {116}
-[from] Computing for function main6
-[from] Computing for function u <-main6
-[from] Done for function u
-[from] Done for function main6
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function u:
- \result FROM \nothing
-[from] Function main6:
- s5 FROM s3; s8
- s6 FROM s3; s4; s8
- cc FROM "toto"[bits 0 to 7]
- Q FROM s7 (and SELF)
- R FROM s3; s4 (and SELF)
- S FROM \nothing (and SELF)
- T FROM s3 (and SELF)
- U FROM s7; s8 (and SELF)
- V FROM s4; s7 (and SELF)
- W FROM s7; s8 (and SELF)
- X FROM s3 (and SELF)
- Y FROM s3; s8 (and SELF)
- Z FROM s3; s4; s8 (and SELF)
- \result FROM "toto"[bits 0 to 7]
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main6:
- s5; s6; cc; Q; R; S; T; U; V; W; X; Y; Z; s; tmp; tmp_0; tmp_1; tmp_2;
- tmp_3; tmp_4; tmp_5; tmp_6; tmp_7; tmp_8; tmp_9; tmp_10; tmp_11; tmp_12;
- tmp_13; tmp_14; __retres
-[inout] Inputs for function main6:
- s5; s6; cc; s3; s4; s7; s8; "toto"[bits 0 to 7]
diff --git a/tests/value/oracle/strings.2.res.oracle b/tests/value/oracle/strings.2.res.oracle
deleted file mode 100644
index daea0f31e7890e94748290ff519bbb703421d0d5..0000000000000000000000000000000000000000
--- a/tests/value/oracle/strings.2.res.oracle
+++ /dev/null
@@ -1,69 +0,0 @@
-[kernel] Parsing tests/value/strings.i (no preprocessing)
-[eva] Analyzing a complete application starting at main7
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- s1[0] ∈ {104}
- [1] ∈ {101}
- [2..3] ∈ {108}
- [4] ∈ {111}
- [5] ∈ {0}
- [6] ∈ {32}
- [7] ∈ {119}
- [8] ∈ {111}
- [9] ∈ {114}
- [10] ∈ {108}
- [11] ∈ {100}
- [12] ∈ {0}
- s2[0] ∈ {104}
- [1] ∈ {101}
- [2..3] ∈ {108}
- [4] ∈ {111}
- [5] ∈ {0}
- s5 ∈ {0}
- s6 ∈ {0}
- cc ∈ {97}
- Q ∈ {0}
- R ∈ {0}
- S ∈ {0}
- T ∈ {0}
- U ∈ {0}
- V ∈ {0}
- W ∈ {0}
- X ∈ {0}
- Y ∈ {0}
- Z ∈ {0}
- s3 ∈ {{ "tutu" }}
- s4 ∈ {{ "tutu" }}
- s7 ∈ {{ "hello\000 world" }}
- s8 ∈ {{ "hello" }}
-[eva:alarm] tests/value/strings.i:101: Warning:
- out of bounds write. assert \valid(tmp);
- (tmp from f?s5 + 2:& c)
-[eva:alarm] tests/value/strings.i:103: Warning:
- out of bounds write. assert \valid(s5);
-[eva:alarm] tests/value/strings.i:105: Warning:
- out of bounds write. assert \valid(s6);
-[eva] Recording results for main7
-[eva] done for function main7
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main7:
- s5 ∈ {{ &c }}
- s6 ∈ {{ &c }}
- R ∈ {84}
- c ∈ {116}
- __retres ∈ {116}
-[from] Computing for function main7
-[from] Done for function main7
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function main7:
- s5 FROM s3; d
- s6 FROM s3; e
- R FROM s3; d; f
- \result FROM s4; "tutu"[bits 0 to 7]
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main7:
- s5; s6; R; c; tmp; __retres
-[inout] Inputs for function main7:
- s5; s6; cc; s3; s4; "tutu"[bits 0 to 7]
diff --git a/tests/value/oracle/strings.3.res.oracle b/tests/value/oracle/strings.3.res.oracle
deleted file mode 100644
index 45b2847cf8c3a1cad1f6fa02a39b71c5a17765df..0000000000000000000000000000000000000000
--- a/tests/value/oracle/strings.3.res.oracle
+++ /dev/null
@@ -1,114 +0,0 @@
-[kernel] Parsing tests/value/strings.i (no preprocessing)
-[eva] Analyzing a complete application starting at main8
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- s1[0] ∈ {104}
- [1] ∈ {101}
- [2..3] ∈ {108}
- [4] ∈ {111}
- [5] ∈ {0}
- [6] ∈ {32}
- [7] ∈ {119}
- [8] ∈ {111}
- [9] ∈ {114}
- [10] ∈ {108}
- [11] ∈ {100}
- [12] ∈ {0}
- s2[0] ∈ {104}
- [1] ∈ {101}
- [2..3] ∈ {108}
- [4] ∈ {111}
- [5] ∈ {0}
- s5 ∈ {0}
- s6 ∈ {0}
- cc ∈ {97}
- Q ∈ {0}
- R ∈ {0}
- S ∈ {0}
- T ∈ {0}
- U ∈ {0}
- V ∈ {0}
- W ∈ {0}
- X ∈ {0}
- Y ∈ {0}
- Z ∈ {0}
- s3 ∈ {{ "tutu" }}
- s4 ∈ {{ "tutu" }}
- s7 ∈ {{ "hello\000 world" }}
- s8 ∈ {{ "hello" }}
-[eva] computing for function assigns <- main8.
- Called from tests/value/strings.i:127.
-[eva] using specification for function assigns
-[eva] tests/value/strings.i:121: Warning:
- no \from part for clause 'assigns *(p + (0 .. s - 1));'
-[eva] Done for function assigns
-[eva] computing for function strcmp <- main8.
- Called from tests/value/strings.i:128.
-[eva:alarm] tests/value/strings.i:114: Warning:
- out of bounds read. assert \valid_read(tmp_0);
- (tmp_0 from s2_0++)
-[eva] Recording results for strcmp
-[eva] Done for function strcmp
-[eva] Recording results for main8
-[eva] done for function main8
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function strcmp:
- s1_0 ∈ {{ &long_chain + [0..29] }}
- s2_0 ∈ {{ &tc + [0..29] }}
- __retres ∈ [-223..121]
-[eva:final-states] Values at end of function main8:
- tc[0..29] ∈ [--..--]
- long_chain[0] ∈ {114}
- [1] ∈ {101}
- [2] ∈ {97}
- [3..4] ∈ {108}
- [5] ∈ {121}
- [6] ∈ {32}
- [7] ∈ {114}
- [8] ∈ {101}
- [9] ∈ {97}
- [10..11] ∈ {108}
- [12] ∈ {121}
- [13] ∈ {32}
- [14] ∈ {114}
- [15] ∈ {101}
- [16] ∈ {97}
- [17..18] ∈ {108}
- [19] ∈ {121}
- [20] ∈ {32}
- [21] ∈ {108}
- [22] ∈ {111}
- [23] ∈ {110}
- [24] ∈ {103}
- [25] ∈ {32}
- [26] ∈ {99}
- [27] ∈ {104}
- [28] ∈ {97}
- [29] ∈ {105}
- [30] ∈ {110}
- [31] ∈ {0}
- x ∈ [-223..121]
-[from] Computing for function strcmp
-[from] Done for function strcmp
-[from] Computing for function main8
-[from] Computing for function assigns <-main8
-[from] Done for function assigns
-[from] Done for function main8
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function assigns:
- tc[0..29] FROM ANYTHING(origin:Unknown) (and SELF)
-[from] Function strcmp:
- \result FROM s1_0; s2_0; tc[0..29]; long_chain[0..30]
-[from] Function main8:
- \result FROM ANYTHING(origin:Unknown)
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function strcmp:
- s1_0; s2_0; tmp; tmp_0; __retres
-[inout] Inputs for function strcmp:
- tc[0..29]; long_chain[0..30]
-[inout] Out (internal) for function main8:
- tc[0..29]; long_chain[0..31]; x
-[inout] Inputs for function main8:
- ANYTHING(origin:Unknown)
diff --git a/tests/value/oracle/strings.res.oracle b/tests/value/oracle/strings.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5e410a5aad929dc5580b43a5d42f68a94d87a59f
--- /dev/null
+++ b/tests/value/oracle/strings.res.oracle
@@ -0,0 +1,428 @@
+[kernel] Parsing tests/value/strings.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ nondet ∈ [--..--]
+ s1[0] ∈ {104}
+ [1] ∈ {101}
+ [2..3] ∈ {108}
+ [4] ∈ {111}
+ [5] ∈ {0}
+ [6] ∈ {32}
+ [7] ∈ {119}
+ [8] ∈ {111}
+ [9] ∈ {114}
+ [10] ∈ {108}
+ [11] ∈ {100}
+ [12] ∈ {0}
+ s2[0] ∈ {104}
+ [1] ∈ {101}
+ [2..3] ∈ {108}
+ [4] ∈ {111}
+ [5] ∈ {0}
+ s3 ∈ {{ "tutu" }}
+ s4 ∈ {{ "tutu" }}
+ s5 ∈ {0}
+ s6 ∈ {0}
+ s7 ∈ {{ "hello\000 world" }}
+ s8 ∈ {{ "hello" }}
+ cc ∈ {97}
+ Q ∈ {0}
+ R ∈ {0}
+ S ∈ {0}
+ T ∈ {0}
+ U ∈ {0}
+ V ∈ {0}
+ W ∈ {0}
+ X ∈ {0}
+ Y ∈ {0}
+ Z ∈ {0}
+[eva] computing for function string_reads <- main.
+ Called from tests/value/strings.i:142.
+[eva] computing for function u <- string_reads <- main.
+ Called from tests/value/strings.i:39.
+[kernel:annot:missing-spec] tests/value/strings.i:39: Warning:
+ Neither code nor specification for function u, generating default assigns from the prototype
+[eva] using specification for function u
+[eva] Done for function u
+[eva:alarm] tests/value/strings.i:39: Warning:
+ out of bounds read. assert \valid_read(p - 4);
+[eva] computing for function u <- string_reads <- main.
+ Called from tests/value/strings.i:42.
+[eva] Done for function u
+[eva:alarm] tests/value/strings.i:42: Warning:
+ out of bounds read. assert \valid_read(p + 12);
+[eva] computing for function u <- string_reads <- main.
+ Called from tests/value/strings.i:44.
+[eva] Done for function u
+[eva] computing for function u <- string_reads <- main.
+ Called from tests/value/strings.i:48.
+[eva] Done for function u
+[eva:alarm] tests/value/strings.i:48: Warning:
+ out of bounds read. assert \valid_read(p - 4);
+[eva] computing for function u <- string_reads <- main.
+ Called from tests/value/strings.i:53.
+[eva] Done for function u
+[eva] computing for function strcpy <- string_reads <- main.
+ Called from tests/value/strings.i:53.
+[eva:alarm] tests/value/strings.i:23: Warning:
+ out of bounds write.
+ assert \valid(tmp_unroll_46);
+ (tmp_unroll_46 from ldst++)
+[kernel] tests/value/strings.i:23: Warning:
+ all target addresses were invalid. This path is assumed to be dead.
+[eva] Recording results for strcpy
+[eva] Done for function strcpy
+[eva] computing for function strlen <- string_reads <- main.
+ Called from tests/value/strings.i:58.
+[eva] Recording results for strlen
+[eva] Done for function strlen
+[eva] Recording results for string_reads
+[eva] Done for function string_reads
+[eva] computing for function string_writes <- main.
+ Called from tests/value/strings.i:143.
+[eva:alarm] tests/value/strings.i:64: Warning:
+ out of bounds write. assert \valid(tmp);
+ (tmp from nondet?s5 + 2:& c)
+[eva:alarm] tests/value/strings.i:66: Warning:
+ out of bounds write. assert \valid(s5);
+[eva:alarm] tests/value/strings.i:68: Warning:
+ out of bounds write. assert \valid(s6);
+[eva] Recording results for string_writes
+[eva] Done for function string_writes
+[eva:locals-escaping] tests/value/strings.i:143: Warning:
+ locals {c} escaping the scope of string_writes through s5
+[eva:locals-escaping] tests/value/strings.i:143: Warning:
+ locals {c} escaping the scope of string_writes through s6
+[eva] computing for function string_comparison <- main.
+ Called from tests/value/strings.i:144.
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:78.
+[eva] Done for function u
+[eva:alarm] tests/value/strings.i:79: Warning:
+ pointer comparison. assert \pointer_comparable((void *)s3, (void *)s4);
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:80.
+[eva] Done for function u
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:82.
+[eva] Done for function u
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:84.
+[eva] Done for function u
+[eva:alarm] tests/value/strings.i:85: Warning:
+ pointer comparison. assert \pointer_comparable((void *)s7, (void *)s8);
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:86.
+[eva] Done for function u
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:88.
+[eva] Done for function u
+[eva:alarm] tests/value/strings.i:89: Warning:
+ pointer comparison.
+ assert \pointer_comparable((void *)(s7 + 1), (void *)(s8 + 1));
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:90.
+[eva] Done for function u
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:92.
+[eva] Done for function u
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:93.
+[eva] Done for function u
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:94.
+[eva] Done for function u
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:95.
+[eva] Done for function u
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:95.
+[eva] Done for function u
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:96.
+[eva] Done for function u
+[eva:alarm] tests/value/strings.i:97: Warning:
+ pointer comparison. assert \pointer_comparable((void *)s5, (void *)s6);
+[eva] computing for function u <- string_comparison <- main.
+ Called from tests/value/strings.i:98.
+[eva] Done for function u
+[eva:alarm] tests/value/strings.i:99: Warning:
+ pointer comparison.
+ assert \pointer_comparable((void *)("oh, hello" + 4), (void *)s7);
+[eva] Recording results for string_comparison
+[eva] Done for function string_comparison
+[eva] computing for function wide_string_comparison <- main.
+ Called from tests/value/strings.i:145.
+[eva:alarm] tests/value/strings.i:111: Warning:
+ pointer comparison. assert \pointer_comparable((void *)w1, (void *)w2);
+[eva:alarm] tests/value/strings.i:114: Warning:
+ pointer comparison. assert \pointer_comparable((void *)w2, (void *)w3);
+[eva] Recording results for wide_string_comparison
+[eva] Done for function wide_string_comparison
+[eva] computing for function long_chain <- main.
+ Called from tests/value/strings.i:146.
+[eva] computing for function assigns <- long_chain <- main.
+ Called from tests/value/strings.i:135.
+[eva] using specification for function assigns
+[eva] tests/value/strings.i:129: Warning:
+ no \from part for clause 'assigns *(p + (0 .. s - 1));'
+[eva] Done for function assigns
+[eva] computing for function strcmp <- long_chain <- main.
+ Called from tests/value/strings.i:136.
+[eva:alarm] tests/value/strings.i:123: Warning:
+ out of bounds read. assert \valid_read(tmp_0);
+ (tmp_0 from s2_0++)
+[eva] Recording results for strcmp
+[eva] Done for function strcmp
+[eva] Recording results for long_chain
+[eva] Done for function long_chain
+[eva] Recording results for main
+[eva] done for function main
+[eva] tests/value/strings.i:23:
+ assertion 'Eva,mem_access' got final status invalid.
+[eva] tests/value/strings.i:39:
+ assertion 'Eva,mem_access' got final status invalid.
+[eva] tests/value/strings.i:42:
+ assertion 'Eva,mem_access' got final status invalid.
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function strcmp:
+ s1_0 ∈ {{ &long_chain_0 + [0..29] }}
+ s2_0 ∈ {{ &tc + [0..29] }}
+ __retres ∈ [-223..121]
+[eva:final-states] Values at end of function long_chain:
+ tc[0..29] ∈ [--..--]
+ long_chain_0[0] ∈ {114}
+ [1] ∈ {101}
+ [2] ∈ {97}
+ [3..4] ∈ {108}
+ [5] ∈ {121}
+ [6] ∈ {32}
+ [7] ∈ {114}
+ [8] ∈ {101}
+ [9] ∈ {97}
+ [10..11] ∈ {108}
+ [12] ∈ {121}
+ [13] ∈ {32}
+ [14] ∈ {114}
+ [15] ∈ {101}
+ [16] ∈ {97}
+ [17..18] ∈ {108}
+ [19] ∈ {121}
+ [20] ∈ {32}
+ [21] ∈ {108}
+ [22] ∈ {111}
+ [23] ∈ {110}
+ [24] ∈ {103}
+ [25] ∈ {32}
+ [26] ∈ {99}
+ [27] ∈ {104}
+ [28] ∈ {97}
+ [29] ∈ {105}
+ [30] ∈ {110}
+ [31] ∈ {0}
+ x ∈ [-223..121]
+[eva:final-states] Values at end of function strcpy:
+ NON TERMINATING FUNCTION
+[eva:final-states] Values at end of function string_writes:
+ s5 ∈ {{ &c }}
+ s6 ∈ {{ &c }}
+ R ∈ {84}
+ c ∈ {116}
+ __retres ∈ {116}
+[eva:final-states] Values at end of function strlen:
+ s ∈ {{ &s1[6] }}
+ l ∈ {5}
+[eva:final-states] Values at end of function string_comparison:
+ s5 ∈ {{ "tutu" ; "hello" }}
+ s6 ∈ {{ "tutu" ; "tutu" ; "hello" }}
+ cc ∈ {116}
+ Q ∈ {0}
+ R ∈ {0; 84}
+ S ∈ {0}
+ T ∈ {0; 101}
+ U ∈ {0}
+ V ∈ {0}
+ W ∈ {0}
+ X ∈ {0; 1}
+ Y ∈ {0; 1}
+ Z ∈ {0; 1}
+ s ∈ {{ "toto" }}
+ __retres ∈ {116}
+[eva:final-states] Values at end of function string_reads:
+ s1[0] ∈ {104}
+ [1] ∈ {101}
+ [2] ∈ {108}
+ [3] ∈ {97}
+ [4] ∈ {111}
+ [5] ∈ {0}
+ [6] ∈ {97}
+ [7] ∈ {119}
+ [8] ∈ {111}
+ [9] ∈ {114}
+ [10] ∈ {108}
+ [11] ∈ {100}
+ [12] ∈ {0}
+ R ∈ {0}
+ S ∈ {0}
+ T ∈ {0; 101}
+ p ∈ {{ &s1[5] ; &s2[3] }}
+ __retres ∈ {5}
+[eva:final-states] Values at end of function wide_string_comparison:
+ w1 ∈ {{ L"abcdef" }}
+ w2 ∈ {{ L"def" }}
+ w3 ∈ {{ L"abc" }}
+ res ∈ {0}
+[eva:final-states] Values at end of function main:
+ s1[0] ∈ {104}
+ [1] ∈ {101}
+ [2] ∈ {108}
+ [3] ∈ {97}
+ [4] ∈ {111}
+ [5] ∈ {0}
+ [6] ∈ {97}
+ [7] ∈ {119}
+ [8] ∈ {111}
+ [9] ∈ {114}
+ [10] ∈ {108}
+ [11] ∈ {100}
+ [12] ∈ {0}
+ s5 ∈ {{ "tutu" ; "hello" }}
+ s6 ∈ {{ "tutu" ; "tutu" ; "hello" }}
+ cc ∈ {116}
+ Q ∈ {0}
+ R ∈ {0; 84}
+ S ∈ {0}
+ T ∈ {0; 101}
+ U ∈ {0}
+ V ∈ {0}
+ W ∈ {0}
+ X ∈ {0; 1}
+ Y ∈ {0; 1}
+ Z ∈ {0; 1}
+[from] Computing for function strcmp
+[from] Done for function strcmp
+[from] Computing for function long_chain
+[from] Computing for function assigns <-long_chain
+[from] Done for function assigns
+[from] Done for function long_chain
+[from] Computing for function strcpy
+[from] Non-terminating function strcpy (no dependencies)
+[from] Done for function strcpy
+[from] Computing for function string_writes
+[from] Done for function string_writes
+[from] Computing for function strlen
+[from] Done for function strlen
+[from] Computing for function string_comparison
+[from] Computing for function u <-string_comparison
+[from] Done for function u
+[from] Done for function string_comparison
+[from] Computing for function string_reads
+[from] Done for function string_reads
+[from] Computing for function wide_string_comparison
+[from] Done for function wide_string_comparison
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function assigns:
+ tc[0..29] FROM ANYTHING(origin:Unknown) (and SELF)
+[from] Function strcmp:
+ \result FROM s1_0; s2_0; tc[0..29]; long_chain_0[0..30]
+[from] Function long_chain:
+ \result FROM ANYTHING(origin:Unknown)
+[from] Function strcpy:
+ NON TERMINATING - NO EFFECTS
+[from] Function string_writes:
+ s5 FROM nondet; s3
+ s6 FROM nondet; s3
+ R FROM nondet; s3
+ \result FROM s4; "tutu"[bits 0 to 7]
+[from] Function strlen:
+ \result FROM s1[0..4]; s
+[from] Function u:
+ \result FROM \nothing
+[from] Function string_comparison:
+ s5 FROM s3; s8
+ s6 FROM s3; s4; s8
+ cc FROM "toto"[bits 0 to 7]
+ Q FROM s7 (and SELF)
+ R FROM s3; s4 (and SELF)
+ S FROM \nothing (and SELF)
+ T FROM s3 (and SELF)
+ U FROM s7; s8 (and SELF)
+ V FROM s4; s7 (and SELF)
+ W FROM s7; s8 (and SELF)
+ X FROM s3 (and SELF)
+ Y FROM s3; s8 (and SELF)
+ Z FROM s3; s4; s8 (and SELF)
+ \result FROM "toto"[bits 0 to 7]
+[from] Function string_reads:
+ s1{[3]; [6]} FROM cc
+ R FROM \nothing (and SELF)
+ S FROM \nothing (and SELF)
+ T FROM s1[1] (and SELF)
+ \result FROM s1{[0..2]; [4]}; cc
+[from] Function wide_string_comparison:
+ \result FROM \nothing
+[from] Function main:
+ s1{[3]; [6]} FROM cc
+ s5 FROM s3; s8
+ s6 FROM s3; s4; s8
+ cc FROM "toto"[bits 0 to 7]
+ Q FROM s7 (and SELF)
+ R FROM nondet; s3; s4
+ S FROM \nothing (and SELF)
+ T FROM s1[1]; s3 (and SELF)
+ U FROM s7; s8 (and SELF)
+ V FROM s4; s7 (and SELF)
+ W FROM s7; s8 (and SELF)
+ X FROM s3 (and SELF)
+ Y FROM s3; s8 (and SELF)
+ Z FROM s3; s4; s8 (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function strcmp:
+ s1_0; s2_0; tmp; tmp_0; __retres
+[inout] Inputs for function strcmp:
+ tc[0..29]; long_chain_0[0..30]
+[inout] Out (internal) for function long_chain:
+ tc[0..29]; long_chain_0[0..31]; x
+[inout] Inputs for function long_chain:
+ ANYTHING(origin:Unknown)
+[inout] Out (internal) for function strcpy:
+ src; ldst; b[0..4]; tmp_unroll_46; tmp_1_unroll_46; tmp_0_unroll_46;
+ tmp_unroll_49; tmp_1_unroll_49; tmp_0_unroll_49; tmp_unroll_52;
+ tmp_1_unroll_52; tmp_0_unroll_52; tmp_unroll_55; tmp_1_unroll_55;
+ tmp_0_unroll_55; tmp_unroll_58; tmp_1_unroll_58; tmp_0_unroll_58;
+ tmp_unroll_61; tmp_1_unroll_61; tmp_0_unroll_61
+[inout] Inputs for function strcpy:
+ a[0..5]
+[inout] Out (internal) for function string_writes:
+ s5; s6; R; c; tmp; __retres
+[inout] Inputs for function string_writes:
+ nondet; s3; s4; s5; s6; cc; "tutu"[bits 0 to 7]
+[inout] Out (internal) for function strlen:
+ s; l; tmp_unroll_106; tmp_unroll_109; tmp_unroll_112; tmp_unroll_115;
+ tmp_unroll_118; tmp_unroll_121
+[inout] Inputs for function strlen:
+ s1[0..5]
+[inout] Out (internal) for function string_comparison:
+ s5; s6; cc; Q; R; S; T; U; V; W; X; Y; Z; s; tmp; tmp_0; tmp_1; tmp_2;
+ tmp_3; tmp_4; tmp_5; tmp_6; tmp_7; tmp_8; tmp_9; tmp_10; tmp_11; tmp_12;
+ tmp_13; tmp_14; __retres
+[inout] Inputs for function string_comparison:
+ s3; s4; s5; s6; s7; s8; cc; "toto"[bits 0 to 7]
+[inout] Out (internal) for function string_reads:
+ s1{[3]; [6]}; R; S; T; p; tmp; tmp_0; tmp_1; tmp_2; a[0..9]; b[0..4];
+ tmp_3; tmp_4; __retres
+[inout] Inputs for function string_reads:
+ s1[0..5]; cc
+[inout] Out (internal) for function wide_string_comparison:
+ w1; w2; w3; res
+[inout] Inputs for function wide_string_comparison:
+ \nothing
+[inout] Out (internal) for function main:
+ s1{[3]; [6]}; s5; s6; cc; Q; R; S; T; U; V; W; X; Y; Z
+[inout] Inputs for function main:
+ ANYTHING(origin:Unknown)
diff --git a/tests/value/oracle/unit_tests.res.oracle b/tests/value/oracle/unit_tests.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..35ce0d1ac58fd2746a03ac9dc7555281595b0f8e
--- /dev/null
+++ b/tests/value/oracle/unit_tests.res.oracle
@@ -0,0 +1,2 @@
+[kernel] Parsing tests/value/unit_tests.i (no preprocessing)
+[eva] Runs unit tests: only faulty operations will be printed.
diff --git a/tests/value/strings.i b/tests/value/strings.i
index f4ca9828f5bfd47f713c0fab8528a6a56cb64c6b..0f6087161602aca84fc72009a38b18e5ccb75272 100644
--- a/tests/value/strings.i
+++ b/tests/value/strings.i
@@ -1,21 +1,23 @@
/* run.config*
- GCC:
- STDOPT: #"-main main1 -eva-no-builtins-auto"
- STDOPT: #"-main main6 -eva-no-builtins-auto"
- STDOPT: #"-main main7 -eva-no-builtins-auto"
- STDOPT: #"-main main8 -slevel-function strcmp:50 -eva-no-builtins-auto"
+ STDOPT: #"-eva-no-builtins-auto -eva-slevel-function strcmp:50"
*/
+
+volatile int nondet;
+
char s1[]="hello\000 world";
char s2[]="hello";
+char *s3="tutu";
+char *s4="tutu";
char *s5, *s6;
+char *s7="hello\x00 world";
+char *s8="hello";
int u(void);
char cc = 'a';
char Q, R, S, T, U, V, W, X, Y, Z;
-char *strcpy(char*dst, char*src)
-{
+char *strcpy(char*dst, char*src) {
char* ldst=dst;
/*@ loop pragma UNROLL 20; */
while (*ldst++ = *src++)
@@ -23,8 +25,7 @@ char *strcpy(char*dst, char*src)
return dst;
}
-unsigned int strlen(char *s)
-{
+unsigned int strlen(char *s) {
unsigned int l=0;
/*@ loop pragma UNROLL 20; */
while(*s++ != 0)
@@ -32,8 +33,7 @@ unsigned int strlen(char *s)
return l;
}
-int main1(void)
-{
+int string_reads() {
char *p;
p = &s1[3];
if (u()) R=*(p-4);
@@ -48,24 +48,30 @@ int main1(void)
if (u()) T=*(p-4);
{
- char a[10] = "Not ok";
- char b [5];
- if (u()) strcpy(b,a);
- }
-
+ char a[10] = "Not ok";
+ char b [5];
+ if (u()) strcpy(b,a);
+ }
+
s1[3]=cc;
s1[6]=cc;
return strlen(s1);
}
+int string_writes() {
+ char c=-1;
+ if (nondet) s5 = s3; else s5 = &c;
+ *(nondet ? s5 + 2 : &c) = 'T';
+ R=c;
+ *s5=' ';
+ if (nondet) s6 = s3+1; else s6 = &c;
+ *s6=cc;
+ c=*s4;
+ return c;
+}
-char *s3="tutu";
-char *s4="tutu";
-char *s7="hello\x00 world";
-char *s8="hello";
-int main6(void)
-{
+int string_comparison() {
char *s;
s = "toto";
cc = *s;
@@ -82,29 +88,32 @@ int main6(void)
if (u())
W = (s7 + 1 == s8 + 1);
if (u())
- X = (s3 == s3);
- s5 = (u()?s3:s8);
+ X = (s3 == s3);
+ s5 = (u()?s3:s8);
if (u())
Y = ((u()?s3:s8) == s5);
- s6 = (u()?(u()?s3:s8):s4);
+ s6 = (u()?(u()?s3:s8):s4);
if (u())
Z = (s5 == s6);
if (u())
- Q = ("oh, hello"+4 == s7);
+ Q = ("oh, hello"+4 == s7);
return cc;
}
-int main7(int d, int e, int f)
-{
- char c=-1;
- if (d) s5 = s3; else s5 = &c;
- *(f ? s5 + 2 : &c) = 'T';
- R=c;
- *s5=' ';
- if (e) s6 = s3+1; else s6 = &c;
- *s6=cc;
- c=*s4;
- return c;
+/* Currently, Eva does not support wide string comparisons: alarms are emitted
+ on any comparison involving a wide string. Tests are minimal for now. */
+int wide_string_comparison() {
+ char* w1 = L"abcdef";
+ char* w2 = L"def";
+ char* w3 = L"abc";
+ int res = 0;
+ /* Must emit a comparison alarm. */
+ if (w1 == w2)
+ res = 1;
+ /* Ideally, should not emit a comparison alarm. */
+ if (w2 == w3)
+ res = -1;
+ return res;
}
int strcmp(const char *s1, const char *s2)
@@ -117,14 +126,22 @@ int strcmp(const char *s1, const char *s2)
return (*(unsigned char *)s1 - *(unsigned char *)--s2);
}
-
//@ assigns p[0..s-1]; ensures \initialized(&p[0..s-1]);
void assigns(char *p, unsigned int s);
-int main8() {
+int long_chain() {
char tc[30];
char long_chain[] = "really really really long chain";
assigns(&tc[0],30);
int x = strcmp(long_chain, tc);
return x;
}
+
+
+void main() {
+ string_reads ();
+ string_writes ();
+ string_comparison ();
+ wide_string_comparison ();
+ long_chain ();
+}
diff --git a/tests/value/unit_tests.i b/tests/value/unit_tests.i
new file mode 100644
index 0000000000000000000000000000000000000000..f480093ba099eda06a2fdca943402b02945c5cce
--- /dev/null
+++ b/tests/value/unit_tests.i
@@ -0,0 +1,7 @@
+/* run.config
+ MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT:
+*/
+/* run.config*
+ DONTRUN:
+*/
diff --git a/tests/value/unit_tests.ml b/tests/value/unit_tests.ml
new file mode 100644
index 0000000000000000000000000000000000000000..48e3b3405bcb13af995b3a50f15aebaa64b09b54
--- /dev/null
+++ b/tests/value/unit_tests.ml
@@ -0,0 +1,3 @@
+(* Programmatic tests of Eva, run by unit_tests.i. *)
+
+let () = Db.Main.extend Eva.Unit_tests.run