From c7112bd6cbf72cec0e577b68740ab0792cd2226d Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 5 Dec 2013 09:27:27 +0100
Subject: [PATCH] [E-ACSL] update according to printer's changes
---
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_arith2.c | 4 ++--
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_cast2.c | 4 ++--
.../e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c | 4 ++--
.../tests/e-acsl-runtime/oracle/gen_integer_constant2.c | 4 ++--
6 files changed, 10 insertions(+), 10 deletions(-)
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 f058a33f3be..489a47330d4 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
@@ -54,8 +54,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
ensures \valid(\old(z));
ensures \initialized(\old(z));
assigns *z, \result;
- assigns *z \from *(str+(0 .. )), base;
- assigns \result \from *(str+(0 .. )), base;
+ assigns *z \from *(str+(0 ..)), base;
+ assigns \result \from *(str+(0 ..)), base;
allocates \old(z);
*/
extern __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z,
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
index 9871fef7221..9866acdacf7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
@@ -85,7 +85,7 @@ extern FILE *__fc_stdout;
FILE __fc_fopen[2];
FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+( .. )); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
int main(void)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
index 9871fef7221..9866acdacf7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
@@ -85,7 +85,7 @@ extern FILE *__fc_stdout;
FILE __fc_fopen[2];
FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
/*@ assigns *__fc_stdout;
- assigns *__fc_stdout \from *(format+( .. )); */
+ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
int main(void)
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 4f53a807a14..4bf7eb61cab 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
@@ -56,8 +56,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
ensures \valid(\old(z));
ensures \initialized(\old(z));
assigns *z, \result;
- assigns *z \from *(str+(0 .. )), base;
- assigns \result \from *(str+(0 .. )), base;
+ assigns *z \from *(str+(0 ..)), base;
+ assigns \result \from *(str+(0 ..)), base;
allocates \old(z);
*/
extern __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z,
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 2ae829bc256..83265194159 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
@@ -36,8 +36,8 @@ axiomatic
ensures \valid(\old(z));
ensures \initialized(\old(z));
assigns *z, \result;
- assigns *z \from *(str+(0 .. )), base;
- assigns \result \from *(str+(0 .. )), base;
+ assigns *z \from *(str+(0 ..)), base;
+ assigns \result \from *(str+(0 ..)), base;
allocates \old(z);
*/
extern __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z,
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 2896cef70f3..06d19150607 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
@@ -46,8 +46,8 @@ extern __attribute__((__FC_BUILTIN__)) void __gmpz_init_set_si(__mpz_struct * /
ensures \valid(\old(z));
ensures \initialized(\old(z));
assigns *z, \result;
- assigns *z \from *(str+(0 .. )), base;
- assigns \result \from *(str+(0 .. )), base;
+ assigns *z \from *(str+(0 ..)), base;
+ assigns \result \from *(str+(0 ..)), base;
allocates \old(z);
*/
extern __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z,
--
GitLab