From f73e5cf79f134fab136527aef33eece9bb629bc7 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 7 Sep 2012 09:03:25 +0000
Subject: [PATCH] [E-ACSL] fixing oracles
---
.../tests/e-acsl-runtime/oracle/arith.1.res.oracle | 12 +-----------
.../tests/e-acsl-runtime/oracle/array.1.res.oracle | 5 +----
.../tests/e-acsl-runtime/oracle/at.1.res.oracle | 6 +-----
.../tests/e-acsl-runtime/oracle/cast.1.res.oracle | 6 +-----
.../e-acsl-runtime/oracle/comparison.1.res.oracle | 6 +-----
.../oracle/function_contract.1.res.oracle | 6 +-----
.../oracle/integer_constant.1.res.oracle | 5 +----
.../e-acsl-runtime/oracle/invariant.1.res.oracle | 5 +----
.../e-acsl-runtime/oracle/labeled_stmt.1.res.oracle | 5 +----
.../tests/e-acsl-runtime/oracle/lazy.1.res.oracle | 5 +----
.../e-acsl-runtime/oracle/linear_search.1.res.oracle | 8 +-------
.../oracle/nested_code_annot.1.res.oracle | 5 +----
.../tests/e-acsl-runtime/oracle/not.1.res.oracle | 5 +----
.../oracle/other_constants.1.res.oracle | 5 +----
.../tests/e-acsl-runtime/oracle/ptr.1.res.oracle | 10 +---------
.../tests/e-acsl-runtime/oracle/quantif.1.res.oracle | 10 +---------
.../tests/e-acsl-runtime/oracle/result.1.res.oracle | 7 +------
.../tests/e-acsl-runtime/oracle/sizeof.1.res.oracle | 5 +----
.../e-acsl-runtime/oracle/stmt_contract.1.res.oracle | 6 +-----
.../tests/e-acsl-runtime/oracle/typedef.1.res.oracle | 5 +----
20 files changed, 20 insertions(+), 107 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
index 847f278af67..d9aa6913031 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
@@ -935,15 +935,11 @@ extern int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z, char const *str,
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2;
@@ -953,7 +949,6 @@ extern void __gmpz_neg(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -964,7 +959,6 @@ extern void __gmpz_add(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -975,7 +969,6 @@ extern void __gmpz_sub(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -986,7 +979,6 @@ extern void __gmpz_mul(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -997,7 +989,6 @@ extern void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -1007,7 +998,6 @@ extern void __gmpz_tdiv_r(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
index ea501c71f67..32676167d9a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
@@ -94,10 +94,7 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
index b45c3443e0b..9f974a7586c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
@@ -361,16 +361,12 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
index ed07f2aae52..617fbeb9b06 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
@@ -205,14 +205,10 @@ extern int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z, char const *str,
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z);
- allocates \nothing;
assigns \nothing; */
extern unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
index a8422130298..8d7271e6ad9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
@@ -428,15 +428,11 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
index 1349b58541f..09ac08bf81e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
@@ -767,16 +767,12 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
index 56383fbba5d..4e94ab1b73f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
@@ -101,10 +101,7 @@ extern int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z, char const *str,
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
index 67addf88e85..08cb2156355 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
@@ -898,10 +898,7 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
index b4b7eb91854..ab7a257340c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
@@ -121,10 +121,7 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
index 850904b8e62..0696b151a6e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
@@ -850,10 +850,7 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
index 8ec0a1bd963..6cbaee68747 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
@@ -614,7 +614,6 @@ extern void __gmpz_init(__mpz_struct * /*[1]*/ z);
extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
/*@ requires \valid(z_orig);
requires \valid(z);
- allocates \nothing;
assigns *z;
assigns *z \from *z_orig;
@@ -628,16 +627,12 @@ extern void __gmpz_set(__mpz_struct * /*[1]*/ z,
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -646,7 +641,6 @@ extern void __gmpz_add(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z);
- allocates \nothing;
assigns \nothing; */
extern unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
index 1dd6cf46a5c..03dd5637ee0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
@@ -177,10 +177,7 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
index 87fa944cb57..6da46777f1c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
@@ -62,10 +62,7 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
index 18fb2471664..72cc668a4e8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
@@ -86,10 +86,7 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
index 108825f9d75..e55d6bf42be 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
@@ -488,16 +488,12 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -508,7 +504,6 @@ extern void __gmpz_add(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -519,7 +514,6 @@ extern void __gmpz_sub(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -530,7 +524,6 @@ extern void __gmpz_mul(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -539,7 +532,6 @@ extern void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z);
- allocates \nothing;
assigns \nothing; */
extern unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
index a24ca4fadd8..9e297890cd4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
@@ -694,7 +694,6 @@ extern void __gmpz_init(__mpz_struct * /*[1]*/ z);
extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
/*@ requires \valid(z_orig);
requires \valid(z);
- allocates \nothing;
assigns *z;
assigns *z \from *z_orig;
@@ -708,16 +707,12 @@ extern void __gmpz_set(__mpz_struct * /*[1]*/ z,
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -728,7 +723,6 @@ extern void __gmpz_add(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -739,7 +733,6 @@ extern void __gmpz_mul(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -750,7 +743,6 @@ extern void __gmpz_tdiv_q(__mpz_struct * /*[1]*/ z1,
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
index 2407d0bb8af..b393f8f389e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
@@ -156,16 +156,12 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
@@ -174,7 +170,6 @@ extern void __gmpz_sub(__mpz_struct * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z);
- allocates \nothing;
assigns \nothing; */
extern unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
index db802e14f78..ac837bb1d27 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
@@ -62,10 +62,7 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ terminates \false;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
index be8d36c24c9..ad0d8330455 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
@@ -475,16 +475,12 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
requires \valid(z2);
requires \valid(z3);
- allocates \nothing;
assigns *z1;
assigns *z1 \from *z2, *z3;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
index 8be306ba07c..50bb0f56db1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
@@ -72,10 +72,7 @@ extern void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z, long n);
extern void __gmpz_clear(__mpz_struct * /*[1]*/ x);
/*@ requires \valid(z1);
requires \valid(z2);
- allocates \nothing;
- assigns \nothing;
-
-*/
+ assigns \nothing; */
extern int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
/*@ terminates \false;
--
GitLab