From fbc77baf79ee0612734069c58a40871687f960bb Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 4 Sep 2013 13:52:27 +0000
Subject: [PATCH] [E-ACSL] fixed bug #1478 when monitored global variables have
initializers
---
src/plugins/e-acsl/doc/Changelog | 2 +
src/plugins/e-acsl/pre_analysis.ml | 147 +++++++++++-------
.../e-acsl/tests/e-acsl-runtime/bts1478.c | 18 +++
.../oracle/bts1478.1.err.oracle | 0
.../oracle/bts1478.1.res.oracle | 52 +++++++
.../e-acsl-runtime/oracle/bts1478.err.oracle | 0
.../e-acsl-runtime/oracle/bts1478.res.oracle | 43 +++++
.../tests/e-acsl-runtime/oracle/gen_bts1478.c | 101 ++++++++++++
.../e-acsl-runtime/oracle/gen_bts14782.c | 130 ++++++++++++++++
9 files changed, 433 insertions(+), 60 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.err.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 0851d76b828..eb1804afe40 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2013/09/04] Fix bug when monitored global variables have
+ initializers (bts #1478).
-* E-ACSL [2013/09/04] Fix bug when mixing -e-acsl-prepare and
running E-ACSL in another project (bts #!1473).
-* E-ACSL [2013/06/26] Fix crash with typedef on pointer types.
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 6a5b8741cc8..7d5b9ba80e6 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -203,6 +203,67 @@ module rec Transfer
let ty = Cil.typeOf e in
is_ptr_or_array ty
+ let rec base_addr_node = function
+ | Lval lv | AddrOf lv | StartOf lv ->
+ (match lv with
+ | Var vi, _ -> Some vi
+ | Mem e, _ -> base_addr e)
+ | BinOp((PlusPI | IndexPI | MinusPI), e1, e2, _) ->
+ if is_ptr_or_array_exp e1 then base_addr e1
+ else begin
+ assert (is_ptr_or_array_exp e2);
+ base_addr e2
+ end
+ | Info(e, _) | CastE(_, e) -> base_addr e
+ | BinOp((MinusPP | PlusA | MinusA | Mult | Div | Mod |Shiftlt | Shiftrt
+ | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr),
+ _, _, _)
+ | UnOp _ | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _
+ | AlignOfE _ ->
+ None
+
+ and base_addr e = base_addr_node e.enode
+
+ let extend_to_expr always state lhost e =
+ let add_vi state vi =
+ if is_ptr_or_array_exp e && (always || Varinfo.Hptset.mem vi state) then
+ match base_addr e with
+ | None -> state
+ | Some vi_e ->
+ Options.feedback ~level:4 ~dkey
+ "monitoring %a from %a."
+ Printer.pp_varinfo vi_e
+ Printer.pp_lval (lhost, NoOffset);
+ Varinfo.Hptset.add vi_e state
+ else
+ state
+ in
+ match lhost with
+ | Var vi -> add_vi state vi
+ | Mem e ->
+ match base_addr e with
+ | None -> Kernel.fatal "no base address for %a" Printer.pp_exp e
+ | Some vi -> add_vi state vi
+
+ (* if [e] contains an address from a base, then also monitor the host *)
+ let rec extend_from_addr state lv e = match e.enode with
+ | AddrOf(lhost, _) ->
+ extend_to_expr true state lhost (Cil.new_exp ~loc:e.eloc (Lval lv)),
+ true
+ | BinOp((PlusPI | IndexPI | MinusPI), e1, e2, _) ->
+ if is_ptr_or_array_exp e1 then extend_from_addr state lv e1
+ else begin
+ assert (is_ptr_or_array_exp e2);
+ extend_from_addr state lv e2
+ end
+ | CastE(_, e) | Info(e, _) -> extend_from_addr state lv e
+ | _ -> state, false
+
+ let handle_assignment state (lhost, _ as lv) e =
+ (* if [e] contains an address from a base, then also monitor the host *)
+ let state, always = extend_from_addr state lv e in
+ extend_to_expr always state lhost e
+
let rec register_term_lval kf varinfos (thost, _) =
let add_vi kf vi =
Options.feedback ~level:4 ~dkey "monitoring %a from annotation of %a."
@@ -309,6 +370,18 @@ module rec Transfer
();
!state_ref
+ let register_initializers state =
+ let rec do_init vi init state = match init with
+ | SingleInit e -> handle_assignment state (Var vi, NoOffset) e
+ | CompoundInit(_, l) ->
+ List.fold_left (fun state (_, init) -> do_init vi init state) state l
+ in
+ let do_one vi init state = match init.init with
+ | None -> state
+ | Some init -> do_init vi init state
+ in
+ Globals.Vars.fold_in_file_order do_one state
+
(** The (backwards) transfer function for a branch. The [(Cil.CurrentLoc.get
())] is set before calling this. If it returns None, then we have some
default handling. Otherwise, the returned data is the data before the
@@ -358,75 +431,29 @@ module rec Transfer
else
state
in
+ let state =
+ (* take initializers into account *)
+ if is_first then
+ let main, lib = Globals.entry_point () in
+ if Kernel_function.equal kf main && not lib then
+ register_initializers state
+ else
+ state
+ else
+ state
+ in
Some state)
- let rec base_addr_node = function
- | Lval lv | AddrOf lv | StartOf lv ->
- (match lv with
- | Var vi, _ -> Some vi
- | Mem e, _ -> base_addr e)
- | BinOp((PlusPI | IndexPI | MinusPI), e1, e2, _) ->
- if is_ptr_or_array_exp e1 then base_addr e1
- else begin
- assert (is_ptr_or_array_exp e2);
- base_addr e2
- end
- | Info(e, _) | CastE(_, e) -> base_addr e
- | BinOp((MinusPP | PlusA | MinusA | Mult | Div | Mod |Shiftlt | Shiftrt
- | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr),
- _, _, _)
- | UnOp _ | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _
- | AlignOfE _ ->
- None
-
- and base_addr e = base_addr_node e.enode
-
(** The (backwards) transfer function for an instruction. The
[(Cil.CurrentLoc.get ())] is set before calling this. If it returns
None, then we have some default handling. Otherwise, the returned data is
the data before the branch (not considering the exception handlers) *)
let doInstr _stmt instr state =
let state = Env.default_varinfos state in
- let extend_to_expr always state lhost e =
- let add_vi state vi =
- if is_ptr_or_array_exp e && (always || Varinfo.Hptset.mem vi state)
- then
- match base_addr e with
- | None -> state
- | Some vi_e ->
- Options.feedback ~level:4 ~dkey
- "monitoring %a from %a."
- Printer.pp_varinfo vi_e
- Printer.pp_lval (lhost, NoOffset);
- Varinfo.Hptset.add vi_e state
- else
- state
- in
- match lhost with
- | Var vi -> add_vi state vi
- | Mem e ->
- match base_addr e with
- | None -> Kernel.fatal "no base address for %a" Printer.pp_exp e
- | Some vi -> add_vi state vi
- in
match instr with
- | Set((lhost, _) as lv, e, _) ->
- (* if [e] contains an address from a base, then also monitor the host *)
- let rec extend_from_addr state e = match e.enode with
- | AddrOf(lhost, _) ->
- extend_to_expr true state lhost (Cil.new_exp ~loc:e.eloc (Lval lv)),
- true
- | BinOp((PlusPI | IndexPI | MinusPI), e1, e2, _) ->
- if is_ptr_or_array_exp e1 then extend_from_addr state e1
- else begin
- assert (is_ptr_or_array_exp e2);
- extend_from_addr state e2
- end
- | CastE(_, e) | Info(e, _) -> extend_from_addr state e
- | _ -> state, false
- in
- let state, always = extend_from_addr state e in
- Dataflow.Done (Some (extend_to_expr always state lhost e))
+ | Set(lv, e, _) ->
+ let state = handle_assignment state lv e in
+ Dataflow.Done (Some state)
| Call(result, f_exp, l, _) ->
(match f_exp.enode with
| Lval(Var vi, NoOffset) ->
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c b/src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c
new file mode 100644
index 00000000000..f36822ef19e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c
@@ -0,0 +1,18 @@
+/* run.config
+ COMMENT: bts #1478 about wrong detection of initializers in pre-analysis
+ EXECNOW: LOG gen_bts1478.c BIN gen_bts1478.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1478.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1478.c > /dev/null && ./gcc_test.sh bts1478
+ EXECNOW: LOG gen_bts14782.c BIN gen_bts14782.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1478.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts14782.c > /dev/null && ./gcc_test.sh bts14782
+*/
+
+int global_i = 0;
+int* global_i_ptr = &global_i;
+
+/*@ requires global_i == 0;
+ requires \valid(global_i_ptr);
+ requires global_i_ptr == &global_i; */
+void loop(void) { }
+
+int main(void) {
+ loop();
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
new file mode 100644
index 00000000000..410b2c5e7e4
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
@@ -0,0 +1,52 @@
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc tests/e-acsl-runtime/bts1478.c"
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __memory_size ∈ [--..--]
+ global_i ∈ {0}
+ global_i_ptr ∈ {{ &global_i }}
+[value] using specification for function __store_block
+tests/e-acsl-runtime/bts1478.c:10:[value] Function __e_acsl_loop: precondition got status valid.
+tests/e-acsl-runtime/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
+tests/e-acsl-runtime/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.
+[value] using specification for function __gmpz_init_set_si
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:62:[value] Function __gmpz_init_set_si: precondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: postcondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:65:[value] Function __gmpz_init_set_si: postcondition got status unknown.
+[value] using specification for function __gmpz_cmp
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:124:[value] Function __gmpz_cmp: precondition got status valid.
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:125:[value] Function __gmpz_cmp: precondition got status valid.
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+[value] using specification for function __valid
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+[value] using specification for function __gmpz_clear
+FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:114:[value] Function __gmpz_clear: precondition got status valid.
+tests/e-acsl-runtime/bts1478.c:10:[value] Function loop: precondition got status valid.
+tests/e-acsl-runtime/bts1478.c:11:[value] Function loop: precondition got status valid.
+tests/e-acsl-runtime/bts1478.c:12:[value] Function loop: precondition got status valid.
+[value] using specification for function __delete_block
+[kernel] warning: Neither code nor specification for function __e_acsl_memory_clean, generating default assigns from the prototype
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values at end of function __e_acsl_memory_init:
+
+[value] Values at end of function loop:
+
+[value] Values at end of function __e_acsl_loop:
+
+[value] Values at end of function main:
+ __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
new file mode 100644
index 00000000000..65cf4fa07b2
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
@@ -0,0 +1,43 @@
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc tests/e-acsl-runtime/bts1478.c"
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+ __fc_random_counter ∈ {0}
+ __fc_rand_max ∈ {32767}
+ __fc_heap_status ∈ [--..--]
+ __memory_size ∈ [--..--]
+ global_i ∈ {0}
+ global_i_ptr ∈ {{ &global_i }}
+[value] using specification for function __store_block
+tests/e-acsl-runtime/bts1478.c:10:[value] Function __e_acsl_loop: precondition got status valid.
+tests/e-acsl-runtime/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
+tests/e-acsl-runtime/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+[value] using specification for function __valid
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/bts1478.c:10:[value] Function loop: precondition got status valid.
+tests/e-acsl-runtime/bts1478.c:11:[value] Function loop: precondition got status valid.
+tests/e-acsl-runtime/bts1478.c:12:[value] Function loop: precondition got status valid.
+[value] using specification for function __delete_block
+[kernel] warning: Neither code nor specification for function __e_acsl_memory_clean, generating default assigns from the prototype
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values at end of function __e_acsl_memory_init:
+
+[value] Values at end of function loop:
+
+[value] Values at end of function __e_acsl_loop:
+
+[value] Values at end of function main:
+ __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
new file mode 100644
index 00000000000..c6381705f85
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
@@ -0,0 +1,101 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned int size_t;
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+/*@
+model __mpz_struct { ℤ n };
+*/
+int __fc_random_counter __attribute__((__unused__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status; */
+
+/*@
+axiomatic
+ dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
+extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+extern size_t __memory_size;
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+ */
+int global_i = 0;
+int *global_i_ptr = & global_i;
+/*@ requires global_i ≡ 0;
+ requires \valid(global_i_ptr);
+ requires global_i_ptr ≡ &global_i;
+ */
+void loop(void)
+{
+ return;
+}
+
+/*@ requires global_i ≡ 0;
+ requires \valid(global_i_ptr);
+ requires global_i_ptr ≡ &global_i;
+ */
+void __e_acsl_loop(void)
+{
+ {
+ int __e_acsl_valid;
+ e_acsl_assert(global_i == 0,(char *)"Precondition",(char *)"loop",
+ (char *)"global_i == 0",10);
+ __e_acsl_valid = __valid((void *)global_i_ptr,sizeof(int));
+ e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"loop",
+ (char *)"\\valid(global_i_ptr)",11);
+ e_acsl_assert(global_i_ptr == & global_i,(char *)"Precondition",
+ (char *)"loop",(char *)"global_i_ptr == &global_i",12);
+ loop();
+ }
+ return;
+}
+
+void __e_acsl_memory_init(void)
+{
+ __store_block((void *)(& global_i_ptr),4U);
+ __store_block((void *)(& global_i),4U);
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init();
+ __e_acsl_loop();
+ __retres = 0;
+ __delete_block((void *)(& global_i_ptr));
+ __delete_block((void *)(& global_i));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
new file mode 100644
index 00000000000..e5ece491f83
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
@@ -0,0 +1,130 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned int size_t;
+/*@ requires predicate ≢ 0;
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+ char *kind,
+ char *fct,
+ char *pred_txt,
+ int line);
+
+/*@
+model __mpz_struct { ℤ n };
+*/
+int __fc_random_counter __attribute__((__unused__));
+unsigned long const __fc_rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status; */
+
+/*@
+axiomatic
+ dynamic_allocation {
+ predicate is_allocable{L}(size_t n)
+ reads __fc_heap_status;
+
+ }
+ */
+/*@ requires ¬\initialized(z);
+ ensures \valid(\old(z));
+ ensures \initialized(\old(z));
+ assigns *z;
+ assigns *z \from n;
+ allocates \old(z);
+ */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
+ long n);
+
+/*@ requires \valid(x);
+ assigns *x; */
+extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+
+/*@ requires \valid(z1);
+ requires \valid(z2);
+ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+ __mpz_struct const * /*[1]*/ z2);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+ size_t size);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ assigns \nothing; */
+extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
+
+extern __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+extern size_t __memory_size;
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+ */
+int global_i = 0;
+int *global_i_ptr = & global_i;
+/*@ requires global_i ≡ 0;
+ requires \valid(global_i_ptr);
+ requires global_i_ptr ≡ &global_i;
+ */
+void loop(void)
+{
+ return;
+}
+
+/*@ requires global_i ≡ 0;
+ requires \valid(global_i_ptr);
+ requires global_i_ptr ≡ &global_i;
+ */
+void __e_acsl_loop(void)
+{
+ {
+ mpz_t __e_acsl_global_i;
+ mpz_t __e_acsl;
+ int __e_acsl_eq;
+ int __e_acsl_valid;
+ __gmpz_init_set_si(__e_acsl_global_i,(long)global_i);
+ __gmpz_init_set_si(__e_acsl,(long)0);
+ __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_global_i),
+ (__mpz_struct const *)(__e_acsl));
+ e_acsl_assert(__e_acsl_eq == 0,(char *)"Precondition",(char *)"loop",
+ (char *)"global_i == 0",10);
+ __e_acsl_valid = __valid((void *)global_i_ptr,sizeof(int));
+ e_acsl_assert(__e_acsl_valid,(char *)"Precondition",(char *)"loop",
+ (char *)"\\valid(global_i_ptr)",11);
+ e_acsl_assert(global_i_ptr == & global_i,(char *)"Precondition",
+ (char *)"loop",(char *)"global_i_ptr == &global_i",12);
+ __gmpz_clear(__e_acsl_global_i);
+ __gmpz_clear(__e_acsl);
+ loop();
+ }
+ return;
+}
+
+void __e_acsl_memory_init(void)
+{
+ __store_block((void *)(& global_i_ptr),4U);
+ __store_block((void *)(& global_i),4U);
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init();
+ __e_acsl_loop();
+ __retres = 0;
+ __delete_block((void *)(& global_i_ptr));
+ __delete_block((void *)(& global_i));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
--
GitLab