From f5cfd9b3e57e3d0d6401ecbcc61ed582e9f48f12 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 2 Aug 2021 17:40:56 +0200
Subject: [PATCH] [eacsl] Fix global C variable __e_acsl_sound_verdict
- The global variable is now a Frama-C built-in and is not monitored;
- The `varinfo` for the variable, retrieved in module `Prepare_ast` is
now exposed;
- The variable is added to every generated code so that it can be used
by a later analysis of E-ACSL.
---
.../e-acsl/instrumentation_model/e_acsl_assert.h | 2 +-
.../src/project_initializer/prepare_ast.ml | 16 ++++++++--------
.../src/project_initializer/prepare_ast.mli | 7 +++++++
.../e-acsl/tests/arith/oracle/gen_arith.c | 2 ++
.../e-acsl/tests/arith/oracle/gen_array.c | 2 ++
src/plugins/e-acsl/tests/arith/oracle/gen_at.c | 2 +-
.../oracle/gen_at_on-purely-logic-variables.c | 2 +-
.../e-acsl/tests/arith/oracle/gen_bitwise.c | 2 ++
src/plugins/e-acsl/tests/arith/oracle/gen_cast.c | 2 ++
.../e-acsl/tests/arith/oracle/gen_comparison.c | 2 ++
.../e-acsl/tests/arith/oracle/gen_functions.c | 2 +-
.../tests/arith/oracle/gen_functions_rec.c | 2 ++
.../tests/arith/oracle/gen_integer_constant.c | 2 ++
src/plugins/e-acsl/tests/arith/oracle/gen_let.c | 2 ++
.../e-acsl/tests/arith/oracle/gen_longlong.c | 2 ++
src/plugins/e-acsl/tests/arith/oracle/gen_not.c | 2 ++
.../e-acsl/tests/arith/oracle/gen_quantif.c | 2 ++
.../e-acsl/tests/arith/oracle/gen_rationals.c | 2 +-
src/plugins/e-acsl/tests/arith/oracle/gen_sum.c | 2 ++
.../e-acsl/tests/bts/oracle/gen_bts1304.c | 2 ++
.../e-acsl/tests/bts/oracle/gen_bts1307.c | 2 +-
.../e-acsl/tests/bts/oracle/gen_bts1324.c | 2 +-
.../e-acsl/tests/bts/oracle/gen_bts1326.c | 2 +-
.../bts/oracle/gen_bts1386_complex_flowgraph.c | 2 ++
.../e-acsl/tests/bts/oracle/gen_bts1390.c | 2 +-
.../e-acsl/tests/bts/oracle/gen_bts1395.c | 2 +-
.../e-acsl/tests/bts/oracle/gen_bts1398.c | 2 ++
.../e-acsl/tests/bts/oracle/gen_bts1399.c | 2 ++
.../e-acsl/tests/bts/oracle/gen_bts1478.c | 2 +-
.../e-acsl/tests/bts/oracle/gen_bts1700.c | 2 ++
.../e-acsl/tests/bts/oracle/gen_bts1717.c | 2 ++
.../e-acsl/tests/bts/oracle/gen_bts1718.c | 2 ++
.../e-acsl/tests/bts/oracle/gen_bts1740.c | 2 ++
.../e-acsl/tests/bts/oracle/gen_bts1837.c | 2 ++
.../e-acsl/tests/bts/oracle/gen_bts2191.c | 2 ++
.../e-acsl/tests/bts/oracle/gen_bts2192.c | 2 +-
.../e-acsl/tests/bts/oracle/gen_bts2231.c | 2 ++
.../e-acsl/tests/bts/oracle/gen_bts2252.c | 2 +-
.../e-acsl/tests/bts/oracle/gen_bts2305.c | 2 ++
.../e-acsl/tests/bts/oracle/gen_bts2386.c | 2 ++
.../e-acsl/tests/bts/oracle/gen_bts2406.c | 2 ++
.../tests/bts/oracle/gen_issue-eacsl-105.c | 2 ++
.../tests/bts/oracle/gen_issue-eacsl-139.c | 2 +-
.../tests/bts/oracle/gen_issue-eacsl-145.c | 2 ++
.../tests/bts/oracle/gen_issue-eacsl-149.c | 2 ++
.../tests/bts/oracle/gen_issue-eacsl-172.c | 2 ++
.../e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c | 2 ++
.../e-acsl/tests/bts/oracle/gen_issue69.c | 2 ++
.../tests/bts/oracle/issue-eacsl-145.res.oracle | 2 ++
.../builtin/oracle/gen_builtin_literal_string.c | 2 ++
.../gen_builtin_literal_string_local_init.c | 2 ++
.../e-acsl/tests/builtin/oracle/gen_strcat.c | 2 +-
.../e-acsl/tests/builtin/oracle/gen_strcmp.c | 2 +-
.../e-acsl/tests/builtin/oracle/gen_strcpy.c | 2 +-
.../e-acsl/tests/builtin/oracle/gen_strlen.c | 2 +-
.../tests/constructs/oracle/gen_acsl_check.c | 2 +-
.../tests/constructs/oracle/gen_decrease.c | 2 +-
.../e-acsl/tests/constructs/oracle/gen_false.c | 2 ++
.../constructs/oracle/gen_function_contract.c | 2 +-
.../e-acsl/tests/constructs/oracle/gen_ghost.c | 2 ++
.../tests/constructs/oracle/gen_invariant.c | 2 ++
.../tests/constructs/oracle/gen_labeled_stmt.c | 2 +-
.../e-acsl/tests/constructs/oracle/gen_lazy.c | 2 ++
.../e-acsl/tests/constructs/oracle/gen_loop.c | 2 ++
.../constructs/oracle/gen_nested_code_annot.c | 2 ++
.../e-acsl/tests/constructs/oracle/gen_result.c | 2 +-
.../e-acsl/tests/constructs/oracle/gen_rte.c | 2 +-
.../tests/constructs/oracle/gen_stmt_contract.c | 2 ++
.../e-acsl/tests/constructs/oracle/gen_true.c | 2 ++
.../e-acsl/tests/constructs/oracle/gen_typedef.c | 2 ++
.../examples/oracle/gen_functions_contiki.c | 2 ++
.../tests/examples/oracle/gen_linear_search.c | 2 +-
.../e-acsl/tests/format/oracle/gen_fprintf.c | 2 +-
.../e-acsl/tests/format/oracle/gen_printf.c | 2 +-
.../tests/full-mtracking/oracle/gen_addrOf.c | 2 ++
.../e-acsl/tests/gmp-only/oracle/gen_arith.c | 2 ++
.../e-acsl/tests/gmp-only/oracle/gen_functions.c | 2 +-
.../e-acsl/tests/memory/oracle/gen_addrOf.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_alias.c | 2 ++
.../tests/memory/oracle/gen_array_overflow.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_base_addr.c | 2 ++
.../tests/memory/oracle/gen_block_length.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_block_valid.c | 2 ++
.../tests/memory/oracle/gen_bypassed_var.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_call.c | 2 +-
.../memory/oracle/gen_compound_initializers.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_constructor.c | 2 ++
.../tests/memory/oracle/gen_ctype_macros.c | 2 +-
.../tests/memory/oracle/gen_decl_in_switch.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_early_exit.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_errno.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_freeable.c | 2 ++
.../tests/memory/oracle/gen_ghost_parameters.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_goto.c | 2 ++
.../tests/memory/oracle/gen_hidden_malloc.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_init.c | 2 ++
.../tests/memory/oracle/gen_init_function.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_initialized.c | 2 ++
.../tests/memory/oracle/gen_literal_string.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_local_goto.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_local_init.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_local_var.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_mainargs.c | 2 +-
.../e-acsl/tests/memory/oracle/gen_memalign.c | 2 +-
.../e-acsl/tests/memory/oracle/gen_memsize.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_null.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_offset.c | 2 ++
.../tests/memory/oracle/gen_other_constants.c | 2 ++
src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_ptr_init.c | 2 ++
.../tests/memory/oracle/gen_ranges_in_builtins.c | 2 +-
.../e-acsl/tests/memory/oracle/gen_separated.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_sizeof.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_stdout.c | 2 ++
.../tests/memory/oracle/gen_struct_initialized.c | 2 ++
.../e-acsl/tests/memory/oracle/gen_valid.c | 2 +-
.../e-acsl/tests/memory/oracle/gen_valid_alias.c | 2 ++
.../tests/memory/oracle/gen_valid_in_contract.c | 2 +-
.../e-acsl/tests/memory/oracle/gen_vector.c | 2 ++
src/plugins/e-acsl/tests/memory/oracle/gen_vla.c | 2 ++
.../e-acsl/tests/special/oracle/gen_builtin.c | 2 +-
.../special/oracle/gen_e-acsl-bittree-model.c | 2 ++
.../special/oracle/gen_e-acsl-compile-dlmalloc.c | 2 ++
.../tests/special/oracle/gen_e-acsl-functions.c | 2 +-
.../tests/special/oracle/gen_e-acsl-instrument.c | 2 +-
.../tests/special/oracle/gen_e-acsl-rt-debug.c | 2 ++
.../special/oracle/gen_e-acsl-segment-model.c | 2 ++
.../tests/special/oracle/gen_e-acsl-valid.c | 2 +-
.../tests/temporal/oracle/gen_t_addr-by-val.c | 2 ++
.../e-acsl/tests/temporal/oracle/gen_t_args.c | 2 ++
.../e-acsl/tests/temporal/oracle/gen_t_array.c | 2 ++
.../e-acsl/tests/temporal/oracle/gen_t_char.c | 2 ++
.../e-acsl/tests/temporal/oracle/gen_t_darray.c | 2 ++
.../tests/temporal/oracle/gen_t_dpointer.c | 2 ++
.../e-acsl/tests/temporal/oracle/gen_t_fptr.c | 2 ++
.../e-acsl/tests/temporal/oracle/gen_t_fun_lib.c | 2 ++
.../e-acsl/tests/temporal/oracle/gen_t_fun_ptr.c | 2 ++
.../e-acsl/tests/temporal/oracle/gen_t_getenv.c | 2 +-
.../tests/temporal/oracle/gen_t_global_init.c | 2 ++
.../e-acsl/tests/temporal/oracle/gen_t_labels.c | 2 ++
.../tests/temporal/oracle/gen_t_lit_string.c | 2 ++
.../tests/temporal/oracle/gen_t_local_init.c | 2 ++
.../tests/temporal/oracle/gen_t_malloc-asan.c | 2 ++
.../e-acsl/tests/temporal/oracle/gen_t_malloc.c | 2 ++
.../e-acsl/tests/temporal/oracle/gen_t_memcpy.c | 2 +-
.../e-acsl/tests/temporal/oracle/gen_t_scope.c | 2 ++
.../e-acsl/tests/temporal/oracle/gen_t_struct.c | 2 ++
.../e-acsl/tests/temporal/oracle/gen_t_while.c | 2 ++
148 files changed, 266 insertions(+), 49 deletions(-)
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 6cc1a782efd..8e0abca525e 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 03412904536..246dd0b7c06 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 65ea62daf18..ba19b909922 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 5ce6877d82a..b5265e84689 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 645c5842435..a559df9509b 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 c8e5107e1e1..e366ee59e16 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 46951ce8751..0cde64feb6c 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 54340192b07..a421b3f34be 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 b41c0d12d81..c63917398ce 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 f28ab0ad20b..896c9741e9e 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 8c84d1d06f7..01bee92554d 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 b766248de7c..db81ac4861a 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 323698c0e1b..096a8cd3446 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 e2cdd5cf877..fc128640194 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 21f7073ae45..0f5ccda8356 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 e3add3ad4d5..2d7529f38a8 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 f84cfba6458..ccb7b6be6c7 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 7f3061dd52d..48483e5005e 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 79eefaaa977..5e70777069f 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 4ec7740d794..ef6ec87ac42 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 2712efec6e0..1f57c126452 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 13ed0297405..c5b6665908d 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 c8bbc5d7f69..e4ce2b0300f 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 02552add425..1b997cf7e67 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 c2f45cea322..3b092ae6734 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 7ffe91bbde5..43a7af62321 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 b2502604424..1709bdc247e 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 bf9d598f181..35354e15a4a 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 2abb8670fe0..db165cf968b 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 87055c52db1..8693ba5674d 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 8eeb9dfe863..9a2a7e93911 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 860f3a8a94e..72cbffe72fd 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 33cb6770be6..ad106a78c1a 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 f99068ea384..e79ccbae463 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 e5962bf77af..870b526f608 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 5f9a57c6e5e..d71a4c41cf7 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 5195a4392ce..4a9f3921fd8 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 65224637492..274ddffd5a5 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 327af999d25..eb8feac0bb5 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 16f7fca7437..c14d3f8d10b 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 7aefc7c01ed..d4fccb9af3c 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 51f9bd0c5a8..2c8298f36dc 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 fc022eb87e2..3afa85d098a 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 5e59848212a..a68b9bc741b 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 f8be21500b2..449ce90d451 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 fc026da4d14..b6559e0ca88 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 b83e193f02f..b393878b816 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 d703479245e..9451a4f466e 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 6ba35db7101..e7143f3c725 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 e5950f81d78..f457dfd771a 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 c3b9b764653..93dcd481afd 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 7fe4c9f0b8e..8fcaa4939fa 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 6b1a1141469..4978156adb8 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 3088f87001a..09d7c8aff99 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 4ef82acb2bc..31d35b177ab 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 b9dd1eabfab..d6c33875d60 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 f7b97420540..35511e6a23c 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 5a93a9a2dce..151b83363c8 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 a04626ffba2..25c759f3ea9 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 bfc28ffc41f..7077d948dbe 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 9ab4056e35a..6fd64a10a3a 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 4f408ceffc9..34b962a29c8 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 77e8d08ae97..3c90b94bef5 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 940e40e29a2..a0ee038cc74 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 da452a0bd68..7272563eed4 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 304ce2af901..6134b7451b4 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 3f4d4e1742a..46859d9e8ed 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 ba7d2c236ce..7b81cee7b80 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 d4cb6243553..8603a3791f0 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 a110449db68..37c835510d0 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 84a91929a61..4238666d02e 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 1d1c09c9a1c..262fe258dc2 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 3d7d734187d..63106e3cbdd 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 6278c452419..1e708d06d7d 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 c4ded4bb662..c27908a810a 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 f16eb040032..cccd91e3f09 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 9970dd39300..bb8d0044c5d 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 f6fdc7f96bb..a72dcdf1649 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 98896d3553e..9c4c45d7584 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 c44a08d55f4..9ddd7c0b569 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 b93d4f3e51c..df3b503ecb9 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 3144471bf22..fe71ab12278 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 fcd70965476..9d1eaa75acf 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 5a07ee12ca1..d653ef1b72c 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 beb03fcadc3..05cebce1b23 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 938d7e78991..f137cea5b81 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 22920e30cf3..bbaf5eeb4f8 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 14df39c49de..14e8e659b1d 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 b41c28f6335..d1c746986f7 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 14c6e24361f..97debe70674 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 2fc8b100ae8..650fa1452d1 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 7abd207dbcb..f804ef702e5 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 e16ba064495..3a4ab987b63 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 600b66499c2..69e63b6f818 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 e3e8cd4ae77..12027e7f5b4 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 dfc3e7b1805..2c00fe4f012 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 6b4322952dc..7a579dc32d3 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 7b595c45c16..ecebc5da9e3 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 98151773942..2ae93f0e987 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 3a5e8b49196..6e6799dbd3b 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 946ce35b056..3f3eb016471 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 20980d2a8fa..c28e90044db 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 ee34b527eac..72d8d0685d1 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 1ff1e767024..2f9c48d8a94 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 88eee2f15a5..df3a77b8d7a 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 d50e1abab50..94b5ca7fced 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 e4e60fa0253..b6b52a83efa 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 c8f4725f2e1..bdb06b362ea 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 96135cb4809..8140477968b 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 414cb99cacd..20fe5e2aa70 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 75af517de67..37909581966 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 d0fb32d3baf..d1ab26cc2eb 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 aad129a5528..7f829ac63e5 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 063472f4dd7..5cf83f20936 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 8d55bb8d9a9..cfc1ad9048e 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 78726b1f91c..2d8ea22d7e5 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 e31671f6f38..bd36506b4f1 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 1f83cc47909..b8910535a12 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 b4d86730b61..f522a84f1dc 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 a0e89b041bb..2816887b72c 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 dad8120db26..40a21f890be 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 8673c9a15aa..46e4f1c6e12 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 5884b0f6c60..59f62c0c1c0 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 f94e292fc42..5b7a9aa5a54 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 61a4e7c62bd..ed4e1a67efd 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 5884b0f6c60..59f62c0c1c0 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 8673c9a15aa..46e4f1c6e12 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 91bf7941f61..1ec0fc0fc61 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 e99bf6424a1..dfc3a961e28 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 0c5e9d16cc3..f5eef9929a5 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 99b174ecf25..eeaf35098d9 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 aa28e2d1ba2..278ff8a5bf3 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 05043365abe..f7db119cba3 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 37e9a60d4f5..53b0044b323 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 aac5aeebeec..bd404c2495b 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 b30e5cc2ac0..8bf4587773b 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 040c516ffe1..64bb8c9ecbf 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 42b6e7cf510..a7cbd526051 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 1441d93306f..2c7e56295af 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 2c25f4df782..b95b720a5ab 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 5c9099b9c65..fddcff05b56 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 c067d5fd690..60563870b56 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 d718f3e61f8..28d445663fa 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 24fe3685108..93a179e2a29 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 ce91bdc96a8..8af8c087c3b 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 4ccf94b71bf..219e3486c17 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 59e1bd61ee5..66b5e2ef099 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 8d25afd44d5..c46be04e1a5 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;
--
GitLab