From a807820899cecbef20617b66a14034c7d97a1c24 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 16 Jun 2014 18:40:05 +0200
Subject: [PATCH] update code and oracles according to Frama-C changes, in
particular interpretation of \valid in presence of const
---
src/plugins/e-acsl/TODO | 1 +
src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h | 36 +++++++++----------
.../tests/e-acsl-runtime/oracle/gen_arith2.c | 28 +++++++--------
.../tests/e-acsl-runtime/oracle/gen_array2.c | 4 +--
.../tests/e-acsl-runtime/oracle/gen_at2.c | 10 +++---
.../e-acsl-runtime/oracle/gen_bts13072.c | 12 +++----
.../e-acsl-runtime/oracle/gen_bts13242.c | 16 ++++-----
.../e-acsl-runtime/oracle/gen_bts13262.c | 12 +++----
.../e-acsl-runtime/oracle/gen_bts13902.c | 12 +++----
.../e-acsl-runtime/oracle/gen_bts13992.c | 10 +++---
.../e-acsl-runtime/oracle/gen_bts14782.c | 4 +--
.../tests/e-acsl-runtime/oracle/gen_cast2.c | 6 ++--
.../e-acsl-runtime/oracle/gen_comparison2.c | 6 ++--
.../oracle/gen_function_contract2.c | 8 ++---
.../tests/e-acsl-runtime/oracle/gen_ghost2.c | 4 +--
.../oracle/gen_integer_constant.c | 4 +--
.../oracle/gen_integer_constant2.c | 4 +--
.../e-acsl-runtime/oracle/gen_invariant2.c | 4 +--
.../e-acsl-runtime/oracle/gen_labeled_stmt2.c | 4 +--
.../tests/e-acsl-runtime/oracle/gen_lazy2.c | 10 +++---
.../oracle/gen_linear_search2.c | 12 +++----
.../oracle/gen_literal_string2.c | 4 +--
.../e-acsl-runtime/oracle/gen_longlong.c | 18 +++++-----
.../e-acsl-runtime/oracle/gen_longlong2.c | 16 ++++-----
.../tests/e-acsl-runtime/oracle/gen_loop2.c | 16 ++++-----
.../oracle/gen_nested_code_annot2.c | 4 +--
.../tests/e-acsl-runtime/oracle/gen_not2.c | 4 +--
.../oracle/gen_other_constants2.c | 4 +--
.../tests/e-acsl-runtime/oracle/gen_ptr2.c | 22 ++++++------
.../e-acsl-runtime/oracle/gen_quantif2.c | 22 ++++++------
.../tests/e-acsl-runtime/oracle/gen_result2.c | 10 +++---
.../tests/e-acsl-runtime/oracle/gen_sizeof2.c | 4 +--
.../oracle/gen_stmt_contract2.c | 8 ++---
.../e-acsl-runtime/oracle/gen_typedef2.c | 4 +--
.../e-acsl-runtime/oracle/gen_valid_alias2.c | 4 +--
.../tests/e-acsl-runtime/oracle/gen_vector2.c | 4 +--
src/plugins/e-acsl/typing.ml | 5 ++-
37 files changed, 178 insertions(+), 178 deletions(-)
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index d6ebf7ed7d8..efbbd3c6aa1 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -80,6 +80,7 @@
(voir aussi result.i et ./at_stmt_contract.i)
- interprétation des tableaux logiques
[Dillon] Windows
+- \valid(p) is not true if p is a const pointer
[to be check]: no call to full_init or initialize for the assigned result of a
function call
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h
index 7ef14b60c2a..7df9fcdec54 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp.h
@@ -43,7 +43,7 @@
extern void __gmpz_init(mpz_t z)
__attribute__((FC_BUILTIN));
-/*@ requires \valid(z_orig);
+/*@ requires \valid_read(z_orig);
@ requires ! \initialized(z);
@ allocates z;
@ ensures \valid(z);
@@ -91,7 +91,7 @@ extern void __gmpz_import (mpz_t z, size_t, int, size_t, int, size_t, const void
/* Assignments */
/***************/
-/*@ requires \valid(z_orig);
+/*@ requires \valid_read(z_orig);
@ requires \valid(z);
// @ ensures z->n == z_orig->n;
@ assigns *z \from *z_orig; */
@@ -124,8 +124,8 @@ extern void __gmpz_clear(mpz_t x)
/* Logical operator */
/********************/
-/*@ requires \valid(z1);
- @ requires \valid(z2);
+/*@ requires \valid_read(z1);
+ @ requires \valid_read(z2);
@ assigns \result \from *z1, *z2; */
extern int __gmpz_cmp(const mpz_t z1, const mpz_t z2)
__attribute__((FC_BUILTIN));
@@ -135,42 +135,42 @@ extern int __gmpz_cmp(const mpz_t z1, const mpz_t z2)
/************************/
/*@ requires \valid(z1);
- @ requires \valid(z2);
+ @ requires \valid_read(z2);
@ assigns *z1 \from *z2; */
extern void __gmpz_neg(mpz_t z1, const mpz_t z2)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z1);
- @ requires \valid(z2);
- @ requires \valid(z3);
+ @ requires \valid_read(z2);
+ @ requires \valid_read(z3);
@ assigns *z1 \from *z2, *z3; */
extern void __gmpz_add(mpz_t z1, const mpz_t z2, const mpz_t z3)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z1);
- @ requires \valid(z2);
- @ requires \valid(z3);
+ @ requires \valid_read(z2);
+ @ requires \valid_read(z3);
@ assigns *z1 \from *z2, *z3; */
extern void __gmpz_sub(mpz_t z1, const mpz_t z2, const mpz_t z3)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z1);
- @ requires \valid(z2);
- @ requires \valid(z3);
+ @ requires \valid_read(z2);
+ @ requires \valid_read(z3);
@ assigns *z1 \from *z2, *z3; */
extern void __gmpz_mul(mpz_t z1, const mpz_t z2, const mpz_t z3)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z1);
- @ requires \valid(z2);
- @ requires \valid(z3);
+ @ requires \valid_read(z2);
+ @ requires \valid_read(z3);
@ assigns *z1 \from *z2, *z3; */
extern void __gmpz_tdiv_q(mpz_t z1, const mpz_t z2, const mpz_t z3)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z1);
- @ requires \valid(z2);
- @ requires \valid(z3);
+ @ requires \valid_read(z2);
+ @ requires \valid_read(z3);
@ assigns *z1 \from *z2, *z3; */
extern void __gmpz_tdiv_r(mpz_t z1, const mpz_t z2, const mpz_t z3)
__attribute__((FC_BUILTIN));
@@ -180,7 +180,7 @@ extern void __gmpz_tdiv_r(mpz_t z1, const mpz_t z2, const mpz_t z3)
/*********************/
/*@ requires \valid(z1);
- @ requires \valid(z2);
+ @ requires \valid_read(z2);
@ assigns *z1 \from *z2;
@ assigns \result \from *z1,*z2; */
extern int __gmpz_com(mpz_t z1, const mpz_t z2)
@@ -190,12 +190,12 @@ extern int __gmpz_com(mpz_t z1, const mpz_t z2)
/* Coercions to C types */
/************************/
-/*@ requires \valid(z);
+/*@ requires \valid_read(z);
@ assigns \result \from *z; */
extern long __gmpz_get_si(const mpz_t z)
__attribute__((FC_BUILTIN));
-/*@ requires \valid(z);
+/*@ requires \valid_read(z);
@ assigns \result \from *z; */
extern unsigned long __gmpz_get_ui(const mpz_t z)
__attribute__((FC_BUILTIN));
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 82008631711..f51c537f6c4 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
@@ -67,8 +67,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
@@ -76,7 +76,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
+ requires \valid_read(z2);
assigns *z1;
assigns *z1 \from *z2;
*/
@@ -84,8 +84,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_neg(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -94,8 +94,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -104,8 +104,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_sub(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -114,8 +114,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -124,8 +124,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -134,7 +134,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_r(__mpz_struct * /*[1]*
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
- requires \valid(z2);
+ requires \valid_read(z2);
assigns *z1, \result;
assigns *z1 \from *z2;
assigns \result \from *z1, *z2;
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 bf258eef4aa..f20a0e8f72b 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
@@ -47,8 +47,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
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 c69173bbeae..679a07f8431 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
@@ -40,7 +40,7 @@ axiomatic
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
-/*@ requires \valid(z_orig);
+/*@ requires \valid_read(z_orig);
requires ¬\initialized(z);
ensures \valid(\old(z));
assigns *z;
@@ -65,8 +65,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
@@ -74,8 +74,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
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 3b4af93775d..444d463a0d2 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
@@ -40,7 +40,7 @@ axiomatic
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
-/*@ requires \valid(z_orig);
+/*@ requires \valid_read(z_orig);
requires ¬\initialized(z);
ensures \valid(\old(z));
assigns *z;
@@ -65,8 +65,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
@@ -74,8 +74,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -83,7 +83,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
-/*@ requires \valid(z);
+/*@ requires \valid_read(z);
assigns \result;
assigns \result \from *z; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
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 89edfb78504..a448bc0be51 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
@@ -50,7 +50,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
-/*@ requires \valid(z_orig);
+/*@ requires \valid_read(z_orig);
requires \valid(z);
assigns *z;
assigns *z \from *z_orig;
@@ -63,8 +63,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_set(__mpz_struct * /*[1]*/ z
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
@@ -72,8 +72,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -82,8 +82,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -91,7 +91,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_sub(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
-/*@ requires \valid(z);
+/*@ requires \valid_read(z);
assigns \result;
assigns \result \from *z; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c
index 8c3ebbe9970..72b0e104ce9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c
@@ -56,8 +56,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
@@ -65,8 +65,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -75,8 +75,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
index b4ea1d9be57..a08c2a6692f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
@@ -60,7 +60,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_ui(__mpz_struct * /
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
-/*@ requires \valid(z_orig);
+/*@ requires \valid_read(z_orig);
requires \valid(z);
assigns *z;
assigns *z \from *z_orig;
@@ -73,8 +73,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_set(__mpz_struct * /*[1]*/ z
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
@@ -82,8 +82,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -91,7 +91,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
-/*@ requires \valid(z);
+/*@ requires \valid_read(z);
assigns \result;
assigns \result \from *z; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
index 9b75f0ffe84..d265181dd9d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
@@ -116,8 +116,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
@@ -125,8 +125,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -134,7 +134,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
-/*@ requires \valid(z);
+/*@ requires \valid_read(z);
assigns \result;
assigns \result \from *z; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
index 2f525371491..dfe69e1c88d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
@@ -47,8 +47,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
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 291d9b6fdc6..98f8ec27baf 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
@@ -69,15 +69,15 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
__mpz_struct const * /*[1]*/ z2);
-/*@ requires \valid(z);
+/*@ requires \valid_read(z);
assigns \result;
assigns \result \from *z; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
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 57592073380..149fb7ae8e9 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
@@ -55,8 +55,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
@@ -64,7 +64,7 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
+ requires \valid_read(z2);
assigns *z1;
assigns *z1 \from *z2;
*/
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 18ed30062a9..4fd16fafea5 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
@@ -55,8 +55,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
@@ -64,8 +64,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
index d117e37824f..edc38d0e77d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
@@ -47,8 +47,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
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 596b7b58c76..8ce91c0dbef 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
@@ -49,8 +49,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
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 24f06299028..44899d75a9d 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
@@ -59,8 +59,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
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 13d42707706..06994dd7f2e 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
@@ -47,8 +47,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
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 36cffb7e59c..7816d4df0c4 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
@@ -47,8 +47,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
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 7482fd27fd7..34ae8c2cefe 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
@@ -40,7 +40,7 @@ axiomatic
*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/ z);
-/*@ requires \valid(z_orig);
+/*@ requires \valid_read(z_orig);
requires ¬\initialized(z);
ensures \valid(\old(z));
assigns *z;
@@ -65,8 +65,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
@@ -74,8 +74,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
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 42e1ad14740..f844748eb6c 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
@@ -50,7 +50,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
-/*@ requires \valid(z_orig);
+/*@ requires \valid_read(z_orig);
requires \valid(z);
assigns *z;
assigns *z \from *z_orig;
@@ -63,8 +63,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_set(__mpz_struct * /*[1]*/ z
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
@@ -72,8 +72,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -81,7 +81,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
-/*@ requires \valid(z);
+/*@ requires \valid_read(z);
assigns \result;
assigns \result \from *z; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
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 9f6168dcc9a..f1c4480d60e 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
@@ -47,8 +47,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
index c03705c4cf4..08df9312e66 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong.c
@@ -68,8 +68,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_import(__mpz_struct * /*[1]*
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
@@ -77,8 +77,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -87,8 +87,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -97,8 +97,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -106,7 +106,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_r(__mpz_struct * /*[1]*
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
-/*@ requires \valid(z);
+/*@ requires \valid_read(z);
assigns \result;
assigns \result \from *z; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
index 1adfb29a181..c83d640e113 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_longlong2.c
@@ -68,8 +68,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_import(__mpz_struct * /*[1]*
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
@@ -77,8 +77,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -87,8 +87,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -97,8 +97,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c
index cad4c41a492..82cb91e3600 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_loop2.c
@@ -50,7 +50,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
-/*@ requires \valid(z_orig);
+/*@ requires \valid_read(z_orig);
requires \valid(z);
assigns *z;
assigns *z \from *z_orig;
@@ -63,8 +63,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_set(__mpz_struct * /*[1]*/ z
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
@@ -72,8 +72,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -82,8 +82,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -91,7 +91,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
-/*@ requires \valid(z);
+/*@ requires \valid_read(z);
assigns \result;
assigns \result \from *z; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
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 e44f41c1996..4b079ab0cc1 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
@@ -47,8 +47,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
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 9a26741265b..a6009c1c2c4 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
@@ -47,8 +47,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
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 3ad84cb6966..e25ff06fa59 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
@@ -51,8 +51,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
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 44d9f3c173f..59051aa42d6 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
@@ -55,8 +55,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
@@ -64,8 +64,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -74,8 +74,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -84,8 +84,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_sub(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -94,8 +94,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -103,7 +103,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
-/*@ requires \valid(z);
+/*@ requires \valid_read(z);
assigns \result;
assigns \result \from *z; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
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 ee2348c85ab..648bbf06274 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
@@ -50,7 +50,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init(__mpz_struct * /*[1]*/
extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /*[1]*/ z,
long n);
-/*@ requires \valid(z_orig);
+/*@ requires \valid_read(z_orig);
requires \valid(z);
assigns *z;
assigns *z \from *z_orig;
@@ -63,8 +63,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_set(__mpz_struct * /*[1]*/ z
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
@@ -72,8 +72,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -82,8 +82,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_add(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -92,8 +92,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_mul(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -102,8 +102,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_tdiv_q(__mpz_struct * /*[1]*
__mpz_struct const * /*[1]*/ z3);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
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 6ec0ed2c7c3..f1a59380544 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
@@ -55,8 +55,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
@@ -64,8 +64,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
@@ -73,7 +73,7 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_sub(__mpz_struct * /*[1]*/ z
__mpz_struct const * /*[1]*/ z2,
__mpz_struct const * /*[1]*/ z3);
-/*@ requires \valid(z);
+/*@ requires \valid_read(z);
assigns \result;
assigns \result \from *z; */
extern __attribute__((__FC_BUILTIN__)) unsigned long __gmpz_get_ui(__mpz_struct const * /*[1]*/ z);
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 9eb072c28e9..116f237427c 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
@@ -47,8 +47,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
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 b52f58679e5..a853808cb26 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
@@ -55,8 +55,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
@@ -64,8 +64,8 @@ extern __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1
__mpz_struct const * /*[1]*/ z2);
/*@ requires \valid(z1);
- requires \valid(z2);
- requires \valid(z3);
+ requires \valid_read(z2);
+ requires \valid_read(z3);
assigns *z1;
assigns *z1 \from *z2, *z3;
*/
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 624b42cfe88..e245eae9e7c 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
@@ -58,8 +58,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
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 13210971418..1923735970b 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
@@ -92,8 +92,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
index e7645e29a74..a69e887eaab 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
@@ -92,8 +92,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
assigns *x \from *x; */
extern __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
-/*@ requires \valid(z1);
- requires \valid(z2);
+/*@ requires \valid_read(z1);
+ requires \valid_read(z2);
assigns \result;
assigns \result \from *z1, *z2;
*/
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 615d30efd7e..11fc2f5e576 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -214,9 +214,8 @@ let type_constant ty = function
if Cil.fitsInInt ILongLong n || Cil.fitsInInt IULongLong n then Interv(n, n)
else Z
| LChr c ->
- (match Cil.charConstToInt c with
- | CInt64(n, _, _) -> Interv(n, n)
- | _ -> assert false)
+ let n = Cil.charConstToInt c in
+ Interv(n, n)
| LStr _ | LWStr _ | LReal _ | LEnum _ -> No_integral ty
let size_of ty =
--
GitLab