diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index efbbd3c6aa1d8fcdb25a24a84a390ae9c89960de..b7e35cba3ac2bcc136a66289027af5655421997a 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -80,7 +80,7 @@
(voir aussi result.i et ./at_stmt_contract.i)
- interprÈtation des tableaux logiques
[Dillon] Windows
-- \valid(p) is not true if p is a const pointer
+- \valid(p) is not true if p is a const pointer (depend on -const-readonly)
[to be check]: no call to full_init or initialize for the assigned result of a
function call
diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index 48c6bfbb92758f54dd5ec98e85e218b2265a5921..f9d7de519916d0d60b6cfe99ea0843d43dee94ef 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -32,47 +32,63 @@ let term_to_exp_ref
: (kernel_function -> Env.t -> typ option -> term -> exp * Env.t) ref
= Extlib.mk_fun "term_to_exp_ref"
-let compute_quantif_guards quantif bounded_vars hyps =
+let compute_quantif_guards quantif bounded_vars hyps =
let error msg pp x =
let msg1 = Pretty_utils.sfprintf msg pp x in
- let msg2 =
+ let msg2 =
Pretty_utils.sfprintf "@[ in quantification@ %a@]"
- Printer.pp_predicate_named quantif
+ Printer.pp_predicate_named quantif
in
Error.untypable (msg1 ^ msg2)
in
- let rec aux acc vars p =
- match p.content with
- | Pand({ content = Prel((Rlt | Rle) as r1, t11, t12) },
- { content = Prel((Rlt | Rle) as r2, t21, t22) }) ->
- let rec terms t12 t21 = match t12.term_node, t21.term_node with
- | TLval(TVar x1, TNoOffset), TLval(TVar x2, TNoOffset) ->
- let v, vars = match vars with
- | [] -> error "@[too much constraint(s)%a@]" (fun _ () -> ()) ()
- | v :: tl ->
- match v.lv_type with
- | Ctype ty when isIntegralType ty -> v, tl
- | Linteger -> v, tl
- | Ltype _ as ty when Logic_const.is_boolean_type ty -> v, tl
- | Ctype _ | Ltype _ | Lvar _ | Lreal | Larrow _ ->
- error "@[non integer variable %a@]" Printer.pp_logic_var v
- in
- if Logic_var.equal x1 x2 && Logic_var.equal x1 v then
- (t11, r1, x1, r2, t22) :: acc, vars
- else
- error "@[invalid binder %a@]" Printer.pp_term t21
- | TLogic_coerce(_, t12), _ -> terms t12 t21
- | _, TLogic_coerce(_, t21) -> terms t12 t21
- | TLval _, _ -> error "@[invalid binder %a@]" Printer.pp_term t21
- | _, _ -> error "@[invalid binder %a@]" Printer.pp_term t12
+ let rec left_term acc vars left_bound t = match t.term_node with
+ | TLogic_coerce(_, t) -> left_term acc vars left_bound t
+ | TLval(TVar x, TNoOffset) ->
+ (* check if [x] is the correct variable *)
+ let v, vars = match vars with
+ | [] -> error "@[too much constraint(s)%a@]" (fun _ () -> ()) ()
+ | v :: tl -> match v.lv_type with
+ | Ctype ty when isIntegralType ty -> v, tl
+ | Linteger -> v, tl
+ | Ltype _ as ty when Logic_const.is_boolean_type ty -> v, tl
+ | Ctype _ | Ltype _ | Lvar _ | Lreal | Larrow _ ->
+ error "@[non integer variable %a@]" Printer.pp_logic_var v
in
- terms t12 t21
- | Pand(p1, p2) ->
- let acc, vars = aux acc vars p1 in
- aux acc vars p2
+ if Logic_var.equal x v then acc, Some (left_bound, x), vars
+ else error "@[invalid binder %a@]" Printer.pp_term t
+ | _ -> error "@[invalid binder %a@]" Printer.pp_term t
+ in
+ let rec parse acc vars p = match p.content with
+ | Pand(p, { content = Prel((Rlt | Rle) as r, t1, t2) }) ->
+ (* && is left-associative in the AST *)
+ let acc, partial, vars = parse acc vars p in
+ (match partial with
+ | None ->
+ (* left part of a new constraint: the searched variable is [t2] *)
+ left_term acc vars (t1, r) t2
+ | Some ((t_left, r_left), v) ->
+ (* right part of an existing constraint: the variable is [t1] *)
+ let rec right_term t = match t.term_node with
+ | TLogic_coerce(_, t) -> right_term t
+ | TLval(TVar x, TNoOffset) ->
+ if Logic_var.equal x v then
+ (* new full constraint found *)
+ (t_left, r_left, x, r, t2) :: acc, None, vars
+ else
+ error "@[invalid binder %a@]" Printer.pp_term t
+ | _ -> error "@[invalid binder %a@]" Printer.pp_term t
+ in
+ right_term t1)
+ | Prel((Rlt | Rle) as r, t1, t2) ->
+ (* left-most predicate: the searched variable is [t2] *)
+ left_term acc vars (t1, r) t2
| _ -> error "@[invalid guard %a@]" Printer.pp_predicate_named p
- in
- let acc, vars = aux [] bounded_vars hyps in
+ in
+ let acc, partial, vars = parse [] bounded_vars hyps in
+ (match partial with
+ | None -> ()
+ | Some(_, x) ->
+ error "@[missing upper-bound for variable %a@]" Printer.pp_logic_var x);
(match vars with
| [] -> ()
| _ :: _ ->
diff --git a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/quantif.res.oracle
index a6abd09b5f71590f9ee7727713126ee368970500..2975935077ad1df1867de1b0a3d8ddeb30011682 100644
--- a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/quantif.res.oracle
@@ -10,35 +10,32 @@ tests/e-acsl-reject/quantif.i:7:[e-acsl] warning: invalid E-ACSL construct
`invalid guard x ≡ 1 in quantification ∀ ℤ x; x ≡ 1 ⇒ x ≥ 0'.
Ignoring annotation.
tests/e-acsl-reject/quantif.i:8:[e-acsl] warning: invalid E-ACSL construct
- `invalid guard 0 ≤ x in quantification ∀ int x; 0 ≤ x ⇒ x ≥ 0'.
+ `missing upper-bound for variable x in quantification ∀ int x; 0 ≤ x ⇒ x ≥ 0'.
Ignoring annotation.
tests/e-acsl-reject/quantif.i:9:[e-acsl] warning: invalid E-ACSL construct
- `non integer variable x in quantification ∀ float x; 0 ≤ x ∧ x ≤ 3 ⇒ x ≥ 0'.
+ `non integer variable x in quantification ∀ float x; 0 ≤ x ≤ 3 ⇒ x ≥ 0'.
Ignoring annotation.
tests/e-acsl-reject/quantif.i:10:[e-acsl] warning: invalid E-ACSL construct
`unguarded variable y in quantification
- ∀ ℤ x, ℤ y; 0 ≤ x ∧ x ≤ 3 ⇒ x ≥ 0'.
+ ∀ ℤ x, ℤ y; 0 ≤ x ≤ 3 ⇒ x ≥ 0'.
Ignoring annotation.
tests/e-acsl-reject/quantif.i:11:[e-acsl] warning: invalid E-ACSL construct
- `too much constraint(s) in quantification
- ∀ ℤ x; (0 ≤ x ∧ x ≤ 3) ∧ (0 ≤ z ∧ z ≤ 3) ⇒ x ≥ 0'.
+ `too much constraint(s) in quantification ∀ ℤ x; 0 ≤ x ≤ 3 ∧ 0 ≤ z ≤ 3 ⇒ x ≥ 0'.
Ignoring annotation.
tests/e-acsl-reject/quantif.i:12:[e-acsl] warning: invalid E-ACSL construct
- `invalid guard (0 ≤ x ∧ x ≤ 3) ∨ (0 ≤ y ∧ y ≤ 3) in quantification
- ∀ ℤ x, ℤ y; (0 ≤ x ∧ x ≤ 3) ∨ (0 ≤ y ∧ y ≤ 3) ⇒ x ≥ 0'.
+ `invalid guard (0 ≤ x ≤ 3) ∨ (0 ≤ y ≤ 3) in quantification
+ ∀ ℤ x, ℤ y; (0 ≤ x ≤ 3) ∨ (0 ≤ y ≤ 3) ⇒ x ≥ 0'.
Ignoring annotation.
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'.
+ `invalid binder x+1 in quantification ∀ int x; 0 ≤ x+1 ≤ 3 ⇒ x ≥ 0'.
Ignoring annotation.
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'.
+ `too much constraint(s) in quantification ∀ ℤ x; 0 ≤ x < 10 ∧ 9 ≤ 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'.
+ 0 ≤ x < 2 ∧ 0 ≤ y < 5 ∧ 0 ≤ z ≤ y ⇒ x+z ≤ y+1'.
Ignoring annotation.
[e-acsl] 9 annotations were ignored, being untypable.
[e-acsl] 1 annotation was ignored, being unsupported.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle
index 38ce731e0a0e0ea119f9f13d3f0249b83b91ec1c..3a30bf8aec24fcb52cee9de54a4d55b62236ad6a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle
@@ -27,8 +27,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
index 38ce731e0a0e0ea119f9f13d3f0249b83b91ec1c..3a30bf8aec24fcb52cee9de54a4d55b62236ad6a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
@@ -27,8 +27,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
index 78d13f82b67c368ee3a63855fa688aa47c86a5b2..4380850af5cb5be9102782b1ab086f8054288284 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c
index 78d13f82b67c368ee3a63855fa688aa47c86a5b2..4380850af5cb5be9102782b1ab086f8054288284 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_addrOf2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
index 21d3dee0e0f030f66ac342a53dc280c04406bcb0..7c2a416c22f799f690a86ec7ad4c1f9820b87658 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c
index 21d3dee0e0f030f66ac342a53dc280c04406bcb0..7c2a416c22f799f690a86ec7ad4c1f9820b87658 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_alias2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
index 8247aa4992b277a595fe1a382605022369903f86..334e3c34ca9b7db16c438acf83923e07c6c236be 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
index f51c537f6c4ced15af767b68e1b77f6e4e98f724..0eab9e5cd7fa387037dd2f44a24e2e0c324a9095 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
index c765bd1a860143148c2b182ed6978dee10a24bf9..093d1bddd8622a9e71d3c57a5a33c495d0b045d7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
index f20a0e8f72bfe69a262e8296a3d83aa8a8e9b9b4..94d787b234f8775898bc8811464c78e00c450906 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_array2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
index a325b76062211a5ed436c20d38fe24a87c00d72a..b2c0219b9e97df176486a9f6ef77cb213b6a524d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
index 679a07f8431622c1124e50b9c3d478be7b7ad873..daf8cec24130d788ee13baa0ecdf4466d8bc2426 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_at2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
index efdb482b820a7b5c40527c92f786aac9dcdd94c6..5c12cd154664374845c638efaff74a3318f22cc9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
@@ -39,8 +39,7 @@ unsigned long const __fc_rand_max = 32767UL;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
index efdb482b820a7b5c40527c92f786aac9dcdd94c6..5c12cd154664374845c638efaff74a3318f22cc9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
@@ -39,8 +39,7 @@ unsigned long const __fc_rand_max = 32767UL;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
index 31a9781a1007907da2d0e67b2dda838bd09e2074..3a29edcd35d64aa35101f8b7a8f815980e0d4728 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
@@ -168,8 +167,7 @@ void __e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
behavior UnderEstimate_Motoring:
assumes \true;
ensures
- *\old(Mtmin_out)≡*\old(Mtmin_in)∧*\old(Mtmin_in)<0.85**\old(
- Mwmin)?
+ *\old(Mtmin_out) ≡ *\old(Mtmin_in) < 0.85**\old(Mwmin)?
*\old(Mtmin_in) ≢ 0.:
0.85**\old(Mwmin) ≢ 0.;
*/
@@ -193,8 +191,7 @@ void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
behavior UnderEstimate_Motoring:
assumes \true;
ensures
- *\old(Mtmin_out)≡*\old(Mtmin_in)∧*\old(Mtmin_in)<0.85**\old(
- Mwmin)?
+ *\old(Mtmin_out) ≡ *\old(Mtmin_in) < 0.85**\old(Mwmin)?
*\old(Mtmin_in) ≢ 0.:
0.85**\old(Mwmin) ≢ 0.;
*/
@@ -278,7 +275,7 @@ void __e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_if = 0.85 * *__e_acsl_at_6 != 0.;
}
e_acsl_assert(__e_acsl_if,(char *)"Postcondition",(char *)"bar",
- (char *)"*\\old(Mtmin_out)==*\\old(Mtmin_in)&&*\\old(Mtmin_in)<0.85**\\old(Mwmin)?\n *\\old(Mtmin_in) != 0.:\n 0.85**\\old(Mwmin) != 0.",
+ (char *)"*\\old(Mtmin_out) == *\\old(Mtmin_in) < 0.85**\\old(Mwmin)?\n *\\old(Mtmin_in) != 0.:\n 0.85**\\old(Mwmin) != 0.",
25);
__delete_block((void *)(& Mtmin_in));
__delete_block((void *)(& Mwmin));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
index 444d463a0d231e1da2b7fd9b979ff96dc8ea30be..7d763463d922f56be8d97d10c7eb67940d061998 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
@@ -246,8 +245,7 @@ void __e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
behavior UnderEstimate_Motoring:
assumes \true;
ensures
- *\old(Mtmin_out)≡*\old(Mtmin_in)∧*\old(Mtmin_in)<0.85**\old(
- Mwmin)?
+ *\old(Mtmin_out) ≡ *\old(Mtmin_in) < 0.85**\old(Mwmin)?
*\old(Mtmin_in) ≢ 0.:
0.85**\old(Mwmin) ≢ 0.;
*/
@@ -271,8 +269,7 @@ void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
behavior UnderEstimate_Motoring:
assumes \true;
ensures
- *\old(Mtmin_out)≡*\old(Mtmin_in)∧*\old(Mtmin_in)<0.85**\old(
- Mwmin)?
+ *\old(Mtmin_out) ≡ *\old(Mtmin_in) < 0.85**\old(Mwmin)?
*\old(Mtmin_in) ≢ 0.:
0.85**\old(Mwmin) ≢ 0.;
*/
@@ -362,7 +359,7 @@ void __e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_if = 0.85 * *__e_acsl_at_6 != 0.;
}
e_acsl_assert(__e_acsl_if,(char *)"Postcondition",(char *)"bar",
- (char *)"*\\old(Mtmin_out)==*\\old(Mtmin_in)&&*\\old(Mtmin_in)<0.85**\\old(Mwmin)?\n *\\old(Mtmin_in) != 0.:\n 0.85**\\old(Mwmin) != 0.",
+ (char *)"*\\old(Mtmin_out) == *\\old(Mtmin_in) < 0.85**\\old(Mwmin)?\n *\\old(Mtmin_in) != 0.:\n 0.85**\\old(Mwmin) != 0.",
25);
__delete_block((void *)(& Mtmin_in));
__delete_block((void *)(& Mwmin));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
index 560261c0f557090fc2db80dc6af50b238e3b0580..978fcbf96444800e08de36db3f557c8f25b2bde8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
@@ -67,7 +66,7 @@ predicate diffSize{L1, L2}(ℤ i) =
\at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
*/
/*@ behavior yes:
- assumes ∀ int i; 0 < i ∧ i < n ⇒ *(t+(i-1)) ≤ *(t+i);
+ assumes ∀ int i; 0 < i < n ⇒ *(t+(i-1)) ≤ *(t+i);
ensures \result ≡ 1;
*/
int sorted(int *t, int n)
@@ -92,7 +91,7 @@ int sorted(int *t, int n)
}
/*@ behavior yes:
- assumes ∀ int i; 0 < i ∧ i < n ⇒ *(t+(i-1)) ≤ *(t+i);
+ assumes ∀ int i; 0 < i < n ⇒ *(t+(i-1)) ≤ *(t+i);
ensures \result ≡ 1;
*/
int __e_acsl_sorted(int *t, int n)
@@ -137,7 +136,7 @@ int __e_acsl_sorted(int *t, int n)
if (! __e_acsl_at) __e_acsl_implies = 1;
else __e_acsl_implies = __retres == 1;
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",(char *)"sorted",
- (char *)"\\old(\\forall int i; 0 < i && i < n ==> *(t+(i-1)) <= *(t+i)) ==> \\result == 1",
+ (char *)"\\old(\\forall int i; 0 < i < n ==> *(t+(i-1)) <= *(t+i)) ==> \\result == 1",
9);
__delete_block((void *)(& t));
return __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
index a448bc0be5105246308c6a50a07a4cc037843706..bd3df265eb6bdd6c69338cd5749e6a920bcb9b26 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
@@ -122,7 +121,7 @@ predicate diffSize{L1, L2}(ℤ i) =
\at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
*/
/*@ behavior yes:
- assumes ∀ int i; 0 < i ∧ i < n ⇒ *(t+(i-1)) ≤ *(t+i);
+ assumes ∀ int i; 0 < i < n ⇒ *(t+(i-1)) ≤ *(t+i);
ensures \result ≡ 1;
*/
int sorted(int *t, int n)
@@ -147,7 +146,7 @@ int sorted(int *t, int n)
}
/*@ behavior yes:
- assumes ∀ int i; 0 < i ∧ i < n ⇒ *(t+(i-1)) ≤ *(t+i);
+ assumes ∀ int i; 0 < i < n ⇒ *(t+(i-1)) ≤ *(t+i);
ensures \result ≡ 1;
*/
int __e_acsl_sorted(int *t, int n)
@@ -245,7 +244,7 @@ int __e_acsl_sorted(int *t, int n)
__gmpz_clear(__e_acsl_8);
}
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",(char *)"sorted",
- (char *)"\\old(\\forall int i; 0 < i && i < n ==> *(t+(i-1)) <= *(t+i)) ==> \\result == 1",
+ (char *)"\\old(\\forall int i; 0 < i < n ==> *(t+(i-1)) <= *(t+i)) ==> \\result == 1",
9);
__delete_block((void *)(& t));
return __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c
index eb2080fc217d181bed7ae86727654bba84fd810b..f6f87a2a1518e9b2bf32fe33cee26a2796fe0dad 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c
@@ -24,8 +24,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c
index 72b0e104ce997eff5875dfc742d5cc92c05b46a8..5e228b6ea9693d6358276bcab2a92982cd232626 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c
@@ -24,8 +24,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
index 2b98891e4a70b7f4f3c062cb2785dbf22e4b3c07..4d7d96f698a84c1350191d3236f13c25d7a9c642 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
@@ -75,14 +74,14 @@ predicate diffSize{L1, L2}(ℤ i) =
\at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
*/
/*@ behavior exists:
- assumes ∃ ℤ i; (0 ≤ i ∧ i < n) ∧ (int)*((char *)buf+i) ≡ c;
+ assumes ∃ ℤ i; 0 ≤ i < n ∧ (int)*((char *)buf+i) ≡ c;
ensures
∀ int j;
- 0 ≤ j ∧ j < \offset((char *)\result) ⇒
+ 0 ≤ j < \offset((char *)\result) ⇒
(int)*((char *)\old(buf)+j) ≢ \old(c);
behavior not_exists:
- assumes ∀ ℤ k; 0 ≤ k ∧ k < n ⇒ (int)*((char *)buf+k) ≢ c;
+ assumes ∀ ℤ k; 0 ≤ k < n ⇒ (int)*((char *)buf+k) ≢ c;
ensures \result ≡ (void *)0;
*/
void *memchr(void const *buf, int c, size_t n)
@@ -116,14 +115,14 @@ void *memchr(void const *buf, int c, size_t n)
}
/*@ behavior exists:
- assumes ∃ ℤ i; (0 ≤ i ∧ i < n) ∧ (int)*((char *)buf+i) ≡ c;
+ assumes ∃ ℤ i; 0 ≤ i < n ∧ (int)*((char *)buf+i) ≡ c;
ensures
∀ int j;
- 0 ≤ j ∧ j < \offset((char *)\result) ⇒
+ 0 ≤ j < \offset((char *)\result) ⇒
(int)*((char *)\old(buf)+j) ≢ \old(c);
behavior not_exists:
- assumes ∀ ℤ k; 0 ≤ k ∧ k < n ⇒ (int)*((char *)buf+k) ≢ c;
+ assumes ∀ ℤ k; 0 ≤ k < n ⇒ (int)*((char *)buf+k) ≢ c;
ensures \result ≡ (void *)0;
*/
void *__e_acsl_memchr(void const *buf, int c, size_t n)
@@ -224,13 +223,13 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
__e_acsl_implies = __e_acsl_forall;
}
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",(char *)"memchr",
- (char *)"\\old(\\exists integer i; (0 <= i && i < n) && (int)*((char *)buf+i) == c) ==>\n(\\forall int j;\n 0 <= j && j < \\offset((char *)\\result) ==>\n (int)*((char *)\\old(buf)+j) != \\old(c))",
+ (char *)"\\old(\\exists integer i; 0 <= i < n && (int)*((char *)buf+i) == c) ==>\n(\\forall int j;\n 0 <= j < \\offset((char *)\\result) ==>\n (int)*((char *)\\old(buf)+j) != \\old(c))",
13);
if (! __e_acsl_at_4) __e_acsl_implies_2 = 1;
else __e_acsl_implies_2 = __retres == (void *)0;
e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
(char *)"memchr",
- (char *)"\\old(\\forall integer k; 0 <= k && k < n ==> (int)*((char *)buf+k) != c) ==>\n\\result == (void *)0",
+ (char *)"\\old(\\forall integer k; 0 <= k < n ==> (int)*((char *)buf+k) != c) ==>\n\\result == (void *)0",
16);
__delete_block((void *)(& buf));
__delete_block((void *)(& __retres));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
index a08c2a6692fd3823e7bfd3d950ad08871ed83095..d285db47dbfb0a91730f51d7a896210db6fe1b4e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
@@ -130,14 +129,14 @@ predicate diffSize{L1, L2}(ℤ i) =
\at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
*/
/*@ behavior exists:
- assumes ∃ ℤ i; (0 ≤ i ∧ i < n) ∧ (int)*((char *)buf+i) ≡ c;
+ assumes ∃ ℤ i; 0 ≤ i < n ∧ (int)*((char *)buf+i) ≡ c;
ensures
∀ int j;
- 0 ≤ j ∧ j < \offset((char *)\result) ⇒
+ 0 ≤ j < \offset((char *)\result) ⇒
(int)*((char *)\old(buf)+j) ≢ \old(c);
behavior not_exists:
- assumes ∀ ℤ k; 0 ≤ k ∧ k < n ⇒ (int)*((char *)buf+k) ≢ c;
+ assumes ∀ ℤ k; 0 ≤ k < n ⇒ (int)*((char *)buf+k) ≢ c;
ensures \result ≡ (void *)0;
*/
void *memchr(void const *buf, int c, size_t n)
@@ -171,14 +170,14 @@ void *memchr(void const *buf, int c, size_t n)
}
/*@ behavior exists:
- assumes ∃ ℤ i; (0 ≤ i ∧ i < n) ∧ (int)*((char *)buf+i) ≡ c;
+ assumes ∃ ℤ i; 0 ≤ i < n ∧ (int)*((char *)buf+i) ≡ c;
ensures
∀ int j;
- 0 ≤ j ∧ j < \offset((char *)\result) ⇒
+ 0 ≤ j < \offset((char *)\result) ⇒
(int)*((char *)\old(buf)+j) ≢ \old(c);
behavior not_exists:
- assumes ∀ ℤ k; 0 ≤ k ∧ k < n ⇒ (int)*((char *)buf+k) ≢ c;
+ assumes ∀ ℤ k; 0 ≤ k < n ⇒ (int)*((char *)buf+k) ≢ c;
ensures \result ≡ (void *)0;
*/
void *__e_acsl_memchr(void const *buf, int c, size_t n)
@@ -369,13 +368,13 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
__gmpz_clear(__e_acsl_j);
}
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",(char *)"memchr",
- (char *)"\\old(\\exists integer i; (0 <= i && i < n) && (int)*((char *)buf+i) == c) ==>\n(\\forall int j;\n 0 <= j && j < \\offset((char *)\\result) ==>\n (int)*((char *)\\old(buf)+j) != \\old(c))",
+ (char *)"\\old(\\exists integer i; 0 <= i < n && (int)*((char *)buf+i) == c) ==>\n(\\forall int j;\n 0 <= j < \\offset((char *)\\result) ==>\n (int)*((char *)\\old(buf)+j) != \\old(c))",
13);
if (! __e_acsl_at_4) __e_acsl_implies_2 = 1;
else __e_acsl_implies_2 = __retres == (void *)0;
e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
(char *)"memchr",
- (char *)"\\old(\\forall integer k; 0 <= k && k < n ==> (int)*((char *)buf+k) != c) ==>\n\\result == (void *)0",
+ (char *)"\\old(\\forall integer k; 0 <= k < n ==> (int)*((char *)buf+k) != c) ==>\n\\result == (void *)0",
16);
__delete_block((void *)(& buf));
__delete_block((void *)(& __retres));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
index 9548021ec848b432f909a5628cf558812031de88..ca81671e63bf5d3315920ec6a7c73bdda1286577 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
@@ -52,8 +52,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
index 9548021ec848b432f909a5628cf558812031de88..ca81671e63bf5d3315920ec6a7c73bdda1286577 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
@@ -52,8 +52,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
index 45a8c5865d8ec62066579026e41ee9a880ad12fe..f430e7f11418a12ae2c468491af2c950816f95cb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
@@ -29,8 +29,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
index d265181dd9d1f38d5cd9adb1f7c1e93cd2627475..3e4d00c33428b5d069971a79f82fae9c81656e80 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
@@ -29,8 +29,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
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
index d9defb9f39085df3a61f9f88a36b6afd350f806e..7bd2cea581d6201fdd73a68ce3cc3e1b3d85ba53 100644
--- 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
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
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
index dfe69e1c88d7f3fc2fa5d1dfcbbb08e5ea8b74f1..4f7107fb96b3079894e75797193557388c12aae6 100644
--- 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
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
index 7258ddac41bf74445d8b0d57912d430c70f90095..3a5217d031e8eab7a4445ebbf472d68b99916e6a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
@@ -26,8 +26,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c
index 87cc310d9afb045bd4e425ed2b6179d0b6fcfd06..605e2c6463deb0ddebb3b36e5619259ed1eee89d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c
index 87cc310d9afb045bd4e425ed2b6179d0b6fcfd06..605e2c6463deb0ddebb3b36e5619259ed1eee89d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
index 4287e8ff2714275b64a6c3ba9de8f6dbeae8d01f..44d387a450dcea2830b9c8ee6adbfc317d1504ae 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
index 4287e8ff2714275b64a6c3ba9de8f6dbeae8d01f..44d387a450dcea2830b9c8ee6adbfc317d1504ae 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
index aa39b2d317a82f1cf1b25bbcc01326f54a2ac159..4243d6ff710010128726074b2591b0f1e9c607fd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
index 98f8ec27baf9ef9d98d37eb48f4021b96a03f7a1..641f5e893549e70fd4bce2d55563c271dfc47294 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
index ceb5d2b3fa7d5e2b05376c4519a9e3336fad3520..10c2fd56df57d3dbed81298cfab6674305f44945 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
index 149fb7ae8e94c66249fe41c431f1e9f48937505d..830ac36df981137ff8ff2637f69036a8bffb90d4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_comparison2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
index 0acbead3158b8a94b1fc1343d2800d3902c870c2..c84595e51e10fb0c16e0effeda261db40900b177 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c
index 0acbead3158b8a94b1fc1343d2800d3902c870c2..c84595e51e10fb0c16e0effeda261db40900b177 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_false2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
index 4ff593abac462a51cf0f7101c755c760df6b1fbf..e8b69159b6cdb4cb070302d5145f7531a1a50f7b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
index 4fd16fafea57599487930b5481f58c816cfa3ca3..0681fe2626466a67586bd5baf3c54f1d53b7562f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_function_contract2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
index c8f1be53be9640ee9d3877e1b9927cc4d6dd487d..b76b7ae944050767bf1e38be584aa4de0f9c1fb5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
index edc38d0e77d6df3015fa1cbff6b8a3b4f37456ad..eec3ef056a30a0eb08ed922ba099af3af2b0e99d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
index 8ce91c0dbef1a5537c983bbde77c4045899e21b6..0ca24f6d3e0362b36c01a135f6b9e30e9faacf89 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
index 44899d75a9d3381987b7bbf7ed7ff310f81b19d2..c094b663632d6ea018577df820d63adfc1d36c36 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
index 9766e975635bafa886aa55e78e37a62ed0607d9a..23a8972897114309b770f4fc593c254633d5f254 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
@@ -49,12 +48,12 @@ int main(void)
int i;
i = 0;
while (i < 10) {
- /*@ invariant 0 ≤ i ∧ i < 10; */
+ /*@ invariant 0 ≤ i < 10; */
{
int __e_acsl_and;
if (0 <= i) __e_acsl_and = i < 10; else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Invariant",(char *)"main",
- (char *)"0 <= i && i < 10",9);
+ (char *)"0 <= i < 10",9);
}
x += i;
/*@ invariant i ≤ x; */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c
index 06994dd7f2eb9302c6256c9bfe70d5269c6ba7ad..37ae7523f9df65948183150a22cc40f0060250a3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_invariant2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
@@ -72,7 +71,7 @@ int main(void)
int i;
i = 0;
while (i < 10) {
- /*@ invariant 0 ≤ i ∧ i < 10; */
+ /*@ invariant 0 ≤ i < 10; */
{
mpz_t __e_acsl;
mpz_t __e_acsl_i;
@@ -96,7 +95,7 @@ int main(void)
}
else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Invariant",(char *)"main",
- (char *)"0 <= i && i < 10",9);
+ (char *)"0 <= i < 10",9);
__gmpz_clear(__e_acsl);
__gmpz_clear(__e_acsl_i);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
index 3f7d2a0d79c8925862fff3e0b6167d8f25ba90bb..cc45f905cef968012f5bf67340e30880a4452ef9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
index 7816d4df0c47d2b5cd26a8421c663aa229e1c76f..121dcba8ef7c27f16c7c5d6fe04e4645aa65e12b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_labeled_stmt2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
index daf1108de6c05159db0d92ade68ec9b724aec005..2d46309daf3dd5d0843ae7d375c79ee1ae91c62a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
@@ -187,12 +186,12 @@ int main(void)
e_acsl_assert(__e_acsl_or_5 == (y != 0),(char *)"Assertion",
(char *)"main",(char *)"(x!=0||y!=0) == (y!=0)",29);
}
- /*@ assert (x≢0∧y≢0) ≡ (x≢0); */
+ /*@ assert (x≢0 ∧ y≢0) ≡ (x≢0); */
{
int __e_acsl_and_5;
if (x != 0) __e_acsl_and_5 = y != 0; else __e_acsl_and_5 = 0;
e_acsl_assert(__e_acsl_and_5 == (x != 0),(char *)"Assertion",
- (char *)"main",(char *)"(x!=0&&y!=0) == (x!=0)",30);
+ (char *)"main",(char *)"(x!=0 && y!=0) == (x!=0)",30);
}
__retres = 0;
return __retres;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c
index 34ae8c2cefe070f0e54e8f1a76c3e40decf421da..b200394ad1ccf91bc7316905e4d1074a56fd7d2c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_lazy2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
@@ -708,7 +707,7 @@ int main(void)
__gmpz_clear(__e_acsl_y_20);
__gmpz_clear(__e_acsl_45);
}
- /*@ assert (x≢0∧y≢0) ≡ (x≢0); */
+ /*@ assert (x≢0 ∧ y≢0) ≡ (x≢0); */
{
mpz_t __e_acsl_x_22;
mpz_t __e_acsl_46;
@@ -743,7 +742,7 @@ int main(void)
__e_acsl_eq_27 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_and_5),
(__mpz_struct const *)(__e_acsl_49));
e_acsl_assert(__e_acsl_eq_27 == 0,(char *)"Assertion",(char *)"main",
- (char *)"(x!=0&&y!=0) == (x!=0)",30);
+ (char *)"(x!=0 && y!=0) == (x!=0)",30);
__gmpz_clear(__e_acsl_x_22);
__gmpz_clear(__e_acsl_46);
__gmpz_clear(__e_acsl_and_5);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
index 12112426a52f0e04e65be70ef0f6c6c1eb880f53..2bfad72eea67d552455643f71429aef80f124aed 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
@@ -41,14 +40,14 @@ predicate diffSize{L1, L2}(ℤ i) =
\at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
*/
int A[10];
-/*@ requires ∀ ℤ i; 0 ≤ i ∧ i < 9 ⇒ A[i] ≤ A[i+1];
+/*@ requires ∀ ℤ i; 0 ≤ i < 9 ⇒ A[i] ≤ A[i+1];
behavior exists:
- assumes ∃ ℤ j; (0 ≤ j ∧ j < 10) ∧ A[j] ≡ elt;
+ assumes ∃ ℤ j; 0 ≤ j < 10 ∧ A[j] ≡ elt;
ensures \result ≡ 1;
behavior not_exists:
- assumes ∀ ℤ j; 0 ≤ j ∧ j < 10 ⇒ A[j] ≢ elt;
+ assumes ∀ ℤ j; 0 ≤ j < 10 ⇒ A[j] ≢ elt;
ensures \result ≡ 0;
*/
int search(int elt)
@@ -77,13 +76,12 @@ int search(int elt)
}
e_acsl_end_loop1: ;
e_acsl_assert(__e_acsl_forall,(char *)"Invariant",(char *)"search",
- (char *)"\\forall integer i; 0 <= i && i < k ==> A[i] < elt",
- 20);
+ (char *)"\\forall integer i; 0 <= i < k ==> A[i] < elt",20);
if (0 <= k) __e_acsl_and = k <= 10; else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Invariant",(char *)"search",
- (char *)"0 <= k && k <= 10",19);
- /*@ loop invariant 0 ≤ k ∧ k ≤ 10;
- loop invariant ∀ ℤ i; 0 ≤ i ∧ i < k ⇒ A[i] < elt;
+ (char *)"0 <= k <= 10",19);
+ /*@ loop invariant 0 ≤ k ≤ 10;
+ loop invariant ∀ ℤ i; 0 ≤ i < k ⇒ A[i] < elt;
*/
while (k < 10) {
if (A[k] == elt) {
@@ -102,7 +100,7 @@ int search(int elt)
k ++;
if (0 <= k) __e_acsl_and_2 = k <= 10; else __e_acsl_and_2 = 0;
e_acsl_assert(__e_acsl_and_2,(char *)"Invariant",(char *)"search",
- (char *)"0 <= k && k <= 10",19);
+ (char *)"0 <= k <= 10",19);
__e_acsl_forall_2 = 1;
__e_acsl_i_2 = 0;
while (1) {
@@ -120,7 +118,7 @@ int search(int elt)
}
e_acsl_end_loop2: ;
e_acsl_assert(__e_acsl_forall_2,(char *)"Invariant",(char *)"search",
- (char *)"\\forall integer i; 0 <= i && i < k ==> A[i] < elt",
+ (char *)"\\forall integer i; 0 <= i < k ==> A[i] < elt",
20);
}
}
@@ -129,14 +127,14 @@ int search(int elt)
return_label: return __retres;
}
-/*@ requires ∀ ℤ i; 0 ≤ i ∧ i < 9 ⇒ A[i] ≤ A[i+1];
+/*@ requires ∀ ℤ i; 0 ≤ i < 9 ⇒ A[i] ≤ A[i+1];
behavior exists:
- assumes ∃ ℤ j; (0 ≤ j ∧ j < 10) ∧ A[j] ≡ elt;
+ assumes ∃ ℤ j; 0 ≤ j < 10 ∧ A[j] ≡ elt;
ensures \result ≡ 1;
behavior not_exists:
- assumes ∀ ℤ j; 0 ≤ j ∧ j < 10 ⇒ A[j] ≢ elt;
+ assumes ∀ ℤ j; 0 ≤ j < 10 ⇒ A[j] ≢ elt;
ensures \result ≡ 0;
*/
int __e_acsl_search(int elt)
@@ -168,7 +166,7 @@ int __e_acsl_search(int elt)
}
e_acsl_end_loop3: ;
e_acsl_assert(__e_acsl_forall,(char *)"Precondition",(char *)"search",
- (char *)"\\forall integer i; 0 <= i && i < 9 ==> A[i] <= A[i+1]",
+ (char *)"\\forall integer i; 0 <= i < 9 ==> A[i] <= A[i+1]",
9);
{
int __e_acsl_forall_2;
@@ -220,13 +218,13 @@ int __e_acsl_search(int elt)
if (! __e_acsl_at) __e_acsl_implies = 1;
else __e_acsl_implies = __retres == 1;
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",(char *)"search",
- (char *)"\\old(\\exists integer j; (0 <= j && j < 10) && A[j] == elt) ==> \\result == 1",
+ (char *)"\\old(\\exists integer j; 0 <= j < 10 && A[j] == elt) ==> \\result == 1",
12);
if (! __e_acsl_at_2) __e_acsl_implies_2 = 1;
else __e_acsl_implies_2 = __retres == 0;
e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
(char *)"search",
- (char *)"\\old(\\forall integer j; 0 <= j && j < 10 ==> A[j] != elt) ==> \\result == 0",
+ (char *)"\\old(\\forall integer j; 0 <= j < 10 ==> A[j] != elt) ==> \\result == 0",
15);
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
index f844748eb6cf8fed0b1cc63b89caadbe57ac130a..fa7fbbfa6f6ced5675cb9d55bbd28f8335d440f2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_linear_search2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
@@ -95,14 +94,14 @@ predicate diffSize{L1, L2}(ℤ i) =
\at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
*/
int A[10];
-/*@ requires ∀ ℤ i; 0 ≤ i ∧ i < 9 ⇒ A[i] ≤ A[i+1];
+/*@ requires ∀ ℤ i; 0 ≤ i < 9 ⇒ A[i] ≤ A[i+1];
behavior exists:
- assumes ∃ ℤ j; (0 ≤ j ∧ j < 10) ∧ A[j] ≡ elt;
+ assumes ∃ ℤ j; 0 ≤ j < 10 ∧ A[j] ≡ elt;
ensures \result ≡ 1;
behavior not_exists:
- assumes ∀ ℤ j; 0 ≤ j ∧ j < 10 ⇒ A[j] ≢ elt;
+ assumes ∀ ℤ j; 0 ≤ j < 10 ⇒ A[j] ≢ elt;
ensures \result ≡ 0;
*/
int search(int elt)
@@ -167,8 +166,7 @@ int search(int elt)
}
e_acsl_end_loop1: ;
e_acsl_assert(__e_acsl_forall,(char *)"Invariant",(char *)"search",
- (char *)"\\forall integer i; 0 <= i && i < k ==> A[i] < elt",
- 20);
+ (char *)"\\forall integer i; 0 <= i < k ==> A[i] < elt",20);
__gmpz_init_set_si(__e_acsl_4,(long)0);
__gmpz_init_set_si(__e_acsl_k_2,(long)k);
__e_acsl_le = __gmpz_cmp((__mpz_struct const *)(__e_acsl_4),
@@ -187,12 +185,12 @@ int search(int elt)
}
else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Invariant",(char *)"search",
- (char *)"0 <= k && k <= 10",19);
+ (char *)"0 <= k <= 10",19);
__gmpz_clear(__e_acsl_i);
__gmpz_clear(__e_acsl_4);
__gmpz_clear(__e_acsl_k_2);
- /*@ loop invariant 0 ≤ k ∧ k ≤ 10;
- loop invariant ∀ ℤ i; 0 ≤ i ∧ i < k ⇒ A[i] < elt;
+ /*@ loop invariant 0 ≤ k ≤ 10;
+ loop invariant ∀ ℤ i; 0 ≤ i < k ⇒ A[i] < elt;
*/
while (k < 10) {
if (A[k] == elt) {
@@ -230,7 +228,7 @@ int search(int elt)
}
else __e_acsl_and_2 = 0;
e_acsl_assert(__e_acsl_and_2,(char *)"Invariant",(char *)"search",
- (char *)"0 <= k && k <= 10",19);
+ (char *)"0 <= k <= 10",19);
__e_acsl_forall_2 = 1;
__gmpz_init(__e_acsl_i_3);
{
@@ -281,7 +279,7 @@ int search(int elt)
}
e_acsl_end_loop2: ;
e_acsl_assert(__e_acsl_forall_2,(char *)"Invariant",(char *)"search",
- (char *)"\\forall integer i; 0 <= i && i < k ==> A[i] < elt",
+ (char *)"\\forall integer i; 0 <= i < k ==> A[i] < elt",
20);
__gmpz_clear(__e_acsl_6);
__gmpz_clear(__e_acsl_k_4);
@@ -293,14 +291,14 @@ int search(int elt)
return_label: return __retres;
}
-/*@ requires ∀ ℤ i; 0 ≤ i ∧ i < 9 ⇒ A[i] ≤ A[i+1];
+/*@ requires ∀ ℤ i; 0 ≤ i < 9 ⇒ A[i] ≤ A[i+1];
behavior exists:
- assumes ∃ ℤ j; (0 ≤ j ∧ j < 10) ∧ A[j] ≡ elt;
+ assumes ∃ ℤ j; 0 ≤ j < 10 ∧ A[j] ≡ elt;
ensures \result ≡ 1;
behavior not_exists:
- assumes ∀ ℤ j; 0 ≤ j ∧ j < 10 ⇒ A[j] ≢ elt;
+ assumes ∀ ℤ j; 0 ≤ j < 10 ⇒ A[j] ≢ elt;
ensures \result ≡ 0;
*/
int __e_acsl_search(int elt)
@@ -371,7 +369,7 @@ int __e_acsl_search(int elt)
}
e_acsl_end_loop3: ;
e_acsl_assert(__e_acsl_forall,(char *)"Precondition",(char *)"search",
- (char *)"\\forall integer i; 0 <= i && i < 9 ==> A[i] <= A[i+1]",
+ (char *)"\\forall integer i; 0 <= i < 9 ==> A[i] <= A[i+1]",
9);
__gmpz_clear(__e_acsl_i);
{
@@ -503,7 +501,7 @@ int __e_acsl_search(int elt)
__gmpz_clear(__e_acsl_12);
}
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",(char *)"search",
- (char *)"\\old(\\exists integer j; (0 <= j && j < 10) && A[j] == elt) ==> \\result == 1",
+ (char *)"\\old(\\exists integer j; 0 <= j < 10 && A[j] == elt) ==> \\result == 1",
12);
if (! __e_acsl_at_2) __e_acsl_implies_2 = 1;
else {
@@ -520,7 +518,7 @@ int __e_acsl_search(int elt)
}
e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
(char *)"search",
- (char *)"\\old(\\forall integer j; 0 <= j && j < 10 ==> A[j] != elt) ==> \\result == 0",
+ (char *)"\\old(\\forall integer j; 0 <= j < 10 ==> A[j] != elt) ==> \\result == 0",
15);
return __retres;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
index 3223de6d50ba6fb17b9dcf5e6e16cbf98fb61ad2..9be1b7fd17707165c8e9c28abef3846770f07a43 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
index f1c4480d60e1fdd1c33915107f6d94a0309d44b5..b2ddbe5b10cbf160817379d9cf10eb76ba3992e3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
index 49b0543c428a69df2f67918a0a871d52c6f411b8..7bd6be967069d604c3549fbe790f8d208a9cf7fa 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
@@ -27,8 +27,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
index 49b0543c428a69df2f67918a0a871d52c6f411b8..7bd6be967069d604c3549fbe790f8d208a9cf7fa 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
@@ -27,8 +27,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
index 08df9312e669efd4b0072ca262abf88f178a145b..1426ccd2a3d858e0d15aefdedab493012b34533c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
index c83d640e1134723c61dd9642964c87a55809bae2..f6f10141afa8648cdf8fc7a9947789e753f775fb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
index c8d331edc7c550479e6c5fbd1dbb892f9789bb94..07e28bd8bd5cf1eeb957a0c2e20e700354e78043 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
@@ -51,8 +50,8 @@ void simple_loop(void)
int __e_acsl_and;
if (0 <= i) __e_acsl_and = i <= 10; else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Invariant",(char *)"simple_loop",
- (char *)"0 <= i && i <= 10",10);
- /*@ loop invariant 0 ≤ i ∧ i ≤ 10; */
+ (char *)"0 <= i <= 10",10);
+ /*@ loop invariant 0 ≤ i ≤ 10; */
while (i < 10) {
sum += i;
{
@@ -60,7 +59,7 @@ void simple_loop(void)
i ++;
if (0 <= i) __e_acsl_and_2 = i <= 10; else __e_acsl_and_2 = 0;
e_acsl_assert(__e_acsl_and_2,(char *)"Invariant",
- (char *)"simple_loop",(char *)"0 <= i && i <= 10",10);
+ (char *)"simple_loop",(char *)"0 <= i <= 10",10);
}
}
}
@@ -77,8 +76,8 @@ void nested_loops(void)
int __e_acsl_and;
if (0 <= i) __e_acsl_and = i <= 10; else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Invariant",(char *)"nested_loops",
- (char *)"0 <= i && i <= 10",17);
- /*@ loop invariant 0 ≤ i ∧ i ≤ 10; */
+ (char *)"0 <= i <= 10",17);
+ /*@ loop invariant 0 ≤ i ≤ 10; */
while (i < 10) {
{
int j;
@@ -120,17 +119,15 @@ void nested_loops(void)
e_acsl_end_loop1: ;
e_acsl_assert(__e_acsl_forall,(char *)"Invariant",
(char *)"nested_loops",
- (char *)"\\forall integer k, integer l;\n (0 <= k && k < i) && (0 <= l && l < j) ==> t[k][l] == k*l",
+ (char *)"\\forall integer k, integer l; 0 <= k < i && 0 <= l < j ==> t[k][l] == k*l",
21);
if (0 <= j) __e_acsl_and_2 = j <= 15; else __e_acsl_and_2 = 0;
e_acsl_assert(__e_acsl_and_2,(char *)"Invariant",
- (char *)"nested_loops",(char *)"0 <= j && j <= 15",
- 19);
- /*@ loop invariant 0 ≤ j ∧ j ≤ 15;
+ (char *)"nested_loops",(char *)"0 <= j <= 15",19);
+ /*@ loop invariant 0 ≤ j ≤ 15;
loop invariant
∀ ℤ k, ℤ l;
- (0 ≤ k ∧ k < i) ∧ (0 ≤ l ∧ l < j) ⇒
- t[k][l] ≡ k*l;
+ 0 ≤ k < i ∧ 0 ≤ l < j ⇒ t[k][l] ≡ k*l;
*/
while (j < 15) {
t[i][j] = i * j;
@@ -142,8 +139,7 @@ void nested_loops(void)
j ++;
if (0 <= j) __e_acsl_and_3 = j <= 15; else __e_acsl_and_3 = 0;
e_acsl_assert(__e_acsl_and_3,(char *)"Invariant",
- (char *)"nested_loops",
- (char *)"0 <= j && j <= 15",19);
+ (char *)"nested_loops",(char *)"0 <= j <= 15",19);
__e_acsl_forall_2 = 1;
__e_acsl_k_2 = 0;
while (1) {
@@ -176,7 +172,7 @@ void nested_loops(void)
e_acsl_end_loop2: ;
e_acsl_assert(__e_acsl_forall_2,(char *)"Invariant",
(char *)"nested_loops",
- (char *)"\\forall integer k, integer l;\n (0 <= k && k < i) && (0 <= l && l < j) ==> t[k][l] == k*l",
+ (char *)"\\forall integer k, integer l; 0 <= k < i && 0 <= l < j ==> t[k][l] == k*l",
21);
}
}
@@ -187,7 +183,7 @@ void nested_loops(void)
i ++;
if (0 <= i) __e_acsl_and_4 = i <= 10; else __e_acsl_and_4 = 0;
e_acsl_assert(__e_acsl_and_4,(char *)"Invariant",
- (char *)"nested_loops",(char *)"0 <= i && i <= 10",17);
+ (char *)"nested_loops",(char *)"0 <= i <= 10",17);
}
}
}
@@ -205,8 +201,8 @@ void unnatural_loop(void)
int __e_acsl_and;
if (0 <= i) __e_acsl_and = i <= 6; else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Invariant",
- (char *)"unnatural_loop",(char *)"0 <= i && i <= 6",28);
- /*@ loop invariant 0 ≤ i ∧ i ≤ 6; */
+ (char *)"unnatural_loop",(char *)"0 <= i <= 6",28);
+ /*@ loop invariant 0 ≤ i ≤ 6; */
while (i < 10) {
if (x == 5) break;
x = i;
@@ -215,8 +211,7 @@ void unnatural_loop(void)
i ++;
if (0 <= i) __e_acsl_and_2 = i <= 6; else __e_acsl_and_2 = 0;
e_acsl_assert(__e_acsl_and_2,(char *)"Invariant",
- (char *)"unnatural_loop",(char *)"0 <= i && i <= 6",
- 28);
+ (char *)"unnatural_loop",(char *)"0 <= i <= 6",28);
}
}
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c
index 82cb91e3600e8300a781886087a7dc65a060109e..24252ed397a0de8a4eaa87dc97e527a357d85d0f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
@@ -134,10 +133,10 @@ void simple_loop(void)
}
else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Invariant",(char *)"simple_loop",
- (char *)"0 <= i && i <= 10",10);
+ (char *)"0 <= i <= 10",10);
__gmpz_clear(__e_acsl);
__gmpz_clear(__e_acsl_i);
- /*@ loop invariant 0 ≤ i ∧ i ≤ 10; */
+ /*@ loop invariant 0 ≤ i ≤ 10; */
while (i < 10) {
sum += i;
{
@@ -164,7 +163,7 @@ void simple_loop(void)
}
else __e_acsl_and_2 = 0;
e_acsl_assert(__e_acsl_and_2,(char *)"Invariant",
- (char *)"simple_loop",(char *)"0 <= i && i <= 10",10);
+ (char *)"simple_loop",(char *)"0 <= i <= 10",10);
__gmpz_clear(__e_acsl_3);
__gmpz_clear(__e_acsl_i_3);
}
@@ -202,10 +201,10 @@ void nested_loops(void)
}
else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Invariant",(char *)"nested_loops",
- (char *)"0 <= i && i <= 10",17);
+ (char *)"0 <= i <= 10",17);
__gmpz_clear(__e_acsl);
__gmpz_clear(__e_acsl_i);
- /*@ loop invariant 0 ≤ i ∧ i ≤ 10; */
+ /*@ loop invariant 0 ≤ i ≤ 10; */
while (i < 10) {
{
int j;
@@ -303,7 +302,7 @@ void nested_loops(void)
e_acsl_end_loop1: ;
e_acsl_assert(__e_acsl_forall,(char *)"Invariant",
(char *)"nested_loops",
- (char *)"\\forall integer k, integer l;\n (0 <= k && k < i) && (0 <= l && l < j) ==> t[k][l] == k*l",
+ (char *)"\\forall integer k, integer l; 0 <= k < i && 0 <= l < j ==> t[k][l] == k*l",
21);
__gmpz_init_set_si(__e_acsl_8,(long)0);
__gmpz_init_set_si(__e_acsl_j_2,(long)j);
@@ -323,17 +322,15 @@ void nested_loops(void)
}
else __e_acsl_and_2 = 0;
e_acsl_assert(__e_acsl_and_2,(char *)"Invariant",
- (char *)"nested_loops",(char *)"0 <= j && j <= 15",
- 19);
+ (char *)"nested_loops",(char *)"0 <= j <= 15",19);
__gmpz_clear(__e_acsl_k);
__gmpz_clear(__e_acsl_l);
__gmpz_clear(__e_acsl_8);
__gmpz_clear(__e_acsl_j_2);
- /*@ loop invariant 0 ≤ j ∧ j ≤ 15;
+ /*@ loop invariant 0 ≤ j ≤ 15;
loop invariant
∀ ℤ k, ℤ l;
- (0 ≤ k ∧ k < i) ∧ (0 ≤ l ∧ l < j) ⇒
- t[k][l] ≡ k*l;
+ 0 ≤ k < i ∧ 0 ≤ l < j ⇒ t[k][l] ≡ k*l;
*/
while (j < 15) {
t[i][j] = i * j;
@@ -364,8 +361,7 @@ void nested_loops(void)
}
else __e_acsl_and_3 = 0;
e_acsl_assert(__e_acsl_and_3,(char *)"Invariant",
- (char *)"nested_loops",
- (char *)"0 <= j && j <= 15",19);
+ (char *)"nested_loops",(char *)"0 <= j <= 15",19);
__e_acsl_forall_2 = 1;
__gmpz_init(__e_acsl_k_3);
__gmpz_init(__e_acsl_l_3);
@@ -457,7 +453,7 @@ void nested_loops(void)
e_acsl_end_loop2: ;
e_acsl_assert(__e_acsl_forall_2,(char *)"Invariant",
(char *)"nested_loops",
- (char *)"\\forall integer k, integer l;\n (0 <= k && k < i) && (0 <= l && l < j) ==> t[k][l] == k*l",
+ (char *)"\\forall integer k, integer l; 0 <= k < i && 0 <= l < j ==> t[k][l] == k*l",
21);
__gmpz_clear(__e_acsl_10);
__gmpz_clear(__e_acsl_j_4);
@@ -491,7 +487,7 @@ void nested_loops(void)
}
else __e_acsl_and_4 = 0;
e_acsl_assert(__e_acsl_and_4,(char *)"Invariant",
- (char *)"nested_loops",(char *)"0 <= i && i <= 10",17);
+ (char *)"nested_loops",(char *)"0 <= i <= 10",17);
__gmpz_clear(__e_acsl_17);
__gmpz_clear(__e_acsl_i_5);
}
@@ -530,10 +526,10 @@ void unnatural_loop(void)
}
else __e_acsl_and = 0;
e_acsl_assert(__e_acsl_and,(char *)"Invariant",
- (char *)"unnatural_loop",(char *)"0 <= i && i <= 6",28);
+ (char *)"unnatural_loop",(char *)"0 <= i <= 6",28);
__gmpz_clear(__e_acsl);
__gmpz_clear(__e_acsl_i);
- /*@ loop invariant 0 ≤ i ∧ i ≤ 6; */
+ /*@ loop invariant 0 ≤ i ≤ 6; */
while (i < 10) {
if (x == 5) break;
x = i;
@@ -561,8 +557,7 @@ void unnatural_loop(void)
}
else __e_acsl_and_2 = 0;
e_acsl_assert(__e_acsl_and_2,(char *)"Invariant",
- (char *)"unnatural_loop",(char *)"0 <= i && i <= 6",
- 28);
+ (char *)"unnatural_loop",(char *)"0 <= i <= 6",28);
__gmpz_clear(__e_acsl_3);
__gmpz_clear(__e_acsl_i_3);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
index ef2552990a1491d903742077e94d975fb4519e07..68b8e12c1e7d1cf95d8f501aa57426bcee5bc276 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c
index 4b079ab0cc12b7049106491136d9a94d97b68a18..bddeaecca43ac0d25ff68020e6c8d5db00c12d9c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_nested_code_annot2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
index 1c0d0332fa6028a385857033e928aa84ac84ee51..382082219bd74e29e3b6eb6f16a5577de9f49a1d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c
index a6009c1c2c4d32b9ade259755dbe3411c443b07e..4c32310f080a86a789cc3d5674c2a931b7ea049a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_not2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
index 32f5d86c99626cd7364507460b2d14078add2108..8093abd3d08701ab1f1cc43c24fb1c97f4141bc5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c
index 32f5d86c99626cd7364507460b2d14078add2108..8093abd3d08701ab1f1cc43c24fb1c97f4141bc5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_null2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
index afa63f7ba33e0979922bfdcfed8e37ce6e0e29a1..d23e55160eaa223c0004825d8c50d2c246138fba 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants.c
@@ -27,8 +27,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c
index e25ff06fa597189b8af9defc20c9241ecc0a4285..55b963b578c55d3d40c4a6e077b5f3fb54423719 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_other_constants2.c
@@ -27,8 +27,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
index f854d7b49be46cdf62b315b95428029093d74556..33b428eb6843299ba58c0c8aeee6d8974cc7c43b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
index 59051aa42d601086b39fa22ceec81b3b0dd30660..91f9702d49d9cb481e557c93951d9c1d8c8fad6f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
index c545933f565de0de097c0df20e399148c16990cc..0e7d2a314f8151b6447223fb2cb1736969f02784 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
index c545933f565de0de097c0df20e399148c16990cc..0e7d2a314f8151b6447223fb2cb1736969f02784 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
index 68298283100daf32b9d4a9b96b461ac88a80906e..e82c4fb12a2b3275a95cd3881e0f057601c1aa3b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
@@ -43,7 +42,7 @@ predicate diffSize{L1, L2}(ℤ i) =
int main(void)
{
int __retres;
- /*@ assert ∀ ℤ x; 0 ≤ x ∧ x ≤ 1 ⇒ x ≡ 0 ∨ x ≡ 1; */
+ /*@ assert ∀ ℤ x; 0 ≤ x ≤ 1 ⇒ x ≡ 0 ∨ x ≡ 1; */
{
int __e_acsl_forall;
int __e_acsl_x;
@@ -65,10 +64,10 @@ int main(void)
}
e_acsl_end_loop1: ;
e_acsl_assert(__e_acsl_forall,(char *)"Assertion",(char *)"main",
- (char *)"\\forall integer x; 0 <= x && x <= 1 ==> x == 0 || x == 1",
+ (char *)"\\forall integer x; 0 <= x <= 1 ==> x == 0 || x == 1",
11);
}
- /*@ assert ∀ ℤ x; 0 < x ∧ x ≤ 1 ⇒ x ≡ 1; */
+ /*@ assert ∀ ℤ x; 0 < x ≤ 1 ⇒ x ≡ 1; */
{
int __e_acsl_forall_2;
int __e_acsl_x_2;
@@ -85,10 +84,9 @@ int main(void)
}
e_acsl_end_loop2: ;
e_acsl_assert(__e_acsl_forall_2,(char *)"Assertion",(char *)"main",
- (char *)"\\forall integer x; 0 < x && x <= 1 ==> x == 1",
- 12);
+ (char *)"\\forall integer x; 0 < x <= 1 ==> x == 1",12);
}
- /*@ assert ∀ ℤ x; 0 < x ∧ x < 1 ⇒ \false; */
+ /*@ assert ∀ ℤ x; 0 < x < 1 ⇒ \false; */
{
int __e_acsl_forall_3;
int __e_acsl_x_3;
@@ -105,10 +103,9 @@ int main(void)
}
e_acsl_end_loop3: ;
e_acsl_assert(__e_acsl_forall_3,(char *)"Assertion",(char *)"main",
- (char *)"\\forall integer x; 0 < x && x < 1 ==> \\false",
- 13);
+ (char *)"\\forall integer x; 0 < x < 1 ==> \\false",13);
}
- /*@ assert ∀ ℤ x; 0 ≤ x ∧ x < 1 ⇒ x ≡ 0; */
+ /*@ assert ∀ ℤ x; 0 ≤ x < 1 ⇒ x ≡ 0; */
{
int __e_acsl_forall_4;
int __e_acsl_x_4;
@@ -125,13 +122,11 @@ int main(void)
}
e_acsl_end_loop4: ;
e_acsl_assert(__e_acsl_forall_4,(char *)"Assertion",(char *)"main",
- (char *)"\\forall integer x; 0 <= x && x < 1 ==> x == 0",
- 14);
+ (char *)"\\forall integer x; 0 <= x < 1 ==> x == 0",14);
}
/*@ assert
∀ ℤ x, ℤ y, ℤ z;
- ((0 ≤ x ∧ x < 2) ∧ (0 ≤ y ∧ y < 5)) ∧
- (0 ≤ z ∧ z ≤ y) ⇒ x+z ≤ y+1;
+ 0 ≤ x < 2 ∧ 0 ≤ y < 5 ∧ 0 ≤ z ≤ y ⇒ x+z ≤ y+1;
*/
{
int __e_acsl_forall_5;
@@ -161,10 +156,10 @@ int main(void)
}
e_acsl_end_loop5: ;
e_acsl_assert(__e_acsl_forall_5,(char *)"Assertion",(char *)"main",
- (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",
+ (char *)"\\forall integer x, integer y, integer z;\n 0 <= x < 2 && 0 <= y < 5 && 0 <= z <= y ==> x+z <= y+1",
18);
}
- /*@ assert ∃ int x; (0 ≤ x ∧ x < 10) ∧ x ≡ 5; */
+ /*@ assert ∃ int x; 0 ≤ x < 10 ∧ x ≡ 5; */
{
int __e_acsl_exists;
int __e_acsl_x_6;
@@ -181,12 +176,12 @@ int main(void)
}
e_acsl_end_loop6: ;
e_acsl_assert(__e_acsl_exists,(char *)"Assertion",(char *)"main",
- (char *)"\\exists int x; (0 <= x && x < 10) && x == 5",23);
+ (char *)"\\exists int x; 0 <= x < 10 && x == 5",23);
}
/*@ assert
∀ int x;
- 0 ≤ x ∧ x < 10 ⇒
- (x%2 ≡ 0 ⇒ (∃ ℤ y; (0 ≤ y ∧ y ≤ x/2) ∧ x ≡ 2*y));
+ 0 ≤ x < 10 ⇒
+ x%2 ≡ 0 ⇒ (∃ ℤ y; 0 ≤ y ≤ x/2 ∧ x ≡ 2*y);
*/
{
int __e_acsl_forall_6;
@@ -225,7 +220,7 @@ int main(void)
}
e_acsl_end_loop8: ;
e_acsl_assert(__e_acsl_forall_6,(char *)"Assertion",(char *)"main",
- (char *)"\\forall int x;\n 0 <= x && x < 10 ==>\n (x%2 == 0 ==> (\\exists integer y; (0 <= y && y <= x/2) && x == 2*y))",
+ (char *)"\\forall int x;\n 0 <= x < 10 ==> x%2 == 0 ==> (\\exists integer y; 0 <= y <= x/2 && x == 2*y)",
27);
}
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
index 648bbf062743f3e7ed3fea7184dfabc659f0d68f..084e9a5ecdcf2b6b325634fa286cd031c44dd6e3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_quantif2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
@@ -122,7 +121,7 @@ predicate diffSize{L1, L2}(ℤ i) =
int main(void)
{
int __retres;
- /*@ assert ∀ ℤ x; 0 ≤ x ∧ x ≤ 1 ⇒ x ≡ 0 ∨ x ≡ 1; */
+ /*@ assert ∀ ℤ x; 0 ≤ x ≤ 1 ⇒ x ≡ 0 ∨ x ≡ 1; */
{
int __e_acsl_forall;
mpz_t __e_acsl_x;
@@ -182,11 +181,11 @@ int main(void)
}
e_acsl_end_loop1: ;
e_acsl_assert(__e_acsl_forall,(char *)"Assertion",(char *)"main",
- (char *)"\\forall integer x; 0 <= x && x <= 1 ==> x == 0 || x == 1",
+ (char *)"\\forall integer x; 0 <= x <= 1 ==> x == 0 || x == 1",
11);
__gmpz_clear(__e_acsl_x);
}
- /*@ assert ∀ ℤ x; 0 < x ∧ x ≤ 1 ⇒ x ≡ 1; */
+ /*@ assert ∀ ℤ x; 0 < x ≤ 1 ⇒ x ≡ 1; */
{
int __e_acsl_forall_2;
mpz_t __e_acsl_x_2;
@@ -243,11 +242,10 @@ int main(void)
}
e_acsl_end_loop2: ;
e_acsl_assert(__e_acsl_forall_2,(char *)"Assertion",(char *)"main",
- (char *)"\\forall integer x; 0 < x && x <= 1 ==> x == 1",
- 12);
+ (char *)"\\forall integer x; 0 < x <= 1 ==> x == 1",12);
__gmpz_clear(__e_acsl_x_2);
}
- /*@ assert ∀ ℤ x; 0 < x ∧ x < 1 ⇒ \false; */
+ /*@ assert ∀ ℤ x; 0 < x < 1 ⇒ \false; */
{
int __e_acsl_forall_3;
mpz_t __e_acsl_x_3;
@@ -296,11 +294,10 @@ int main(void)
}
e_acsl_end_loop3: ;
e_acsl_assert(__e_acsl_forall_3,(char *)"Assertion",(char *)"main",
- (char *)"\\forall integer x; 0 < x && x < 1 ==> \\false",
- 13);
+ (char *)"\\forall integer x; 0 < x < 1 ==> \\false",13);
__gmpz_clear(__e_acsl_x_3);
}
- /*@ assert ∀ ℤ x; 0 ≤ x ∧ x < 1 ⇒ x ≡ 0; */
+ /*@ assert ∀ ℤ x; 0 ≤ x < 1 ⇒ x ≡ 0; */
{
int __e_acsl_forall_4;
mpz_t __e_acsl_x_4;
@@ -349,14 +346,12 @@ int main(void)
}
e_acsl_end_loop4: ;
e_acsl_assert(__e_acsl_forall_4,(char *)"Assertion",(char *)"main",
- (char *)"\\forall integer x; 0 <= x && x < 1 ==> x == 0",
- 14);
+ (char *)"\\forall integer x; 0 <= x < 1 ==> x == 0",14);
__gmpz_clear(__e_acsl_x_4);
}
/*@ assert
∀ ℤ x, ℤ y, ℤ z;
- ((0 ≤ x ∧ x < 2) ∧ (0 ≤ y ∧ y < 5)) ∧
- (0 ≤ z ∧ z ≤ y) ⇒ x+z ≤ y+1;
+ 0 ≤ x < 2 ∧ 0 ≤ y < 5 ∧ 0 ≤ z ≤ y ⇒ x+z ≤ y+1;
*/
{
int __e_acsl_forall_5;
@@ -473,13 +468,13 @@ int main(void)
}
e_acsl_end_loop5: ;
e_acsl_assert(__e_acsl_forall_5,(char *)"Assertion",(char *)"main",
- (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",
+ (char *)"\\forall integer x, integer y, integer z;\n 0 <= x < 2 && 0 <= y < 5 && 0 <= z <= y ==> x+z <= y+1",
18);
__gmpz_clear(__e_acsl_x_5);
__gmpz_clear(__e_acsl_y);
__gmpz_clear(__e_acsl_z);
}
- /*@ assert ∃ int x; (0 ≤ x ∧ x < 10) ∧ x ≡ 5; */
+ /*@ assert ∃ int x; 0 ≤ x < 10 ∧ x ≡ 5; */
{
int __e_acsl_exists;
mpz_t __e_acsl_x_6;
@@ -528,13 +523,13 @@ int main(void)
}
e_acsl_end_loop6: ;
e_acsl_assert(__e_acsl_exists,(char *)"Assertion",(char *)"main",
- (char *)"\\exists int x; (0 <= x && x < 10) && x == 5",23);
+ (char *)"\\exists int x; 0 <= x < 10 && x == 5",23);
__gmpz_clear(__e_acsl_x_6);
}
/*@ assert
∀ int x;
- 0 ≤ x ∧ x < 10 ⇒
- (x%2 ≡ 0 ⇒ (∃ ℤ y; (0 ≤ y ∧ y ≤ x/2) ∧ x ≡ 2*y));
+ 0 ≤ x < 10 ⇒
+ x%2 ≡ 0 ⇒ (∃ ℤ y; 0 ≤ y ≤ x/2 ∧ x ≡ 2*y);
*/
{
int __e_acsl_forall_6;
@@ -672,7 +667,7 @@ int main(void)
}
e_acsl_end_loop8: ;
e_acsl_assert(__e_acsl_forall_6,(char *)"Assertion",(char *)"main",
- (char *)"\\forall int x;\n 0 <= x && x < 10 ==>\n (x%2 == 0 ==> (\\exists integer y; (0 <= y && y <= x/2) && x == 2*y))",
+ (char *)"\\forall int x;\n 0 <= x < 10 ==> x%2 == 0 ==> (\\exists integer y; 0 <= y <= x/2 && x == 2*y)",
27);
__gmpz_clear(__e_acsl_x_7);
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
index fadefe1f3e4dd1b22887eb41dd864ead6f18f3bc..e8685f59e56c8e0baa0aae5782830e89ade8651b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c
index f1a5938054474a0a2f8864f191fed31f1f14c06c..20be0ff6fb6ae6f6096041f39144bd8d7977e8ca 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_result2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
index 863e5ba0a29c55b08fbb8ffefa3a5a95f70f9d04..2e3479a99328e165ca68b55dc4b103f6248e98f7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c
index 116f237427ca61ee7e4995da5a47d60a51ce2c3c..344882461a926bd2f3c0a85dbf445e6995495567 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_sizeof2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
index 6db54aa859e440e04b04ac9a53e236aa6b15b96d..59e0838f370fbdd9e595e6000ee9b9eeb9be9253 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c
index a853808cb266edb6b1780a0527869d9db77cde59..fb771c6f28be6584bcc5ca59b3a6023232302448 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stmt_contract2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
index 8e1101b3c274577c907db2076ca18e7e38f7b5a9..5a38c0f03be523bd3a5bbf073ae1838114e91a02 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c
index 8e1101b3c274577c907db2076ca18e7e38f7b5a9..5a38c0f03be523bd3a5bbf073ae1838114e91a02 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_true2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c
index eecf507b2d7032218855b88f1b129b41d47ab47d..40f1c88d544b199f9dca56d107d49a6639d60c04 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef.c
@@ -24,8 +24,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c
index e245eae9e7c82a6e4de74f4d7c8f2ff62951ad0b..c9264147a19dd461f724575702f5806d0b900e6b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_typedef2.c
@@ -24,8 +24,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
index d6f5642b29065594aba77fcb0f93eb2cdb6cd9fd..ba6769188c7dc703bff2b67d6d6b3779228a3862 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
@@ -318,7 +317,7 @@ int main(void)
__store_block((void *)(& a),8UL);
__full_init((void *)(& n));
n = 0;
- /*@ assert (¬\valid(a) ∧ ¬\valid(b)) ∧ ¬\valid(X); */
+ /*@ assert ¬\valid(a) ∧ ¬\valid(b) ∧ ¬\valid(X); */
{
int __e_acsl_initialized;
int __e_acsl_and;
@@ -351,11 +350,11 @@ int main(void)
}
else __e_acsl_and_4 = 0;
e_acsl_assert(__e_acsl_and_4,(char *)"Assertion",(char *)"main",
- (char *)"(!\\valid(a) && !\\valid(b)) && !\\valid(X)",35);
+ (char *)"!\\valid(a) && !\\valid(b) && !\\valid(X)",35);
}
__full_init((void *)(& a));
a = (int *)__e_acsl_malloc(sizeof(int));
- /*@ assert (\valid(a) ∧ ¬\valid(b)) ∧ ¬\valid(X); */
+ /*@ assert \valid(a) ∧ ¬\valid(b) ∧ ¬\valid(X); */
{
int __e_acsl_initialized_3;
int __e_acsl_and_5;
@@ -388,10 +387,10 @@ int main(void)
}
else __e_acsl_and_8 = 0;
e_acsl_assert(__e_acsl_and_8,(char *)"Assertion",(char *)"main",
- (char *)"(\\valid(a) && !\\valid(b)) && !\\valid(X)",37);
+ (char *)"\\valid(a) && !\\valid(b) && !\\valid(X)",37);
}
X = a;
- /*@ assert (\valid(a) ∧ ¬\valid(b)) ∧ \valid(X); */
+ /*@ assert \valid(a) ∧ ¬\valid(b) ∧ \valid(X); */
{
int __e_acsl_initialized_5;
int __e_acsl_and_9;
@@ -424,11 +423,11 @@ int main(void)
}
else __e_acsl_and_12 = 0;
e_acsl_assert(__e_acsl_and_12,(char *)"Assertion",(char *)"main",
- (char *)"(\\valid(a) && !\\valid(b)) && \\valid(X)",39);
+ (char *)"\\valid(a) && !\\valid(b) && \\valid(X)",39);
}
__full_init((void *)(& b));
b = __e_acsl_f(& n);
- /*@ assert (\valid(a) ‚àß \valid(b)) ‚àß \valid(X); */
+ /*@ assert \valid(a) ‚àß \valid(b) ‚àß \valid(X); */
{
int __e_acsl_initialized_7;
int __e_acsl_and_13;
@@ -461,10 +460,10 @@ int main(void)
}
else __e_acsl_and_16 = 0;
e_acsl_assert(__e_acsl_and_16,(char *)"Assertion",(char *)"main",
- (char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",41);
+ (char *)"\\valid(a) && \\valid(b) && \\valid(X)",41);
}
X = b;
- /*@ assert (\valid(a) ‚àß \valid(b)) ‚àß \valid(X); */
+ /*@ assert \valid(a) ‚àß \valid(b) ‚àß \valid(X); */
{
int __e_acsl_initialized_9;
int __e_acsl_and_17;
@@ -497,7 +496,7 @@ int main(void)
}
else __e_acsl_and_20 = 0;
e_acsl_assert(__e_acsl_and_20,(char *)"Assertion",(char *)"main",
- (char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",43);
+ (char *)"\\valid(a) && \\valid(b) && \\valid(X)",43);
}
__full_init((void *)(& c));
c = & a;
@@ -581,7 +580,7 @@ int main(void)
(char *)"\\valid(*(*d))",47);
}
__e_acsl_free((void *)a);
- /*@ assert (¬\valid(a) ∧ \valid(b)) ∧ \valid(X); */
+ /*@ assert ¬\valid(a) ∧ \valid(b) ∧ \valid(X); */
{
int __e_acsl_initialized_17;
int __e_acsl_and_27;
@@ -614,7 +613,7 @@ int main(void)
}
else __e_acsl_and_30 = 0;
e_acsl_assert(__e_acsl_and_30,(char *)"Assertion",(char *)"main",
- (char *)"(!\\valid(a) && \\valid(b)) && \\valid(X)",49);
+ (char *)"!\\valid(a) && \\valid(b) && \\valid(X)",49);
}
/*@ assert \valid(&Z); */
{
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
index d6f5642b29065594aba77fcb0f93eb2cdb6cd9fd..ba6769188c7dc703bff2b67d6d6b3779228a3862 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
@@ -318,7 +317,7 @@ int main(void)
__store_block((void *)(& a),8UL);
__full_init((void *)(& n));
n = 0;
- /*@ assert (¬\valid(a) ∧ ¬\valid(b)) ∧ ¬\valid(X); */
+ /*@ assert ¬\valid(a) ∧ ¬\valid(b) ∧ ¬\valid(X); */
{
int __e_acsl_initialized;
int __e_acsl_and;
@@ -351,11 +350,11 @@ int main(void)
}
else __e_acsl_and_4 = 0;
e_acsl_assert(__e_acsl_and_4,(char *)"Assertion",(char *)"main",
- (char *)"(!\\valid(a) && !\\valid(b)) && !\\valid(X)",35);
+ (char *)"!\\valid(a) && !\\valid(b) && !\\valid(X)",35);
}
__full_init((void *)(& a));
a = (int *)__e_acsl_malloc(sizeof(int));
- /*@ assert (\valid(a) ∧ ¬\valid(b)) ∧ ¬\valid(X); */
+ /*@ assert \valid(a) ∧ ¬\valid(b) ∧ ¬\valid(X); */
{
int __e_acsl_initialized_3;
int __e_acsl_and_5;
@@ -388,10 +387,10 @@ int main(void)
}
else __e_acsl_and_8 = 0;
e_acsl_assert(__e_acsl_and_8,(char *)"Assertion",(char *)"main",
- (char *)"(\\valid(a) && !\\valid(b)) && !\\valid(X)",37);
+ (char *)"\\valid(a) && !\\valid(b) && !\\valid(X)",37);
}
X = a;
- /*@ assert (\valid(a) ∧ ¬\valid(b)) ∧ \valid(X); */
+ /*@ assert \valid(a) ∧ ¬\valid(b) ∧ \valid(X); */
{
int __e_acsl_initialized_5;
int __e_acsl_and_9;
@@ -424,11 +423,11 @@ int main(void)
}
else __e_acsl_and_12 = 0;
e_acsl_assert(__e_acsl_and_12,(char *)"Assertion",(char *)"main",
- (char *)"(\\valid(a) && !\\valid(b)) && \\valid(X)",39);
+ (char *)"\\valid(a) && !\\valid(b) && \\valid(X)",39);
}
__full_init((void *)(& b));
b = __e_acsl_f(& n);
- /*@ assert (\valid(a) ‚àß \valid(b)) ‚àß \valid(X); */
+ /*@ assert \valid(a) ‚àß \valid(b) ‚àß \valid(X); */
{
int __e_acsl_initialized_7;
int __e_acsl_and_13;
@@ -461,10 +460,10 @@ int main(void)
}
else __e_acsl_and_16 = 0;
e_acsl_assert(__e_acsl_and_16,(char *)"Assertion",(char *)"main",
- (char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",41);
+ (char *)"\\valid(a) && \\valid(b) && \\valid(X)",41);
}
X = b;
- /*@ assert (\valid(a) ‚àß \valid(b)) ‚àß \valid(X); */
+ /*@ assert \valid(a) ‚àß \valid(b) ‚àß \valid(X); */
{
int __e_acsl_initialized_9;
int __e_acsl_and_17;
@@ -497,7 +496,7 @@ int main(void)
}
else __e_acsl_and_20 = 0;
e_acsl_assert(__e_acsl_and_20,(char *)"Assertion",(char *)"main",
- (char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",43);
+ (char *)"\\valid(a) && \\valid(b) && \\valid(X)",43);
}
__full_init((void *)(& c));
c = & a;
@@ -581,7 +580,7 @@ int main(void)
(char *)"\\valid(*(*d))",47);
}
__e_acsl_free((void *)a);
- /*@ assert (¬\valid(a) ∧ \valid(b)) ∧ \valid(X); */
+ /*@ assert ¬\valid(a) ∧ \valid(b) ∧ \valid(X); */
{
int __e_acsl_initialized_17;
int __e_acsl_and_27;
@@ -614,7 +613,7 @@ int main(void)
}
else __e_acsl_and_30 = 0;
e_acsl_assert(__e_acsl_and_30,(char *)"Assertion",(char *)"main",
- (char *)"(!\\valid(a) && \\valid(b)) && \\valid(X)",49);
+ (char *)"!\\valid(a) && \\valid(b) && \\valid(X)",49);
}
/*@ assert \valid(&Z); */
{
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
index 6ac30ce1b033b4095f82841be1a55714702d13c9..b0646a1db2bf4995a6238c4e27acfc984b29bd51 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
index 1923735970b546cb5336f86a50e692f79e73437a..1b01805b47aff8dd1956f73589589b21bb8511db 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
index 4cebebc641f25d981295e83f1bee48f31ec27b82..17fc089ed6f51ebc2db689b5d226bfdb9799b359 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
@@ -27,8 +27,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
index 4cebebc641f25d981295e83f1bee48f31ec27b82..17fc089ed6f51ebc2db689b5d226bfdb9799b359 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
@@ -27,8 +27,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
index 6a4bba4d5230101329af954584c32a06347ae2dd..5aaf6de4691a292c80f717f4d3a89db636d6e2f0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
index a69e887eaab1594e00a236e95f1607aa6bdfe2b7..6a6d0a7043f6f18a6f70e2631145fcb2e66eadc7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
@@ -23,8 +23,7 @@ unsigned long const __fc_rand_max = (unsigned long)32767;
/*@ ghost extern int __fc_heap_status; */
/*@
-axiomatic
- dynamic_allocation {
+axiomatic dynamic_allocation {
predicate is_allocable{L}(size_t n)
reads __fc_heap_status;