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 f058a33f3becaaf25bbbf7f86106851de4cd41f9..489a47330d4ca861b06a431f0ca326f8e12910dd 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 9871fef722126a319ac1fe45597581c40b2cc5e6..9866acdacf7365137e57b4ad742efa8eb9517266 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 9871fef722126a319ac1fe45597581c40b2cc5e6..9866acdacf7365137e57b4ad742efa8eb9517266 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 4f53a807a146cec90c1850efbfb391c52103185f..4bf7eb61caba72a833cf94fe6cc373922d229a49 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 2ae829bc256e4244068b26453a07fa26d7510f11..832651941592a06b88d4e09966f3ff82dee4b47e 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 2896cef70f3e2e86f10a47122c54324143e837dd..06d19150607000d59921da84b59fa0cd1626a22c 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,