diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index df879e37fc5588ebc14d1521f7a0e7a596ae45c8..71481fe42d5b94cb94e1b92a455fef88d93b54f5 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 cff5b2751d6e1d20bd6803911f6013654ee1eac1..61f4be606ac1bc1982de97a220820b64db4f2fda 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 c64541b82ecbbc07f098337e2312bf23862acbb5..235be390b24e20a76e23edb05c69b4bced3a43b1 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 39f2d61baa64f8842d39ce9a5b04d152b5cbe9da..90b103f4ab3bb6b8538f9cca42c1b20dcba5f459 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 01e4d9a8f5f556e83ddb826c9ec1b175fb6bc418..82cd984dc01d37dd7884793ee7e51b03af8af463 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 acdc0b586bf4ec2067b9065715e9de7b24d2d1ab..4d3126edad2404a047f7c9a19c50306e8b18a764 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 a1c62138e59dcfbe0e1b2b1cb74a880bc1b44004..4d878792f9c46daaee5a612e589fb70b5be276b4 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 f8580d0ae210f70a9ce4fd2bb4984bd602757c5c..7c8b6eeb8e15c09e3507a5fd5536863ca0805d28 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 2ff86ae97cd59caf91cf3b77f9474966bca8649d..4cb2ebcb6756ee733addd7fc7bc80780016b0a6e 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 d3826d9bbaae36cb593578eaff0cf2c5061f5383..4e1ca198c5e152fe41b2e6a6e0edc87e4f9cddec 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... *)