diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index 1e2d56fb9935e243654b7e3b948e0db4a1127595..0b4ee5f8e644c949701383da3e72b66aed620391 100644 --- a/src/plugins/e-acsl/Makefile.in +++ b/src/plugins/e-acsl/Makefile.in @@ -34,7 +34,19 @@ PLUGIN_DYNAMIC:=@DYNAMIC_E_ACSL@ PLUGIN_NAME:=E_ACSL PLUGIN_CMO:= local_config options read_header misc mpz env visit main PLUGIN_HAS_MLI:=yes + +# Enable -warn-error, but do not distribute the plug-in with this option being +# activated +ifeq ($(HAS_OCAML312),yes) +DEV_FLAGS=-warn-error +a +else +DEV_FLAGS=-warn-error A +endif +PLUGIN_BFLAGS:=$(DEV_FLAGS) +PLUGIN_OFLAGS:=$(DEV_FLAGS) + PLUGIN_DISTRIBUTED:=no + PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure PLUGIN_DISTRIB_BIN:=no PLUGIN_GENERATED:= $(PLUGIN_DIR)/local_config.ml diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle index f5299d613e3215ab39503336f464d4ec95178b3a..053bf7e9d44ac221abbbadbf1a9212398ec30abf 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle @@ -5,8 +5,6 @@ PROJECT_FILE.i:122:[value] Assertion got status valid. [value] Recording results for main [value] done for function main -[dominators] computing for function main -[dominators] done for function main [value] ====== VALUES COMPUTED ====== [value] Values for function main: __retres ∈ {0} diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle index 29c479093c4afd62dae6b494153f1df815a24f58..12974be380e8a566651605cb672623a3ce66026d 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle @@ -773,8 +773,6 @@ PROJECT_FILE.i:115:[from] Non terminating function (no dependencies) [from] Done for function mpz_cdiv_q [from] Computing for function mpz_mod_ui [from] Done for function mpz_mod_ui -[dominators] computing for function main -[dominators] done for function main [value] ====== VALUES COMPUTED ====== [value] Values for function e_acsl_fail: NON TERMINATING FUNCTION diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle index 56926dd12392cb6357b6be7e201545d163c7f0fc..3528b36ac7db878498df716ce13ed77a7f0f2f4a 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle @@ -6,8 +6,6 @@ PROJECT_FILE.i:124:[value] Assertion got status valid. PROJECT_FILE.i:127:[value] Assertion got status valid. [value] Recording results for main [value] done for function main -[dominators] computing for function main -[dominators] done for function main [value] ====== VALUES COMPUTED ====== [value] Values for function main: __retres ∈ {0} diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle index 1dbd4b98860ea4b5c9ff03ff22c36f0ba0883933..c9ad92ac9296f62f4995ca4c0114a22dfc13ead7 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle @@ -235,8 +235,6 @@ PROJECT_FILE.i:115:[from] Non terminating function (no dependencies) [from] Done for function e_acsl_fail [from] Computing for function mpz_clear [from] Done for function mpz_clear -[dominators] computing for function main -[dominators] done for function main [value] ====== VALUES COMPUTED ====== [value] Values for function e_acsl_fail: NON TERMINATING FUNCTION diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle index b08ec2010033d4ad68c82dc24e3eb38d143497b8..24253371af660236be11f86766760b03bb1a3143 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle @@ -4,8 +4,6 @@ [value] Values of globals at initialization [value] Recording results for main [value] done for function main -[dominators] computing for function main -[dominators] done for function main [value] ====== VALUES COMPUTED ====== [value] Values for function main: __retres ∈ {0} diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle index a5656a259232c0bebe4153ce01544d7d9c1073c1..7c32de6c3323d5d843c99e5650cd727ead9a1939 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle @@ -104,8 +104,6 @@ PROJECT_FILE.i:115:[from] Non terminating function (no dependencies) [from] Done for function mpz_clear [from] Computing for function mpz_init_set_str [from] Done for function mpz_init_set_str -[dominators] computing for function main -[dominators] done for function main [value] ====== VALUES COMPUTED ====== [value] Values for function e_acsl_fail: NON TERMINATING FUNCTION diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle index f94afe6073f04783b675eeb967d625bf22413e4c..2ec30eb619bc6f7fbe1746b6679df212b66d8e88 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle @@ -267,8 +267,6 @@ PROJECT_FILE.i:115:[from] Non terminating function (no dependencies) [from] Done for function mpz_init_set_ui [from] Computing for function mpz_init [from] Done for function mpz_init -[dominators] computing for function main -[dominators] done for function main [value] ====== VALUES COMPUTED ====== [value] Values for function e_acsl_fail: NON TERMINATING FUNCTION diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle index fa6ef018fe6f6711d9822205ab3d1a66bce1db9e..18513fdc127e40021e4ccfdb4565958e333abd48 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle @@ -175,8 +175,6 @@ PROJECT_FILE.i:115:[from] Non terminating function (no dependencies) [from] Done for function e_acsl_fail [from] Computing for function mpz_clear [from] Done for function mpz_clear -[dominators] computing for function main -[dominators] done for function main [value] ====== VALUES COMPUTED ====== [value] Values for function e_acsl_fail: NON TERMINATING FUNCTION diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle index 284b88b7f17f480cf648c46434baf59ccc8df55e..eb0e616ce0c6ec66de325c01094f5c25bfaaa1a2 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle @@ -5,8 +5,6 @@ PROJECT_FILE.i:122:[value] Assertion got status valid. [value] Recording results for main [value] done for function main -[dominators] computing for function main -[dominators] done for function main [value] ====== VALUES COMPUTED ====== [value] Values for function main: __retres ∈ {0} diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle index 746755d74446d382a5c8b7de21cc89aaff989802..f0a4498c9421ad4f29ea0c75a4c4b82bb466e69e 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle @@ -51,8 +51,6 @@ PROJECT_FILE.i:115:[from] Non terminating function (no dependencies) [from] Done for function e_acsl_fail [from] Computing for function mpz_clear [from] Done for function mpz_clear -[dominators] computing for function main -[dominators] done for function main [value] ====== VALUES COMPUTED ====== [value] Values for function e_acsl_fail: NON TERMINATING FUNCTION diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle index 40c2d4ed02de5d21ce1042f0eecc42f0e7d6917b..8da14fb3b3c6dbeb84a6a5db79811583918841f1 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle @@ -6,8 +6,6 @@ PROJECT_FILE.i:121:[value] Assertion got status valid. PROJECT_FILE.i:124:[value] Assertion got status valid. [value] Recording results for main [value] done for function main -[dominators] computing for function main -[dominators] done for function main [value] ====== VALUES COMPUTED ====== [value] Values for function main: x ∈ {0} diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle index 33ec1631826643fb4ac9c02105ded5de1ca7cb80..44d1237a75d1d21d3d5c4acf1570cff142a3e3e2 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle @@ -5,8 +5,6 @@ PROJECT_FILE.i:122:[value] Assertion got status valid. [value] Recording results for main [value] done for function main -[dominators] computing for function main -[dominators] done for function main [value] ====== VALUES COMPUTED ====== [value] Values for function main: __retres ∈ {0} diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml index 5cff01c8156b74d7bcb315f615c6d7f03e991dd8..503da378af1bdace0a96f6b4dbd16af4c4298978 100644 --- a/src/plugins/e-acsl/visit.ml +++ b/src/plugins/e-acsl/visit.ml @@ -263,6 +263,7 @@ let rec named_predicate_to_exp env p = | Pvalid_range _ -> Misc.not_yet "\\valid_range" | Pfresh _ -> Misc.not_yet "\\fresh" | Psubtype _ -> Misc.not_yet "subtyping relation" + | Pinitialized _ -> Misc.not_yet "\\initialized" (* ************************************************************************** *) (* [convert_*] converts a given ACSL annotation into the corresponding C