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

[tests] update oracles according to kernel changes

parent 9d6ecce5
No related branches found
No related tags found
No related merge requests found
...@@ -18,7 +18,7 @@ ...@@ -18,7 +18,7 @@
__e_acsl_internal_heap ∈ [--..--] __e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--] __memory_size ∈ [--..--]
__fc_stdout ∈ {{ NULL ; &S___fc_stdout }} __fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
__fc_fopen[0..1] ∈ {0} __fc_fopen[0..511] ∈ {0}
_p__fc_fopen ∈ {{ &__fc_fopen }} _p__fc_fopen ∈ {{ &__fc_fopen }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈ S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
[--..--] [--..--]
......
...@@ -18,7 +18,7 @@ ...@@ -18,7 +18,7 @@
__e_acsl_internal_heap ∈ [--..--] __e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--] __memory_size ∈ [--..--]
__fc_stdout ∈ {{ NULL ; &S___fc_stdout }} __fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
__fc_fopen[0..1] ∈ {0} __fc_fopen[0..511] ∈ {0}
_p__fc_fopen ∈ {{ &__fc_fopen }} _p__fc_fopen ∈ {{ &__fc_fopen }}
S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈ S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
[--..--] [--..--]
......
...@@ -82,7 +82,7 @@ predicate diffSize{L1, L2}(ℤ i) = ...@@ -82,7 +82,7 @@ predicate diffSize{L1, L2}(ℤ i) =
*/ */
extern FILE *__fc_stdout; extern FILE *__fc_stdout;
FILE __fc_fopen[2]; FILE __fc_fopen[512];
FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen); FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
/*@ assigns *__fc_stdout; /*@ assigns *__fc_stdout;
assigns *__fc_stdout \from *(format+(..)); */ assigns *__fc_stdout \from *(format+(..)); */
......
...@@ -82,7 +82,7 @@ predicate diffSize{L1, L2}(ℤ i) = ...@@ -82,7 +82,7 @@ predicate diffSize{L1, L2}(ℤ i) =
*/ */
extern FILE *__fc_stdout; extern FILE *__fc_stdout;
FILE __fc_fopen[2]; FILE __fc_fopen[512];
FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen); FILE const *_p__fc_fopen = (FILE const *)(__fc_fopen);
/*@ assigns *__fc_stdout; /*@ assigns *__fc_stdout;
assigns *__fc_stdout \from *(format+(..)); */ assigns *__fc_stdout \from *(format+(..)); */
......
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