From bba18f6e5d170ccecb476829f6b597b22b18ac4b Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 7 Dec 2012 09:07:49 +0000
Subject: [PATCH] [E-ACSL] update according to kernel's printer changes
---
.../e-acsl-reject/oracle/quantif.res.oracle | 23 ++--
.../e-acsl-runtime/oracle/empty.1.res.oracle | 6 +-
.../e-acsl-runtime/oracle/empty.res.oracle | 6 +-
.../tests/e-acsl-runtime/oracle/gen_addrOf.c | 6 +-
.../tests/e-acsl-runtime/oracle/gen_addrOf2.c | 6 +-
.../tests/e-acsl-runtime/oracle/gen_arith.c | 6 +-
.../tests/e-acsl-runtime/oracle/gen_arith2.c | 51 ++++-----
.../tests/e-acsl-runtime/oracle/gen_array.c | 6 +-
.../tests/e-acsl-runtime/oracle/gen_array2.c | 17 ++-
.../tests/e-acsl-runtime/oracle/gen_at.c | 16 +--
.../tests/e-acsl-runtime/oracle/gen_at2.c | 42 +++-----
.../tests/e-acsl-runtime/oracle/gen_bts1304.c | 21 ++--
.../e-acsl-runtime/oracle/gen_bts13042.c | 21 ++--
.../tests/e-acsl-runtime/oracle/gen_bts1307.c | 48 ++++-----
.../e-acsl-runtime/oracle/gen_bts13072.c | 76 ++++++-------
.../tests/e-acsl-runtime/oracle/gen_bts1324.c | 26 +++--
.../e-acsl-runtime/oracle/gen_bts13242.c | 46 ++++----
.../tests/e-acsl-runtime/oracle/gen_cast.c | 6 +-
.../tests/e-acsl-runtime/oracle/gen_cast2.c | 33 +++---
.../e-acsl-runtime/oracle/gen_comparison.c | 12 +--
.../e-acsl-runtime/oracle/gen_comparison2.c | 32 +++---
.../tests/e-acsl-runtime/oracle/gen_false.c | 6 +-
.../tests/e-acsl-runtime/oracle/gen_false2.c | 6 +-
.../oracle/gen_function_contract.c | 75 ++++++-------
.../oracle/gen_function_contract2.c | 77 ++++++-------
.../oracle/gen_integer_constant.c | 17 ++-
.../oracle/gen_integer_constant2.c | 24 ++---
.../e-acsl-runtime/oracle/gen_invariant.c | 14 +--
.../e-acsl-runtime/oracle/gen_invariant2.c | 19 ++--
.../e-acsl-runtime/oracle/gen_labeled_stmt.c | 8 +-
.../e-acsl-runtime/oracle/gen_labeled_stmt2.c | 19 ++--
.../tests/e-acsl-runtime/oracle/gen_lazy.c | 101 +++++++++---------
.../tests/e-acsl-runtime/oracle/gen_lazy2.c | 52 ++++-----
.../e-acsl-runtime/oracle/gen_linear_search.c | 28 +++--
.../oracle/gen_linear_search2.c | 50 ++++-----
.../oracle/gen_literal_string.c | 25 +++--
.../oracle/gen_literal_string2.c | 36 +++----
.../e-acsl-runtime/oracle/gen_localvar.c | 38 +++----
.../e-acsl-runtime/oracle/gen_localvar2.c | 38 +++----
.../oracle/gen_nested_code_annot.c | 6 +-
.../oracle/gen_nested_code_annot2.c | 17 ++-
.../tests/e-acsl-runtime/oracle/gen_not.c | 6 +-
.../tests/e-acsl-runtime/oracle/gen_not2.c | 17 ++-
.../tests/e-acsl-runtime/oracle/gen_null.c | 6 +-
.../tests/e-acsl-runtime/oracle/gen_null2.c | 6 +-
.../oracle/gen_other_constants.c | 6 +-
.../oracle/gen_other_constants2.c | 17 ++-
.../tests/e-acsl-runtime/oracle/gen_ptr.c | 23 ++--
.../tests/e-acsl-runtime/oracle/gen_ptr2.c | 45 ++++----
.../tests/e-acsl-runtime/oracle/gen_quantif.c | 66 ++++++------
.../e-acsl-runtime/oracle/gen_quantif2.c | 86 +++++++--------
.../tests/e-acsl-runtime/oracle/gen_result.c | 12 +--
.../tests/e-acsl-runtime/oracle/gen_result2.c | 34 +++---
.../tests/e-acsl-runtime/oracle/gen_sizeof.c | 6 +-
.../tests/e-acsl-runtime/oracle/gen_sizeof2.c | 17 ++-
.../e-acsl-runtime/oracle/gen_stmt_contract.c | 24 ++---
.../oracle/gen_stmt_contract2.c | 38 +++----
.../tests/e-acsl-runtime/oracle/gen_true.c | 6 +-
.../tests/e-acsl-runtime/oracle/gen_true2.c | 6 +-
.../tests/e-acsl-runtime/oracle/gen_typedef.c | 6 +-
.../e-acsl-runtime/oracle/gen_typedef2.c | 24 ++---
.../tests/e-acsl-runtime/oracle/gen_valid.c | 67 ++++++------
.../tests/e-acsl-runtime/oracle/gen_valid2.c | 67 ++++++------
.../e-acsl-runtime/oracle/gen_valid_alias.c | 63 +++++------
.../e-acsl-runtime/oracle/gen_valid_alias2.c | 72 ++++++-------
.../oracle/gen_valid_in_contract.c | 34 +++---
.../oracle/gen_valid_in_contract2.c | 34 +++---
67 files changed, 878 insertions(+), 1072 deletions(-)
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 297f12265b3..ed7651c6406 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
@@ -16,28 +16,29 @@ 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'.
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'.
+ `unguarded variable y in quantification
+ ∀ ℤ x, ℤ y; 0 ≤ x ∧ 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 ∧ x ≤ 3) ∧ (0 ≤ z ∧ 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 ∧ x ≤ 3) ∨ (0 ≤ y ∧ y ≤ 3) in quantification
+ ∀ ℤ x, ℤ y; (0 ≤ x ∧ x ≤ 3) ∨ (0 ≤ y ∧ 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'.
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 ∧ x < 10) ∧ (9 ≤ x ∧ x < 20) ⇒ x > z'.
Ignoring annotation.
tests/e-acsl-reject/quantif.i:15:[e-acsl] warning: invalid E-ACSL construct
- `invalid binder y in quantification ∀ ℤ x, ℤ z, ℤ y;
- ((0 ≤ x ∧ x < 2) ∧ (0 ≤ y ∧ y < 5)) ∧ (0 ≤ z ∧ z ≤ y) ⇒
- x+z ≤ y+1'.
+ `invalid binder y in quantification
+ ∀ ℤ x, ℤ z, ℤ y;
+ ((0 ≤ x ∧ x < 2) ∧ (0 ≤ y ∧ y < 5)) ∧ (0 ≤ z ∧ z ≤ y) ⇒
+ x+z ≤ y+1'.
Ignoring annotation.
[e-acsl] 9 annotations were ignored, being untypable.
[e-acsl] 1 annotation was ignored, being unsupported.
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 e07a3c52ceb..4a148eb0e47 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
@@ -40,14 +40,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 e07a3c52ceb..4a148eb0e47 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
@@ -40,14 +40,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 a9d312c47d8..4fe9c71cee4 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 a9d312c47d8..4fe9c71cee4 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 a4b008e0703..e258cf1b07f 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 0696eceb271..1f18e3648db 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
@@ -24,51 +24,42 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
- allocates \old(z);
-
assigns *z;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from str, base;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z,
char const *str,
int base);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
assigns *z1;
assigns *z1 \from *z2;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_neg(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
@@ -76,8 +67,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_neg(__mpz_struct * /*[1]*/ z
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
@@ -86,8 +76,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_sub(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
@@ -96,8 +85,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_sub(__mpz_struct * /*[1]*/ z
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
@@ -106,8 +94,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
@@ -116,8 +103,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_r(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
@@ -125,8 +111,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_r(__mpz_struct * /*[1]*
requires \valid(z2);
assigns *z1;
assigns *z1 \from *z2;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_com(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
int __fc_random_counter __attribute__((__unused__));
@@ -141,14 +126,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 9dab2ef8e62..0aa165a1d9b 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 8d4f7c19246..03a2e7f920c 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
@@ -24,22 +24,19 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
int __fc_random_counter __attribute__((__unused__));
@@ -54,14 +51,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 553e15d8a5f..b33883fc248 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -52,19 +52,19 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int A = 0;
-/*@ ensures \at(A,Post) ≡ 3; */
+/*@ ensures \at(A,Post) ≡ 3; */
void f(void)
{
int __e_acsl_at_6;
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 0eb4912a2ac..525de6cdafc 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
@@ -24,41 +24,34 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
- allocates \old(z);
-
assigns *z;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
/*@ requires \valid(z_orig);
requires ¬\initialized(z);
ensures \valid(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from *z_orig;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set(__mpz_struct * /*[1]*/ z,
__mpz_struct const * /*[1]*/ z_orig);
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
@@ -66,8 +59,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
@@ -83,14 +75,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -101,19 +93,19 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int A = 0;
-/*@ ensures \at(A,Post) ≡ 3; */
+/*@ ensures \at(A,Post) ≡ 3; */
void f(void)
{
int __e_acsl_at_6;
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 a6910b32407..c55f81da07a 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
@@ -50,14 +50,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -68,22 +68,21 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒
- \initialized((char *)\old(ptr)+(0..\old(size)-1));
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
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 a6910b32407..c55f81da07a 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
@@ -50,14 +50,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -68,22 +68,21 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒
- \initialized((char *)\old(ptr)+(0..\old(size)-1));
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
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 15fb4cc4625..aae8c9dd45a 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -52,40 +52,38 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒
- \initialized((char *)\old(ptr)+(0..\old(size)-1));
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
/*@ requires \valid(Mtmax_in);
requires \valid(Mwmax);
requires \valid(Mtmax_out);
+
behavior OverEstimate_Motoring:
assumes \true;
- ensures *\old(Mtmax_out) ≡
- *\old(Mtmax_in)+(5-((5/80)**\old(Mwmax))*0.4);
-
-
-*/
+ ensures
+ *\old(Mtmax_out) ≡ *\old(Mtmax_in)+(5-((5/80)**\old(Mwmax))*0.4);
+ */
void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
{
float *__e_acsl_at_3;
@@ -177,13 +175,15 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
/*@ requires \valid(Mtmin_in);
requires \valid(Mwmin);
requires \valid(Mtmin_out);
+
behavior UnderEstimate_Motoring:
assumes \true;
- ensures *\old(Mtmin_out)≡*\old(Mtmin_in)∧*\old(Mtmin_in)<0.85**
- \old(Mwmin)? *\old(Mtmin_in) ≢ 0.: 0.85**\old(Mwmin) ≢ 0.;
-
-
-*/
+ ensures
+ *\old(Mtmin_out)≡*\old(Mtmin_in)∧*\old(Mtmin_in)<0.85**\old(
+ Mwmin)?
+ *\old(Mtmin_in) ≢ 0.:
+ 0.85**\old(Mwmin) ≢ 0.;
+ */
void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
{
float *__e_acsl_at_6;
@@ -243,7 +243,7 @@ void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
if (__e_acsl_and) { __e_acsl_if = *__e_acsl_at_5 != 0.; }
else { __e_acsl_if = 0.85 * *__e_acsl_at_6 != 0.; }
e_acsl_assert(__e_acsl_if,(char *)"Postcondition",
- (char *)"*\\old(Mtmin_out)==*\\old(Mtmin_in)&&*\\old(Mtmin_in)<0.85**\\old(Mwmin)?\n *\\old(Mtmin_in) != 0.: 0.85**\\old(Mwmin) != 0.",
+ (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.",
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 a9bcd84bb2d..d16978e28bf 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
@@ -24,41 +24,34 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
- allocates \old(z);
-
assigns *z;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
/*@ requires \valid(z_orig);
requires ¬\initialized(z);
ensures \valid(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from *z_orig;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set(__mpz_struct * /*[1]*/ z,
__mpz_struct const * /*[1]*/ z_orig);
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
@@ -66,13 +59,12 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)2147483647;
@@ -86,14 +78,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -104,40 +96,38 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒
- \initialized((char *)\old(ptr)+(0..\old(size)-1));
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
/*@ requires \valid(Mtmax_in);
requires \valid(Mwmax);
requires \valid(Mtmax_out);
+
behavior OverEstimate_Motoring:
assumes \true;
- ensures *\old(Mtmax_out) ≡
- *\old(Mtmax_in)+(5-((5/80)**\old(Mwmax))*0.4);
-
-
-*/
+ ensures
+ *\old(Mtmax_out) ≡ *\old(Mtmax_in)+(5-((5/80)**\old(Mwmax))*0.4);
+ */
void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
{
float *__e_acsl_at_3;
@@ -251,13 +241,15 @@ void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
/*@ requires \valid(Mtmin_in);
requires \valid(Mwmin);
requires \valid(Mtmin_out);
+
behavior UnderEstimate_Motoring:
assumes \true;
- ensures *\old(Mtmin_out)≡*\old(Mtmin_in)∧*\old(Mtmin_in)<0.85**
- \old(Mwmin)? *\old(Mtmin_in) ≢ 0.: 0.85**\old(Mwmin) ≢ 0.;
-
-
-*/
+ ensures
+ *\old(Mtmin_out)≡*\old(Mtmin_in)∧*\old(Mtmin_in)<0.85**\old(
+ Mwmin)?
+ *\old(Mtmin_in) ≢ 0.:
+ 0.85**\old(Mwmin) ≢ 0.;
+ */
void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
{
float *__e_acsl_at_6;
@@ -323,7 +315,7 @@ void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
if (__e_acsl_2) { __e_acsl_if = *__e_acsl_at_5 != 0.; }
else { __e_acsl_if = 0.85 * *__e_acsl_at_6 != 0.; }
e_acsl_assert(__e_acsl_if,(char *)"Postcondition",
- (char *)"*\\old(Mtmin_out)==*\\old(Mtmin_in)&&*\\old(Mtmin_in)<0.85**\\old(Mwmin)?\n *\\old(Mtmin_in) != 0.: 0.85**\\old(Mwmin) != 0.",
+ (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.",
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 9eb0a8dd321..0c8681e9eda 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -52,26 +52,24 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
/*@ behavior yes:
assumes ∀ long long i; 0 < i ∧ i < n ⇒ *(t+(i-1)) ≤ *(t+i);
ensures \result ≡ 1;
-
-
-*/
+ */
int sorted(int *t, int n)
{
int __e_acsl_at;
@@ -85,8 +83,7 @@ int sorted(int *t, int n)
__e_acsl_forall = 1;
__e_acsl_i = (long long)(0 + 1);
while (1) {
- if (__e_acsl_i < n) { ; }
- else { break; }
+ if (__e_acsl_i < n) { ; } else { break; }
{
int __e_acsl_valid_read;
int __e_acsl_valid_read_2;
@@ -124,7 +121,8 @@ int sorted(int *t, int n)
}
__retres = 1;
return_label: /* internal */
- { int __e_acsl_implies;
+ {
+ int __e_acsl_implies;
if (! __e_acsl_at) { __e_acsl_implies = 1; }
else { __e_acsl_implies = __retres == 1; }
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
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 1c9055649ca..c6aafbec4bc 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
@@ -24,38 +24,32 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
- allocates \old(z);
-
assigns *z;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(z_orig);
requires \valid(z);
assigns *z;
assigns *z \from *z_orig;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_set(__mpz_struct * /*[1]*/ z,
__mpz_struct const * /*[1]*/ z_orig);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
@@ -63,8 +57,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
@@ -73,13 +66,12 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_sub(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)2147483647;
@@ -93,14 +85,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -111,23 +103,21 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
/*@ behavior yes:
assumes ∀ ℤ i; 0 < i ∧ i < n ⇒ *(t+(i-1)) ≤ *(t+i);
ensures \result ≡ 1;
-
-
-*/
+ */
int sorted(int *t, int n)
{
int __e_acsl_at;
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 76482d48662..516aa6bb8a3 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 0aa885a4827..fa4a18bac43 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
@@ -24,51 +24,42 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_ui(__mpz_struct * /*[1]*/ z,
unsigned long n);
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from str, base;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z,
char const *str,
int base);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)2147483647;
@@ -82,14 +73,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 998753278e7..37b420d66f8 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -52,12 +52,12 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int main(void)
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 1fea02cc9ed..909225b9ca8 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
@@ -24,38 +24,32 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
- allocates \old(z);
-
assigns *z;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
assigns *z1;
assigns *z1 \from *z2;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_neg(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
int __fc_random_counter __attribute__((__unused__));
@@ -70,14 +64,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -88,12 +82,12 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int main(void)
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 a1bb7293ca2..269d857ccad 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 a1bb7293ca2..269d857ccad 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 cf1ecaa48f4..cd9b58ab0ff 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -55,7 +55,7 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int X = 0;
int Y = 2;
-/*@ ensures X ≡ 1; */
+/*@ ensures X ≡ 1; */
void f(void)
{
X = 1;
@@ -64,7 +64,7 @@ void f(void)
}
/*@ ensures X ≡ 2;
- ensures Y ≡ 2; */
+ ensures Y ≡ 2; */
void g(void)
{
X = 2;
@@ -73,7 +73,7 @@ void g(void)
return;
}
-/*@ requires X ≡ 2; */
+/*@ requires X ≡ 2; */
void h(void)
{
e_acsl_assert(X == 2,(char *)"Precondition",(char *)"X == 2",19);
@@ -82,7 +82,7 @@ void h(void)
}
/*@ requires X ≡ 3;
- requires Y ≡ 2; */
+ requires Y ≡ 2; */
void i(void)
{
e_acsl_assert(X == 3,(char *)"Precondition",(char *)"X == 3",23);
@@ -94,14 +94,12 @@ void i(void)
/*@ behavior b1:
requires X ≡ 5;
ensures X ≡ 3;
-
+
behavior b2:
requires X ≡ 3+Y;
requires Y ≡ 2;
ensures X ≡ Y+1;
-
-
-*/
+ */
void j(void)
{
e_acsl_assert(X == 5,(char *)"Precondition",(char *)"X == 5",29);
@@ -118,15 +116,13 @@ void j(void)
/*@ behavior b1:
assumes X ≡ 1;
requires X ≡ 0;
-
+
behavior b2:
assumes X ≡ 3;
assumes Y ≡ 2;
requires X ≡ 3;
requires X+Y ≡ 5;
-
-
-*/
+ */
void k(void)
{
{
@@ -138,27 +134,25 @@ void k(void)
if (! (X == 1)) { __e_acsl_implies = 1; }
else { __e_acsl_implies = X == 0; }
e_acsl_assert(__e_acsl_implies,(char *)"Precondition",
- (char *)"X == 1 ==>\nX == 0",40);
- if (X == 3) { __e_acsl_and = Y == 2; }
- else { __e_acsl_and = 0; }
+ (char *)"X == 1 ==> X == 0",40);
+ if (X == 3) { __e_acsl_and = Y == 2; } else { __e_acsl_and = 0; }
if (! __e_acsl_and) { __e_acsl_implies_2 = 1; }
else { __e_acsl_implies_2 = X == 3; }
e_acsl_assert(__e_acsl_implies_2,(char *)"Precondition",
- (char *)"X == 3 && Y == 2 ==>\nX == 3",44);
- if (X == 3) { __e_acsl_and_2 = Y == 2; }
- else { __e_acsl_and_2 = 0; }
+ (char *)"X == 3 && Y == 2 ==> X == 3",44);
+ if (X == 3) { __e_acsl_and_2 = Y == 2; } else { __e_acsl_and_2 = 0; }
if (! __e_acsl_and_2) { __e_acsl_implies_3 = 1; }
else { __e_acsl_implies_3 = (long long)X + (long long)Y == (long long)5;
}
e_acsl_assert(__e_acsl_implies_3,(char *)"Precondition",
- (char *)"X == 3 && Y == 2 ==>\nX+Y == 5",45);
+ (char *)"X == 3 && Y == 2 ==> X+Y == 5",45);
X += Y;
}
return;
}
-/*@ ensures X ≡ 5; */
+/*@ ensures X ≡ 5; */
int l(void)
{
/*@ assert Y ≡ 2; */
@@ -170,15 +164,13 @@ int l(void)
/*@ behavior b1:
assumes X ≡ 7;
ensures X ≡ 95;
-
+
behavior b2:
assumes X ≡ 5;
assumes Y ≡ 2;
ensures X ≡ 7;
ensures X ≡ \old(X)+Y;
-
-
-*/
+ */
void m(void)
{
int __e_acsl_at_4;
@@ -186,15 +178,15 @@ void m(void)
int __e_acsl_at_2;
int __e_acsl_at;
__e_acsl_at_4 = X;
- { int __e_acsl_and_2;
- if (X == 5) { __e_acsl_and_2 = Y == 2; }
- else { __e_acsl_and_2 = 0; }
+ {
+ int __e_acsl_and_2;
+ if (X == 5) { __e_acsl_and_2 = Y == 2; } else { __e_acsl_and_2 = 0; }
__e_acsl_at_3 = __e_acsl_and_2;
}
- { int __e_acsl_and;
- if (X == 5) { __e_acsl_and = Y == 2; }
- else { __e_acsl_and = 0; }
+ {
+ int __e_acsl_and;
+ if (X == 5) { __e_acsl_and = Y == 2; } else { __e_acsl_and = 0; }
__e_acsl_at_2 = __e_acsl_and;
}
@@ -207,17 +199,17 @@ void m(void)
if (! __e_acsl_at) { __e_acsl_implies = 1; }
else { __e_acsl_implies = X == 95; }
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
- (char *)"\\old(X == 7) ==>\nX == 95",58);
+ (char *)"\\old(X == 7) ==> X == 95",58);
if (! __e_acsl_at_2) { __e_acsl_implies_2 = 1; }
else { __e_acsl_implies_2 = X == 7; }
e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
- (char *)"\\old(X == 5 && Y == 2) ==>\nX == 7",62);
+ (char *)"\\old(X == 5 && Y == 2) ==> X == 7",62);
if (! __e_acsl_at_3) { __e_acsl_implies_3 = 1; }
else {
__e_acsl_implies_3 = (long long)X == (long long)__e_acsl_at_4 + (long long)Y;
}
e_acsl_assert(__e_acsl_implies_3,(char *)"Postcondition",
- (char *)"\\old(X == 5 && Y == 2) ==>\nX == \\old(X)+Y",63);
+ (char *)"\\old(X == 5 && Y == 2) ==> X == \\old(X)+Y",63);
return;
}
@@ -225,16 +217,15 @@ void m(void)
/*@ requires X > 0;
requires X < 10;
+
behavior b1:
assumes X ≡ 7;
ensures X ≡ 8;
-
+
behavior b2:
assumes X ≡ 5;
ensures X ≡ 98;
-
-
-*/
+ */
void n(void)
{
int __e_acsl_at_2;
@@ -250,11 +241,11 @@ void n(void)
if (! __e_acsl_at) { __e_acsl_implies = 1; }
else { __e_acsl_implies = X == 8; }
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
- (char *)"\\old(X == 7) ==>\nX == 8",71);
+ (char *)"\\old(X == 7) ==> X == 8",71);
if (! __e_acsl_at_2) { __e_acsl_implies_2 = 1; }
else { __e_acsl_implies_2 = X == 98; }
e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
- (char *)"\\old(X == 5) ==>\nX == 98",74);
+ (char *)"\\old(X == 5) ==> X == 98",74);
return;
}
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 d7c7a14f371..6da7fdbc424 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
@@ -24,30 +24,25 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
- allocates \old(z);
-
assigns *z;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
@@ -55,8 +50,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
@@ -72,14 +66,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -93,7 +87,7 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int X = 0;
int Y = 2;
-/*@ ensures X ≡ 1; */
+/*@ ensures X ≡ 1; */
void f(void)
{
X = 1;
@@ -115,7 +109,7 @@ void f(void)
}
/*@ ensures X ≡ 2;
- ensures Y ≡ 2; */
+ ensures Y ≡ 2; */
void g(void)
{
X = 2;
@@ -144,7 +138,7 @@ void g(void)
}
-/*@ requires X ≡ 2; */
+/*@ requires X ≡ 2; */
void h(void)
{
{
@@ -166,7 +160,7 @@ void h(void)
}
/*@ requires X ≡ 3;
- requires Y ≡ 2; */
+ requires Y ≡ 2; */
void i(void)
{
{
@@ -201,14 +195,12 @@ void i(void)
/*@ behavior b1:
requires X ≡ 5;
ensures X ≡ 3;
-
+
behavior b2:
requires X ≡ 3+Y;
requires Y ≡ 2;
ensures X ≡ Y+1;
-
-
-*/
+ */
void j(void)
{
{
@@ -286,15 +278,13 @@ void j(void)
/*@ behavior b1:
assumes X ≡ 1;
requires X ≡ 0;
-
+
behavior b2:
assumes X ≡ 3;
assumes Y ≡ 2;
requires X ≡ 3;
requires X+Y ≡ 5;
-
-
-*/
+ */
void k(void)
{
{
@@ -327,7 +317,7 @@ void k(void)
__gmpz_clear(__e_acsl_2);
}
e_acsl_assert(__e_acsl_implies,(char *)"Precondition",
- (char *)"X == 1 ==>\nX == 0",40);
+ (char *)"X == 1 ==> X == 0",40);
__gmpz_init_set_si(__e_acsl_3,(long)3);
__e_acsl_eq_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X),
(__mpz_struct const *)(__e_acsl_3));
@@ -358,7 +348,7 @@ void k(void)
__gmpz_clear(__e_acsl_5);
}
e_acsl_assert(__e_acsl_implies_2,(char *)"Precondition",
- (char *)"X == 3 && Y == 2 ==>\nX == 3",44);
+ (char *)"X == 3 && Y == 2 ==> X == 3",44);
__e_acsl_eq_6 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_X),
(__mpz_struct const *)(__e_acsl_3));
if (__e_acsl_eq_6 == 0) {
@@ -396,7 +386,7 @@ void k(void)
__gmpz_clear(__e_acsl_7);
}
e_acsl_assert(__e_acsl_implies_3,(char *)"Precondition",
- (char *)"X == 3 && Y == 2 ==>\nX+Y == 5",45);
+ (char *)"X == 3 && Y == 2 ==> X+Y == 5",45);
__gmpz_clear(__e_acsl_X);
__gmpz_clear(__e_acsl);
__gmpz_clear(__e_acsl_3);
@@ -406,7 +396,7 @@ void k(void)
return;
}
-/*@ ensures X ≡ 5; */
+/*@ ensures X ≡ 5; */
int l(void)
{
/*@ assert Y ≡ 2; */
@@ -443,15 +433,13 @@ int l(void)
/*@ behavior b1:
assumes X ≡ 7;
ensures X ≡ 95;
-
+
behavior b2:
assumes X ≡ 5;
assumes Y ≡ 2;
ensures X ≡ 7;
ensures X ≡ \old(X)+Y;
-
-
-*/
+ */
void m(void)
{
int __e_acsl_at_4;
@@ -545,7 +533,7 @@ void m(void)
__gmpz_clear(__e_acsl_2);
}
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
- (char *)"\\old(X == 7) ==>\nX == 95",58);
+ (char *)"\\old(X == 7) ==> X == 95",58);
if (! __e_acsl_at_2) { __e_acsl_implies_2 = 1; }
else {
mpz_t __e_acsl_X_4;
@@ -560,7 +548,7 @@ void m(void)
__gmpz_clear(__e_acsl_5);
}
e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
- (char *)"\\old(X == 5 && Y == 2) ==>\nX == 7",62);
+ (char *)"\\old(X == 5 && Y == 2) ==> X == 7",62);
if (! __e_acsl_at_3) { __e_acsl_implies_3 = 1; }
else {
mpz_t __e_acsl_X_6;
@@ -583,7 +571,7 @@ void m(void)
__gmpz_clear(__e_acsl_add);
}
e_acsl_assert(__e_acsl_implies_3,(char *)"Postcondition",
- (char *)"\\old(X == 5 && Y == 2) ==>\nX == \\old(X)+Y",63);
+ (char *)"\\old(X == 5 && Y == 2) ==> X == \\old(X)+Y",63);
return;
}
@@ -591,16 +579,15 @@ void m(void)
/*@ requires X > 0;
requires X < 10;
+
behavior b1:
assumes X ≡ 7;
ensures X ≡ 8;
-
+
behavior b2:
assumes X ≡ 5;
ensures X ≡ 98;
-
-
-*/
+ */
void n(void)
{
int __e_acsl_at_2;
@@ -669,7 +656,7 @@ void n(void)
__gmpz_clear(__e_acsl_4);
}
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
- (char *)"\\old(X == 7) ==>\nX == 8",71);
+ (char *)"\\old(X == 7) ==> X == 8",71);
if (! __e_acsl_at_2) { __e_acsl_implies_2 = 1; }
else {
mpz_t __e_acsl_X_5;
@@ -684,7 +671,7 @@ void n(void)
__gmpz_clear(__e_acsl_6);
}
e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
- (char *)"\\old(X == 5) ==>\nX == 98",74);
+ (char *)"\\old(X == 5) ==> X == 98",74);
return;
}
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 63ec734eab0..7f62a62af5b 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
@@ -24,23 +24,20 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from str, base;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z,
char const *str,
int base);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
int __fc_random_counter __attribute__((__unused__));
@@ -55,14 +52,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 903c77ad57c..bed5fafffe4 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
@@ -24,35 +24,29 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from str, base;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z,
char const *str,
int base);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
int __fc_random_counter __attribute__((__unused__));
@@ -67,14 +61,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 cb446f01de2..514a0f203f5 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -63,11 +63,11 @@ int main(void)
i = 0;
while (i < 10) {
/*@ invariant 0 ≤ i ∧ i < 10; */
- { int __e_acsl_and;
- if (0 <= i) { __e_acsl_and = i < 10; }
- else { __e_acsl_and = 0; }
+ {
+ 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 *)"0 <= i &&\ni < 10",9);
+ (char *)"0 <= i && i < 10",9);
}
x += i;
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 a202ee37bf0..f2f2b377680 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
@@ -24,22 +24,19 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
int __fc_random_counter __attribute__((__unused__));
@@ -54,14 +51,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -106,7 +103,7 @@ int main(void)
}
else { __e_acsl_and = 0; }
e_acsl_assert(__e_acsl_and,(char *)"Invariant",
- (char *)"0 <= i &&\ni < 10",9);
+ (char *)"0 <= i && 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 7522e8193a6..dc42cb828f6 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -54,7 +54,7 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int X = 0;
-/*@ ensures X ≡ 3; */
+/*@ ensures X ≡ 3; */
int main(void)
{
int __retres;
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 56d97c82954..59880e9df06 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
@@ -24,22 +24,19 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
int __fc_random_counter __attribute__((__unused__));
@@ -54,14 +51,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -74,7 +71,7 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int X = 0;
-/*@ ensures X ≡ 3; */
+/*@ ensures X ≡ 3; */
int main(void)
{
int __retres;
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 cafb2c69504..bf25d56191f 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -61,73 +61,75 @@ int main(void)
x = 0;
y = 1;
/*@ assert x ≡ 0 ∧ y ≡ 1; */
- { int __e_acsl_and;
- if (x == 0) { __e_acsl_and = y == 1; }
- else { __e_acsl_and = 0; }
+ {
+ int __e_acsl_and;
+ if (x == 0) { __e_acsl_and = y == 1; } else { __e_acsl_and = 0; }
e_acsl_assert(__e_acsl_and,(char *)"Assertion",
- (char *)"x == 0 &&\ny == 1",11);
+ (char *)"x == 0 && y == 1",11);
}
/*@ assert ¬(x ≢ 0 ∧ y ≡ 1/0); */
- { int __e_acsl_and_2;
- if (x != 0) { __e_acsl_and_2 = y == 1 / 0; }
- else { __e_acsl_and_2 = 0; }
+ {
+ int __e_acsl_and_2;
+ if (x != 0) { __e_acsl_and_2 = y == 1 / 0; } else { __e_acsl_and_2 = 0; }
e_acsl_assert(! __e_acsl_and_2,(char *)"Assertion",
(char *)"!(x != 0 && y == 1/0)",12);
}
/*@ assert y ≡ 1 ∨ x ≡ 1; */
- { int __e_acsl_or;
- if (y == 1) { __e_acsl_or = 1; }
- else { __e_acsl_or = x == 1; }
- e_acsl_assert(__e_acsl_or,(char *)"Assertion",
- (char *)"y == 1 ||\nx == 1",13);
+ {
+ int __e_acsl_or;
+ if (y == 1) { __e_acsl_or = 1; } else { __e_acsl_or = x == 1; }
+ e_acsl_assert(__e_acsl_or,(char *)"Assertion",(char *)"y == 1 || x == 1",
+ 13);
}
/*@ assert x ≡ 0 ∨ y ≡ 1/0; */
- { int __e_acsl_or_2;
- if (x == 0) { __e_acsl_or_2 = 1; }
- else { __e_acsl_or_2 = y == 1 / 0; }
+ {
+ int __e_acsl_or_2;
+ if (x == 0) { __e_acsl_or_2 = 1; } else { __e_acsl_or_2 = y == 1 / 0; }
e_acsl_assert(__e_acsl_or_2,(char *)"Assertion",
- (char *)"x == 0 ||\ny == 1/0",14);
+ (char *)"x == 0 || y == 1/0",14);
}
/*@ assert x ≡ 0 ⇒ y ≡ 1; */
- { int __e_acsl_implies;
+ {
+ int __e_acsl_implies;
if (! (x == 0)) { __e_acsl_implies = 1; }
else { __e_acsl_implies = y == 1; }
e_acsl_assert(__e_acsl_implies,(char *)"Assertion",
- (char *)"x == 0 ==>\ny == 1",15);
+ (char *)"x == 0 ==> y == 1",15);
}
/*@ assert x ≡ 1 ⇒ y ≡ 1/0; */
- { int __e_acsl_implies_2;
+ {
+ int __e_acsl_implies_2;
if (! (x == 1)) { __e_acsl_implies_2 = 1; }
else { __e_acsl_implies_2 = y == 1 / 0; }
e_acsl_assert(__e_acsl_implies_2,(char *)"Assertion",
- (char *)"x == 1 ==>\ny == 1/0",16);
+ (char *)"x == 1 ==> y == 1/0",16);
}
/*@ assert x≢0? x ≢ 0: y ≢ 0; */
- { int __e_acsl_if;
- if (x != 0) { __e_acsl_if = x != 0; }
- else { __e_acsl_if = y != 0; }
+ {
+ int __e_acsl_if;
+ if (x != 0) { __e_acsl_if = x != 0; } else { __e_acsl_if = y != 0; }
e_acsl_assert(__e_acsl_if,(char *)"Assertion",
(char *)"x!=0? x != 0: y != 0",17);
}
/*@ assert y≢0? y ≢ 0: x ≢ 0; */
- { int __e_acsl_if_2;
- if (y != 0) { __e_acsl_if_2 = y != 0; }
- else { __e_acsl_if_2 = x != 0; }
+ {
+ int __e_acsl_if_2;
+ if (y != 0) { __e_acsl_if_2 = y != 0; } else { __e_acsl_if_2 = x != 0; }
e_acsl_assert(__e_acsl_if_2,(char *)"Assertion",
(char *)"y!=0? y != 0: x != 0",18);
}
/*@ assert x≡1? x ≡ 18: x ≡ 0; */
- { int __e_acsl_if_3;
- if (x == 1) { __e_acsl_if_3 = x == 18; }
- else { __e_acsl_if_3 = x == 0; }
+ {
+ int __e_acsl_if_3;
+ if (x == 1) { __e_acsl_if_3 = x == 18; } else { __e_acsl_if_3 = x == 0; }
e_acsl_assert(__e_acsl_if_3,(char *)"Assertion",
(char *)"x==1? x == 18: x == 0",19);
}
@@ -146,7 +148,7 @@ int main(void)
}
else { __e_acsl_equiv = 0; }
e_acsl_assert(__e_acsl_equiv,(char *)"Assertion",
- (char *)"x == 2 <==>\ny == 3",22);
+ (char *)"x == 2 <==> y == 3",22);
}
/*@ assert x ≡ 0 ⇔ y ≡ 1; */
@@ -163,13 +165,13 @@ int main(void)
}
else { __e_acsl_equiv_2 = 0; }
e_acsl_assert(__e_acsl_equiv_2,(char *)"Assertion",
- (char *)"x == 0 <==>\ny == 1",23);
+ (char *)"x == 0 <==> y == 1",23);
}
/*@ assert ((x≢0? x: y)≢0) ≡ (x≡0); */
- { int __e_acsl_if_4;
- if (x != 0) { __e_acsl_if_4 = x; }
- else { __e_acsl_if_4 = y; }
+ {
+ int __e_acsl_if_4;
+ if (x != 0) { __e_acsl_if_4 = x; } else { __e_acsl_if_4 = y; }
e_acsl_assert((__e_acsl_if_4 != 0) == (x == 0),(char *)"Assertion",
(char *)"((x!=0? x: y)!=0) == (x==0)",26);
}
@@ -178,37 +180,36 @@ int main(void)
{
int __e_acsl_and_3;
int __e_acsl_or_3;
- if (x != 0) { __e_acsl_and_3 = y != 0; }
- else { __e_acsl_and_3 = 0; }
+ if (x != 0) { __e_acsl_and_3 = y != 0; } else { __e_acsl_and_3 = 0; }
if (__e_acsl_and_3) { __e_acsl_or_3 = 1; }
else { __e_acsl_or_3 = y != 0; }
e_acsl_assert(__e_acsl_or_3,(char *)"Assertion",
- (char *)"(x != 0 && y != 0) ||\ny != 0",27);
+ (char *)"(x != 0 && y != 0) || y != 0",27);
}
/*@ assert (x ≢ 0 ∨ y ≢ 0) ∧ y ≡ 1; */
- { int __e_acsl_or_4;
+ {
+ int __e_acsl_or_4;
int __e_acsl_and_4;
- if (x != 0) { __e_acsl_or_4 = 1; }
- else { __e_acsl_or_4 = y != 0; }
+ if (x != 0) { __e_acsl_or_4 = 1; } else { __e_acsl_or_4 = y != 0; }
if (__e_acsl_or_4) { __e_acsl_and_4 = y == 1; }
else { __e_acsl_and_4 = 0; }
e_acsl_assert(__e_acsl_and_4,(char *)"Assertion",
- (char *)"(x != 0 || y != 0) &&\ny == 1",28);
+ (char *)"(x != 0 || y != 0) && y == 1",28);
}
/*@ assert (x≢0∨y≢0) ≡ (y≢0); */
- { int __e_acsl_or_5;
- if (x != 0) { __e_acsl_or_5 = 1; }
- else { __e_acsl_or_5 = y != 0; }
+ {
+ int __e_acsl_or_5;
+ if (x != 0) { __e_acsl_or_5 = 1; } else { __e_acsl_or_5 = y != 0; }
e_acsl_assert(__e_acsl_or_5 == (y != 0),(char *)"Assertion",
(char *)"(x!=0||y!=0) == (y!=0)",29);
}
/*@ 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; }
+ {
+ 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 *)"(x!=0&&y!=0) == (x!=0)",30);
}
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 edf976ab916..a5c8c725340 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
@@ -24,41 +24,34 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
- allocates \old(z);
-
assigns *z;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
/*@ requires \valid(z_orig);
requires ¬\initialized(z);
ensures \valid(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from *z_orig;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set(__mpz_struct * /*[1]*/ z,
__mpz_struct const * /*[1]*/ z_orig);
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
@@ -66,8 +59,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
@@ -83,14 +75,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -133,7 +125,7 @@ int main(void)
}
else { __e_acsl_and = 0; }
e_acsl_assert(__e_acsl_and,(char *)"Assertion",
- (char *)"x == 0 &&\ny == 1",11);
+ (char *)"x == 0 && y == 1",11);
__gmpz_clear(__e_acsl_x);
__gmpz_clear(__e_acsl);
}
@@ -204,8 +196,8 @@ int main(void)
__gmpz_clear(__e_acsl_x_3);
__gmpz_clear(__e_acsl_7);
}
- e_acsl_assert(__e_acsl_or,(char *)"Assertion",
- (char *)"y == 1 ||\nx == 1",13);
+ e_acsl_assert(__e_acsl_or,(char *)"Assertion",(char *)"y == 1 || x == 1",
+ 13);
__gmpz_clear(__e_acsl_y_3);
__gmpz_clear(__e_acsl_6);
}
@@ -248,7 +240,7 @@ int main(void)
__gmpz_clear(__e_acsl_div_2);
}
e_acsl_assert(__e_acsl_or_2,(char *)"Assertion",
- (char *)"x == 0 ||\ny == 1/0",14);
+ (char *)"x == 0 || y == 1/0",14);
__gmpz_clear(__e_acsl_x_4);
__gmpz_clear(__e_acsl_8);
}
@@ -277,7 +269,7 @@ int main(void)
__gmpz_clear(__e_acsl_12);
}
e_acsl_assert(__e_acsl_implies,(char *)"Assertion",
- (char *)"x == 0 ==>\ny == 1",15);
+ (char *)"x == 0 ==> y == 1",15);
__gmpz_clear(__e_acsl_x_5);
__gmpz_clear(__e_acsl_11);
}
@@ -320,7 +312,7 @@ int main(void)
__gmpz_clear(__e_acsl_div_3);
}
e_acsl_assert(__e_acsl_implies_2,(char *)"Assertion",
- (char *)"x == 1 ==>\ny == 1/0",16);
+ (char *)"x == 1 ==> y == 1/0",16);
__gmpz_clear(__e_acsl_x_6);
__gmpz_clear(__e_acsl_13);
}
@@ -497,7 +489,7 @@ int main(void)
}
else { __e_acsl_equiv = 0; }
e_acsl_assert(__e_acsl_equiv,(char *)"Assertion",
- (char *)"x == 2 <==>\ny == 3",22);
+ (char *)"x == 2 <==> y == 3",22);
__gmpz_clear(__e_acsl_x_13);
__gmpz_clear(__e_acsl_25);
}
@@ -554,7 +546,7 @@ int main(void)
}
else { __e_acsl_equiv_2 = 0; }
e_acsl_assert(__e_acsl_equiv_2,(char *)"Assertion",
- (char *)"x == 0 <==>\ny == 1",23);
+ (char *)"x == 0 <==> y == 1",23);
__gmpz_clear(__e_acsl_x_15);
__gmpz_clear(__e_acsl_29);
}
@@ -641,7 +633,7 @@ int main(void)
__gmpz_clear(__e_acsl_38);
}
e_acsl_assert(__e_acsl_or_3,(char *)"Assertion",
- (char *)"(x != 0 && y != 0) ||\ny != 0",27);
+ (char *)"(x != 0 && y != 0) || y != 0",27);
__gmpz_clear(__e_acsl_x_19);
__gmpz_clear(__e_acsl_36);
}
@@ -684,7 +676,7 @@ int main(void)
}
else { __e_acsl_and_4 = 0; }
e_acsl_assert(__e_acsl_and_4,(char *)"Assertion",
- (char *)"(x != 0 || y != 0) &&\ny == 1",28);
+ (char *)"(x != 0 || y != 0) && y == 1",28);
__gmpz_clear(__e_acsl_x_20);
__gmpz_clear(__e_acsl_39);
}
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 2f78b0c7833..6a3f7f640df 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -55,16 +55,15 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int A[10];
/*@ requires ∀ int i; 0 ≤ i ∧ i < 9 ⇒ A[i] ≤ A[i+1];
+
behavior exists:
assumes ∃ int j; (0 ≤ j ∧ j < 10) ∧ A[j] ≡ elt;
ensures \result ≡ 1;
-
+
behavior not_exists:
assumes ∀ int j; 0 ≤ j ∧ j < 10 ⇒ A[j] ≢ elt;
ensures \result ≡ 0;
-
-
-*/
+ */
int search(int elt)
{
int __e_acsl_at_2;
@@ -77,8 +76,7 @@ int search(int elt)
__e_acsl_forall = 1;
__e_acsl_i = 0;
while (1) {
- if (__e_acsl_i < 9) { ; }
- else { break; }
+ if (__e_acsl_i < 9) { ; } else { break; }
e_acsl_assert(__e_acsl_i + 1 < 10,(char *)"Precondition",
(char *)"index_bound: (int)(__e_acsl_i+1) < 10",9);
e_acsl_assert(0 <= __e_acsl_i + 1,(char *)"Precondition",
@@ -95,7 +93,7 @@ int search(int elt)
}
e_acsl_end_loop1: /* internal */ ;
e_acsl_assert(__e_acsl_forall,(char *)"Precondition",
- (char *)"\\forall int i; 0 <= i && i < 9 ==>\nA[i] <= A[i+1]",
+ (char *)"\\forall int i; 0 <= i && i < 9 ==> A[i] <= A[i+1]",
9);
{
int __e_acsl_forall_2;
@@ -103,8 +101,7 @@ int search(int elt)
__e_acsl_forall_2 = 1;
__e_acsl_j_2 = 0;
while (1) {
- if (__e_acsl_j_2 < 10) { ; }
- else { break; }
+ if (__e_acsl_j_2 < 10) { ; } else { break; }
e_acsl_assert(__e_acsl_j_2 < 10,(char *)"Postcondition",
(char *)"index_bound: __e_acsl_j_2 < 10",14);
e_acsl_assert(0 <= __e_acsl_j_2,(char *)"Postcondition",
@@ -125,8 +122,7 @@ int search(int elt)
__e_acsl_exists = 0;
__e_acsl_j = 0;
while (1) {
- if (__e_acsl_j < 10) { ; }
- else { break; }
+ if (__e_acsl_j < 10) { ; } else { break; }
e_acsl_assert(__e_acsl_j < 10,(char *)"Postcondition",
(char *)"index_bound: __e_acsl_j < 10",11);
e_acsl_assert(0 <= __e_acsl_j,(char *)"Postcondition",
@@ -165,12 +161,12 @@ int 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 *)"\\old(\\exists int j; (0 <= j && j < 10) && A[j] == elt) ==>\n\\result == 1",
+ (char *)"\\old(\\exists int j; (0 <= j && 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 *)"\\old(\\forall int j; 0 <= j && j < 10 ==> A[j] != elt) ==>\n\\result == 0",
+ (char *)"\\old(\\forall int j; 0 <= j && 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 74938e7d3a2..f3271862806 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
@@ -24,38 +24,32 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
- allocates \old(z);
-
assigns *z;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(z_orig);
requires \valid(z);
assigns *z;
assigns *z \from *z_orig;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_set(__mpz_struct * /*[1]*/ z,
__mpz_struct const * /*[1]*/ z_orig);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
@@ -63,13 +57,12 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)2147483647;
@@ -83,14 +76,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -104,16 +97,15 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int A[10];
/*@ requires ∀ ℤ i; 0 ≤ i ∧ i < 9 ⇒ A[i] ≤ A[i+1];
+
behavior exists:
assumes ∃ ℤ j; (0 ≤ j ∧ j < 10) ∧ A[j] ≡ elt;
ensures \result ≡ 1;
-
+
behavior not_exists:
assumes ∀ ℤ j; 0 ≤ j ∧ j < 10 ⇒ A[j] ≢ elt;
ensures \result ≡ 0;
-
-
-*/
+ */
int search(int elt)
{
int __e_acsl_at_2;
@@ -186,7 +178,7 @@ int search(int elt)
}
e_acsl_end_loop1: /* internal */ ;
e_acsl_assert(__e_acsl_forall,(char *)"Precondition",
- (char *)"\\forall integer i; 0 <= i && i < 9 ==>\nA[i] <= A[i+1]",
+ (char *)"\\forall integer i; 0 <= i && i < 9 ==> A[i] <= A[i+1]",
9);
__gmpz_clear(__e_acsl_i);
{
@@ -208,8 +200,7 @@ int search(int elt)
__gmpz_init_set_si(__e_acsl_15,(long)10);
__e_acsl_lt_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_j_3),
(__mpz_struct const *)(__e_acsl_15));
- if (__e_acsl_lt_3 < 0) { ; }
- else { break; }
+ if (__e_acsl_lt_3 < 0) { ; } else { break; }
__gmpz_clear(__e_acsl_15);
}
@@ -268,8 +259,7 @@ int search(int elt)
__gmpz_init_set_si(__e_acsl_10,(long)10);
__e_acsl_lt_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_j),
(__mpz_struct const *)(__e_acsl_10));
- if (__e_acsl_lt_2 < 0) { ; }
- else { break; }
+ if (__e_acsl_lt_2 < 0) { ; } else { break; }
__gmpz_clear(__e_acsl_10);
}
@@ -344,7 +334,7 @@ int search(int elt)
__gmpz_clear(__e_acsl_12);
}
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
- (char *)"\\old(\\exists integer j; (0 <= j && j < 10) && A[j] == elt) ==>\n\\result == 1",
+ (char *)"\\old(\\exists integer j; (0 <= j && j < 10) && A[j] == elt) ==> \\result == 1",
12);
if (! __e_acsl_at_2) { __e_acsl_implies_2 = 1; }
else {
@@ -360,7 +350,7 @@ int search(int elt)
__gmpz_clear(__e_acsl_17);
}
e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
- (char *)"\\old(\\forall integer j; 0 <= j && j < 10 ==> A[j] != elt) ==>\n\\result == 0",
+ (char *)"\\old(\\forall integer j; 0 <= j && 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 02532f4105b..815c8b0a5c2 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -52,26 +52,25 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒
- \initialized((char *)\old(ptr)+(0..\old(size)-1));
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
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 3d8a44702c8..643eabb51e6 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
@@ -24,22 +24,19 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
int __fc_random_counter __attribute__((__unused__));
@@ -54,14 +51,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -72,26 +69,25 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __literal_string(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒
- \initialized((char *)\old(ptr)+(0..\old(size)-1));
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
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 155fc10a7b1..9feba2ca0ba 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
@@ -37,36 +37,37 @@ axiomatic
}
*/
-/*@ allocates \result;
-
- assigns __fc_heap_status;
+/*@ assigns __fc_heap_status;
assigns __fc_heap_status \from size, __fc_heap_status;
- assigns \result
- \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
behavior allocation:
assumes is_allocable(size);
ensures \fresh{Old, Here}(\result,\old(size));
assigns __fc_heap_status;
assigns __fc_heap_status \from size, __fc_heap_status;
assigns \result \from size, __fc_heap_status;
+
behavior no_allocation:
assumes ¬is_allocable(size);
ensures \result ≡ \null;
- allocates \nothing;assigns \result \from \nothing;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
complete behaviors no_allocation, allocation;
disjoint behaviors no_allocation, allocation;
-
-*/
+ */
extern void *__malloc(size_t size);
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -77,21 +78,20 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒
- \initialized((char *)\old(ptr)+(0..\old(size)-1));
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
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 155fc10a7b1..9feba2ca0ba 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
@@ -37,36 +37,37 @@ axiomatic
}
*/
-/*@ allocates \result;
-
- assigns __fc_heap_status;
+/*@ assigns __fc_heap_status;
assigns __fc_heap_status \from size, __fc_heap_status;
- assigns \result
- \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
behavior allocation:
assumes is_allocable(size);
ensures \fresh{Old, Here}(\result,\old(size));
assigns __fc_heap_status;
assigns __fc_heap_status \from size, __fc_heap_status;
assigns \result \from size, __fc_heap_status;
+
behavior no_allocation:
assumes ¬is_allocable(size);
ensures \result ≡ \null;
- allocates \nothing;assigns \result \from \nothing;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
complete behaviors no_allocation, allocation;
disjoint behaviors no_allocation, allocation;
-
-*/
+ */
extern void *__malloc(size_t size);
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -77,21 +78,20 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒
- \initialized((char *)\old(ptr)+(0..\old(size)-1));
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
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 8a9cb1a398a..bb92a143361 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 134fda2f5c1..4aeea4b3b6c 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
@@ -24,22 +24,19 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
int __fc_random_counter __attribute__((__unused__));
@@ -54,14 +51,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 b0dc51be470..f15ad255c86 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 7cc57dc3d79..78f473968c9 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
@@ -24,22 +24,19 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
int __fc_random_counter __attribute__((__unused__));
@@ -54,14 +51,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 b57e6ed966c..f42d74413e2 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 b57e6ed966c..f42d74413e2 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 36de55e744e..e2677fe53e4 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
@@ -38,14 +38,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 8a1f66a2269..8f87c901769 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
@@ -28,22 +28,19 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
int __fc_random_counter __attribute__((__unused__));
@@ -58,14 +55,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 350ad96022e..b160fb8ba93 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -52,25 +52,24 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒
- \initialized((char *)\old(ptr)+(0..\old(size)-1));
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
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 a58a8694f9e..1982eac838b 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
@@ -24,30 +24,25 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
- allocates \old(z);
-
assigns *z;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
@@ -55,8 +50,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
@@ -65,8 +59,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_sub(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
@@ -75,8 +68,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_sub(__mpz_struct * /*[1]*/ z
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
@@ -85,13 +77,12 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)2147483647;
@@ -105,14 +96,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -123,15 +114,15 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int main(void)
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 a74c55dac9f..bd567c9d4bf 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -63,9 +63,9 @@ int main(void)
__e_acsl_forall = 1;
__e_acsl_x = 0;
while (1) {
- if (__e_acsl_x <= 1) { ; }
- else { break; }
- { int __e_acsl_or;
+ if (__e_acsl_x <= 1) { ; } else { break; }
+ {
+ int __e_acsl_or;
if (__e_acsl_x == 0) { __e_acsl_or = 1; }
else { __e_acsl_or = __e_acsl_x == 1; }
if (__e_acsl_or) { ; }
@@ -78,7 +78,7 @@ int main(void)
}
e_acsl_end_loop1: /* internal */ ;
e_acsl_assert(__e_acsl_forall,(char *)"Assertion",
- (char *)"\\forall int x; 0 <= x && x <= 1 ==>\nx == 0 || x == 1",
+ (char *)"\\forall int x; 0 <= x && x <= 1 ==> x == 0 || x == 1",
11);
}
@@ -89,8 +89,7 @@ int main(void)
__e_acsl_forall_2 = 1;
__e_acsl_x_2 = 0 + 1;
while (1) {
- if (__e_acsl_x_2 <= 1) { ; }
- else { break; }
+ if (__e_acsl_x_2 <= 1) { ; } else { break; }
if (__e_acsl_x_2 == 1) { ; }
else {
__e_acsl_forall_2 = 0;
@@ -99,7 +98,7 @@ int main(void)
}
e_acsl_end_loop2: /* internal */ ;
e_acsl_assert(__e_acsl_forall_2,(char *)"Assertion",
- (char *)"\\forall int x; 0 < x && x <= 1 ==>\nx == 1",12);
+ (char *)"\\forall int x; 0 < x && x <= 1 ==> x == 1",12);
}
/*@ assert ∀ int x; 0 < x ∧ x < 1 ⇒ \false; */
@@ -109,8 +108,7 @@ int main(void)
__e_acsl_forall_3 = 1;
__e_acsl_x_3 = 0 + 1;
while (1) {
- if (__e_acsl_x_3 < 1) { ; }
- else { break; }
+ if (__e_acsl_x_3 < 1) { ; } else { break; }
if (0) { ; }
else {
__e_acsl_forall_3 = 0;
@@ -119,7 +117,7 @@ int main(void)
}
e_acsl_end_loop3: /* internal */ ;
e_acsl_assert(__e_acsl_forall_3,(char *)"Assertion",
- (char *)"\\forall int x; 0 < x && x < 1 ==>\n\\false",13);
+ (char *)"\\forall int x; 0 < x && x < 1 ==> \\false",13);
}
/*@ assert ∀ int x; 0 ≤ x ∧ x < 1 ⇒ x ≡ 0; */
@@ -129,8 +127,7 @@ int main(void)
__e_acsl_forall_4 = 1;
__e_acsl_x_4 = 0;
while (1) {
- if (__e_acsl_x_4 < 1) { ; }
- else { break; }
+ if (__e_acsl_x_4 < 1) { ; } else { break; }
if (__e_acsl_x_4 == 0) { ; }
else {
__e_acsl_forall_4 = 0;
@@ -139,12 +136,13 @@ int main(void)
}
e_acsl_end_loop4: /* internal */ ;
e_acsl_assert(__e_acsl_forall_4,(char *)"Assertion",
- (char *)"\\forall int x; 0 <= x && x < 1 ==>\nx == 0",14);
+ (char *)"\\forall int x; 0 <= x && x < 1 ==> x == 0",14);
}
- /*@ assert ∀ int x, int y, int z;
- ((0 ≤ x ∧ x < 2) ∧ (0 ≤ y ∧ y < 5)) ∧ (0 ≤ z ∧ z ≤ y)
- ⇒ x+z ≤ y+1;
+ /*@ assert
+ ∀ int x, int y, int z;
+ ((0 ≤ x ∧ x < 2) ∧ (0 ≤ y ∧ y < 5)) ∧
+ (0 ≤ z ∧ z ≤ y) ⇒ x+z ≤ y+1;
*/
{
int __e_acsl_forall_5;
@@ -154,16 +152,13 @@ int main(void)
__e_acsl_forall_5 = 1;
__e_acsl_x_5 = 0;
while (1) {
- if (__e_acsl_x_5 < 2) { ; }
- else { break; }
+ if (__e_acsl_x_5 < 2) { ; } else { break; }
__e_acsl_y = 0;
while (1) {
- if (__e_acsl_y < 5) { ; }
- else { break; }
+ if (__e_acsl_y < 5) { ; } else { break; }
__e_acsl_z = 0;
while (1) {
- if (__e_acsl_z <= __e_acsl_y) { ; }
- else { break; }
+ if (__e_acsl_z <= __e_acsl_y) { ; } else { break; }
if (__e_acsl_x_5 + __e_acsl_z <= __e_acsl_y + 1) { ; }
else {
__e_acsl_forall_5 = 0;
@@ -176,7 +171,7 @@ int main(void)
}
e_acsl_end_loop5: /* internal */ ;
e_acsl_assert(__e_acsl_forall_5,(char *)"Assertion",
- (char *)"\\forall int x, int y, int z;\n((0 <= x && x < 2) && (0 <= y && y < 5)) && (0 <= z && z <= y) ==>\nx+z <= y+1",
+ (char *)"\\forall int x, int y, int z;\n ((0 <= x && x < 2) && (0 <= y && y < 5)) && (0 <= z && z <= y) ==>\n x+z <= y+1",
18);
}
@@ -187,8 +182,7 @@ int main(void)
__e_acsl_exists = 0;
__e_acsl_x_6 = 0;
while (1) {
- if (__e_acsl_x_6 < 10) { ; }
- else { break; }
+ if (__e_acsl_x_6 < 10) { ; } else { break; }
if (! (__e_acsl_x_6 == 5)) { ; }
else {
__e_acsl_exists = 1;
@@ -197,11 +191,13 @@ int main(void)
}
e_acsl_end_loop6: /* internal */ ;
e_acsl_assert(__e_acsl_exists,(char *)"Assertion",
- (char *)"\\exists int x; (0 <= x && x < 10) &&\nx == 5",23);
+ (char *)"\\exists int x; (0 <= x && x < 10) && x == 5",23);
}
- /*@ assert ∀ int x; 0 ≤ x ∧ x < 10 ⇒
- (x%2 ≡ 0 ⇒ (∃ int y; (0 ≤ y ∧ y ≤ x/2) ∧ x ≡ 2*y));
+ /*@ assert
+ ∀ int x;
+ 0 ≤ x ∧ x < 10 ⇒
+ (x%2 ≡ 0 ⇒ (∃ int y; (0 ≤ y ∧ y ≤ x/2) ∧ x ≡ 2*y));
*/
{
int __e_acsl_forall_6;
@@ -209,8 +205,7 @@ int main(void)
__e_acsl_forall_6 = 1;
__e_acsl_x_7 = 0;
while (1) {
- if (__e_acsl_x_7 < 10) { ; }
- else { break; }
+ if (__e_acsl_x_7 < 10) { ; } else { break; }
{
int __e_acsl_implies;
if (! (__e_acsl_x_7 % 2 == 0)) { __e_acsl_implies = 1; }
@@ -220,8 +215,7 @@ int main(void)
__e_acsl_exists_2 = 0;
__e_acsl_y_2 = 0;
while (1) {
- if (__e_acsl_y_2 <= __e_acsl_x_7 / 2) { ; }
- else { break; }
+ if (__e_acsl_y_2 <= __e_acsl_x_7 / 2) { ; } else { break; }
if (! (__e_acsl_x_7 == 2 * __e_acsl_y_2)) { ; }
else {
__e_acsl_exists_2 = 1;
@@ -241,7 +235,7 @@ int main(void)
}
e_acsl_end_loop8: /* internal */ ;
e_acsl_assert(__e_acsl_forall_6,(char *)"Assertion",
- (char *)"\\forall int x; 0 <= x && x < 10 ==>\n(x%2 == 0 ==> (\\exists int y; (0 <= y && y <= x/2) && x == 2*y))",
+ (char *)"\\forall int x;\n 0 <= x && x < 10 ==>\n (x%2 == 0 ==> (\\exists int y; (0 <= y && y <= x/2) && x == 2*y))",
27);
}
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 75dd28c2944..a6d2368138e 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
@@ -24,38 +24,32 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
- allocates \old(z);
-
assigns *z;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(z_orig);
requires \valid(z);
assigns *z;
assigns *z \from *z_orig;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_set(__mpz_struct * /*[1]*/ z,
__mpz_struct const * /*[1]*/ z_orig);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
@@ -63,8 +57,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
@@ -73,8 +66,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
@@ -83,8 +75,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
@@ -93,8 +84,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_r(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
@@ -110,14 +100,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -195,7 +185,7 @@ int main(void)
}
e_acsl_end_loop1: /* internal */ ;
e_acsl_assert(__e_acsl_forall,(char *)"Assertion",
- (char *)"\\forall integer x; 0 <= x && x <= 1 ==>\nx == 0 || x == 1",
+ (char *)"\\forall integer x; 0 <= x && x <= 1 ==> x == 0 || x == 1",
11);
__gmpz_clear(__e_acsl_x);
}
@@ -228,8 +218,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_9,(long)1);
__e_acsl_le_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_2),
(__mpz_struct const *)(__e_acsl_9));
- if (__e_acsl_le_2 <= 0) { ; }
- else { break; }
+ if (__e_acsl_le_2 <= 0) { ; } else { break; }
__gmpz_clear(__e_acsl_9);
}
@@ -261,7 +250,7 @@ int main(void)
}
e_acsl_end_loop2: /* internal */ ;
e_acsl_assert(__e_acsl_forall_2,(char *)"Assertion",
- (char *)"\\forall integer x; 0 < x && x <= 1 ==>\nx == 1",
+ (char *)"\\forall integer x; 0 < x && x <= 1 ==> x == 1",
12);
__gmpz_clear(__e_acsl_x_2);
}
@@ -317,7 +306,7 @@ int main(void)
}
e_acsl_end_loop3: /* internal */ ;
e_acsl_assert(__e_acsl_forall_3,(char *)"Assertion",
- (char *)"\\forall integer x; 0 < x && x < 1 ==>\n\\false",
+ (char *)"\\forall integer x; 0 < x && x < 1 ==> \\false",
13);
__gmpz_clear(__e_acsl_x_3);
}
@@ -342,8 +331,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_17,(long)1);
__e_acsl_lt_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_4),
(__mpz_struct const *)(__e_acsl_17));
- if (__e_acsl_lt_2 < 0) { ; }
- else { break; }
+ if (__e_acsl_lt_2 < 0) { ; } else { break; }
__gmpz_clear(__e_acsl_17);
}
@@ -375,14 +363,15 @@ int main(void)
}
e_acsl_end_loop4: /* internal */ ;
e_acsl_assert(__e_acsl_forall_4,(char *)"Assertion",
- (char *)"\\forall integer x; 0 <= x && x < 1 ==>\nx == 0",
+ (char *)"\\forall integer x; 0 <= x && 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;
+ /*@ assert
+ ∀ ℤ x, ℤ y, ℤ z;
+ ((0 ≤ x ∧ x < 2) ∧ (0 ≤ y ∧ y < 5)) ∧
+ (0 ≤ z ∧ z ≤ y) ⇒ x+z ≤ y+1;
*/
{
int __e_acsl_forall_5;
@@ -407,8 +396,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_26,(long)2);
__e_acsl_lt_4 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_5),
(__mpz_struct const *)(__e_acsl_26));
- if (__e_acsl_lt_4 < 0) { ; }
- else { break; }
+ if (__e_acsl_lt_4 < 0) { ; } else { break; }
__gmpz_clear(__e_acsl_26);
}
@@ -426,8 +414,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_23,(long)5);
__e_acsl_lt_3 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_y),
(__mpz_struct const *)(__e_acsl_23));
- if (__e_acsl_lt_3 < 0) { ; }
- else { break; }
+ if (__e_acsl_lt_3 < 0) { ; } else { break; }
__gmpz_clear(__e_acsl_23);
}
@@ -510,7 +497,7 @@ int main(void)
}
e_acsl_end_loop5: /* internal */ ;
e_acsl_assert(__e_acsl_forall_5,(char *)"Assertion",
- (char *)"\\forall integer x, integer y, integer z;\n((0 <= x && x < 2) && (0 <= y && y < 5)) && (0 <= z && z <= y) ==>\nx+z <= y+1",
+ (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",
18);
__gmpz_clear(__e_acsl_x_5);
__gmpz_clear(__e_acsl_y);
@@ -537,8 +524,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_30,(long)10);
__e_acsl_lt_5 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_6),
(__mpz_struct const *)(__e_acsl_30));
- if (__e_acsl_lt_5 < 0) { ; }
- else { break; }
+ if (__e_acsl_lt_5 < 0) { ; } else { break; }
__gmpz_clear(__e_acsl_30);
}
@@ -570,13 +556,15 @@ int main(void)
}
e_acsl_end_loop6: /* internal */ ;
e_acsl_assert(__e_acsl_exists,(char *)"Assertion",
- (char *)"\\exists integer x; (0 <= x && x < 10) &&\nx == 5",
+ (char *)"\\exists integer x; (0 <= x && x < 10) && x == 5",
23);
__gmpz_clear(__e_acsl_x_6);
}
- /*@ assert ∀ ℤ x; 0 ≤ x ∧ x < 10 ⇒
- (x%2 ≡ 0 ⇒ (∃ ℤ y; (0 ≤ y ∧ y ≤ x/2) ∧ x ≡ 2*y));
+ /*@ assert
+ ∀ ℤ x;
+ 0 ≤ x ∧ x < 10 ⇒
+ (x%2 ≡ 0 ⇒ (∃ ℤ y; (0 ≤ y ∧ y ≤ x/2) ∧ x ≡ 2*y));
*/
{
int __e_acsl_forall_6;
@@ -597,8 +585,7 @@ int main(void)
__gmpz_init_set_si(__e_acsl_40,(long)10);
__e_acsl_lt_6 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_7),
(__mpz_struct const *)(__e_acsl_40));
- if (__e_acsl_lt_6 < 0) { ; }
- else { break; }
+ if (__e_acsl_lt_6 < 0) { ; } else { break; }
__gmpz_clear(__e_acsl_40);
}
@@ -654,8 +641,7 @@ int main(void)
(__mpz_struct const *)(__e_acsl_36));
__e_acsl_le_5 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_y_2),
(__mpz_struct const *)(__e_acsl_div));
- if (__e_acsl_le_5 <= 0) { ; }
- else { break; }
+ if (__e_acsl_le_5 <= 0) { ; } else { break; }
__gmpz_clear(__e_acsl_36);
__gmpz_clear(__e_acsl_37);
__gmpz_clear(__e_acsl_div);
@@ -722,7 +708,7 @@ int main(void)
}
e_acsl_end_loop8: /* internal */ ;
e_acsl_assert(__e_acsl_forall_6,(char *)"Assertion",
- (char *)"\\forall integer x; 0 <= x && x < 10 ==>\n(x%2 == 0 ==> (\\exists integer y; (0 <= y && y <= x/2) && x == 2*y))",
+ (char *)"\\forall integer x;\n 0 <= x && x < 10 ==>\n (x%2 == 0 ==> (\\exists integer y; (0 <= y && 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 6e4003c9bae..998780a9701 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -53,7 +53,7 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
-/*@ ensures \result ≡ (int)(\old(x)-\old(x)); */
+/*@ ensures \result ≡ (int)(\old(x)-\old(x)); */
int f(int x)
{
int __e_acsl_at_2;
@@ -76,14 +76,14 @@ int f(int x)
}
int Y = 1;
-/*@ ensures \result ≡ Y; */
+/*@ ensures \result ≡ Y; */
int g(int x)
{
e_acsl_assert(x == Y,(char *)"Postcondition",(char *)"\\result == Y",18);
return (x);
}
-/*@ ensures \result ≡ 0; */
+/*@ ensures \result ≡ 0; */
int h(void)
{
int __retres;
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 e0559483cf1..e0facaf62be 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
@@ -24,30 +24,25 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
- allocates \old(z);
-
assigns *z;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
@@ -55,13 +50,12 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_sub(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
int __fc_random_counter __attribute__((__unused__));
unsigned long const __fc_rand_max = (unsigned long)2147483647;
@@ -75,14 +69,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -94,7 +88,7 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
}
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
-/*@ ensures \result ≡ (int)(\old(x)-\old(x)); */
+/*@ ensures \result ≡ (int)(\old(x)-\old(x)); */
int f(int x)
{
int __e_acsl_at_2;
@@ -130,7 +124,7 @@ int f(int x)
}
int Y = 1;
-/*@ ensures \result ≡ Y; */
+/*@ ensures \result ≡ Y; */
int g(int x)
{
{
@@ -150,7 +144,7 @@ int g(int x)
}
-/*@ ensures \result ≡ 0; */
+/*@ ensures \result ≡ 0; */
int h(void)
{
int __retres;
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 7b5500ad988..c174e68f743 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 ee470d936bb..6a35a11f471 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
@@ -24,22 +24,19 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
int __fc_random_counter __attribute__((__unused__));
@@ -54,14 +51,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 578bcadf1ea..d0b02f172bb 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -83,12 +83,11 @@ int main(void)
/*@ behavior b1:
requires x ≡ 5;
ensures x ≡ 3;
-
+
behavior b2:
requires x ≡ 3+y;
requires y ≡ 2;
ensures x ≡ y+1;
-
*/
{
e_acsl_assert(x == 5,(char *)"Precondition",(char *)"x == 5",24);
@@ -104,13 +103,12 @@ int main(void)
/*@ behavior b1:
assumes x ≡ 1;
requires x ≡ 0;
-
+
behavior b2:
assumes x ≡ 3;
assumes y ≡ 2;
requires x ≡ 3;
requires x+y ≡ 5;
-
*/
{
int __e_acsl_implies;
@@ -121,20 +119,18 @@ int main(void)
if (! (x == 1)) { __e_acsl_implies = 1; }
else { __e_acsl_implies = x == 0; }
e_acsl_assert(__e_acsl_implies,(char *)"Precondition",
- (char *)"x == 1 ==>\nx == 0",34);
- if (x == 3) { __e_acsl_and = y == 2; }
- else { __e_acsl_and = 0; }
+ (char *)"x == 1 ==> x == 0",34);
+ if (x == 3) { __e_acsl_and = y == 2; } else { __e_acsl_and = 0; }
if (! __e_acsl_and) { __e_acsl_implies_2 = 1; }
else { __e_acsl_implies_2 = x == 3; }
e_acsl_assert(__e_acsl_implies_2,(char *)"Precondition",
- (char *)"x == 3 && y == 2 ==>\nx == 3",38);
- if (x == 3) { __e_acsl_and_2 = y == 2; }
- else { __e_acsl_and_2 = 0; }
+ (char *)"x == 3 && y == 2 ==> x == 3",38);
+ if (x == 3) { __e_acsl_and_2 = y == 2; } else { __e_acsl_and_2 = 0; }
if (! __e_acsl_and_2) { __e_acsl_implies_3 = 1; }
else { __e_acsl_implies_3 = (long long)x + (long long)y == (long long)5;
}
e_acsl_assert(__e_acsl_implies_3,(char *)"Precondition",
- (char *)"x == 3 && y == 2 ==>\nx+y == 5",39);
+ (char *)"x == 3 && y == 2 ==> x+y == 5",39);
x += y;
}
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 cd84872b88a..772fdbcdc1a 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
@@ -24,30 +24,25 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
- allocates \old(z);
-
assigns *z;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
@@ -55,8 +50,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
requires \valid(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
@@ -72,14 +66,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -186,12 +180,11 @@ int main(void)
/*@ behavior b1:
requires x ≡ 5;
ensures x ≡ 3;
-
+
behavior b2:
requires x ≡ 3+y;
requires y ≡ 2;
ensures x ≡ y+1;
-
*/
{
mpz_t __e_acsl_x_6;
@@ -265,13 +258,12 @@ int main(void)
/*@ behavior b1:
assumes x ≡ 1;
requires x ≡ 0;
-
+
behavior b2:
assumes x ≡ 3;
assumes y ≡ 2;
requires x ≡ 3;
requires x+y ≡ 5;
-
*/
{
mpz_t __e_acsl_x_7;
@@ -303,7 +295,7 @@ int main(void)
__gmpz_clear(__e_acsl_12);
}
e_acsl_assert(__e_acsl_implies,(char *)"Precondition",
- (char *)"x == 1 ==>\nx == 0",34);
+ (char *)"x == 1 ==> x == 0",34);
__gmpz_init_set_si(__e_acsl_13,(long)3);
__e_acsl_eq_14 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_7),
(__mpz_struct const *)(__e_acsl_13));
@@ -334,7 +326,7 @@ int main(void)
__gmpz_clear(__e_acsl_15);
}
e_acsl_assert(__e_acsl_implies_2,(char *)"Precondition",
- (char *)"x == 3 && y == 2 ==>\nx == 3",38);
+ (char *)"x == 3 && y == 2 ==> x == 3",38);
__e_acsl_eq_17 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_x_7),
(__mpz_struct const *)(__e_acsl_13));
if (__e_acsl_eq_17 == 0) {
@@ -372,7 +364,7 @@ int main(void)
__gmpz_clear(__e_acsl_17);
}
e_acsl_assert(__e_acsl_implies_3,(char *)"Precondition",
- (char *)"x == 3 && y == 2 ==>\nx+y == 5",39);
+ (char *)"x == 3 && y == 2 ==> x+y == 5",39);
__gmpz_clear(__e_acsl_x_7);
__gmpz_clear(__e_acsl_11);
__gmpz_clear(__e_acsl_13);
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 3ebfc147bb7..82e3cdb879f 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 3ebfc147bb7..82e3cdb879f 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
@@ -34,14 +34,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 dfa7b129aae..f2204f36c8c 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
@@ -35,14 +35,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 eb01f870fd2..bfdd29db4d7 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
@@ -25,34 +25,28 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_ui(__mpz_struct * /*[1]*/ z,
unsigned long n);
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
int __fc_random_counter __attribute__((__unused__));
@@ -67,14 +61,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
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 b2526df20c3..bc1f297a0f0 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
@@ -33,55 +33,57 @@ axiomatic
}
*/
-/*@ allocates \result;
-
- assigns __fc_heap_status;
+/*@ assigns __fc_heap_status;
assigns __fc_heap_status \from size, __fc_heap_status;
- assigns \result
- \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
behavior allocation:
assumes is_allocable(size);
ensures \fresh{Old, Here}(\result,\old(size));
assigns __fc_heap_status;
assigns __fc_heap_status \from size, __fc_heap_status;
assigns \result \from size, __fc_heap_status;
+
behavior no_allocation:
assumes ¬is_allocable(size);
ensures \result ≡ \null;
- allocates \nothing;assigns \result \from \nothing;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
complete behaviors no_allocation, allocation;
disjoint behaviors no_allocation, allocation;
-
-*/
+ */
extern void *__malloc(size_t size);
-/*@ frees p;
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+ frees p;
- assigns __fc_heap_status;
- assigns __fc_heap_status
- \from __fc_heap_status;
behavior deallocation:
assumes p ≢ \null;
requires \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
+
behavior no_deallocation:
assumes p ≡ \null;
- allocates \nothing;assigns \nothing;
+ assigns \nothing;
+ allocates \nothing;
+
complete behaviors no_deallocation, deallocation;
disjoint behaviors no_deallocation, deallocation;
-
-*/
+ */
extern void __free(void *p);
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -92,27 +94,26 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒
- \initialized((char *)\old(ptr)+(0..\old(size)-1));
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int *X;
/*@ requires \valid(x);
- ensures \valid(\result); */
+ ensures \valid(\result); */
int *f(int *x)
{
int *y;
@@ -212,7 +213,7 @@ int main(void)
}
else { __e_acsl_and_4 = 0; }
e_acsl_assert(__e_acsl_and_4,(char *)"Assertion",
- (char *)"(!\\valid(a) && !\\valid(b)) &&\n!\\valid(X)",27);
+ (char *)"(!\\valid(a) && !\\valid(b)) && !\\valid(X)",27);
}
__full_init((void *)(& a));
@@ -250,7 +251,7 @@ int main(void)
}
else { __e_acsl_and_8 = 0; }
e_acsl_assert(__e_acsl_and_8,(char *)"Assertion",
- (char *)"(\\valid(a) && !\\valid(b)) &&\n!\\valid(X)",29);
+ (char *)"(\\valid(a) && !\\valid(b)) && !\\valid(X)",29);
}
__full_init((void *)(& X));
@@ -288,7 +289,7 @@ int main(void)
}
else { __e_acsl_and_12 = 0; }
e_acsl_assert(__e_acsl_and_12,(char *)"Assertion",
- (char *)"(\\valid(a) && !\\valid(b)) &&\n\\valid(X)",31);
+ (char *)"(\\valid(a) && !\\valid(b)) && \\valid(X)",31);
}
__full_init((void *)(& b));
@@ -326,7 +327,7 @@ int main(void)
}
else { __e_acsl_and_16 = 0; }
e_acsl_assert(__e_acsl_and_16,(char *)"Assertion",
- (char *)"(\\valid(a) && \\valid(b)) &&\n\\valid(X)",33);
+ (char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",33);
}
__full_init((void *)(& X));
@@ -364,7 +365,7 @@ int main(void)
}
else { __e_acsl_and_20 = 0; }
e_acsl_assert(__e_acsl_and_20,(char *)"Assertion",
- (char *)"(\\valid(a) && \\valid(b)) &&\n\\valid(X)",35);
+ (char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",35);
}
__free((void *)a);
@@ -401,7 +402,7 @@ int main(void)
}
else { __e_acsl_and_24 = 0; }
e_acsl_assert(__e_acsl_and_24,(char *)"Assertion",
- (char *)"(!\\valid(a) && \\valid(b)) &&\n\\valid(X)",37);
+ (char *)"(!\\valid(a) && \\valid(b)) && \\valid(X)",37);
}
__retres = 0;
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 b2526df20c3..bc1f297a0f0 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
@@ -33,55 +33,57 @@ axiomatic
}
*/
-/*@ allocates \result;
-
- assigns __fc_heap_status;
+/*@ assigns __fc_heap_status;
assigns __fc_heap_status \from size, __fc_heap_status;
- assigns \result
- \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
behavior allocation:
assumes is_allocable(size);
ensures \fresh{Old, Here}(\result,\old(size));
assigns __fc_heap_status;
assigns __fc_heap_status \from size, __fc_heap_status;
assigns \result \from size, __fc_heap_status;
+
behavior no_allocation:
assumes ¬is_allocable(size);
ensures \result ≡ \null;
- allocates \nothing;assigns \result \from \nothing;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
complete behaviors no_allocation, allocation;
disjoint behaviors no_allocation, allocation;
-
-*/
+ */
extern void *__malloc(size_t size);
-/*@ frees p;
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+ frees p;
- assigns __fc_heap_status;
- assigns __fc_heap_status
- \from __fc_heap_status;
behavior deallocation:
assumes p ≢ \null;
requires \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
+
behavior no_deallocation:
assumes p ≡ \null;
- allocates \nothing;assigns \nothing;
+ assigns \nothing;
+ allocates \nothing;
+
complete behaviors no_deallocation, deallocation;
disjoint behaviors no_deallocation, deallocation;
-
-*/
+ */
extern void __free(void *p);
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -92,27 +94,26 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒
- \initialized((char *)\old(ptr)+(0..\old(size)-1));
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
int *X;
/*@ requires \valid(x);
- ensures \valid(\result); */
+ ensures \valid(\result); */
int *f(int *x)
{
int *y;
@@ -212,7 +213,7 @@ int main(void)
}
else { __e_acsl_and_4 = 0; }
e_acsl_assert(__e_acsl_and_4,(char *)"Assertion",
- (char *)"(!\\valid(a) && !\\valid(b)) &&\n!\\valid(X)",27);
+ (char *)"(!\\valid(a) && !\\valid(b)) && !\\valid(X)",27);
}
__full_init((void *)(& a));
@@ -250,7 +251,7 @@ int main(void)
}
else { __e_acsl_and_8 = 0; }
e_acsl_assert(__e_acsl_and_8,(char *)"Assertion",
- (char *)"(\\valid(a) && !\\valid(b)) &&\n!\\valid(X)",29);
+ (char *)"(\\valid(a) && !\\valid(b)) && !\\valid(X)",29);
}
__full_init((void *)(& X));
@@ -288,7 +289,7 @@ int main(void)
}
else { __e_acsl_and_12 = 0; }
e_acsl_assert(__e_acsl_and_12,(char *)"Assertion",
- (char *)"(\\valid(a) && !\\valid(b)) &&\n\\valid(X)",31);
+ (char *)"(\\valid(a) && !\\valid(b)) && \\valid(X)",31);
}
__full_init((void *)(& b));
@@ -326,7 +327,7 @@ int main(void)
}
else { __e_acsl_and_16 = 0; }
e_acsl_assert(__e_acsl_and_16,(char *)"Assertion",
- (char *)"(\\valid(a) && \\valid(b)) &&\n\\valid(X)",33);
+ (char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",33);
}
__full_init((void *)(& X));
@@ -364,7 +365,7 @@ int main(void)
}
else { __e_acsl_and_20 = 0; }
e_acsl_assert(__e_acsl_and_20,(char *)"Assertion",
- (char *)"(\\valid(a) && \\valid(b)) &&\n\\valid(X)",35);
+ (char *)"(\\valid(a) && \\valid(b)) && \\valid(X)",35);
}
__free((void *)a);
@@ -401,7 +402,7 @@ int main(void)
}
else { __e_acsl_and_24 = 0; }
e_acsl_assert(__e_acsl_and_24,(char *)"Assertion",
- (char *)"(!\\valid(a) && \\valid(b)) &&\n\\valid(X)",37);
+ (char *)"(!\\valid(a) && \\valid(b)) && \\valid(X)",37);
}
__retres = 0;
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 bd2c5f40514..5c1967666ef 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
@@ -33,55 +33,57 @@ axiomatic
}
*/
-/*@ allocates \result;
-
- assigns __fc_heap_status;
+/*@ assigns __fc_heap_status;
assigns __fc_heap_status \from size, __fc_heap_status;
- assigns \result
- \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
behavior allocation:
assumes is_allocable(size);
ensures \fresh{Old, Here}(\result,\old(size));
assigns __fc_heap_status;
assigns __fc_heap_status \from size, __fc_heap_status;
assigns \result \from size, __fc_heap_status;
+
behavior no_allocation:
assumes ¬is_allocable(size);
ensures \result ≡ \null;
- allocates \nothing;assigns \result \from \nothing;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
complete behaviors no_allocation, allocation;
disjoint behaviors no_allocation, allocation;
-
-*/
+ */
extern void *__malloc(size_t size);
-/*@ frees p;
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+ frees p;
- assigns __fc_heap_status;
- assigns __fc_heap_status
- \from __fc_heap_status;
behavior deallocation:
assumes p ≢ \null;
requires \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
+
behavior no_deallocation:
assumes p ≡ \null;
- allocates \nothing;assigns \nothing;
+ assigns \nothing;
+ allocates \nothing;
+
complete behaviors no_deallocation, deallocation;
disjoint behaviors no_deallocation, deallocation;
-
-*/
+ */
extern void __free(void *p);
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -92,27 +94,26 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid_read(void *ptr,
size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒
- \initialized((char *)\old(ptr)+(0..\old(size)-1));
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
@@ -153,7 +154,7 @@ int main(void)
}
else { __e_acsl_and_3 = 0; }
e_acsl_assert(__e_acsl_and_3,(char *)"Assertion",
- (char *)"!\\valid(a) &&\n!\\valid(b)",12);
+ (char *)"!\\valid(a) && !\\valid(b)",12);
}
__full_init((void *)(& a));
@@ -188,7 +189,7 @@ int main(void)
}
else { __e_acsl_and_6 = 0; }
e_acsl_assert(__e_acsl_and_6,(char *)"Assertion",
- (char *)"\\valid(a) &&\n\\valid(b)",16);
+ (char *)"\\valid(a) && \\valid(b)",16);
}
/*@ assert *b ≡ n; */
@@ -234,7 +235,7 @@ int main(void)
}
else { __e_acsl_and_10 = 0; }
e_acsl_assert(__e_acsl_and_10,(char *)"Assertion",
- (char *)"!\\valid(a) &&\n!\\valid(b)",19);
+ (char *)"!\\valid(a) && !\\valid(b)",19);
}
__retres = 0;
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 abafc070936..10cc3e9c09f 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
@@ -24,22 +24,19 @@ model __mpz_struct { ℤ n };
*/
/*@ requires ¬\initialized(z);
ensures \valid(\old(z));
-
ensures \initialized(\old(z));
- allocates \old(z);
-
assigns *z;
assigns *z \from n;
-
-*/
+ allocates \old(z);
+ */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
/*@ requires \valid(x);
- assigns *x; */
+ assigns *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- assigns \nothing; */
+ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
int __fc_random_counter __attribute__((__unused__));
@@ -53,55 +50,57 @@ axiomatic
}
*/
-/*@ allocates \result;
-
- assigns __fc_heap_status;
+/*@ assigns __fc_heap_status;
assigns __fc_heap_status \from size, __fc_heap_status;
- assigns \result
- \from size, __fc_heap_status;
+ assigns \result \from size, __fc_heap_status;
+ allocates \result;
+
behavior allocation:
assumes is_allocable(size);
ensures \fresh{Old, Here}(\result,\old(size));
assigns __fc_heap_status;
assigns __fc_heap_status \from size, __fc_heap_status;
assigns \result \from size, __fc_heap_status;
+
behavior no_allocation:
assumes ¬is_allocable(size);
ensures \result ≡ \null;
- allocates \nothing;assigns \result \from \nothing;
+ assigns \result \from \nothing;
+ allocates \nothing;
+
complete behaviors no_allocation, allocation;
disjoint behaviors no_allocation, allocation;
-
-*/
+ */
extern void *__malloc(size_t size);
-/*@ frees p;
+/*@ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status;
+ frees p;
- assigns __fc_heap_status;
- assigns __fc_heap_status
- \from __fc_heap_status;
behavior deallocation:
assumes p ≢ \null;
requires \freeable(p);
ensures \allocable(\old(p));
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status;
+
behavior no_deallocation:
assumes p ≡ \null;
- allocates \nothing;assigns \nothing;
+ assigns \nothing;
+ allocates \nothing;
+
complete behaviors no_deallocation, deallocation;
disjoint behaviors no_deallocation, deallocation;
-
-*/
+ */
extern void __free(void *p);
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -112,24 +111,23 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __initialize(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒
- \initialized((char *)\old(ptr)+(0..\old(size)-1));
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
@@ -170,7 +168,7 @@ int main(void)
}
else { __e_acsl_and_3 = 0; }
e_acsl_assert(__e_acsl_and_3,(char *)"Assertion",
- (char *)"!\\valid(a) &&\n!\\valid(b)",12);
+ (char *)"!\\valid(a) && !\\valid(b)",12);
}
__full_init((void *)(& a));
@@ -205,7 +203,7 @@ int main(void)
}
else { __e_acsl_and_6 = 0; }
e_acsl_assert(__e_acsl_and_6,(char *)"Assertion",
- (char *)"\\valid(a) &&\n\\valid(b)",16);
+ (char *)"\\valid(a) && \\valid(b)",16);
}
/*@ assert *b ≡ n; */
@@ -249,7 +247,7 @@ int main(void)
}
else { __e_acsl_and_9 = 0; }
e_acsl_assert(__e_acsl_and_9,(char *)"Assertion",
- (char *)"!\\valid(a) &&\n!\\valid(b)",19);
+ (char *)"!\\valid(a) && !\\valid(b)",19);
}
__retres = 0;
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 cb8c6c4bcd2..b52dfeec5b4 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
@@ -38,14 +38,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -56,35 +56,32 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒
- \initialized((char *)\old(ptr)+(0..\old(size)-1));
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
/*@ behavior B1:
assumes l ≡ \null;
ensures \result ≡ \old(l);
-
+
behavior B2:
assumes ¬\valid(l);
assumes ¬\valid(l->next);
ensures \result ≡ \old(l);
-
-
-*/
+ */
struct list *f(struct list *l)
{
struct list *__e_acsl_at_4;
@@ -113,7 +110,8 @@ struct list *f(struct list *l)
}
else { __e_acsl_and = 0; }
__e_acsl_and_2 = ! __e_acsl_and;
- } else { __e_acsl_and_2 = 0; }
+ }
+ else { __e_acsl_and_2 = 0; }
__e_acsl_at_3 = __e_acsl_and_2;
}
@@ -137,11 +135,11 @@ struct list *f(struct list *l)
if (! __e_acsl_at) { __e_acsl_implies = 1; }
else { __e_acsl_implies = __retres == __e_acsl_at_2; }
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
- (char *)"\\old(l == \\null) ==>\n\\result == \\old(l)",18);
+ (char *)"\\old(l == \\null) ==> \\result == \\old(l)",18);
if (! __e_acsl_at_3) { __e_acsl_implies_2 = 1; }
else { __e_acsl_implies_2 = __retres == __e_acsl_at_4; }
e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
- (char *)"\\old(!\\valid(l) && !\\valid(l->next)) ==>\n\\result == \\old(l)",
+ (char *)"\\old(!\\valid(l) && !\\valid(l->next)) ==> \\result == \\old(l)",
22);
__delete_block((void *)(& l));
return (__retres);
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 cb8c6c4bcd2..b52dfeec5b4 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
@@ -38,14 +38,14 @@ axiomatic
}
*/
/*@ ensures \false;
- assigns \nothing; */
+ assigns \nothing; */
extern void exit(int status);
extern FILE *__fc_stdout;
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+(..)); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
/*@ requires predicate ≢ 0;
- assigns \nothing; */
+ assigns \nothing; */
void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
{
if (! predicate) {
@@ -56,35 +56,32 @@ void e_acsl_assert(int predicate, char *kind, char *pred_txt, int line)
return;
}
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
size_t size);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
-/*@ assigns \nothing; */
+/*@ assigns \nothing; */
extern __attribute__((__FC_BUILTIN__)) int __valid(void *ptr, size_t size);
/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
- ensures \result ≡ 1 ⇒
- \initialized((char *)\old(ptr)+(0..\old(size)-1));
+ ensures
+ \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0..\old(size)-1));
assigns \nothing;
-
-*/
+ */
extern __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
size_t size);
extern __attribute__((__FC_BUILTIN__)) void __clean(void);
/*@ behavior B1:
assumes l ≡ \null;
ensures \result ≡ \old(l);
-
+
behavior B2:
assumes ¬\valid(l);
assumes ¬\valid(l->next);
ensures \result ≡ \old(l);
-
-
-*/
+ */
struct list *f(struct list *l)
{
struct list *__e_acsl_at_4;
@@ -113,7 +110,8 @@ struct list *f(struct list *l)
}
else { __e_acsl_and = 0; }
__e_acsl_and_2 = ! __e_acsl_and;
- } else { __e_acsl_and_2 = 0; }
+ }
+ else { __e_acsl_and_2 = 0; }
__e_acsl_at_3 = __e_acsl_and_2;
}
@@ -137,11 +135,11 @@ struct list *f(struct list *l)
if (! __e_acsl_at) { __e_acsl_implies = 1; }
else { __e_acsl_implies = __retres == __e_acsl_at_2; }
e_acsl_assert(__e_acsl_implies,(char *)"Postcondition",
- (char *)"\\old(l == \\null) ==>\n\\result == \\old(l)",18);
+ (char *)"\\old(l == \\null) ==> \\result == \\old(l)",18);
if (! __e_acsl_at_3) { __e_acsl_implies_2 = 1; }
else { __e_acsl_implies_2 = __retres == __e_acsl_at_4; }
e_acsl_assert(__e_acsl_implies_2,(char *)"Postcondition",
- (char *)"\\old(!\\valid(l) && !\\valid(l->next)) ==>\n\\result == \\old(l)",
+ (char *)"\\old(!\\valid(l) && !\\valid(l->next)) ==> \\result == \\old(l)",
22);
__delete_block((void *)(& l));
return (__retres);
--
GitLab