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 73d3ac2b865191eaf0bab61e438854128a8e74b8..877d15f251ecc37cde876cc196034793d12306f1 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..511] ∈ {0} + __fc_fopen[0..1] ∈ {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 73d3ac2b865191eaf0bab61e438854128a8e74b8..877d15f251ecc37cde876cc196034793d12306f1 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..511] ∈ {0} + __fc_fopen[0..1] ∈ {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 7cbe7d91981b3b8f32b4307dd9e44fdbcd322c09..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 @@ -82,7 +82,7 @@ predicate diffSize{L1, L2}(ℤ i) = */ extern FILE *__fc_stdout; -FILE __fc_fopen[512]; +FILE __fc_fopen[2]; 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 7cbe7d91981b3b8f32b4307dd9e44fdbcd322c09..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 @@ -82,7 +82,7 @@ predicate diffSize{L1, L2}(ℤ i) = */ extern FILE *__fc_stdout; -FILE __fc_fopen[512]; +FILE __fc_fopen[2]; FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen); /*@ assigns *__fc_stdout; assigns *__fc_stdout \from *(format+(..)); */