diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h
index 6cc1a782efda5697df633cd2724aaf60b78eaf92..8e0abca525ef72a6df812d0d7f33ca81974d730d 100644
--- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h
+++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h
@@ -37,7 +37,7 @@
     becomes unsound.
     TODO: may only happen for annotations containing memory-related properties.
     For arithmetic properties, the verdict is always sound (?). */
-extern int eacsl_runtime_sound_verdict;
+extern int __attribute__((FC_BUILTIN)) eacsl_runtime_sound_verdict;
 
 /*! \brief Runtime assertion verifying a given predicate
  *  \param pred  integer code of a predicate
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index 03412904536ad3accfd326822f958609c0bfc1cf..246dd0b7c06fada5a1b973f8160e64a15e7051cf 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -357,8 +357,11 @@ let sound_verdict_vi =
      let vi = Cil.makeGlobalVar name Cil.intType in
      vi.vstorage <- Extern;
      vi.vreferenced <- true;
+     vi.vattr <- Cil.addAttribute (Attr ("FC_BUILTIN", [])) vi.vattr;
      vi)
 
+let sound_verdict () = Lazy.force sound_verdict_vi
+
 let is_variadic_function vi = match Cil.unrollType vi.vtype with
   | TFun(_, _, variadic, _) -> variadic
   | _ -> false
@@ -460,14 +463,11 @@ let prepare_file file =
   let rev_globals, new_defs =
     List.fold_left prepare_global ([], []) file.globals
   in
-  match new_defs with
-  | [] -> ()
-  | _ :: _ ->
-    (* insert the new_definitions at the end and reverse back the globals *)
-    let globals = List.fold_left (fun acc g -> g :: acc) new_defs rev_globals in
-    (* insert [__e_acsl_sound_verdict] at the beginning *)
-    let sg = GVarDecl(Lazy.force sound_verdict_vi, Location.unknown) in
-    file.globals <- sg :: globals
+  (* insert the new_definitions at the end and reverse back the globals *)
+  let globals = List.fold_left (fun acc g -> g :: acc) new_defs rev_globals in
+  (* insert [__e_acsl_sound_verdict] at the beginning *)
+  let sg = GVarDecl(Lazy.force sound_verdict_vi, Location.unknown) in
+  file.globals <- sg :: globals
 
 let prepare () =
   Options.feedback ~level:2 "prepare AST for E-ACSL transformations";
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
index 65ea62daf1854443f8523737c7f519d9e18e9dd6..ba19b9099225af2b839a2a14c018b5f39699ccca 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
@@ -28,7 +28,14 @@
     - in case of temporal validity checks, adding the attribute "aligned" to
       variables that are not sufficiently aligned. *)
 
+open Cil_types
+
 val prepare: unit -> unit
+(** Prepare the AST *)
+
+val sound_verdict: unit -> varinfo
+(** @return the [varinfo] representing the E-ACSL global variable that indicates
+    whether the verdict emitted by E-ACSL is sound. *)
 
 (*
 Local Variables:
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_arith.c b/src/plugins/e-acsl/tests/arith/oracle/gen_arith.c
index 5ce6877d82a476d998be85727df53fe21e51b893..b5265e84689baf60970908ecedb04ac709995ca4 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_arith.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_array.c b/src/plugins/e-acsl/tests/arith/oracle/gen_array.c
index 645c58424351419e826f56c1e82acc48cdb9323f..a559df9509be6126a04b2fd99afee5802bcd06ce 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_array.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_array.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int T1[3];
 int T2[4];
 void arrays(void)
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_at.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
index c8e5107e1e1f4b4b1be200b7be19f6441c5fed5b..e366ee59e16590f960eed506947d418c24054c28 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 int A = 0;
 /*@ ensures \at(A,Post) 鈮� 3; */
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
index 46951ce87513b423dadef689c42e265455fe0090..0cde64feb6c6745954e0305b2062da612cd23daa 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ ensures
       鈭€ 鈩� n;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c b/src/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c
index 54340192b07b7754f52a4ea9b5bef4152f4659d7..a421b3f34be98f1262171bae25bb49543f502d90 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void f_signed(int a, int b)
 {
   int c = a << 2;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_cast.c b/src/plugins/e-acsl/tests/arith/oracle/gen_cast.c
index b41c0d12d81d3df99b65d279b82ee7f56f21f45a..c63917398ce804719d214b63f16611b26dde0abd 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_cast.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_cast.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/arith/oracle/gen_comparison.c
index f28ab0ad20bdcf0b3982e755a344599f45a457ad..896c9741e9e3f85ef4c5b4514957d95dd66fefa9 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_comparison.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
index 8c84d1d06f78e6f23a4143d4c57e5af2b74f32d6..01bee92554d4ba9b4a1afdffd46105c24119d22f 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 struct mystruct {
    int k ;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
index b766248de7c8fd4d07f231228583ebb240bd00a3..db81ac4861afcc39d08be6801e059e5487d9da9b 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 /*@ logic 鈩� f1(鈩� n) = n 鈮� 0? 0: f1(n - 1) + n;
 
 */
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c
index 323698c0e1bb72d4549223c8810ed2c8a0add9e7..096a8cd3446a6c4be1db87566422c47b0b779115 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_let.c b/src/plugins/e-acsl/tests/arith/oracle/gen_let.c
index e2cdd5cf8775e54a96933bd51ba247480c1c2f88..fc1286401944a1619be841a2955b31bc529a9863 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_let.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_let.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 struct __anonstruct_r_1 {
    int x ;
    int y ;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_longlong.c b/src/plugins/e-acsl/tests/arith/oracle/gen_longlong.c
index 21f7073ae453abd87367cfa6774390b8b8e87753..0f5ccda83561746d941997379e9f0036da97727c 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_longlong.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 unsigned long long my_pow(unsigned int x, unsigned int n)
 {
   unsigned long long __retres;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_not.c b/src/plugins/e-acsl/tests/arith/oracle/gen_not.c
index e3add3ad4d530e0529a9ee3407e386df906e17b8..2d7529f38a85bb12e2e44733e6e42c645db55bb7 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_not.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_not.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
index f84cfba6458ecf2235e9cef3f3a2156c4237bff1..ccb7b6be6c70a0c451370dc96bd0c040840da300 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 /*@
 predicate p1(鈩� i, 鈩� j, 鈩� k) =
   0 鈮� i < 10 鈭� 1 < j 鈮� 11 鈭� 2 鈮� k 鈮� 12;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c b/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
index 7f3061dd52d69fc9629598966f3b69636c1a45fa..48483e5005eb25658b1c6445273aa9f38fe1ba7f 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ ensures \let delta = 1;
       \let avg_real = (\old(a) + \old(b)) / 2;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c b/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c
index 79eefaaa977b91903db1f67c99e2ab676614acce..5e70777069f3e532c1c5d602600e2824a295e93b 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
index 4ec7740d794c29be57fde5711f7d5b0a3ab0cd77..ef6ec87ac427333fcee748159cf6993c89461ecf 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 struct msgA {
    int type ;
    int a[2] ;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index 2712efec6e0b9af270b4a9e7a5765befb2f546d8..1f57c1264523dccaf72db598e93285e3c4e267f4 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ requires \valid(Mtmax_in);
     requires \valid(Mwmax);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
index 13ed0297405f65dfe311bba7774f244843545953..c5b6665908d3ef321c781e0f937751855faea388 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ behavior yes:
       assumes 鈭€ int i; 0 < i < n 鈬� *(t + (i - 1)) 鈮� *(t + i);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
index c8bbc5d7f696dbaad60a728c4422bd85e32e8fe5..e4ce2b0300f7f706214481bd5aebe66730f3fdd7 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 typedef int ArrayInt[5];
 /*@ ensures
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1386_complex_flowgraph.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1386_complex_flowgraph.c
index 02552add425756b02c26807c25d7ffb1cac95659..1b997cf7e674d9090b7b2d3ef1c870a9f539a731 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1386_complex_flowgraph.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1386_complex_flowgraph.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void duffcopy(char *to, char *from, int count)
 {
   __e_acsl_store_block((void *)(& from),(size_t)8);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
index c2f45cea322e293d26571b0d08951a4fc69d3281..3b092ae6734c01a72b86c39495bbafe588b7b386 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -4,7 +4,7 @@
 #include "stdlib.h"
 char *__gen_e_acsl_literal_string;
 char *__gen_e_acsl_literal_string_2;
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ behavior exists:
       assumes 鈭� 鈩� i; 0 鈮� i < (int)n 鈭� (int)*((char *)buf + i) 鈮� c;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
index 7ffe91bbde5d7c8b8cc2d47711157452d4ab25d5..43a7af62321ad4c751529a56682cc17359f4d944 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ requires n > 0; */
 int __gen_e_acsl_fact(int n);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
index b2502604424c79e5576efefd1144796c64e6b129..1709bdc247e2c455a34cd1ea655f48e80062dda7 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 char *__gen_e_acsl_literal_string;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void __e_acsl_globals_init(void)
 {
   static char __e_acsl_already_run = 0;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
index bf9d598f181b32139925c72b5a3bcd8411c40411..35354e15a4a3ee1319c32cb1f7bf4ddc15c63cf0 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 struct spongeStateStruct {
    unsigned char __attribute__((__aligned__(32))) state[1600 / 8] ;
    unsigned char __attribute__((__aligned__(32))) dataQueue[1536 / 8] ;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
index 2abb8670fe03f71bfe75a0a6d99f242edfba2885..db165cf968b0feb27509a9dc850f350451db638a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 int global_i;
 
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
index 87055c52db17464bcb1f6fbdb560cbf9ebdab401..8693ba5674dc21b587de1116c5b1435728d596ba 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 struct toto {
    
 };
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
index 8eeb9dfe8635b8238e61cbb7a413b962fca3129e..9a2a7e9391158f898b1cba0ad1574b9f5c06437b 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
index 860f3a8a94ec642c6776bb45a82643a5ddf61958..72cbffe72fd40fbc12fa3e175543b6e7cb7afc47 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
index 33cb6770be6bfe20d329132e407d8496ca074e33..ad106a78c1acd219b8461c1b51e26c97c631c53e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
index f99068ea384d20c4153c0d158bc6e0c3fe79f0c7..e79ccbae463cd4ea3afee5dd6424896e73a369b2 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
@@ -4,6 +4,8 @@
 char *__gen_e_acsl_literal_string_3;
 char *__gen_e_acsl_literal_string;
 char *__gen_e_acsl_literal_string_2;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 char *S = (char *)"foo";
 int f(void)
 {
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
index e5962bf77af9661d2b7a739f62ec1cb78d95337b..870b526f6088c16276eeccaae8e7d5c4227395a6 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
@@ -3,6 +3,8 @@
 #include "stdio.h"
 char *__gen_e_acsl_literal_string;
 char *__gen_e_acsl_literal_string_2;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 struct ST {
    char *str ;
    int num ;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
index 5f9a57c6e5e8b55db0f7595d66b3c6348c8fc8e0..d71a4c41cf78610b9bd88b1f2eb3f8163381ee20 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
@@ -3,7 +3,7 @@
 #include "stdio.h"
 #include "stdlib.h"
 char *__gen_e_acsl_literal_string;
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ requires valid_nptr: \valid_read(nptr);
     assigns \result;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
index 5195a4392ce024ad955a9bdf4dcab89452e2f393..4a9f3921fd81ea700be58509c3bfa0b8b8d879f3 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 long A = (long)0;
 int main(void)
 {
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
index 65224637492ba5dafa3b4f4633c0bbeea345539a..274ddffd5a5f726b17ef162602dbcbb81ab67dd7 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
@@ -4,7 +4,7 @@
 #include "stdlib.h"
 #include "string.h"
 char *__gen_e_acsl_literal_string;
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ requires valid_nstring_src: valid_read_nstring(src, n);
     requires room_nstring: \valid(dest + (0 .. n - 1));
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c
index 327af999d255e34319a0073d8f6157c59a7cc582..eb8feac0bb5ce7b32232c4c7d5651544cf1378ee 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 struct bitfields {
    int i : 2 ;
    _Bool j : 1 ;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c
index 16f7fca7437145cb0c09bf84725b312a9ad9ee0b..c14d3f8d10bbc266726a8691ce04c6bfa0351b7d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 char *__gen_e_acsl_literal_string;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void f(void const *s, int c, unsigned long n)
 {
   __e_acsl_store_block((void *)(& s),(size_t)8);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c
index 7aefc7c01edd90fdfc8d85a440001a077bc02a38..d4fccb9af3cf84d9d342d4e891e6c9d047425548 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 char const tab[];
 char t[10];
 void __e_acsl_globals_init(void)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-105.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-105.c
index 51f9bd0c5a8fe7ac9aede249eecc9c8c3f271e0e..2c8298f36dcc6d763a4cc60d01d33974af5234ef 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-105.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-105.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int f(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c
index fc022eb87e23d5d0f8d2684a78e2659c99efeb5c..3afa85d098a2e38ed8d4238474cdf1b541f9240b 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 struct X {
    int i ;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-145.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-145.c
index 5e59848212a2c447424afe0361bddb14c4548d75..a68b9bc741b31ab13eb9d5a949b3d22fdc9f8fc4 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-145.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-145.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int G = 0;
 void __e_acsl_globals_init(void)
 {
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c
index f8be21500b2e3acf531f87309718cba4c249f1fb..449ce90d451850b5c88d723862104a04baa6e899 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-149.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(int argc, char **argv)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-172.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-172.c
index fc026da4d148cc8c2687c8506992e1dae583cfd6..b6559e0ca88ee21fbfa019998a6a521e0d64e8c9 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-172.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-172.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 double d2 = 11.;
 int main(void)
 {
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c
index b83e193f02ff582da79def45864e71198e617a07..b393878b81667c3905f85884978ae39509f363f6 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 short a;
 char b(void)
 {
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c
index d703479245e0c336419a59d7edd94154720e66c1..9451a4f466ed83bd64cf3c1cbf2bd5fd64b2746b 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle
index 6ba35db71012b7ebbbcda4ab76c4f1e1901af221..e7143f3c725aded195940c498f03c556c7d0d222 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle
@@ -7,6 +7,8 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   G 鈭� {0}
+  __e_acsl_sound_verdict 鈭� [--..--]
+  __e_acsl_sound_verdict 鈭� [--..--]
   __e_acsl_heap_allocation_size 鈭� [--..--]
   __e_acsl_heap_allocated_blocks 鈭� [--..--]
   __fc_heap_status 鈭� [--..--]
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_builtin_literal_string.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_builtin_literal_string.c
index e5950f81d786a1284cf59b6880c77f26070f06d2..f457dfd771a8c76e09af205888795157c0950a05 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_builtin_literal_string.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_builtin_literal_string.c
@@ -3,6 +3,8 @@
 #include "stdio.h"
 #include "string.h"
 char *__gen_e_acsl_literal_string;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void __e_acsl_globals_init(void)
 {
   static char __e_acsl_already_run = 0;
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_builtin_literal_string_local_init.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_builtin_literal_string_local_init.c
index c3b9b764653aa7a972e75a909e458ba40db58700..93dcd481afdc60b43b20dc4f9acfe2457e4e5fc3 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_builtin_literal_string_local_init.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_builtin_literal_string_local_init.c
@@ -3,6 +3,8 @@
 #include "stdio.h"
 #include "string.h"
 char *__gen_e_acsl_literal_string;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void __e_acsl_globals_init(void)
 {
   static char __e_acsl_already_run = 0;
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
index 7fe4c9f0b8ebd55209651c6c7349fdfe2fd23df3..8fcaa4939fa2822e07db038d270f84e953eb61b6 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
@@ -38,7 +38,7 @@ char *__gen_e_acsl_literal_string_3;
 char *__gen_e_acsl_literal_string_5;
 char *__gen_e_acsl_literal_string_4;
 char *__gen_e_acsl_literal_string_7;
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ exits status: \exit_status 鈮� \old(status);
     ensures never_terminates: \false;
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
index 6b1a1141469dc4b7fa4ce39adff55d37630e04cb..4978156adb82bb9eb258f8b32483a3eac1814850 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
@@ -41,7 +41,7 @@ char *__gen_e_acsl_literal_string_2;
 char *__gen_e_acsl_literal_string_3;
 char *__gen_e_acsl_literal_string_5;
 char *__gen_e_acsl_literal_string_4;
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ exits status: \exit_status 鈮� 0;
     ensures never_terminates: \false;
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
index 3088f87001a3f77ab98f69969ba7f2f46065cce2..09d7c8aff99774f2f54b0736fe7e629c70e14bf3 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
@@ -33,7 +33,7 @@ char *__gen_e_acsl_literal_string_3;
 char *__gen_e_acsl_literal_string_5;
 char *__gen_e_acsl_literal_string_4;
 char *__gen_e_acsl_literal_string_8;
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ exits status: \exit_status 鈮� \old(status);
     ensures never_terminates: \false;
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
index 4ef82acb2bc57aa6cc37466db271b4b6cb98996c..31d35b177ab125883571d57ce33666ae24ac8e6e 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
@@ -24,7 +24,7 @@ char *__gen_e_acsl_literal_string_3;
 char *__gen_e_acsl_literal_string_5;
 char *__gen_e_acsl_literal_string_4;
 char *__gen_e_acsl_literal_string_6;
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ exits status: \exit_status 鈮� 0;
     ensures never_terminates: \false;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_acsl_check.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_acsl_check.c
index b9dd1eabfab0eb696099faf0ced112795c6a48ed..d6c33875d6093cf058a4ec369c57e8a702191643 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_acsl_check.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_acsl_check.c
@@ -2,7 +2,7 @@
 #include "stddef.h"
 #include "stdio.h"
 char *__gen_e_acsl_literal_string;
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ check requires a 鈮� 0;
     check ensures \result 鈮� 0; */
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_decrease.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_decrease.c
index f7b974205400d3cc2e7b01e80412975f1a7a9a96..35511e6a23c1c1cacc1d714f69fc6a5940764528 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_decrease.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_decrease.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 int f(int x)
 {
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_false.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_false.c
index 5a93a9a2dce0beccca152f92a0f25cca2bf23710..151b83363c85c392231098dd41f3d5b31390f78a 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_false.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_false.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c
index a04626ffba214ea1f48e194d55e679a2e1682c42..25c759f3ea90c05e3333efb2506a5c2cd92ca811 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 int X = 0;
 int Y = 2;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_ghost.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_ghost.c
index bfc28ffc41f4ddab273c7f729b8fa51709ffda1e..7077d948dbea1d2a06fa63448afb9a3a38a23086 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_ghost.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_ghost.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int G = 0;
 int *P;
 void __e_acsl_globals_init(void)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_invariant.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_invariant.c
index 9ab4056e35a884ee69ee1f9a244cac075ee73cec..6fd64a10a3a0e8c9157213a3ac76e3f998448303 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_invariant.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_invariant.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_labeled_stmt.c
index 4f408ceffc9676fec7876cd533e7ce7eb881ccaf..34b962a29c8a36cc2f3616b611250f5bfd3643fa 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_labeled_stmt.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 int X = 0;
 /*@ ensures X 鈮� 3; */
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_lazy.c
index 77e8d08ae976c83afe88e3f692fdde0fcbc1fdfc..3c90b94bef5d46b34a8e55f313501d1af4fa380a 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_lazy.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_loop.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_loop.c
index 940e40e29a2c47bdf22e0120820ba6df44afe719..a0ee038cc74acef95d0700b3fd7f0302ba180afe 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_loop.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_loop.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void simple_loop(void)
 {
   int sum = 0;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_nested_code_annot.c
index da452a0bd68e1cee37a14f81a037d5a144b758b4..7272563eed4875328c16d8a3bc65e2ee71eaa075 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_nested_code_annot.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_nested_code_annot.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_result.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_result.c
index 304ce2af9013bb7d3a830f511a6daa1d79130d59..6134b7451b42719463abda4a18903884236bb0c8 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_result.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_result.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ ensures \result 鈮� (int)(\old(x) - \old(x)); */
 int __gen_e_acsl_f(int x);
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c
index 3f4d4e1742aded9bcea40850f40020f0cc3ab3d5..46859d9e8ed08d0815cc9c57a674096b5e838124 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ requires 1 % a 鈮� 1;
     ensures 1 % \old(b) 鈮� 1;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_stmt_contract.c
index ba7d2c236ce070c6106851618e922554d5ab26ab..7b81cee7b804ad1fc0f0fd9f8e285ce744ec26c3 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_stmt_contract.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   __e_acsl_contract_t *__gen_e_acsl_contract_3;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_true.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_true.c
index d4cb624355302617e58fa695d2c900df117ec3ba..8603a3791f0c798d405a2bb2427aab63c5dee226 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_true.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_true.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_typedef.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_typedef.c
index a110449db682eacc4794823226a9f8bad9db28ba..37c835510d0afd252ff79c46964fda3048a0a0f1 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_typedef.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_typedef.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 typedef unsigned char uint8;
 int main(void)
 {
diff --git a/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c b/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c
index 84a91929a6160d6724e7ddbb1b25c723d7e60da7..4238666d02ed9e9f3feb384735ea6246bf07c528 100644
--- a/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c
+++ b/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 struct list {
    struct list *next ;
    int value ;
diff --git a/src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c
index 1d1c09c9a1c43b961399140bb92f593a82b931a4..262fe258dc2fa6b5bf8ab516b18ab188b5c87f7e 100644
--- a/src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 int A[10];
 /*@ requires 鈭€ 鈩� i; 0 鈮� i < 9 鈬� A[i] 鈮� A[i + 1];
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
index 3d7d734187d62b4f1dbc073f4ca2ffaf947356be..63106e3cbddbc2d928f20e06174ca8c03cc217b7 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
@@ -39,7 +39,7 @@ char *__gen_e_acsl_literal_string_22;
 char *__gen_e_acsl_literal_string_20;
 char *__gen_e_acsl_literal_string_17;
 char *__gen_e_acsl_literal_string_18;
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ exits status: \exit_status 鈮� \old(status);
     ensures never_terminates: \false;
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
index 6278c45241946aebba0469949eddcadb0cdab369..1e708d06d7dc588a674e6be9cd444634a801e8b7 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
@@ -350,7 +350,7 @@ char *__gen_e_acsl_literal_string_317;
 char *__gen_e_acsl_literal_string_321;
 char *__gen_e_acsl_literal_string_34;
 char *__gen_e_acsl_literal_string_323;
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ exits status: \exit_status 鈮� 0;
     ensures never_terminates: \false;
diff --git a/src/plugins/e-acsl/tests/full-mtracking/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mtracking/oracle/gen_addrOf.c
index c4ded4bb662c257e0895b3a6c562e9b8e43cf2fd..c27908a810ae4afeb3133a51443f953f0b1598e5 100644
--- a/src/plugins/e-acsl/tests/full-mtracking/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/full-mtracking/oracle/gen_addrOf.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void f(void)
 {
   int m;
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_arith.c b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_arith.c
index f16eb0400327daa187a796a76512227d0a297298..cccd91e3f09bc928795a0e758ee46b26b82f36d9 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_arith.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
index 9970dd39300ea063b00215fe732e68a4a2b4c2c7..bb8d0044c5d975a0e8109b5df77057099103af97 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 struct mystruct {
    int k ;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/memory/oracle/gen_addrOf.c
index f6fdc7f96bb07cc0aa12544d165aa0371df80fa4..a72dcdf164931adbca303c4de06fa37ed6d65c50 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_addrOf.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void f(void)
 {
   int m;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_alias.c b/src/plugins/e-acsl/tests/memory/oracle/gen_alias.c
index 98896d3553ea187b415d0d773dfb096065f173a7..9c4c45d7584536e1b3998771f7eb31599b5134d6 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_alias.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_alias.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void f(int *dest, int val)
 {
   __e_acsl_store_block((void *)(& dest),(size_t)8);
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_array_overflow.c b/src/plugins/e-acsl/tests/memory/oracle/gen_array_overflow.c
index c44a08d55f48294e4b0833b682e9584cc53e9524..9ddd7c0b569e52ac51fabaf2ece1c78ecb2847ee 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_array_overflow.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_array_overflow.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 struct dat {
    int arr[4] ;
 };
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_base_addr.c b/src/plugins/e-acsl/tests/memory/oracle/gen_base_addr.c
index b93d4f3e51c902e1ecbe8feb6e1be70c2b796bc7..df3b503ecb9c9d7a4cfecbc76de75042ff1ab23a 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_base_addr.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_base_addr.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int A[4] = {1, 2, 3, 4};
 int *PA;
 void __e_acsl_globals_init(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_block_length.c b/src/plugins/e-acsl/tests/memory/oracle/gen_block_length.c
index 3144471bf22ccaf4d163783680ae1b4609575a56..fe71ab122788e51417f97d655b22442bf014b5e4 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_block_length.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_block_length.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int A[4] = {1, 2, 3, 4};
 int *PA;
 void __e_acsl_globals_init(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_block_valid.c b/src/plugins/e-acsl/tests/memory/oracle/gen_block_valid.c
index fcd70965476d3eac65bbf64406645a2b171c9b07..9d1eaa75acfa938878e946a33853cb08b0dddcb3 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_block_valid.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_block_valid.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int A = 1;
 int B = 2;
 int C = 3;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c b/src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c
index 5a07ee12ca1bf742f5224c0b7fdaf6ab681488de..d653ef1b72cd342eedd3be2463fa125897925df7 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(int argc, char const **argv)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_call.c b/src/plugins/e-acsl/tests/memory/oracle/gen_call.c
index beb03fcadc35aa87462b519376ae44dbaab9cc8c..05cebce1b23a476393181cf9c2adfbfd1ce1d460 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_call.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_call.c
@@ -2,7 +2,7 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ ensures \valid(\result); */
 int *__gen_e_acsl_f(int *x, int *y);
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_compound_initializers.c b/src/plugins/e-acsl/tests/memory/oracle/gen_compound_initializers.c
index 938d7e789913afb56167d5da028a4f8607bf7d41..f137cea5b81d90b43b28d38a22c6fa8ef7690497 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_compound_initializers.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_compound_initializers.c
@@ -6,6 +6,8 @@ char *__gen_e_acsl_literal_string;
 char *__gen_e_acsl_literal_string_2;
 char *__gen_e_acsl_literal_string_4;
 char *__gen_e_acsl_literal_string_5;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 struct ST {
    char *str ;
    int num ;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_constructor.c b/src/plugins/e-acsl/tests/memory/oracle/gen_constructor.c
index 22920e30cf3e971afc38fc0f5f90df42bfc023b4..bbaf5eeb4f80a7ea5ef446e38b84b77330801a5d 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_constructor.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_constructor.c
@@ -4,6 +4,8 @@
 #include "stdlib.h"
 char *__gen_e_acsl_literal_string_2;
 char *__gen_e_acsl_literal_string;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void f(void) __attribute__((__constructor__));
 void f(void)
 {
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c
index 14df39c49de616b956464109a7d7354b843e1e2b..14e8e659b1d09100f4d4c310c8b0cb1b661848e7 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c
@@ -2,7 +2,7 @@
 #include "ctype.h"
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ requires c_uchar_or_eof: (0 鈮� c 鈮� 255) 鈭� c 鈮� -1;
     assigns \result;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c b/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c
index b41c28f63357760482f3f60665b17f396753a4ed..d1c746986f7c443ccb2a2be070215f3e337a211b 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void decl_in_switch(int value)
 {
   __e_acsl_store_block((void *)(& value),(size_t)4);
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c b/src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c
index 14c6e24361ffcb92a3124a8b4f6b4a157287c02f..97debe7067496c41e72d83021d6c520bfef6cc1d 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int goto_bts(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_errno.c b/src/plugins/e-acsl/tests/memory/oracle/gen_errno.c
index 2fc8b100ae8939fbad15c506c5509f0ccbadf1e2..650fa1452d15e1a37ac372f27dd49d07e088b049 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_errno.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_errno.c
@@ -3,6 +3,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void __e_acsl_globals_init(void)
 {
   static char __e_acsl_already_run = 0;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_freeable.c b/src/plugins/e-acsl/tests/memory/oracle/gen_freeable.c
index 7abd207dbcbd4c4d5cbfe4f6706e696ba27d2608..f804ef702e5b85b114de9eb6f80a4028faac9e05 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_freeable.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_freeable.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 char array[1024];
 void __e_acsl_globals_init(void)
 {
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ghost_parameters.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ghost_parameters.c
index e16ba064495c8f55c56d9c584c913cf85c3e4f38..3a4ab987b63e5b69037c11eae9ff02bad1d2c87d 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_ghost_parameters.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_ghost_parameters.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void function(int a, int b, int c, int d)
 {
   return;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_goto.c b/src/plugins/e-acsl/tests/memory/oracle/gen_goto.c
index 600b66499c294ed5e276133788835a65a661c66a..69e63b6f818cf9f048e19ccc325f7da87b4fe5cb 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_goto.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_goto.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 char a;
 void __e_acsl_globals_init(void)
 {
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c b/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c
index e3e8cd4ae773b5c4b6f5f0e3d795946667d2053b..12027e7f5b4c03febb957c737441d3a1629edf80 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c
@@ -3,6 +3,8 @@
 #include "stdio.h"
 #include "stdlib.h"
 char *__gen_e_acsl_literal_string;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void __e_acsl_globals_init(void)
 {
   static char __e_acsl_already_run = 0;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_init.c b/src/plugins/e-acsl/tests/memory/oracle/gen_init.c
index dfc3e7b1805cd58a815dc1f4f059bd8e69195bba..2c00fe4f0123d8e938d9c23e024aa61b4169cd55 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_init.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_init.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int a = 0;
 int b;
 void __e_acsl_globals_init(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c b/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c
index 6b4322952dc1b9a80766894a70789edfc7038604..7a579dc32d3c6c660a14d042948f8dc16e2191e1 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_initialized.c b/src/plugins/e-acsl/tests/memory/oracle/gen_initialized.c
index 7b595c45c169a2449c957d47c66eed0216b1103b..ecebc5da9e304428b2b62d79680ba460cdc0e971 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_initialized.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_initialized.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int A = 0;
 int B;
 void __e_acsl_globals_init(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/memory/oracle/gen_literal_string.c
index 981517739425a6a07fe3609da5e061e2b8a5990b..2ae93f0e98702ed7be0bdee03dbead5ad0a820e7 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_literal_string.c
@@ -7,6 +7,8 @@ char *__gen_e_acsl_literal_string;
 char *__gen_e_acsl_literal_string_4;
 char *__gen_e_acsl_literal_string_3;
 char *__gen_e_acsl_literal_string_2;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void);
 
 char *T = (char *)"bar";
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_local_goto.c b/src/plugins/e-acsl/tests/memory/oracle/gen_local_goto.c
index 3a5e8b4919639645401873e100e262e0a0a13dda..6e6799dbd3b55a8f7f620c04a1b7b3534a24b925 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_local_goto.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_local_goto.c
@@ -5,6 +5,8 @@ char *__gen_e_acsl_literal_string_2;
 char *__gen_e_acsl_literal_string_3;
 char *__gen_e_acsl_literal_string;
 char *__gen_e_acsl_literal_string_4;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void __e_acsl_globals_init(void)
 {
   static char __e_acsl_already_run = 0;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c b/src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c
index 946ce35b05636f8bdb682530c16f0ce766d03438..3f3eb016471db26f2a2bd53d2d08d815b8ec1a6b 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int X = 0;
 int *p = & X;
 int f(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_local_var.c b/src/plugins/e-acsl/tests/memory/oracle/gen_local_var.c
index 20980d2a8fae65639778c83c2e4f3f6f1834ce43..c28e90044db2844a13012bd4948d0e7c90d57b17 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_local_var.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_local_var.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 struct list {
    int element ;
    struct list *next ;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c
index ee34b527eac4bf9ebdfa8cbeb968cad5f16e5746..72d8d0685d14f5e77f6e60be928e447d25c13a6c 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c
@@ -2,7 +2,7 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "string.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ requires valid_string_s: valid_read_string(s);
     ensures acsl_c_equiv: \result 鈮� strlen(\old(s));
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c b/src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c
index 1ff1e767024be9ad08350ef5a7a34ad99187b7f9..2f9c48d8a945ad526d97dbb871b9689e4d534d93 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c
@@ -2,7 +2,7 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ requires valid_memptr: \valid(memptr);
     requires
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_memsize.c b/src/plugins/e-acsl/tests/memory/oracle/gen_memsize.c
index 88eee2f15a5dcbb0c10fc377bf5c355574323fce..df3a77b8d7a83dbe3650e8f9cfe3704ad8bdd2c5 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_memsize.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_memsize.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 extern size_t __e_acsl_heap_allocation_size;
 
 int main(int argc, char **argv)
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_null.c b/src/plugins/e-acsl/tests/memory/oracle/gen_null.c
index d50e1abab50839d82e63c5cdf379c66cad5b9352..94b5ca7fced84d99b2962d761dae2484f5fdfc81 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_null.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_null.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_offset.c b/src/plugins/e-acsl/tests/memory/oracle/gen_offset.c
index e4e60fa025322747e2e9d7e0d9bdc85d78d3be3c..b6b52a83efa197495cd28c47be378cd2ca9ef3cf 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_offset.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_offset.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int A[4] = {1, 2, 3, 4};
 int *PA;
 void __e_acsl_globals_init(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_other_constants.c b/src/plugins/e-acsl/tests/memory/oracle/gen_other_constants.c
index c8f4725f2e1036c72bdaa7dc13929cac93550f1f..bdb06b362ea7fc1d2139e35fff28b3eb42e347fe 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_other_constants.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 enum bool {
     false = 0,
     true = 1
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c
index 96135cb480944a162fee42d8ac034f2f900ac226..8140477968bc3dc5a5630a28cf40be6698728164 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ptr_init.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ptr_init.c
index 414cb99cacd8346139b495f4a00b4e6c148f9a20..20fe5e2aa706b69157afcddc19cad5cedbf77c10 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_ptr_init.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_ptr_init.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int *A;
 int *B;
 void f(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
index 75af517de674f5cbbd46334051db14ab629e1f01..379095819663d4d5c9ea19235966217930c73bea 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
@@ -2,7 +2,7 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 struct S {
    int a[2] ;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_separated.c b/src/plugins/e-acsl/tests/memory/oracle/gen_separated.c
index d0fb32d3baf2778e9244daa5d55edb8278707f89..d1ab26cc2eb68711e15231c8fd9dab0201e112c5 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_separated.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_separated.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/memory/oracle/gen_sizeof.c
index aad129a5528b4f3ba80963ef1e7b2e427c9456f6..7f829ac63e5df4c4572c65e993be3e6e17f49838 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_sizeof.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c
index 063472f4dd76c7e27ce67e13a6d91e6725d1e40c..5cf83f209365a5a2030b660c350f5e6c0880a938 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void __e_acsl_globals_init(void)
 {
   static char __e_acsl_already_run = 0;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_struct_initialized.c b/src/plugins/e-acsl/tests/memory/oracle/gen_struct_initialized.c
index 8d55bb8d9a94c379bde4dce93d111f37a6418e26..cfc1ad9048e8045e97dc8923de8b2dac5b084b8b 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_struct_initialized.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_struct_initialized.c
@@ -3,6 +3,8 @@
 #include "stdint.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 struct __anonstruct_int32_pair_t_1 {
    int32_t a ;
    int32_t b ;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_valid.c b/src/plugins/e-acsl/tests/memory/oracle/gen_valid.c
index 78726b1f91ccfb02793f6b4a1bfa2e2b8f557051..2d8ea22d7e537e1025a5d520baf0c40e9a916c2c 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_valid.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_valid.c
@@ -2,7 +2,7 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 int *X;
 int Z;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/memory/oracle/gen_valid_alias.c
index e31671f6f38b5d0b7f307c84a66630ba220d17fb..bd36506b4f1487339a94a483e2eac8484eae8caf 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_valid_alias.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_valid_alias.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
index 1f83cc4790973b5768444ee02798d4d6b94d8e3e..b8910535a12c93389c032a422e0f2d5df6a56e5b 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
@@ -2,7 +2,7 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 struct list {
    int element ;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_vector.c b/src/plugins/e-acsl/tests/memory/oracle/gen_vector.c
index b4d86730b61f8e6db833efc6f1c26d9ed85e4e81..f522a84f1dc6d5c40dff444831cf795f4ab12930 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_vector.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_vector.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int LAST;
 int *new_inversed(int len, int *v)
 {
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_vla.c b/src/plugins/e-acsl/tests/memory/oracle/gen_vla.c
index a0e89b041bb4cb8f4797b51395fb2788d110974d..2816887b72ce54bfe6226cf6fbca9b0d33dfb3fe 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_vla.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_vla.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int LEN = 10;
 int main(int argc, char **argv)
 {
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c b/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c
index dad8120db26c802a2abfaa86a7f8d6e035a998f1..40a21f890be549217f97ce1769b183c1f25c6d05 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 int incr(int x);
 
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-bittree-model.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-bittree-model.c
index 8673c9a15aa2ccbb782ab75e2700cd10b95d9cf2..46e4f1c6e1263fd048fef601610db2db1befa0b8 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-bittree-model.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-bittree-model.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-compile-dlmalloc.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-compile-dlmalloc.c
index 5884b0f6c6078320062404a8fcf96f5158f24dc4..59f62c0c1c0649b220ba956a3414a42bbac15bab 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-compile-dlmalloc.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-compile-dlmalloc.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c
index f94e292fc4234e8a9714433db943824ea6ea9922..5b7a9aa5a54c55c6da9021d3deb9049e90f50475 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ requires \initialized(p);
     requires *p 鈮� 0;
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c
index 61a4e7c62bdaca2fcdeb4e0058b468ecf89b4797..ed4e1a67efd2dc591d07e2bdcbba10a42d43e78d 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c
@@ -2,7 +2,7 @@
 #include "stdarg.h"
 #include "stddef.h"
 #include "stdio.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 int __gen_e_acsl_uninstrument1(int *p);
 
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-rt-debug.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-rt-debug.c
index 5884b0f6c6078320062404a8fcf96f5158f24dc4..59f62c0c1c0649b220ba956a3414a42bbac15bab 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-rt-debug.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-rt-debug.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-segment-model.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-segment-model.c
index 8673c9a15aa2ccbb782ab75e2700cd10b95d9cf2..46e4f1c6e1263fd048fef601610db2db1befa0b8 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-segment-model.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-segment-model.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c
index 91bf7941f61c7da887f82376a49311743af8e827..1ec0fc0fc6106d101670dd1cc3607cf5902d581a 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c
@@ -2,7 +2,7 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ requires \valid(y);
     requires *x 鈮� 0;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c
index e99bf6424a11e3c6dca10b17822de9acc653668d..dfc3a961e287759cb75665bcf1d12a5be972ccf2 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdint.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(int argc, char **argv)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_args.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_args.c
index 0c5e9d16cc39d57ca71e22da2a38c6369103538b..f5eef9929a553ac34af169aa1d9f7dbf2e00e0c2 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_args.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_args.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(int argc, char const **argv)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_array.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_array.c
index 99b174ecf2558c495a760bd762298ec106970b64..eeaf35098d9063a05a60c115df43445f8b7c70ab 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_array.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_array.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_char.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_char.c
index aa28e2d1ba2e320d33174cecb821163673e6c955..278ff8a5bf3ae3a85a22a15995c85498096867ab 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_char.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_char.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(int argc, char const **argv)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_darray.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_darray.c
index 05043365abe053ca54808128c6c4819b00e4e381..f7db119cba3c3dd19958d504cdf6c114d5d866fb 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_darray.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_darray.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void area_triangle(double (*vertices)[4])
 {
   {
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c
index 37e9a60d4f5c18d36a413067d2aa1cb477f7a304..53b0044b3238c5ffb4eb8025aba47338062d3cb9 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fptr.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fptr.c
index aac5aeebeecb968c052ba03ecd9f822fb7347eed..bd404c2495b123c84defafbd864297fa1f115718 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fptr.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fptr.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int *foo(int *p)
 {
   int *q = p;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c
index b30e5cc2ac00faad0c3eac9bff60b76b9741fd94..8bf4587773b7c260cd914718238b962456138a96 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c
@@ -3,6 +3,8 @@
 #include "stdio.h"
 #include "stdlib.h"
 char *__gen_e_acsl_literal_string;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void __e_acsl_globals_init(void)
 {
   static char __e_acsl_already_run = 0;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_ptr.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_ptr.c
index 040c516ffe185147d768a73f082e94c7b381d5e7..64bb8c9ecbf2e566cb4a05fa510668b941c25e74 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_ptr.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_ptr.c
@@ -3,6 +3,8 @@
 #include "stdint.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int *pfun(char c, int *p, int *p2, int *p3, int *p4, int i)
 {
   __e_acsl_store_block((void *)(& p),(size_t)8);
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c
index 42b6e7cf5101a2cbe54895b6447cfff6d4fd5f86..a7cbd526051d8702b1c73fb405d6d506c413f64b 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c
@@ -4,7 +4,7 @@
 #include "stdlib.h"
 char *__gen_e_acsl_literal_string_2;
 char *__gen_e_acsl_literal_string;
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ requires valid_name: valid_read_string(name);
     ensures null_or_valid_result: \result 鈮� \null 鈭� \valid(\result);
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c
index 1441d93306f2a6a82463ceeab431cf7224e8dfe8..2c7e56295afe8dc71f695a3a895ac207e5276f3b 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c
@@ -5,6 +5,8 @@ char *__gen_e_acsl_literal_string;
 char *__gen_e_acsl_literal_string_2;
 char *__gen_e_acsl_literal_string_4;
 char *__gen_e_acsl_literal_string_3;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 struct tree_desc {
    int *extra_bits ;
 };
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_labels.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_labels.c
index 2c25f4df78218431d07990b44ff81c311ec5c1bf..b95b720a5abcd74aa474e0e2b95907d02ea4027f 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_labels.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_labels.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void foo(int *a, int *b)
 {
   __e_acsl_store_block((void *)(& b),(size_t)8);
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_lit_string.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_lit_string.c
index 5c9099b9c654912614fa7b24bbdf12ed702be245..fddcff05b56a1d384803849ac3223922986f0edf 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_lit_string.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_lit_string.c
@@ -3,6 +3,8 @@
 #include "stdio.h"
 char *__gen_e_acsl_literal_string_2;
 char *__gen_e_acsl_literal_string;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void __e_acsl_globals_init(void)
 {
   static char __e_acsl_already_run = 0;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_local_init.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_local_init.c
index c067d5fd6904735f39272a36c6cb016258490e25..60563870b5677420f600fdb6d3f5217ad8dc8954 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_local_init.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_local_init.c
@@ -8,6 +8,8 @@ char *__gen_e_acsl_literal_string_2;
 char *__gen_e_acsl_literal_string_5;
 char *__gen_e_acsl_literal_string_7;
 char *__gen_e_acsl_literal_string_6;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 struct tree_desc {
    int *extra_bits ;
 };
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc-asan.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc-asan.c
index d718f3e61f84379b9b8a5e95995335bf3cbae46f..28d445663fa2d5681b645ac2dc174e1e7685c768 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc-asan.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc-asan.c
@@ -3,6 +3,8 @@
 #include "stdio.h"
 #include "stdlib.h"
 char *__gen_e_acsl_literal_string;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 void __e_acsl_globals_init(void)
 {
   static char __e_acsl_already_run = 0;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc.c
index 24fe3685108a070480565ffc57065d5e9c846536..93a179e2a29395b84dc30359889e3331d28443b9 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
index ce91bdc96a856e17c20c9c142944a8f1fc3f16cb..8af8c087c3b391b737072dc49f6d3baf545023f7 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
@@ -3,7 +3,7 @@
 #include "stdio.h"
 #include "stdlib.h"
 #include "string.h"
-extern int __e_acsl_sound_verdict;
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
 
 /*@ requires valid_dest: valid_or_empty(dest, n);
     requires valid_src: valid_read_or_empty(src, n);
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c
index 4ccf94b71bf362c1fb7fdab4916c766de891e3f8..219e3486c175a4e505fe45fb7d8fef78025a6e41 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_struct.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_struct.c
index 59e1bd61ee55c8eeb7901c36a5cfe7fdbfdbafd9..66b5e2ef099ebbbe6e1a2485161d5c8614f061af 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_struct.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_struct.c
@@ -2,6 +2,8 @@
 #include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 struct temporal_t {
    char *p ;
    char *q ;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
index 8d25afd44d519f11a71e9c2a5d3160666a4c9a72..c46be04e1a5f209abe3710a60d6f3dde50d82eb0 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
@@ -1,6 +1,8 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
+extern  __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
 int main(void)
 {
   int __retres;