From d40f4febe66e11e6e7792b7dc45951386f03509c Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 26 Aug 2015 09:57:20 +0200
Subject: [PATCH] [tests] updated wrt libc changes
---
src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle | 2 +-
src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle | 2 +-
src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c | 2 +-
src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c | 2 +-
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c | 6 +++---
.../e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c | 6 +++---
.../e-acsl/tests/e-acsl-runtime/oracle/stdout.0.res.oracle | 2 +-
.../e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle | 2 +-
8 files changed, 12 insertions(+), 12 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle
index a36a786f4a7..99d1861463a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle
@@ -12,7 +12,7 @@
__memory_size ∈ [--..--]
stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
__fc_fopen[0..511] ∈ {0}
- _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
+ __p_fc_fopen ∈ {{ &__fc_fopen[0] }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
[--..--]
[0].[bits 80 to 95] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle
index a36a786f4a7..99d1861463a 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle
@@ -12,7 +12,7 @@
__memory_size ∈ [--..--]
stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
__fc_fopen[0..511] ∈ {0}
- _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
+ __p_fc_fopen ∈ {{ &__fc_fopen[0] }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
[--..--]
[0].[bits 80 to 95] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
index 824fd59670d..97bd608c9bf 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
@@ -74,7 +74,7 @@ predicate diffSize{L1, L2}(ℤ i) =
extern FILE *stdout;
FILE __fc_fopen[512];
-FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
+FILE * const __p_fc_fopen = __fc_fopen;
/*@ assigns *__fc_stdout;
assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c
index 824fd59670d..97bd608c9bf 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c
@@ -74,7 +74,7 @@ predicate diffSize{L1, L2}(ℤ i) =
extern FILE *stdout;
FILE __fc_fopen[512];
-FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
+FILE * const __p_fc_fopen = __fc_fopen;
/*@ assigns *__fc_stdout;
assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
index e76fadd5536..3ff340ccd40 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
@@ -103,16 +103,16 @@ predicate diffSize{L1, L2}(ℤ i) =
extern FILE *stdout;
FILE __fc_fopen[512];
-FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
+FILE * const __p_fc_fopen = __fc_fopen;
/*@ ensures \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 512-1]);
assigns \result;
- assigns \result \from *(filename+(..)), *(mode+(..)), _p__fc_fopen;
+ assigns \result \from *(filename+(..)), *(mode+(..)), __p_fc_fopen;
*/
extern FILE *fopen(char const *filename, char const *mode);
/*@ ensures \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 512-1]);
assigns \result;
- assigns \result \from *(filename+(..)), *(mode+(..)), _p__fc_fopen;
+ assigns \result \from *(filename+(..)), *(mode+(..)), __p_fc_fopen;
*/
FILE *__e_acsl_fopen(char const *filename, char const *mode)
{
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
index e76fadd5536..3ff340ccd40 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
@@ -103,16 +103,16 @@ predicate diffSize{L1, L2}(ℤ i) =
extern FILE *stdout;
FILE __fc_fopen[512];
-FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
+FILE * const __p_fc_fopen = __fc_fopen;
/*@ ensures \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 512-1]);
assigns \result;
- assigns \result \from *(filename+(..)), *(mode+(..)), _p__fc_fopen;
+ assigns \result \from *(filename+(..)), *(mode+(..)), __p_fc_fopen;
*/
extern FILE *fopen(char const *filename, char const *mode);
/*@ ensures \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 512-1]);
assigns \result;
- assigns \result \from *(filename+(..)), *(mode+(..)), _p__fc_fopen;
+ assigns \result \from *(filename+(..)), *(mode+(..)), __p_fc_fopen;
*/
FILE *__e_acsl_fopen(char const *filename, char const *mode)
{
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.0.res.oracle
index 5dac462dde6..fb49c3698c3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.0.res.oracle
@@ -19,7 +19,7 @@ FRAMAC_SHARE/libc/stdio.h:107:[e-acsl] warning: E-ACSL construct `logic function
__memory_size ∈ [--..--]
stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
__fc_fopen[0..511] ∈ {0}
- _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
+ __p_fc_fopen ∈ {{ &__fc_fopen[0] }}
__e_acsl_literal_string ∈ {0}
__e_acsl_literal_string_2 ∈ {0}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
index 77c34888293..c0cb27bc5fd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle
@@ -19,7 +19,7 @@ FRAMAC_SHARE/libc/stdio.h:106:[e-acsl] warning: E-ACSL construct `logic function
__memory_size ∈ [--..--]
stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
__fc_fopen[0..511] ∈ {0}
- _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
+ __p_fc_fopen ∈ {{ &__fc_fopen[0] }}
__e_acsl_literal_string ∈ {0}
__e_acsl_literal_string_2 ∈ {0}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
--
GitLab