[e-acsl] fix bug with typedef

[e-acsl] universal quantifications done (including testing)

src/plugins/e-acsl/TODO

@@ -32,7 +32,7 @@
 - [Bernard] avoir une fonction
   e_acsl_trace_behavior(char *bhv_name) {}
 à appeler dès qu'un behavior est activé
-- meilleur schéma de compilation des assumes:
+- meilleur schéma de compilation des assumes (not possible in multi-bhv?):
   if (assume_bhv) {
     e_acsl_trace_behavior(bhv_name);
     requires_bhv;

src/plugins/e-acsl/env.ml

@@ -172,9 +172,7 @@ module Logic_binding = struct
   let add env logic_v =
   let v_ref = ref Varinfo.dummy in
   let mk v _ = v_ref := v; [] in
-  let ty = 
-    (* TODO: yet incorrect. Waiting for the type system... *)
-    match logic_v.lv_type with
+  let ty = match logic_v.lv_type with
     | Ctype ty -> ty
     | Linteger -> Mpz.t
     | Ltype _ | Lvar _ | Lreal | Larrow _ -> assert false
@@ -228,7 +226,7 @@ let extend_stmt_in_place env stmt ~pre block =
     env
 
 let push env = 
-  (*  Options.feedback "push";*)
+(*  Options.feedback "push (was %d)" (List.length env.env_stack);*)
   let local_env = { block_info = empty_block; mpz_tbl = empty_mpz_tbl } in
   { env with env_stack = local_env :: env.env_stack }
 
@@ -239,7 +237,7 @@ let pop env =
 
 type where = Before | Middle | After
 let pop_and_get env stmt ~global_clear where =
-(*  Options.feedback "pop_and_get";*)
+  (*  Options.feedback "pop_and_get (%d)" (List.length env.env_stack); *)
   let local_env, tl = top env in
   let clear = 
     if global_clear then 

src/plugins/e-acsl/misc.mli

@@ -33,6 +33,7 @@ val new_lval: ?loc:Location.t -> varinfo -> exp
 (* [TODO] put it in the Frama-C kernel? *)
 
 val mk_call: ?loc:Location.t -> ?result:lval -> string -> exp list -> stmt
+
 val mk_e_acsl_guard: ?reverse:bool -> exp -> predicate named -> stmt
 val e_acsl_header: unit -> global
 

src/plugins/e-acsl/mpz.ml

@@ -39,23 +39,33 @@ let apply_on_var funname e = Misc.mk_call ("__gmpz_" ^ funname) [ e ]
 let init = apply_on_var "init"
 let clear = apply_on_var "clear"
 
-let init_set v e =
+let get_set_suffix_and_arg e = 
   let ty = typeOf e in
-  if is_t ty then
-    Misc.mk_call "__gmpz_init_set" [ v; e ]
+  if is_t ty then "", [ e ]
   else
-    let fname, args = match ty with
-      | TInt((IBool | IChar | IUChar | IUInt | IUShort | IULong), _) ->
-	"ui", [ e ]
-      | TInt((ISChar | IShort | IInt | ILong), _) -> "si", [ e ]
-      | TInt((ILongLong | IULongLong), _) -> assert false
-      | TPtr(TInt(IChar, _), _) ->
-	"str",
+    match unrollType ty with
+    | TInt(IChar, _) -> 
+      (if theMachine.char_is_unsigned then "_ui" else "_si"), [ e ]
+    | TInt((IBool | IUChar | IUInt | IUShort | IULong), _) ->
+      "_ui", [ e ]
+    | TInt((ISChar | IShort | IInt | ILong), _) -> "_si", [ e ]
+    | TInt((ILongLong | IULongLong), _) -> assert false
+    | TPtr(TInt(IChar, _), _) ->
+      "_str",
 	(* decimal base for the number given as string *)
-	[ e; integer ~loc:Location.unknown 10 ]
-      | _ -> assert false
-    in
-    Misc.mk_call ("__gmpz_init_set_" ^ fname) (v :: args)
+      [ e; integer ~loc:Location.unknown 10 ]
+    | _ -> assert false
+
+let generic_affect fname lv ev e =
+  let ty = typeOf ev in
+  if is_t ty then 
+    let suf, args = get_set_suffix_and_arg e in
+    Misc.mk_call (fname ^ suf) (ev :: args)
+  else
+    mkStmtOneInstr ~valid_sid:true (Set(lv, e, Location.unknown))
+
+let init_set = generic_affect "__gmpz_init_set"
+let affect = generic_affect "__gmpz_set"
 
 (*
 Local Variables:

src/plugins/e-acsl/mpz.mli

@@ -36,13 +36,17 @@ val is_t: typ -> bool
 val init: exp -> stmt
   (** build stmt "mpz_init(v)" *)
 
-val init_set: exp -> exp -> stmt
-  (** build stmt "mpz_init_set*(v, e)" with the good function 'set' according
-      to the type of e *)
+val init_set: lval -> exp -> exp -> stmt
+(** [init_set x_as_lv x_as_exp e] builds stmt [x = e] or [mpz_init_set*(v, e)]
+    with the good function 'set' according to the type of e *)
 
 val clear: exp -> stmt
 (** build stmt "mpz_clear(v)" *)
 
+val affect: lval -> exp -> exp -> stmt
+(** [affect x_as_lv x_as_exp e] builds stmt [x = e] or [mpz_set*(e)] with the
+    good function 'set' according to the type of e *)
+
 (*
 Local Variables:
 compile-command: "make"

src/plugins/e-acsl/options.ml

@@ -33,7 +33,7 @@ module Check =
   False
     (struct
       let option_name = "-e-acsl-check"
-      let help = "abort on E-ACSL type checking error"
+      let help = "only type check E-ACSL annotated program"
       let kind = `Correctness
      end)
 

src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h

@@ -20,17 +20,20 @@
 /*                                                                        */
 /**************************************************************************/
 
-/*****************/
-/* GMP functions */
-/*****************/
+/******************/
+/* GMP prototypes */
+/******************/
 
-// initilializers
+/****************/
+/* Initializers */
+/****************/
 
 /*@ ensures \valid(x);
   @ assigns *x; */
 extern void __gmpz_init(mpz_t x);
 
-/*@ ensures \valid(z);
+/*@ requires \valid(z_orig);
+  @ ensures \valid(z);
   @ assigns *z; */
 extern void __gmpz_init_set(mpz_t z, const mpz_t z_orig);
 
@@ -46,19 +49,44 @@ extern void __gmpz_init_set_si(mpz_t z, signed long int n);
   @ assigns *z; */
 extern int __gmpz_init_set_str(mpz_t z, const char *str, int base);
 
-// finalizer
+/***************/
+/* Assignments */
+/***************/
+
+/*@ requires \valid(z_orig);
+  @ requires \valid(z);
+  @ assigns *z; */
+extern void __gmpz_set(mpz_t z, const mpz_t z_orig);
+
+/*@ requires \valid(z);
+  @ assigns *z \from n; */
+extern void __gmpz_set_ui(mpz_t z, unsigned long int n);
+
+/*@ requires \valid(z);
+  @ assigns *z \from n; */
+extern void __gmpz_set_si(mpz_t z, signed long int n);
+
+/*************/
+/* Finalizer */
+/*************/
 
 /*@ requires \valid(x);
   @ assigns *x; */
 extern void __gmpz_clear(mpz_t x);
 
-// logical and arithmetic operators
+/********************/
+/* Logical operator */
+/********************/
 
 /*@ requires \valid(z1);
   @ requires \valid(z2);
   @ assigns \nothing; */
 extern int __gmpz_cmp(const mpz_t z1, const mpz_t z2);
 
+/***********************/
+/* Arithmetic operator */
+/***********************/
+
 /*@ requires \valid(z1);
   @ requires \valid(z2);
   @ assigns *z1; */
@@ -99,7 +127,9 @@ extern void __gmpz_tdiv_q(mpz_t z1, const mpz_t z2, const mpz_t z3);
   @ assigns *z1; */
 extern void __gmpz_tdiv_r(mpz_t z1, const mpz_t z2, const mpz_t z3);
 
-// coercions to C int
+/************************/
+/* Coercions to C types */
+/************************/
 
 /*@ requires \valid(z); 
   @ assigns \nothing; */

src/plugins/e-acsl/tests/e-acsl-reject/oracle/quantif.res.oracle

@@ -14,7 +14,7 @@ tests/e-acsl-reject/quantif.i:10:[e-acsl] warning: invalid E-ACSL construct
                   (∀ ℤ x, ℤ y; 0 ≤ x ∧ x ≤ 3 ⇒ x ≥ 0)'.
                   Ignoring annotation.
 tests/e-acsl-reject/quantif.i:11:[e-acsl] warning: invalid E-ACSL construct
-                  `unquantified variable z in quantification
+                  `too much constraint(s) in quantification
                   (∀ ℤ x; (0 ≤ x ∧ x ≤ 3) ∧ (0 ≤ z ∧ z ≤ 3) ⇒ x ≥ 0)'.
                   Ignoring annotation.
 tests/e-acsl-reject/quantif.i:12:[e-acsl] warning: invalid E-ACSL construct
@@ -25,5 +25,15 @@ tests/e-acsl-reject/quantif.i:12:[e-acsl] warning: invalid E-ACSL construct
 tests/e-acsl-reject/quantif.i:13:[e-acsl] warning: invalid E-ACSL construct
                   `invalid binder x+1 in quantification (∀ int x; 0 ≤ x+1 ∧ x+1 ≤ 3 ⇒ x ≥ 0)'.
                   Ignoring annotation.
-[e-acsl] 7 annotations were ignored, being untypable.
+tests/e-acsl-reject/quantif.i:14:[e-acsl] warning: invalid E-ACSL construct
+                  `too much constraint(s) in quantification
+                  (∀ ℤ x; (0 ≤ x ∧ x < 10) ∧ (9 ≤ x ∧ x < 20) ⇒ x > z)'.
+                  Ignoring annotation.
+tests/e-acsl-reject/quantif.i:15:[e-acsl] warning: invalid E-ACSL construct
+                  `invalid binder y in quantification
+                  (∀ ℤ x, ℤ z, ℤ y;
+                    ((0 ≤ x ∧ x < 2) ∧ (0 ≤ y ∧ y < 5)) ∧ (0 ≤ z ∧ z ≤ y) ⇒
+                    x+z ≤ y+1)'.
+                  Ignoring annotation.
+[e-acsl] 9 annotations were ignored, being untypable.
 [e-acsl] 1 annotation was ignored, being unsupported.

src/plugins/e-acsl/tests/e-acsl-reject/quantif.i

@@ -11,5 +11,8 @@ int main(void) {
   /*@ assert \forall integer x; 0 <= x <= 3 && 0 <= z <= 3 ==> x >= 0; */
   /*@ assert \forall integer x,y; 0 <= x <= 3 || 0 <= y <= 3 ==> x >= 0; */
   /*@ assert \forall int x; 0 <= x+1 <= 3 ==> x >= 0; */
+  /*@ assert \forall integer x; 0 <= x < 10 && 9 <= x < 20 ==> x > z; */
+  /*@ assert \forall integer x,z,y; 0 <= x < 2 && 0 <= y < 5 && 0 <= z <= y
+    ==> x+z <= y+1; */ 
   return 0;
 }

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

@@ -2,7 +2,7 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-PROJECT_FILE.i:200:[value] Assertion got status valid.
+PROJECT_FILE.i:230:[value] Assertion got status valid.
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======

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

@@ -8,29 +8,29 @@ tests/e-acsl-runtime/array.i:14:[e-acsl] warning: missing guard for ensuring tha
 [value] Values of globals at initialization
         T1[0..2] ∈ {0}
         T2[0..3] ∈ {0}
-PROJECT_FILE.i:202:[value] entering loop for the first time
-PROJECT_FILE.i:206:[value] assigning non deterministic value for the first time
-PROJECT_FILE.i:211:[value] entering loop for the first time
-PROJECT_FILE.i:218:[value] Assertion got status unknown.
+PROJECT_FILE.i:232:[value] entering loop for the first time
+PROJECT_FILE.i:236:[value] assigning non deterministic value for the first time
+PROJECT_FILE.i:241:[value] entering loop for the first time
+PROJECT_FILE.i:248:[value] Assertion got status unknown.
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:219.
+        Called from PROJECT_FILE.i:249.
 [value] computing for function printf <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
-PROJECT_FILE.i:183:[value] Function exit: postcondition got status invalid.
+        Called from PROJECT_FILE.i:223.
+PROJECT_FILE.i:213:[value] Function exit: postcondition got status invalid.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
-PROJECT_FILE.i:221:[value] Assertion got status unknown.
+PROJECT_FILE.i:251:[value] Assertion got status unknown.
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:222.
+        Called from PROJECT_FILE.i:252.
 [value] computing for function printf <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail

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

@@ -4,50 +4,50 @@ tests/e-acsl-runtime/cast.i:18:[e-acsl] warning: missing guard for ensuring that
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-PROJECT_FILE.i:202:[value] Assertion got status valid.
+PROJECT_FILE.i:232:[value] Assertion got status valid.
 [value] computing for function __gmpz_init_set_str <- main.
-        Called from PROJECT_FILE.i:206.
-PROJECT_FILE.i:79:[value] Function __gmpz_init_set_str: postcondition got status valid.
+        Called from PROJECT_FILE.i:236.
+PROJECT_FILE.i:82:[value] Function __gmpz_init_set_str: postcondition got status valid.
 [value] Done for function __gmpz_init_set_str
 [value] computing for function __gmpz_get_si <- main.
-        Called from PROJECT_FILE.i:207.
-PROJECT_FILE.i:138:[value] Function __gmpz_get_si: precondition got status valid.
+        Called from PROJECT_FILE.i:237.
+PROJECT_FILE.i:168:[value] Function __gmpz_get_si: precondition got status valid.
 [value] Done for function __gmpz_get_si
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:208.
+        Called from PROJECT_FILE.i:238.
 [value] computing for function printf <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
-PROJECT_FILE.i:183:[value] Function exit: postcondition got status invalid.
+        Called from PROJECT_FILE.i:223.
+PROJECT_FILE.i:213:[value] Function exit: postcondition got status invalid.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:209.
-PROJECT_FILE.i:85:[value] Function __gmpz_clear: precondition got status valid.
+        Called from PROJECT_FILE.i:239.
+PROJECT_FILE.i:107:[value] Function __gmpz_clear: precondition got status valid.
 [value] Done for function __gmpz_clear
-PROJECT_FILE.i:213:[value] Assertion got status valid.
+PROJECT_FILE.i:243:[value] Assertion got status valid.
 [value] computing for function __gmpz_init_set_str <- main.
-        Called from PROJECT_FILE.i:217.
+        Called from PROJECT_FILE.i:247.
 [value] Done for function __gmpz_init_set_str
 [value] computing for function __gmpz_get_ui <- main.
-        Called from PROJECT_FILE.i:218.
-PROJECT_FILE.i:142:[value] Function __gmpz_get_ui: precondition got status valid.
+        Called from PROJECT_FILE.i:248.
+PROJECT_FILE.i:172:[value] Function __gmpz_get_ui: precondition got status valid.
 [value] Done for function __gmpz_get_ui
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:220.
+        Called from PROJECT_FILE.i:250.
 [value] computing for function printf <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:222.
+        Called from PROJECT_FILE.i:252.
 [value] Done for function __gmpz_clear
 [value] Recording results for main
 [value] done for function main

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

@@ -2,279 +2,279 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-PROJECT_FILE.i:203:[value] Assertion got status valid.
-PROJECT_FILE.i:206:[value] Assertion got status valid.
-PROJECT_FILE.i:209:[value] Assertion got status valid.
+PROJECT_FILE.i:233:[value] Assertion got status valid.
+PROJECT_FILE.i:236:[value] Assertion got status valid.
+PROJECT_FILE.i:239:[value] Assertion got status valid.
 [value] computing for function __gmpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:214.
-PROJECT_FILE.i:75:[value] Function __gmpz_init_set_si: postcondition got status valid.
+        Called from PROJECT_FILE.i:244.
+PROJECT_FILE.i:78:[value] Function __gmpz_init_set_si: postcondition got status valid.
 [value] Done for function __gmpz_init_set_si
 [value] computing for function __gmpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:215.
+        Called from PROJECT_FILE.i:245.
 [value] Done for function __gmpz_init_set_si
 [value] computing for function __gmpz_cmp <- main.
-        Called from PROJECT_FILE.i:216.
-PROJECT_FILE.i:91:[value] Function __gmpz_cmp: precondition got status valid.
-PROJECT_FILE.i:92:[value] Function __gmpz_cmp: precondition got status valid.
+        Called from PROJECT_FILE.i:246.
+PROJECT_FILE.i:115:[value] Function __gmpz_cmp: precondition got status valid.
+PROJECT_FILE.i:116:[value] Function __gmpz_cmp: precondition got status valid.
 [value] Done for function __gmpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:217.
+        Called from PROJECT_FILE.i:247.
 [value] computing for function printf <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
-PROJECT_FILE.i:183:[value] Function exit: postcondition got status invalid.
+        Called from PROJECT_FILE.i:223.
+PROJECT_FILE.i:213:[value] Function exit: postcondition got status invalid.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:218.
-PROJECT_FILE.i:85:[value] Function __gmpz_clear: precondition got status valid.
+        Called from PROJECT_FILE.i:248.
+PROJECT_FILE.i:107:[value] Function __gmpz_clear: precondition got status valid.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:219.
+        Called from PROJECT_FILE.i:249.
 [value] Done for function __gmpz_clear
-PROJECT_FILE.i:223:[value] Assertion got status valid.
+PROJECT_FILE.i:253:[value] Assertion got status valid.
 [value] computing for function __gmpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:228.
+        Called from PROJECT_FILE.i:258.
 [value] Done for function __gmpz_init_set_si
 [value] computing for function __gmpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:229.
+        Called from PROJECT_FILE.i:259.
 [value] Done for function __gmpz_init_set_si
 [value] computing for function __gmpz_cmp <- main.
-        Called from PROJECT_FILE.i:230.
+        Called from PROJECT_FILE.i:260.
 [value] Done for function __gmpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:231.
+        Called from PROJECT_FILE.i:261.
 [value] computing for function printf <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:232.
+        Called from PROJECT_FILE.i:262.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:233.
+        Called from PROJECT_FILE.i:263.
 [value] Done for function __gmpz_clear
-PROJECT_FILE.i:238:[value] Assertion got status valid.
-PROJECT_FILE.i:241:[value] Assertion got status unknown.
-PROJECT_FILE.i:244:[value] Assertion got status valid.
-PROJECT_FILE.i:247:[value] Assertion got status valid.
-PROJECT_FILE.i:250:[value] Assertion got status valid.
-PROJECT_FILE.i:253:[value] Assertion got status valid.
-PROJECT_FILE.i:256:[value] Assertion got status valid.
-PROJECT_FILE.i:259:[value] Assertion got status valid.
-PROJECT_FILE.i:262:[value] Assertion got status valid.
+PROJECT_FILE.i:268:[value] Assertion got status valid.
+PROJECT_FILE.i:271:[value] Assertion got status unknown.
+PROJECT_FILE.i:274:[value] Assertion got status valid.
+PROJECT_FILE.i:277:[value] Assertion got status valid.
+PROJECT_FILE.i:280:[value] Assertion got status valid.
+PROJECT_FILE.i:283:[value] Assertion got status valid.
+PROJECT_FILE.i:286:[value] Assertion got status valid.
+PROJECT_FILE.i:289:[value] Assertion got status valid.
+PROJECT_FILE.i:292:[value] Assertion got status valid.
 [value] computing for function __gmpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:268.
+        Called from PROJECT_FILE.i:298.
 [value] Done for function __gmpz_init_set_si
 [value] computing for function __gmpz_init <- main.
-        Called from PROJECT_FILE.i:269.
-PROJECT_FILE.i:63:[value] Function __gmpz_init: postcondition got status valid.
+        Called from PROJECT_FILE.i:299.
+PROJECT_FILE.i:65:[value] Function __gmpz_init: postcondition got status valid.
 [value] Done for function __gmpz_init
 [value] computing for function __gmpz_neg <- main.
-        Called from PROJECT_FILE.i:270.
-PROJECT_FILE.i:101:[value] Function __gmpz_neg: precondition got status valid.
-PROJECT_FILE.i:102:[value] Function __gmpz_neg: precondition got status valid.
+        Called from PROJECT_FILE.i:300.
+PROJECT_FILE.i:129:[value] Function __gmpz_neg: precondition got status valid.
+PROJECT_FILE.i:130:[value] Function __gmpz_neg: precondition got status valid.
 [value] Done for function __gmpz_neg
 [value] computing for function __gmpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:271.
+        Called from PROJECT_FILE.i:301.
 [value] Done for function __gmpz_init_set_si
 [value] computing for function __gmpz_cmp <- main.
-        Called from PROJECT_FILE.i:272.
+        Called from PROJECT_FILE.i:302.
 [value] Done for function __gmpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:273.
+        Called from PROJECT_FILE.i:303.
 [value] computing for function printf <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:274.
+        Called from PROJECT_FILE.i:304.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:275.
+        Called from PROJECT_FILE.i:305.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:276.
+        Called from PROJECT_FILE.i:306.
 [value] Done for function __gmpz_clear
-PROJECT_FILE.i:280:[value] Assertion got status valid.
+PROJECT_FILE.i:310:[value] Assertion got status valid.
 [value] computing for function __gmpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:286.
+        Called from PROJECT_FILE.i:316.
 [value] Done for function __gmpz_init_set_si
 [value] computing for function __gmpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:287.
+        Called from PROJECT_FILE.i:317.
 [value] Done for function __gmpz_init_set_si
 [value] computing for function __gmpz_init <- main.
-        Called from PROJECT_FILE.i:288.
+        Called from PROJECT_FILE.i:318.
 [value] Done for function __gmpz_init
 [value] computing for function __gmpz_neg <- main.
-        Called from PROJECT_FILE.i:289.
+        Called from PROJECT_FILE.i:319.
 [value] Done for function __gmpz_neg
 [value] computing for function __gmpz_cmp <- main.
-        Called from PROJECT_FILE.i:290.
+        Called from PROJECT_FILE.i:320.
 [value] Done for function __gmpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:291.
+        Called from PROJECT_FILE.i:321.
 [value] computing for function printf <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:292.
+        Called from PROJECT_FILE.i:322.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:293.
+        Called from PROJECT_FILE.i:323.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:294.
+        Called from PROJECT_FILE.i:324.
 [value] Done for function __gmpz_clear
-PROJECT_FILE.i:298:[value] Assertion got status valid.
+PROJECT_FILE.i:328:[value] Assertion got status valid.
 [value] computing for function __gmpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:304.
+        Called from PROJECT_FILE.i:334.
 [value] Done for function __gmpz_init_set_si
 [value] computing for function __gmpz_init <- main.
-        Called from PROJECT_FILE.i:305.
+        Called from PROJECT_FILE.i:335.
 [value] Done for function __gmpz_init
 [value] computing for function __gmpz_neg <- main.
-        Called from PROJECT_FILE.i:306.
+        Called from PROJECT_FILE.i:336.
 [value] Done for function __gmpz_neg
 [value] computing for function __gmpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:307.
+        Called from PROJECT_FILE.i:337.
 [value] Done for function __gmpz_init_set_si
 [value] computing for function __gmpz_cmp <- main.
-        Called from PROJECT_FILE.i:308.
+        Called from PROJECT_FILE.i:338.
 [value] Done for function __gmpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:309.
+        Called from PROJECT_FILE.i:339.
 [value] computing for function printf <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:310.
+        Called from PROJECT_FILE.i:340.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:311.
+        Called from PROJECT_FILE.i:341.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:312.
+        Called from PROJECT_FILE.i:342.
 [value] Done for function __gmpz_clear
-PROJECT_FILE.i:316:[value] Assertion got status valid.
+PROJECT_FILE.i:346:[value] Assertion got status valid.
 [value] computing for function __gmpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:322.
+        Called from PROJECT_FILE.i:352.
 [value] Done for function __gmpz_init_set_si
 [value] computing for function __gmpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:323.
+        Called from PROJECT_FILE.i:353.
 [value] Done for function __gmpz_init_set_si
 [value] computing for function __gmpz_init <- main.
-        Called from PROJECT_FILE.i:324.
+        Called from PROJECT_FILE.i:354.
 [value] Done for function __gmpz_init
 [value] computing for function __gmpz_neg <- main.
-        Called from PROJECT_FILE.i:325.
+        Called from PROJECT_FILE.i:355.
 [value] Done for function __gmpz_neg
 [value] computing for function __gmpz_cmp <- main.
-        Called from PROJECT_FILE.i:326.
+        Called from PROJECT_FILE.i:356.
 [value] Done for function __gmpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:327.
+        Called from PROJECT_FILE.i:357.
 [value] computing for function printf <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:328.
+        Called from PROJECT_FILE.i:358.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:329.
+        Called from PROJECT_FILE.i:359.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:330.
+        Called from PROJECT_FILE.i:360.
 [value] Done for function __gmpz_clear
-PROJECT_FILE.i:334:[value] Assertion got status valid.
+PROJECT_FILE.i:364:[value] Assertion got status valid.
 [value] computing for function __gmpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:339.
+        Called from PROJECT_FILE.i:369.
 [value] Done for function __gmpz_init_set_si
 [value] computing for function __gmpz_init <- main.
-        Called from PROJECT_FILE.i:340.
+        Called from PROJECT_FILE.i:370.
 [value] Done for function __gmpz_init
 [value] computing for function __gmpz_neg <- main.
-        Called from PROJECT_FILE.i:341.
+        Called from PROJECT_FILE.i:371.
 [value] Done for function __gmpz_neg
 [value] computing for function __gmpz_cmp <- main.
-        Called from PROJECT_FILE.i:342.
+        Called from PROJECT_FILE.i:372.
 [value] Done for function __gmpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:343.
+        Called from PROJECT_FILE.i:373.
 [value] computing for function printf <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:344.
+        Called from PROJECT_FILE.i:374.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:345.
+        Called from PROJECT_FILE.i:375.
 [value] Done for function __gmpz_clear
-PROJECT_FILE.i:349:[value] Assertion got status valid.
+PROJECT_FILE.i:379:[value] Assertion got status valid.
 [value] computing for function __gmpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:355.
+        Called from PROJECT_FILE.i:385.
 [value] Done for function __gmpz_init_set_si
 [value] computing for function __gmpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:356.
+        Called from PROJECT_FILE.i:386.
 [value] Done for function __gmpz_init_set_si
 [value] computing for function __gmpz_init <- main.
-        Called from PROJECT_FILE.i:357.
+        Called from PROJECT_FILE.i:387.
 [value] Done for function __gmpz_init
 [value] computing for function __gmpz_neg <- main.
-        Called from PROJECT_FILE.i:358.
+        Called from PROJECT_FILE.i:388.
 [value] Done for function __gmpz_neg
 [value] computing for function __gmpz_cmp <- main.
-        Called from PROJECT_FILE.i:359.
+        Called from PROJECT_FILE.i:389.
 [value] Done for function __gmpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:360.
+        Called from PROJECT_FILE.i:390.
 [value] computing for function printf <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:361.
+        Called from PROJECT_FILE.i:391.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:362.
+        Called from PROJECT_FILE.i:392.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:363.
+        Called from PROJECT_FILE.i:393.
 [value] Done for function __gmpz_clear
 [value] Recording results for main
 [value] done for function main

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

@@ -9,7 +9,8 @@ typedef __mpz_struct mpz_t[1];
 /*@ ensures \valid(\old(x));
     assigns *x;  */
 extern void __gmpz_init(__mpz_struct * /*[1]*/ x);
-/*@ ensures \valid(\old(z));
+/*@ requires \valid(z_orig);
+    ensures \valid(\old(z));
     assigns *z;  */
 extern void __gmpz_init_set(__mpz_struct * /*[1]*/ z,
                             __mpz_struct const * /*[1]*/ z_orig);

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.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 mpz_t[1];
+/*@ ensures \valid(\old(x));
+    assigns *x;  */
+extern void __gmpz_init(__mpz_struct * /*[1]*/ x);
+/*@ ensures \valid(\old(z));
+    assigns *z;
+    assigns *z \from n;  */
+extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
+/*@ requires \valid(z_orig);
+    requires \valid(z);
+    assigns *z;  */
+extern void __gmpz_set(__mpz_struct * /*[1]*/ z,
+                       __mpz_struct const * /*[1]*/ z_orig);
+/*@ requires \valid(x);
+    assigns *x;  */
+extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+    requires \valid(z2);
+    assigns \nothing;  */
+extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+                      __mpz_struct const * /*[1]*/ z2);
+/*@ requires \valid(z1);
+    requires \valid(z2);
+    requires \valid(z3);
+    assigns *z1; 
+*/
+extern void __gmpz_add(__mpz_struct * /*[1]*/ z1,
+                       __mpz_struct const * /*[1]*/ z2,
+                       __mpz_struct const * /*[1]*/ z3);
+/*@ terminates \false;
+    ensures \false;
+    assigns \nothing;  */
+extern void exit(int status);
+/*@ assigns \nothing;  */
+extern int printf(char const * , ...);
+void e_acsl_fail(char *msg)
+{
+  printf("%s\n",msg);
+  exit(1);
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  int a;
+  a = -1;
+  /*@ assert ∀ ℤ x; 0 ≤ x ∧ x ≤ 1 ⇒ x ≡ 0 ∨ x ≡ 1; */ ;
+  {
+    mpz_t e_acsl_1;
+    int e_acsl_2;
+    e_acsl_2 = 1;
+    __gmpz_init((__mpz_struct *)(e_acsl_1));
+    {
+      mpz_t e_acsl_8;
+      __gmpz_init_set_si((__mpz_struct *)(e_acsl_8),(long)0);
+      __gmpz_set((__mpz_struct *)(e_acsl_1),(__mpz_struct const *)(e_acsl_8));
+      __gmpz_clear((__mpz_struct *)(e_acsl_8));
+    }
+    
+    while (1) {
+      {
+        mpz_t e_acsl_9;
+        int e_acsl_10;
+        __gmpz_init_set_si((__mpz_struct *)(e_acsl_9),(long)1);
+        e_acsl_10 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
+                               (__mpz_struct const *)(e_acsl_9));
+        if (! (e_acsl_10 <= 0)) { break; }
+        __gmpz_clear((__mpz_struct *)(e_acsl_9));
+      }
+      
+      {
+        mpz_t e_acsl_3;
+        int e_acsl_4;
+        int e_acsl_7;
+        __gmpz_init_set_si((__mpz_struct *)(e_acsl_3),(long)0);
+        e_acsl_4 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
+                              (__mpz_struct const *)(e_acsl_3));
+        if (e_acsl_4 == 0) { e_acsl_7 = 1; }
+        else {
+          mpz_t e_acsl_5;
+          int e_acsl_6;
+          __gmpz_init_set_si((__mpz_struct *)(e_acsl_5),(long)1);
+          e_acsl_6 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
+                                (__mpz_struct const *)(e_acsl_5));
+          e_acsl_7 = e_acsl_6 == 0;
+          __gmpz_clear((__mpz_struct *)(e_acsl_5));
+        }
+        __gmpz_clear((__mpz_struct *)(e_acsl_3));
+        if (! e_acsl_7) {
+          e_acsl_2 = 0;
+          goto e_acsl_end_loop1; }
+      }
+      
+      {
+        mpz_t e_acsl_11;
+        mpz_t e_acsl_12;
+        __gmpz_init_set_si((__mpz_struct *)(e_acsl_11),(long)((char)1));
+        __gmpz_init((__mpz_struct *)(e_acsl_12));
+        __gmpz_add((__mpz_struct *)(e_acsl_12),
+                   (__mpz_struct const *)(e_acsl_1),
+                   (__mpz_struct const *)(e_acsl_11));
+        __gmpz_set((__mpz_struct *)(e_acsl_1),
+                   (__mpz_struct const *)(e_acsl_12));
+        __gmpz_clear((__mpz_struct *)(e_acsl_11));
+        __gmpz_clear((__mpz_struct *)(e_acsl_12));
+      }
+      
+    }
+    e_acsl_end_loop1: ;
+    if (! e_acsl_2) {
+      e_acsl_fail((char *)"(\\forall integer x; 0 <= x && x <= 1 ==> x == 0 || x == 1)");
+    }
+    __gmpz_clear((__mpz_struct *)(e_acsl_1));
+  }
+  
+  /*@ assert ∀ ℤ x; 0 < x ∧ x ≤ 1 ⇒ x ≡ 1; */ ;
+  {
+    mpz_t e_acsl_13;
+    int e_acsl_14;
+    e_acsl_14 = 1;
+    __gmpz_init((__mpz_struct *)(e_acsl_13));
+    {
+      mpz_t e_acsl_17;
+      mpz_t e_acsl_18;
+      mpz_t e_acsl_19;
+      __gmpz_init_set_si((__mpz_struct *)(e_acsl_17),(long)0);
+      __gmpz_init_set_si((__mpz_struct *)(e_acsl_18),(long)((char)1));
+      __gmpz_init((__mpz_struct *)(e_acsl_19));
+      __gmpz_add((__mpz_struct *)(e_acsl_19),
+                 (__mpz_struct const *)(e_acsl_17),
+                 (__mpz_struct const *)(e_acsl_18));
+      __gmpz_set((__mpz_struct *)(e_acsl_13),
+                 (__mpz_struct const *)(e_acsl_19));
+      __gmpz_clear((__mpz_struct *)(e_acsl_17));
+      __gmpz_clear((__mpz_struct *)(e_acsl_18));
+      __gmpz_clear((__mpz_struct *)(e_acsl_19));
+    }
+    
+    while (1) {
+      {
+        mpz_t e_acsl_20;
+        int e_acsl_21;
+        __gmpz_init_set_si((__mpz_struct *)(e_acsl_20),(long)1);
+        e_acsl_21 = __gmpz_cmp((__mpz_struct const *)(e_acsl_13),
+                               (__mpz_struct const *)(e_acsl_20));
+        if (! (e_acsl_21 <= 0)) { break; }
+        __gmpz_clear((__mpz_struct *)(e_acsl_20));
+      }
+      
+      {
+        mpz_t e_acsl_15;
+        int e_acsl_16;
+        __gmpz_init_set_si((__mpz_struct *)(e_acsl_15),(long)1);
+        e_acsl_16 = __gmpz_cmp((__mpz_struct const *)(e_acsl_13),
+                               (__mpz_struct const *)(e_acsl_15));
+        __gmpz_clear((__mpz_struct *)(e_acsl_15));
+        if (! (e_acsl_16 == 0)) {
+          e_acsl_14 = 0;
+          goto e_acsl_end_loop2; }
+      }
+      
+      {
+        mpz_t e_acsl_22;
+        mpz_t e_acsl_23;
+        __gmpz_init_set_si((__mpz_struct *)(e_acsl_22),(long)((char)1));
+        __gmpz_init((__mpz_struct *)(e_acsl_23));
+        __gmpz_add((__mpz_struct *)(e_acsl_23),
+                   (__mpz_struct const *)(e_acsl_13),
+                   (__mpz_struct const *)(e_acsl_22));
+        __gmpz_set((__mpz_struct *)(e_acsl_13),
+                   (__mpz_struct const *)(e_acsl_23));
+        __gmpz_clear((__mpz_struct *)(e_acsl_22));
+        __gmpz_clear((__mpz_struct *)(e_acsl_23));
+      }
+      
+    }
+    e_acsl_end_loop2: ;
+    if (! e_acsl_14) {
+      e_acsl_fail((char *)"(\\forall integer x; 0 < x && x <= 1 ==> x == 1)");
+    }
+    __gmpz_clear((__mpz_struct *)(e_acsl_13));
+  }
+  
+  /*@ assert ∀ ℤ x; 0 < x ∧ x < 1 ⇒ \false; */ ;
+  {
+    mpz_t e_acsl_24;
+    int e_acsl_25;
+    e_acsl_25 = 1;
+    __gmpz_init((__mpz_struct *)(e_acsl_24));
+    {
+      mpz_t e_acsl_26;
+      mpz_t e_acsl_27;
+      mpz_t e_acsl_28;
+      __gmpz_init_set_si((__mpz_struct *)(e_acsl_26),(long)0);
+      __gmpz_init_set_si((__mpz_struct *)(e_acsl_27),(long)((char)1));
+      __gmpz_init((__mpz_struct *)(e_acsl_28));
+      __gmpz_add((__mpz_struct *)(e_acsl_28),
+                 (__mpz_struct const *)(e_acsl_26),
+                 (__mpz_struct const *)(e_acsl_27));
+      __gmpz_set((__mpz_struct *)(e_acsl_24),
+                 (__mpz_struct const *)(e_acsl_28));
+      __gmpz_clear((__mpz_struct *)(e_acsl_26));
+      __gmpz_clear((__mpz_struct *)(e_acsl_27));
+      __gmpz_clear((__mpz_struct *)(e_acsl_28));
+    }
+    
+    while (1) {
+      {
+        mpz_t e_acsl_29;
+        int e_acsl_30;
+        __gmpz_init_set_si((__mpz_struct *)(e_acsl_29),(long)1);
+        e_acsl_30 = __gmpz_cmp((__mpz_struct const *)(e_acsl_24),
+                               (__mpz_struct const *)(e_acsl_29));
+        if (! (e_acsl_30 < 0)) { break; }
+        __gmpz_clear((__mpz_struct *)(e_acsl_29));
+      }
+      
+      e_acsl_25 = 0;
+      goto e_acsl_end_loop3;
+      {
+        mpz_t e_acsl_31;
+        mpz_t e_acsl_32;
+        __gmpz_init_set_si((__mpz_struct *)(e_acsl_31),(long)((char)1));
+        __gmpz_init((__mpz_struct *)(e_acsl_32));
+        __gmpz_add((__mpz_struct *)(e_acsl_32),
+                   (__mpz_struct const *)(e_acsl_24),
+                   (__mpz_struct const *)(e_acsl_31));
+        __gmpz_set((__mpz_struct *)(e_acsl_24),
+                   (__mpz_struct const *)(e_acsl_32));
+        __gmpz_clear((__mpz_struct *)(e_acsl_31));
+        __gmpz_clear((__mpz_struct *)(e_acsl_32));
+      }
+      
+    }
+    e_acsl_end_loop3: ;
+    if (! e_acsl_25) {
+      e_acsl_fail((char *)"(\\forall integer x; 0 < x && x < 1 ==> \\false)");
+    }
+    __gmpz_clear((__mpz_struct *)(e_acsl_24));
+  }
+  
+  /*@ assert ∀ ℤ x; 0 ≤ x ∧ x < 1 ⇒ x ≡ 0; */ ;
+  {
+    mpz_t e_acsl_33;
+    int e_acsl_34;
+    e_acsl_34 = 1;
+    __gmpz_init((__mpz_struct *)(e_acsl_33));
+    {
+      mpz_t e_acsl_37;
+      __gmpz_init_set_si((__mpz_struct *)(e_acsl_37),(long)0);
+      __gmpz_set((__mpz_struct *)(e_acsl_33),
+                 (__mpz_struct const *)(e_acsl_37));
+      __gmpz_clear((__mpz_struct *)(e_acsl_37));
+    }
+    
+    while (1) {
+      {
+        mpz_t e_acsl_38;
+        int e_acsl_39;
+        __gmpz_init_set_si((__mpz_struct *)(e_acsl_38),(long)1);
+        e_acsl_39 = __gmpz_cmp((__mpz_struct const *)(e_acsl_33),
+                               (__mpz_struct const *)(e_acsl_38));
+        if (! (e_acsl_39 < 0)) { break; }
+        __gmpz_clear((__mpz_struct *)(e_acsl_38));
+      }
+      
+      {
+        mpz_t e_acsl_35;
+        int e_acsl_36;
+        __gmpz_init_set_si((__mpz_struct *)(e_acsl_35),(long)0);
+        e_acsl_36 = __gmpz_cmp((__mpz_struct const *)(e_acsl_33),
+                               (__mpz_struct const *)(e_acsl_35));
+        __gmpz_clear((__mpz_struct *)(e_acsl_35));
+        if (! (e_acsl_36 == 0)) {
+          e_acsl_34 = 0;
+          goto e_acsl_end_loop4; }
+      }
+      
+      {
+        mpz_t e_acsl_40;
+        mpz_t e_acsl_41;
+        __gmpz_init_set_si((__mpz_struct *)(e_acsl_40),(long)((char)1));
+        __gmpz_init((__mpz_struct *)(e_acsl_41));
+        __gmpz_add((__mpz_struct *)(e_acsl_41),
+                   (__mpz_struct const *)(e_acsl_33),
+                   (__mpz_struct const *)(e_acsl_40));
+        __gmpz_set((__mpz_struct *)(e_acsl_33),
+                   (__mpz_struct const *)(e_acsl_41));
+        __gmpz_clear((__mpz_struct *)(e_acsl_40));
+        __gmpz_clear((__mpz_struct *)(e_acsl_41));
+      }
+      
+    }
+    e_acsl_end_loop4: ;
+    if (! e_acsl_34) {
+      e_acsl_fail((char *)"(\\forall integer x; 0 <= x && x < 1 ==> x == 0)");
+    }
+    __gmpz_clear((__mpz_struct *)(e_acsl_33));
+  }
+  
+  /*@
+  assert ∀ ℤ x, ℤ y, ℤ z;
+  ((0 ≤ x ∧ x < 2) ∧ (0 ≤ y ∧ y < 5)) ∧ (0 ≤ z ∧ z ≤ y) ⇒
+  x+z ≤ y+1; */ ;
+  {
+    mpz_t e_acsl_42;
+    mpz_t e_acsl_43;
+    mpz_t e_acsl_44;
+    int e_acsl_45;
+    e_acsl_45 = 1;
+    __gmpz_init((__mpz_struct *)(e_acsl_44));
+    __gmpz_init((__mpz_struct *)(e_acsl_43));
+    __gmpz_init((__mpz_struct *)(e_acsl_42));
+    {
+      mpz_t e_acsl_59;
+      __gmpz_init_set_si((__mpz_struct *)(e_acsl_59),(long)0);
+      __gmpz_set((__mpz_struct *)(e_acsl_42),
+                 (__mpz_struct const *)(e_acsl_59));
+      __gmpz_clear((__mpz_struct *)(e_acsl_59));
+    }
+    
+    while (1) {
+      {
+        mpz_t e_acsl_60;
+        int e_acsl_61;
+        __gmpz_init_set_si((__mpz_struct *)(e_acsl_60),(long)2);
+        e_acsl_61 = __gmpz_cmp((__mpz_struct const *)(e_acsl_42),
+                               (__mpz_struct const *)(e_acsl_60));
+        if (! (e_acsl_61 < 0)) { break; }
+        __gmpz_clear((__mpz_struct *)(e_acsl_60));
+      }
+      
+      {
+        mpz_t e_acsl_54;
+        __gmpz_init_set_si((__mpz_struct *)(e_acsl_54),(long)0);
+        __gmpz_set((__mpz_struct *)(e_acsl_43),
+                   (__mpz_struct const *)(e_acsl_54));
+        __gmpz_clear((__mpz_struct *)(e_acsl_54));
+      }
+      
+      while (1) {
+        {
+          mpz_t e_acsl_55;
+          int e_acsl_56;
+          __gmpz_init_set_si((__mpz_struct *)(e_acsl_55),(long)5);
+          e_acsl_56 = __gmpz_cmp((__mpz_struct const *)(e_acsl_43),
+                                 (__mpz_struct const *)(e_acsl_55));
+          if (! (e_acsl_56 < 0)) { break; }
+          __gmpz_clear((__mpz_struct *)(e_acsl_55));
+        }
+        
+        {
+          mpz_t e_acsl_50;
+          __gmpz_init_set_si((__mpz_struct *)(e_acsl_50),(long)0);
+          __gmpz_set((__mpz_struct *)(e_acsl_44),
+                     (__mpz_struct const *)(e_acsl_50));
+          __gmpz_clear((__mpz_struct *)(e_acsl_50));
+        }
+        
+        while (1) {
+          {
+            int e_acsl_51;
+            e_acsl_51 = __gmpz_cmp((__mpz_struct const *)(e_acsl_44),
+                                   (__mpz_struct const *)(e_acsl_43));
+            if (! (e_acsl_51 <= 0)) { break; }
+          }
+          
+          {
+            mpz_t e_acsl_46;
+            mpz_t e_acsl_47;
+            mpz_t e_acsl_48;
+            int e_acsl_49;
+            __gmpz_init((__mpz_struct *)(e_acsl_46));
+            __gmpz_add((__mpz_struct *)(e_acsl_46),
+                       (__mpz_struct const *)(e_acsl_42),
+                       (__mpz_struct const *)(e_acsl_44));
+            __gmpz_init_set_si((__mpz_struct *)(e_acsl_47),(long)1);
+            __gmpz_init((__mpz_struct *)(e_acsl_48));
+            __gmpz_add((__mpz_struct *)(e_acsl_48),
+                       (__mpz_struct const *)(e_acsl_43),
+                       (__mpz_struct const *)(e_acsl_47));
+            e_acsl_49 = __gmpz_cmp((__mpz_struct const *)(e_acsl_46),
+                                   (__mpz_struct const *)(e_acsl_48));
+            __gmpz_clear((__mpz_struct *)(e_acsl_46));
+            __gmpz_clear((__mpz_struct *)(e_acsl_47));
+            __gmpz_clear((__mpz_struct *)(e_acsl_48));
+            if (! (e_acsl_49 <= 0)) {
+              e_acsl_45 = 0;
+              goto e_acsl_end_loop5; }
+          }
+          
+          {
+            mpz_t e_acsl_52;
+            mpz_t e_acsl_53;
+            __gmpz_init_set_si((__mpz_struct *)(e_acsl_52),(long)((char)1));
+            __gmpz_init((__mpz_struct *)(e_acsl_53));
+            __gmpz_add((__mpz_struct *)(e_acsl_53),
+                       (__mpz_struct const *)(e_acsl_44),
+                       (__mpz_struct const *)(e_acsl_52));
+            __gmpz_set((__mpz_struct *)(e_acsl_44),
+                       (__mpz_struct const *)(e_acsl_53));
+            __gmpz_clear((__mpz_struct *)(e_acsl_52));
+            __gmpz_clear((__mpz_struct *)(e_acsl_53));
+          }
+          
+        }
+        {
+          mpz_t e_acsl_57;
+          mpz_t e_acsl_58;
+          __gmpz_init_set_si((__mpz_struct *)(e_acsl_57),(long)((char)1));
+          __gmpz_init((__mpz_struct *)(e_acsl_58));
+          __gmpz_add((__mpz_struct *)(e_acsl_58),
+                     (__mpz_struct const *)(e_acsl_43),
+                     (__mpz_struct const *)(e_acsl_57));
+          __gmpz_set((__mpz_struct *)(e_acsl_43),
+                     (__mpz_struct const *)(e_acsl_58));
+          __gmpz_clear((__mpz_struct *)(e_acsl_57));
+          __gmpz_clear((__mpz_struct *)(e_acsl_58));
+        }
+        
+      }
+      {
+        mpz_t e_acsl_62;
+        mpz_t e_acsl_63;
+        __gmpz_init_set_si((__mpz_struct *)(e_acsl_62),(long)((char)1));
+        __gmpz_init((__mpz_struct *)(e_acsl_63));
+        __gmpz_add((__mpz_struct *)(e_acsl_63),
+                   (__mpz_struct const *)(e_acsl_42),
+                   (__mpz_struct const *)(e_acsl_62));
+        __gmpz_set((__mpz_struct *)(e_acsl_42),
+                   (__mpz_struct const *)(e_acsl_63));
+        __gmpz_clear((__mpz_struct *)(e_acsl_62));
+        __gmpz_clear((__mpz_struct *)(e_acsl_63));
+      }
+      
+    }
+    e_acsl_end_loop5: ;
+    if (! e_acsl_45) {
+      e_acsl_fail((char *)"(\\forall integer x, integer y, integer z;\n  ((0 <= x && x < 2) && (0 <= y && y < 5)) && (0 <= z && z <= y) ==>\n  x+z <= y+1)");
+    }
+    __gmpz_clear((__mpz_struct *)(e_acsl_42));
+    __gmpz_clear((__mpz_struct *)(e_acsl_43));
+    __gmpz_clear((__mpz_struct *)(e_acsl_44));
+  }
+  
+  __retres = 0;
+  return (__retres);
+}
+
+

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.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 mpz_t[1];
+typedef unsigned char uint8;
+/*@ ensures \valid(\old(z));
+    assigns *z;
+    assigns *z \from n;  */
+extern void __gmpz_init_set_ui(__mpz_struct * /*[1]*/ z, unsigned long n);
+/*@ ensures \valid(\old(z));
+    assigns *z;
+    assigns *z \from n;  */
+extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
+/*@ requires \valid(x);
+    assigns *x;  */
+extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+    requires \valid(z2);
+    assigns \nothing;  */
+extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+                      __mpz_struct const * /*[1]*/ z2);
+/*@ terminates \false;
+    ensures \false;
+    assigns \nothing;  */
+extern void exit(int status);
+/*@ assigns \nothing;  */
+extern int printf(char const * , ...);
+void e_acsl_fail(char *msg)
+{
+  printf("%s\n",msg);
+  exit(1);
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  uint8 x;
+  x = (unsigned char)0;
+  /*@ assert x ≡ 0; */ ;
+  {
+    mpz_t e_acsl_1;
+    mpz_t e_acsl_2;
+    int e_acsl_3;
+    __gmpz_init_set_ui((__mpz_struct *)(e_acsl_1),(unsigned long)x);
+    __gmpz_init_set_si((__mpz_struct *)(e_acsl_2),(long)0);
+    e_acsl_3 = __gmpz_cmp((__mpz_struct const *)(e_acsl_1),
+                          (__mpz_struct const *)(e_acsl_2));
+    if (! (e_acsl_3 == 0)) { e_acsl_fail((char *)"(x == 0)"); }
+    __gmpz_clear((__mpz_struct *)(e_acsl_1));
+    __gmpz_clear((__mpz_struct *)(e_acsl_2));
+  }
+  
+  __retres = 0;
+  return (__retres);
+}
+
+

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

@@ -2,32 +2,32 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-PROJECT_FILE.i:199:[value] Assertion got status valid.
-PROJECT_FILE.i:203:[value] Assertion got status valid.
-PROJECT_FILE.i:206:[value] Assertion got status valid.
+PROJECT_FILE.i:229:[value] Assertion got status valid.
+PROJECT_FILE.i:233:[value] Assertion got status valid.
+PROJECT_FILE.i:236:[value] Assertion got status valid.
 [value] computing for function __gmpz_init_set_str <- main.
-        Called from PROJECT_FILE.i:210.
-PROJECT_FILE.i:79:[value] Function __gmpz_init_set_str: postcondition got status valid.
+        Called from PROJECT_FILE.i:240.
+PROJECT_FILE.i:82:[value] Function __gmpz_init_set_str: postcondition got status valid.
 [value] Done for function __gmpz_init_set_str
 [value] computing for function __gmpz_cmp <- main.
-        Called from PROJECT_FILE.i:211.
-PROJECT_FILE.i:91:[value] Function __gmpz_cmp: precondition got status valid.
-PROJECT_FILE.i:92:[value] Function __gmpz_cmp: precondition got status valid.
+        Called from PROJECT_FILE.i:241.
+PROJECT_FILE.i:115:[value] Function __gmpz_cmp: precondition got status valid.
+PROJECT_FILE.i:116:[value] Function __gmpz_cmp: precondition got status valid.
 [value] Done for function __gmpz_cmp
 [value] computing for function e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:213.
+        Called from PROJECT_FILE.i:243.
 [value] computing for function printf <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
+        Called from PROJECT_FILE.i:223.
 [value] Done for function printf
 [value] computing for function exit <- e_acsl_fail <- main.
-        Called from PROJECT_FILE.i:193.
-PROJECT_FILE.i:183:[value] Function exit: postcondition got status invalid.
+        Called from PROJECT_FILE.i:223.
+PROJECT_FILE.i:213:[value] Function exit: postcondition got status invalid.
 [value] Done for function exit
 [value] Recording results for e_acsl_fail
 [value] Done for function e_acsl_fail
 [value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:215.
-PROJECT_FILE.i:85:[value] Function __gmpz_clear: precondition got status valid.
+        Called from PROJECT_FILE.i:245.
+PROJECT_FILE.i:107:[value] Function __gmpz_clear: precondition got status valid.
 [value] Done for function __gmpz_clear
 [value] Recording results for main
 [value] done for function main