diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index d6ebf7ed7d8e1ec7df7e7928941672078e390c01..efbbd3c6aa1d8fcdb25a24a84a390ae9c89960de 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 7ef14b60c2addc67b82b06188045a0e045a23b4b..7df9fcdec5428123ca49b940e7d6ea0d74262515 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 820086317114462508624a70a06064a4945a2433..f51c537f6c4ced15af767b68e1b77f6e4e98f724 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 bf258eef4aa8b408b9f9f6614ed08ae1140ea16b..f20a0e8f72bfe69a262e8296a3d83aa8a8e9b9b4 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 c69173bbeae7168a53b9f1c88f132b95e8bda473..679a07f8431622c1124e50b9c3d478be7b7ad873 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 3b4af93775d4e858061c87f93a503a03dc7ff2ab..444d463a0d231e1da2b7fd9b979ff96dc8ea30be 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 89edfb78504c7af7a6753a678d3f93c8c27952e0..a448bc0be5105246308c6a50a07a4cc037843706 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 8c3ebbe99700f48e7476ffde0cfdbf6f473e803d..72b0e104ce997eff5875dfc742d5cc92c05b46a8 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 b4ea1d9be57be3006931d9da16780fea4f06541e..a08c2a6692fd3823e7bfd3d950ad08871ed83095 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 9b75f0ffe84564c135e12bad95eabd3e811ef524..d265181dd9d1f38d5cd9adb1f7c1e93cd2627475 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 2f5253714910fda4ff031c1058dcd8c4d0e1a4db..dfe69e1c88d7f3fc2fa5d1dfcbbb08e5ea8b74f1 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 291d9b6fdc6db0e2bfeb1adcf8df77a4bf982024..98f8ec27baf9ef9d98d37eb48f4021b96a03f7a1 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 5759207338083c55c108456a88bb4448b11e0aad..149fb7ae8e94c66249fe41c431f1e9f48937505d 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 18ed30062a9047a7c040b1997af25ec767a75a13..4fd16fafea57599487930b5481f58c816cfa3ca3 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 d117e37824f81a1787743d3fcb9d9d4986aefbf7..edc38d0e77d6df3015fa1cbff6b8a3b4f37456ad 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 596b7b58c76cbd7859636f3ab82d3b348314657d..8ce91c0dbef1a5537c983bbde77c4045899e21b6 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 24f06299028b9211179101a8f3bf4947f93cb32b..44899d75a9d3381987b7bbf7ed7ff310f81b19d2 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 13d42707706e11ac2d102ed1e9e75f5b8e469227..06994dd7f2eb9302c6256c9bfe70d5269c6ba7ad 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 36cffb7e59c81717cca1db5d380dd1940e68f000..7816d4df0c47d2b5cd26a8421c663aa229e1c76f 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 7482fd27fd74c812d4f7c825fbfa40f08912ca22..34ae8c2cefe070f0e54e8f1a76c3e40decf421da 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 42e1ad147407904ec6b650760a3556f148b9db2b..f844748eb6cf8fed0b1cc63b89caadbe57ac130a 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 9f6168dcc9a5e92b35164120addc3adeb4bb02f7..f1c4480d60e1fdd1c33915107f6d94a0309d44b5 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 c03705c4cf4c88fecb78112efa5f35308c6aa614..08df9312e669efd4b0072ca262abf88f178a145b 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 1adfb29a18108f461487273c013749d66cffb736..c83d640e1134723c61dd9642964c87a55809bae2 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 cad4c41a492a588be98576c86e287205451fb83c..82cb91e3600e8300a781886087a7dc65a060109e 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 e44f41c1996a57d9e12e6f7c86becdec64587faf..4b079ab0cc12b7049106491136d9a94d97b68a18 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 9a26741265bbe2a4ff8713917c7430f6e12db4f1..a6009c1c2c4d32b9ade259755dbe3411c443b07e 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 3ad84cb6966ff8e0be24c1e57320cdc16f4a624d..e25ff06fa597189b8af9defc20c9241ecc0a4285 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 44d9f3c173f4765c975913345a70f92504e91329..59051aa42d601086b39fa22ceec81b3b0dd30660 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 ee2348c85abb33d831fea492d0ada74b81bf9d28..648bbf062743f3e7ed3fea7184dfabc659f0d68f 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 6ec0ed2c7c3b2513bc15bd5d47694adcc840bbba..f1a5938054474a0a2f8864f191fed31f1f14c06c 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 9eb072c28e9e88766e62ba30e11221227be11cee..116f237427ca61ee7e4995da5a47d60a51ce2c3c 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 b52f58679e5d7326aaba30891ae6cfb041a92c21..a853808cb266edb6b1780a0527869d9db77cde59 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 624b42cfe889dfe466c516ebfd8043e14d2f0843..e245eae9e7c82a6e4de74f4d7c8f2ff62951ad0b 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 1321097141898e1b21435751b8d4bca0d446aad1..1923735970b546cb5336f86a50e692f79e73437a 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 e7645e29a7488e9c4f185cf8088f6504b80c3938..a69e887eaab1594e00a236e95f1607aa6bdfe2b7 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 615d30efd7e59adee38ee97038f998c67bdcc0c4..11fc2f5e576dd0e72b99d2e4d48d00e612722efa 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 =