Skip to content
Snippets Groups Projects
Commit d40f4feb authored by Julien Signoles's avatar Julien Signoles
Browse files

[tests] updated wrt libc changes

parent 28126fee
No related branches found
No related tags found
No related merge requests found
...@@ -12,7 +12,7 @@ ...@@ -12,7 +12,7 @@
__memory_size ∈ [--..--] __memory_size ∈ [--..--]
stdout ∈ {{ NULL ; &S___fc_stdout[0] }} stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
__fc_fopen[0..511] ∈ {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} ∈ S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
[--..--] [--..--]
[0].[bits 80 to 95] ∈ UNINITIALIZED [0].[bits 80 to 95] ∈ UNINITIALIZED
......
...@@ -12,7 +12,7 @@ ...@@ -12,7 +12,7 @@
__memory_size ∈ [--..--] __memory_size ∈ [--..--]
stdout ∈ {{ NULL ; &S___fc_stdout[0] }} stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
__fc_fopen[0..511] ∈ {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} ∈ S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
[--..--] [--..--]
[0].[bits 80 to 95] ∈ UNINITIALIZED [0].[bits 80 to 95] ∈ UNINITIALIZED
......
...@@ -74,7 +74,7 @@ predicate diffSize{L1, L2}(ℤ i) = ...@@ -74,7 +74,7 @@ predicate diffSize{L1, L2}(ℤ i) =
extern FILE *stdout; extern FILE *stdout;
FILE __fc_fopen[512]; 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;
assigns *__fc_stdout \from *(format+(..)); */ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...); extern int printf(char const *format , ...);
......
...@@ -74,7 +74,7 @@ predicate diffSize{L1, L2}(ℤ i) = ...@@ -74,7 +74,7 @@ predicate diffSize{L1, L2}(ℤ i) =
extern FILE *stdout; extern FILE *stdout;
FILE __fc_fopen[512]; 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;
assigns *__fc_stdout \from *(format+(..)); */ assigns *__fc_stdout \from *(format+(..)); */
extern int printf(char const *format , ...); extern int printf(char const *format , ...);
......
...@@ -103,16 +103,16 @@ predicate diffSize{L1, L2}(ℤ i) = ...@@ -103,16 +103,16 @@ predicate diffSize{L1, L2}(ℤ i) =
extern FILE *stdout; extern FILE *stdout;
FILE __fc_fopen[512]; 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]); /*@ ensures \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 512-1]);
assigns \result; 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); extern FILE *fopen(char const *filename, char const *mode);
/*@ ensures \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 512-1]); /*@ ensures \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 512-1]);
assigns \result; 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) FILE *__e_acsl_fopen(char const *filename, char const *mode)
{ {
......
...@@ -103,16 +103,16 @@ predicate diffSize{L1, L2}(ℤ i) = ...@@ -103,16 +103,16 @@ predicate diffSize{L1, L2}(ℤ i) =
extern FILE *stdout; extern FILE *stdout;
FILE __fc_fopen[512]; 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]); /*@ ensures \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 512-1]);
assigns \result; 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); extern FILE *fopen(char const *filename, char const *mode);
/*@ ensures \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 512-1]); /*@ ensures \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 512-1]);
assigns \result; 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) FILE *__e_acsl_fopen(char const *filename, char const *mode)
{ {
......
...@@ -19,7 +19,7 @@ FRAMAC_SHARE/libc/stdio.h:107:[e-acsl] warning: E-ACSL construct `logic function ...@@ -19,7 +19,7 @@ FRAMAC_SHARE/libc/stdio.h:107:[e-acsl] warning: E-ACSL construct `logic function
__memory_size ∈ [--..--] __memory_size ∈ [--..--]
stdout ∈ {{ NULL ; &S___fc_stdout[0] }} stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
__fc_fopen[0..511] ∈ {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 ∈ {0}
__e_acsl_literal_string_2 ∈ {0} __e_acsl_literal_string_2 ∈ {0}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈ S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
......
...@@ -19,7 +19,7 @@ FRAMAC_SHARE/libc/stdio.h:106:[e-acsl] warning: E-ACSL construct `logic function ...@@ -19,7 +19,7 @@ FRAMAC_SHARE/libc/stdio.h:106:[e-acsl] warning: E-ACSL construct `logic function
__memory_size ∈ [--..--] __memory_size ∈ [--..--]
stdout ∈ {{ NULL ; &S___fc_stdout[0] }} stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
__fc_fopen[0..511] ∈ {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 ∈ {0}
__e_acsl_literal_string_2 ∈ {0} __e_acsl_literal_string_2 ∈ {0}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈ S___fc_stdout[0]{.__fc_stdio_id; .__fc_position; .__fc_error; .__fc_eof} ∈
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment