From 3384b7f8ff6fb67181ea351d32e2a9df6cb04670 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 30 Jun 2014 10:15:30 +0200
Subject: [PATCH] [tests] updated according to pretty printer changes [quantif]
updated according to AST changes: && is now left-associative
---
src/plugins/e-acsl/TODO | 2 +-
src/plugins/e-acsl/quantif.ml | 82 +++++++++++--------
.../e-acsl-reject/oracle/quantif.res.oracle | 21 ++---
.../e-acsl-runtime/oracle/empty.1.res.oracle | 3 +-
.../e-acsl-runtime/oracle/empty.res.oracle | 3 +-
.../tests/e-acsl-runtime/oracle/gen_addrOf.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_addrOf2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_alias.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_alias2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_arith.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_arith2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_array.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_array2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_at.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_at2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_bts1304.c | 3 +-
.../e-acsl-runtime/oracle/gen_bts13042.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_bts1307.c | 11 +--
.../e-acsl-runtime/oracle/gen_bts13072.c | 11 +--
.../tests/e-acsl-runtime/oracle/gen_bts1324.c | 9 +-
.../e-acsl-runtime/oracle/gen_bts13242.c | 9 +-
.../tests/e-acsl-runtime/oracle/gen_bts1326.c | 3 +-
.../e-acsl-runtime/oracle/gen_bts13262.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_bts1390.c | 19 ++---
.../e-acsl-runtime/oracle/gen_bts13902.c | 19 ++---
.../tests/e-acsl-runtime/oracle/gen_bts1398.c | 3 +-
.../e-acsl-runtime/oracle/gen_bts13982.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_bts1399.c | 3 +-
.../e-acsl-runtime/oracle/gen_bts13992.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_bts1478.c | 3 +-
.../e-acsl-runtime/oracle/gen_bts14782.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_bts1700.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_bts1717.c | 3 +-
.../e-acsl-runtime/oracle/gen_bts17172.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_call.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_call2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_cast.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_cast2.c | 3 +-
.../e-acsl-runtime/oracle/gen_comparison.c | 3 +-
.../e-acsl-runtime/oracle/gen_comparison2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_false.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_false2.c | 3 +-
.../oracle/gen_function_contract.c | 3 +-
.../oracle/gen_function_contract2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_ghost.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_ghost2.c | 3 +-
.../oracle/gen_integer_constant.c | 3 +-
.../oracle/gen_integer_constant2.c | 3 +-
.../e-acsl-runtime/oracle/gen_invariant.c | 7 +-
.../e-acsl-runtime/oracle/gen_invariant2.c | 7 +-
.../e-acsl-runtime/oracle/gen_labeled_stmt.c | 3 +-
.../e-acsl-runtime/oracle/gen_labeled_stmt2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_lazy.c | 7 +-
.../tests/e-acsl-runtime/oracle/gen_lazy2.c | 7 +-
.../e-acsl-runtime/oracle/gen_linear_search.c | 34 ++++----
.../oracle/gen_linear_search2.c | 34 ++++----
.../oracle/gen_literal_string.c | 3 +-
.../oracle/gen_literal_string2.c | 3 +-
.../e-acsl-runtime/oracle/gen_localvar.c | 3 +-
.../e-acsl-runtime/oracle/gen_localvar2.c | 3 +-
.../e-acsl-runtime/oracle/gen_longlong.c | 3 +-
.../e-acsl-runtime/oracle/gen_longlong2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_loop.c | 37 ++++-----
.../tests/e-acsl-runtime/oracle/gen_loop2.c | 37 ++++-----
.../oracle/gen_nested_code_annot.c | 3 +-
.../oracle/gen_nested_code_annot2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_not.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_not2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_null.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_null2.c | 3 +-
.../oracle/gen_other_constants.c | 3 +-
.../oracle/gen_other_constants2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_ptr.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_ptr2.c | 3 +-
.../e-acsl-runtime/oracle/gen_ptr_init.c | 3 +-
.../e-acsl-runtime/oracle/gen_ptr_init2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_quantif.c | 37 ++++-----
.../e-acsl-runtime/oracle/gen_quantif2.c | 37 ++++-----
.../tests/e-acsl-runtime/oracle/gen_result.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_result2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_sizeof.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_sizeof2.c | 3 +-
.../e-acsl-runtime/oracle/gen_stmt_contract.c | 3 +-
.../oracle/gen_stmt_contract2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_true.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_true2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_typedef.c | 3 +-
.../e-acsl-runtime/oracle/gen_typedef2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_valid.c | 27 +++---
.../tests/e-acsl-runtime/oracle/gen_valid2.c | 27 +++---
.../e-acsl-runtime/oracle/gen_valid_alias.c | 3 +-
.../e-acsl-runtime/oracle/gen_valid_alias2.c | 3 +-
.../oracle/gen_valid_in_contract.c | 3 +-
.../oracle/gen_valid_in_contract2.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_vector.c | 3 +-
.../tests/e-acsl-runtime/oracle/gen_vector2.c | 3 +-
96 files changed, 302 insertions(+), 404 deletions(-)
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index efbbd3c6aa1..b7e35cba3ac 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 48c6bfbb927..f9d7de51991 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 a6abd09b5f7..2975935077a 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 38ce731e0a0..3a30bf8aec2 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 38ce731e0a0..3a30bf8aec2 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 78d13f82b67..4380850af5c 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 78d13f82b67..4380850af5c 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 21d3dee0e0f..7c2a416c22f 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 21d3dee0e0f..7c2a416c22f 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 8247aa4992b..334e3c34ca9 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 f51c537f6c4..0eab9e5cd7f 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 c765bd1a860..093d1bddd86 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 f20a0e8f72b..94d787b234f 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 a325b760622..b2c0219b9e9 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 679a07f8431..daf8cec2413 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 efdb482b820..5c12cd15466 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 efdb482b820..5c12cd15466 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 31a9781a100..3a29edcd35d 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 444d463a0d2..7d763463d92 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 560261c0f55..978fcbf9644 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 a448bc0be51..bd3df265eb6 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 eb2080fc217..f6f87a2a151 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 72b0e104ce9..5e228b6ea96 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 2b98891e4a7..4d7d96f698a 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 a08c2a6692f..d285db47dbf 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 9548021ec84..ca81671e63b 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 9548021ec84..ca81671e63b 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 45a8c5865d8..f430e7f1141 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 d265181dd9d..3e4d00c3342 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 d9defb9f390..7bd2cea581d 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 dfe69e1c88d..4f7107fb96b 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 7258ddac41b..3a5217d031e 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 87cc310d9af..605e2c6463d 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 87cc310d9af..605e2c6463d 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 4287e8ff271..44d387a450d 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 4287e8ff271..44d387a450d 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 aa39b2d317a..4243d6ff710 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 98f8ec27baf..641f5e89354 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 ceb5d2b3fa7..10c2fd56df5 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 149fb7ae8e9..830ac36df98 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 0acbead3158..c84595e51e1 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 0acbead3158..c84595e51e1 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 4ff593abac4..e8b69159b6c 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 4fd16fafea5..0681fe26264 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 c8f1be53be9..b76b7ae9440 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 edc38d0e77d..eec3ef056a3 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 8ce91c0dbef..0ca24f6d3e0 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 44899d75a9d..c094b663632 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 9766e975635..23a89728971 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 06994dd7f2e..37ae7523f9d 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 3f7d2a0d79c..cc45f905cef 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 7816d4df0c4..121dcba8ef7 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 daf1108de6c..2d46309daf3 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 34ae8c2cefe..b200394ad1c 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 12112426a52..2bfad72eea6 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 f844748eb6c..fa7fbbfa6f6 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 3223de6d50b..9be1b7fd177 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 f1c4480d60e..b2ddbe5b10c 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 49b0543c428..7bd6be96706 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 49b0543c428..7bd6be96706 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 08df9312e66..1426ccd2a3d 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 c83d640e113..f6f10141afa 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 c8d331edc7c..07e28bd8bd5 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 82cb91e3600..24252ed397a 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 ef2552990a1..68b8e12c1e7 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 4b079ab0cc1..bddeaecca43 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 1c0d0332fa6..382082219bd 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 a6009c1c2c4..4c32310f080 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 32f5d86c996..8093abd3d08 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 32f5d86c996..8093abd3d08 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 afa63f7ba33..d23e55160ea 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 e25ff06fa59..55b963b578c 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 f854d7b49be..33b428eb684 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 59051aa42d6..91f9702d49d 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 c545933f565..0e7d2a314f8 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 c545933f565..0e7d2a314f8 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 68298283100..e82c4fb12a2 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 648bbf06274..084e9a5ecdc 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 fadefe1f3e4..e8685f59e56 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 f1a59380544..20be0ff6fb6 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 863e5ba0a29..2e3479a9932 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 116f237427c..344882461a9 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 6db54aa859e..59e0838f370 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 a853808cb26..fb771c6f28b 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 8e1101b3c27..5a38c0f03be 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 8e1101b3c27..5a38c0f03be 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 eecf507b2d7..40f1c88d544 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 e245eae9e7c..c9264147a19 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 d6f5642b290..ba6769188c7 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 d6f5642b290..ba6769188c7 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 6ac30ce1b03..b0646a1db2b 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 1923735970b..1b01805b47a 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 4cebebc641f..17fc089ed6f 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 4cebebc641f..17fc089ed6f 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 6a4bba4d523..5aaf6de4691 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 a69e887eaab..6a6d0a7043f 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;
--
GitLab