From 31f85f215347323da17a7a313df17de4675eadbc Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 18 Feb 2014 10:48:16 +0100
Subject: [PATCH] [tests] update oracles according to kernel changes

---
 .../e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle     | 2 +-
 .../e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle       | 2 +-
 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 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
index 877d15f251e..73d3ac2b865 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
@@ -18,7 +18,7 @@
   __e_acsl_internal_heap ∈ [--..--]
   __memory_size ∈ [--..--]
   __fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
-  __fc_fopen[0..1] ∈ {0}
+  __fc_fopen[0..511] ∈ {0}
   _p__fc_fopen ∈ {{ &__fc_fopen }}
   S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
                [--..--]
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
index 877d15f251e..73d3ac2b865 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
@@ -18,7 +18,7 @@
   __e_acsl_internal_heap ∈ [--..--]
   __memory_size ∈ [--..--]
   __fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
-  __fc_fopen[0..1] ∈ {0}
+  __fc_fopen[0..511] ∈ {0}
   _p__fc_fopen ∈ {{ &__fc_fopen }}
   S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
                [--..--]
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 9866acdacf7..7cbe7d91981 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
@@ -82,7 +82,7 @@ predicate diffSize{L1, L2}(ℤ i) =
  */
 extern FILE *__fc_stdout;
 
-FILE __fc_fopen[2];
+FILE __fc_fopen[512];
 FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
 /*@ assigns *__fc_stdout;
     assigns *__fc_stdout \from *(format+(..)); */
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 9866acdacf7..7cbe7d91981 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
@@ -82,7 +82,7 @@ predicate diffSize{L1, L2}(ℤ i) =
  */
 extern FILE *__fc_stdout;
 
-FILE __fc_fopen[2];
+FILE __fc_fopen[512];
 FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
 /*@ assigns *__fc_stdout;
     assigns *__fc_stdout \from *(format+(..)); */
-- 
GitLab