[E-ACSL] fixed bug #1478 when monitored global variables have initializers

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.

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) ->

src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c

+/* 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;
+}

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle

+[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}

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle

+[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}

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c

+/* 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;
+}
+
+

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c

+/* 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;
+}
+
+