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 a36a786f4a782f06e8c54a75812777f4cf8c3050..99d1861463a6dcc225e00eb28b7435708ae8e927 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 a36a786f4a782f06e8c54a75812777f4cf8c3050..99d1861463a6dcc225e00eb28b7435708ae8e927 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 824fd59670dca868d0f94224849955f1df822170..97bd608c9bf3e8d9404530bb6027dcb372b6a2e0 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 824fd59670dca868d0f94224849955f1df822170..97bd608c9bf3e8d9404530bb6027dcb372b6a2e0 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 e76fadd5536b507742da4dc861e8e59275008081..3ff340ccd402065db0d57fabdb17dbf0ab1d484a 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 e76fadd5536b507742da4dc861e8e59275008081..3ff340ccd402065db0d57fabdb17dbf0ab1d484a 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 5dac462dde66e0b01d200112e639d250b9c89968..fb49c3698c32ef96cf5a665efb857c996306c35f 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 77c34888293ad059c26533a40ff9b1d3b6ea51e7..c0cb27bc5fd0cba905f3854ffad52e06fb56390d 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} ∈