From aeb135661fcce192ff787aae429c766b33d9069d Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 1 Jun 2011 12:47:14 +0000
Subject: [PATCH] update according to kernel changes + -warn-error
---
src/plugins/e-acsl/Makefile.in | 12 ++++++++++++
.../tests/e-acsl-runtime/oracle/addrOf.res.oracle | 2 --
.../tests/e-acsl-runtime/oracle/arith.res.oracle | 2 --
.../tests/e-acsl-runtime/oracle/cast.res.oracle | 2 --
.../e-acsl-runtime/oracle/comparison.res.oracle | 2 --
.../tests/e-acsl-runtime/oracle/false.res.oracle | 2 --
.../oracle/integer_constant.res.oracle | 2 --
.../tests/e-acsl-runtime/oracle/lazy.res.oracle | 2 --
.../oracle/nested_code_annot.res.oracle | 2 --
.../tests/e-acsl-runtime/oracle/not.res.oracle | 2 --
.../e-acsl-runtime/oracle/other_constants.res.oracle | 2 --
.../tests/e-acsl-runtime/oracle/sizeof.res.oracle | 2 --
.../tests/e-acsl-runtime/oracle/true.res.oracle | 2 --
src/plugins/e-acsl/visit.ml | 1 +
14 files changed, 13 insertions(+), 24 deletions(-)
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 1e2d56fb993..0b4ee5f8e64 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 f5299d613e3..053bf7e9d44 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 29c479093c4..12974be380e 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 56926dd1239..3528b36ac7d 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 1dbd4b98860..c9ad92ac929 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 b08ec201003..24253371af6 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 a5656a25923..7c32de6c332 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 f94afe6073f..2ec30eb619b 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 fa6ef018fe6..18513fdc127 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 284b88b7f17..eb0e616ce0c 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 746755d7444..f0a4498c942 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 40c2d4ed02d..8da14fb3b3c 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 33ec1631826..44d1237a75d 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 5cff01c8156..503da378af1 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
--
GitLab