From 1094023d5291725f900e65ba8b3f2481dbd5db02 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 12 Jun 2012 09:09:41 +0000
Subject: [PATCH] [e-acsl] synchronizing with trunk + trying to fix share
 directory issue

---
 src/plugins/e-acsl/Makefile.in                |  7 +------
 src/plugins/e-acsl/env.ml                     |  9 +++++++-
 src/plugins/e-acsl/options.ml                 |  1 +
 .../e-acsl-runtime/oracle/at.1.res.oracle     | 21 +++++++------------
 .../tests/e-acsl-runtime/oracle/at.res.oracle | 21 +++++++------------
 .../oracle/comparison.1.res.oracle            |  3 +--
 .../oracle/comparison.res.oracle              |  3 +--
 .../oracle/other_constants.1.res.oracle       |  3 +--
 .../oracle/other_constants.res.oracle         |  3 +--
 src/plugins/e-acsl/visit.ml                   |  6 +++---
 10 files changed, 31 insertions(+), 46 deletions(-)

diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index df879e37fc5..71481fe42d5 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -200,15 +200,10 @@ include $(FRAMAC_SHARE)/Makefile.dynamic
 
 ifeq (@MAY_RUN_TESTS@,yes)
 
-ifeq ($(FRAMAC_INTERNAL),yes)
-SHARE:=-e-acsl-share ./share/e-acsl
-else
-SHARE:=
-endif
 $(E_ACSL_DIR)/tests/test_config: $(E_ACSL_DIR)/tests/test_config.in \
 				$(E_ACSL_DIR)/Makefile
 	$(PRINT_MAKING) $@
-	$(SED) -e "s|@SHARE@|$(SHARE)|g" \
+	$(SED) -e "s|@SHARE@|-e-acsl-share $(E_ACSL_DIR)/share/e-acsl|g" \
 	       -e "s|@SEDCMD@|`which sed `|g" $< > $@
 
 endif
diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index cff5b2751d6..61f4be606ac 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -228,12 +228,19 @@ let current_kf env =
 
 let get_visitor env = env.visitor
 
+let emitter = 
+  Emitter.create
+    "E-ACSL" 
+    [ Emitter.Code_annot ] 
+    ~correctness:[ Options.Gmp_only.parameter ]
+    ~tuning:[]
+
 let add_assert env stmt annot = 
   match current_kf env with
   | None -> assert false (* TODO: ??? *)
   | Some kf ->
     Queue.add
-      (fun () -> Annotations.add_assert kf stmt [ !global_state ] annot) 
+      (fun () -> Annotations.add_assert emitter ~kf stmt annot) 
       env.visitor#get_filling_actions
 
 let add_stmt env stmt =
diff --git a/src/plugins/e-acsl/options.ml b/src/plugins/e-acsl/options.ml
index c64541b82ec..235be390b24 100644
--- a/src/plugins/e-acsl/options.ml
+++ b/src/plugins/e-acsl/options.ml
@@ -20,6 +20,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+let () = Plugin.is_share_visible ()
 module P = Plugin.Register
   (struct
      let name = "E-ACSL"
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
index 39f2d61baa6..90b103f4ab3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
@@ -92,8 +92,7 @@ PROJECT_FILE.i:258:[value] Assertion got status valid.
 [value] computing for function __gmpz_clear <- f <- main.
         Called from PROJECT_FILE.i:268.
 [value] Done for function __gmpz_clear
-PROJECT_FILE.i:272:[value] cannot evaluate ACSL term,
-        unsupported ACSL construct: \at() on a C label
+PROJECT_FILE.i:272:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
 PROJECT_FILE.i:272:[value] Assertion got status unknown.
 [value] computing for function __gmpz_init_set_si <- f <- main.
         Called from PROJECT_FILE.i:277.
@@ -134,8 +133,7 @@ PROJECT_FILE.i:286:[value] Assertion got status valid.
 [value] computing for function __gmpz_clear <- f <- main.
         Called from PROJECT_FILE.i:297.
 [value] Done for function __gmpz_clear
-PROJECT_FILE.i:301:[value] cannot evaluate ACSL term,
-        unsupported ACSL construct: \at() on a C label
+PROJECT_FILE.i:301:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
 PROJECT_FILE.i:301:[value] Assertion got status unknown.
 [value] computing for function __gmpz_init_set_si <- f <- main.
         Called from PROJECT_FILE.i:306.
@@ -178,8 +176,7 @@ PROJECT_FILE.i:301:[value] Assertion got status unknown.
 PROJECT_FILE.i:242:[value] Function f: postcondition got status valid.
 [value] Recording results for f
 [value] Done for function f
-PROJECT_FILE.i:429:[value] cannot evaluate ACSL term,
-        unsupported ACSL construct: \at() on a C label
+PROJECT_FILE.i:429:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
 PROJECT_FILE.i:429:[value] Assertion got status unknown.
 [value] computing for function __gmpz_init_set_si <- main.
         Called from PROJECT_FILE.i:434.
@@ -200,8 +197,7 @@ PROJECT_FILE.i:429:[value] Assertion got status unknown.
 [value] computing for function __gmpz_clear <- main.
         Called from PROJECT_FILE.i:439.
 [value] Done for function __gmpz_clear
-PROJECT_FILE.i:443:[value] cannot evaluate ACSL term,
-        unsupported ACSL construct: \at() on a C label
+PROJECT_FILE.i:443:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
 PROJECT_FILE.i:443:[value] Assertion got status unknown.
 [value] computing for function __gmpz_init_set_si <- main.
         Called from PROJECT_FILE.i:447.
@@ -216,8 +212,7 @@ PROJECT_FILE.i:443:[value] Assertion got status unknown.
 [value] computing for function __gmpz_clear <- main.
         Called from PROJECT_FILE.i:450.
 [value] Done for function __gmpz_clear
-PROJECT_FILE.i:454:[value] cannot evaluate ACSL term,
-        unsupported ACSL construct: \at() on a C label
+PROJECT_FILE.i:454:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
 PROJECT_FILE.i:454:[value] Assertion got status unknown.
 [value] computing for function __gmpz_init_set_si <- main.
         Called from PROJECT_FILE.i:460.
@@ -249,8 +244,7 @@ PROJECT_FILE.i:454:[value] Assertion got status unknown.
 [value] Done for function __gmpz_clear
 [value] computing for function g <- main.
         Called from PROJECT_FILE.i:472.
-PROJECT_FILE.i:351:[value] cannot evaluate ACSL term,
-        unsupported ACSL construct: \at() on a C label
+PROJECT_FILE.i:351:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
 PROJECT_FILE.i:351:[value] Assertion got status unknown.
 [value] computing for function __gmpz_init_set_si <- g <- main.
         Called from PROJECT_FILE.i:356.
@@ -271,8 +265,7 @@ PROJECT_FILE.i:351:[value] Assertion got status unknown.
 [value] computing for function __gmpz_clear <- g <- main.
         Called from PROJECT_FILE.i:362.
 [value] Done for function __gmpz_clear
-PROJECT_FILE.i:367:[value] cannot evaluate ACSL term,
-        unsupported ACSL construct: \at() on a C label
+PROJECT_FILE.i:367:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
 PROJECT_FILE.i:367:[value] Assertion got status unknown.
 [value] computing for function __gmpz_init_set_si <- g <- main.
         Called from PROJECT_FILE.i:373.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
index 01e4d9a8f5f..82cd984dc01 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
@@ -22,8 +22,7 @@ PROJECT_FILE.i:258:[value] Assertion got status valid.
         Called from PROJECT_FILE.i:259.
 [value] Recording results for e_acsl_assert
 [value] Done for function e_acsl_assert
-PROJECT_FILE.i:261:[value] cannot evaluate ACSL term,
-        unsupported ACSL construct: \at() on a C label
+PROJECT_FILE.i:261:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
 PROJECT_FILE.i:261:[value] Assertion got status unknown.
 [value] computing for function e_acsl_assert <- f <- main.
         Called from PROJECT_FILE.i:262.
@@ -34,8 +33,7 @@ PROJECT_FILE.i:264:[value] Assertion got status valid.
         Called from PROJECT_FILE.i:266.
 [value] Recording results for e_acsl_assert
 [value] Done for function e_acsl_assert
-PROJECT_FILE.i:268:[value] cannot evaluate ACSL term,
-        unsupported ACSL construct: \at() on a C label
+PROJECT_FILE.i:268:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
 PROJECT_FILE.i:268:[value] Assertion got status unknown.
 [value] computing for function e_acsl_assert <- f <- main.
         Called from PROJECT_FILE.i:269.
@@ -48,22 +46,19 @@ PROJECT_FILE.i:268:[value] Assertion got status unknown.
 PROJECT_FILE.i:242:[value] Function f: postcondition got status valid.
 [value] Recording results for f
 [value] Done for function f
-PROJECT_FILE.i:328:[value] cannot evaluate ACSL term,
-        unsupported ACSL construct: \at() on a C label
+PROJECT_FILE.i:328:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
 PROJECT_FILE.i:328:[value] Assertion got status unknown.
 [value] computing for function e_acsl_assert <- main.
         Called from PROJECT_FILE.i:329.
 [value] Recording results for e_acsl_assert
 [value] Done for function e_acsl_assert
-PROJECT_FILE.i:331:[value] cannot evaluate ACSL term,
-        unsupported ACSL construct: \at() on a C label
+PROJECT_FILE.i:331:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
 PROJECT_FILE.i:331:[value] Assertion got status unknown.
 [value] computing for function e_acsl_assert <- main.
         Called from PROJECT_FILE.i:332.
 [value] Recording results for e_acsl_assert
 [value] Done for function e_acsl_assert
-PROJECT_FILE.i:335:[value] cannot evaluate ACSL term,
-        unsupported ACSL construct: \at() on a C label
+PROJECT_FILE.i:335:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
 PROJECT_FILE.i:335:[value] Assertion got status unknown.
 [value] computing for function e_acsl_assert <- main.
         Called from PROJECT_FILE.i:336.
@@ -71,15 +66,13 @@ PROJECT_FILE.i:335:[value] Assertion got status unknown.
 [value] Done for function e_acsl_assert
 [value] computing for function g <- main.
         Called from PROJECT_FILE.i:339.
-PROJECT_FILE.i:296:[value] cannot evaluate ACSL term,
-        unsupported ACSL construct: \at() on a C label
+PROJECT_FILE.i:296:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
 PROJECT_FILE.i:296:[value] Assertion got status unknown.
 [value] computing for function e_acsl_assert <- g <- main.
         Called from PROJECT_FILE.i:297.
 [value] Recording results for e_acsl_assert
 [value] Done for function e_acsl_assert
-PROJECT_FILE.i:301:[value] cannot evaluate ACSL term,
-        unsupported ACSL construct: \at() on a C label
+PROJECT_FILE.i:301:[value] cannot evaluate ACSL term, unsupported ACSL construct: \at() on a C label
 PROJECT_FILE.i:301:[value] Assertion got status unknown.
 [value] computing for function e_acsl_assert <- g <- main.
         Called from PROJECT_FILE.i:303.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
index acdc0b586bf..4d3126edad2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
@@ -96,8 +96,7 @@ PROJECT_FILE.i:306:[value] Assertion got status valid.
 PROJECT_FILE.i:231:[value] Function e_acsl_assert: precondition got status valid.
 [value] Recording results for e_acsl_assert
 [value] Done for function e_acsl_assert
-PROJECT_FILE.i:309:[value] cannot evaluate ACSL term,
-        unsupported ACSL construct: unsupported ACSL construct "toto"
+PROJECT_FILE.i:309:[value] cannot evaluate ACSL term, unsupported ACSL construct: constant strings
 PROJECT_FILE.i:309:[value] Assertion got status unknown.
 [value] computing for function e_acsl_assert <- main.
         Called from PROJECT_FILE.i:310.
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 a1c62138e59..4d878792f9c 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
@@ -28,8 +28,7 @@ PROJECT_FILE.i:262:[value] Assertion got status valid.
         Called from PROJECT_FILE.i:263.
 [value] Recording results for e_acsl_assert
 [value] Done for function e_acsl_assert
-PROJECT_FILE.i:265:[value] cannot evaluate ACSL term,
-        unsupported ACSL construct: unsupported ACSL construct "toto"
+PROJECT_FILE.i:265:[value] cannot evaluate ACSL term, unsupported ACSL construct: constant strings
 PROJECT_FILE.i:265:[value] Assertion got status unknown.
 [value] computing for function e_acsl_assert <- main.
         Called from PROJECT_FILE.i:266.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
index f8580d0ae21..7c8b6eeb8e1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
@@ -2,8 +2,7 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-PROJECT_FILE.i:248:[value] cannot evaluate ACSL term,
-        unsupported ACSL construct: unsupported ACSL construct "toto"
+PROJECT_FILE.i:248:[value] cannot evaluate ACSL term, unsupported ACSL construct: constant strings
 PROJECT_FILE.i:248:[value] Assertion got status unknown.
 [value] computing for function e_acsl_assert <- main.
         Called from PROJECT_FILE.i:249.
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 2ff86ae97cd..4cb2ebcb675 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
@@ -2,8 +2,7 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-PROJECT_FILE.i:248:[value] cannot evaluate ACSL term,
-        unsupported ACSL construct: unsupported ACSL construct "toto"
+PROJECT_FILE.i:248:[value] cannot evaluate ACSL term, unsupported ACSL construct: constant strings
 PROJECT_FILE.i:248:[value] Assertion got status unknown.
 [value] computing for function e_acsl_assert <- main.
         Called from PROJECT_FILE.i:249.
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index d3826d9bbaa..4e1ca198c5e 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -663,7 +663,7 @@ class e_acsl_visitor prj generate = object (self)
       funspec :=
 	Cil.visitCilFunspec
 	(self :> Cil.cilVisitor)
-	(Kernel_function.get_spec old_kf);
+	(Annotations.funspec old_kf);
       DoChildren
     with Not_found ->
       (* function without code *)
@@ -712,8 +712,8 @@ class e_acsl_visitor prj generate = object (self)
     (* [TODO] potential BUG HERE since the annotations tbl is the one of the old
        project. *)
     let env, new_annots =
-      Annotations.single_fold_stmt
-	(fun (User old_a | AI(_, old_a)) (env, new_annots) -> 
+      Annotations.fold_code_annot
+	(fun _ (User old_a | AI(_, old_a)) (env, new_annots) -> 
 	  let a =
             (* [VP] Don't use Visitor here, as it will fill the
 	       queue in the middle of the computation... *)
-- 
GitLab