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

update oracles

parent cc4157bd
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
+ 10
− 8
View file @ 6e110768
...@@ -17,25 +17,27 @@ ...@@ -17,25 +17,27 @@
__e_acsl_init ∈ [--..--] __e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--] __e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--] __memory_size ∈ [--..--]
__fc_stdout ∈ {{ NULL ; &S___fc_stdout }} __fc_stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
__fc_fopen[0..511] ∈ {0} __fc_fopen[0..511] ∈ {0}
_p__fc_fopen ∈ {{ &__fc_fopen }} _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
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} ∈
[--..--] [--..--]
[0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }} [0].__fc_inode ∈
{{ NULL ; &S___fc_inode_0_S___fc_stdout[0] }}
[1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈ [1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
[--..--] [--..--]
[1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }} [1].__fc_inode ∈
{{ NULL ; &S___fc_inode_1_S___fc_stdout[0] }}
S___fc_inode_0_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks} ∈ S___fc_inode_0_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks} ∈
[--..--] [--..--]
[0].__fc_real_data ∈ [0].__fc_real_data ∈
{{ NULL ; {{ NULL ;
&S___fc_real_data_0_S___fc_inode_0_S___fc_stdout }} &S___fc_real_data_0_S___fc_inode_0_S___fc_stdout[0] }}
{[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks}} ∈ {[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks}} ∈
[--..--] [--..--]
[1].__fc_real_data ∈ [1].__fc_real_data ∈
{{ NULL ; {{ NULL ;
&S___fc_real_data_1_S___fc_inode_0_S___fc_stdout }} &S___fc_real_data_1_S___fc_inode_0_S___fc_stdout[0] }}
[1].__fc_real_data_max_size ∈ [--..--] [1].__fc_real_data_max_size ∈ [--..--]
S___fc_real_data_0_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--] S___fc_real_data_0_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_real_data_1_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--] S___fc_real_data_1_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
...@@ -43,12 +45,12 @@ ...@@ -43,12 +45,12 @@
[--..--] [--..--]
[0].__fc_real_data ∈ [0].__fc_real_data ∈
{{ NULL ; {{ NULL ;
&S___fc_real_data_0_S___fc_inode_1_S___fc_stdout }} &S___fc_real_data_0_S___fc_inode_1_S___fc_stdout[0] }}
{[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks}} ∈ {[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks}} ∈
[--..--] [--..--]
[1].__fc_real_data ∈ [1].__fc_real_data ∈
{{ NULL ; {{ NULL ;
&S___fc_real_data_1_S___fc_inode_1_S___fc_stdout }} &S___fc_real_data_1_S___fc_inode_1_S___fc_stdout[0] }}
[1].__fc_real_data_max_size ∈ [--..--] [1].__fc_real_data_max_size ∈ [--..--]
S___fc_real_data_0_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--] S___fc_real_data_0_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
S___fc_real_data_1_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--] S___fc_real_data_1_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
......
src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
+ 10
− 8
View file @ 6e110768
...@@ -17,25 +17,27 @@ ...@@ -17,25 +17,27 @@
__e_acsl_init ∈ [--..--] __e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--] __e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--] __memory_size ∈ [--..--]
__fc_stdout ∈ {{ NULL ; &S___fc_stdout }} __fc_stdout ∈ {{ NULL ; &S___fc_stdout[0] }}
__fc_fopen[0..511] ∈ {0} __fc_fopen[0..511] ∈ {0}
_p__fc_fopen ∈ {{ &__fc_fopen }} _p__fc_fopen ∈ {{ &__fc_fopen[0] }}
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} ∈
[--..--] [--..--]
[0].__fc_inode ∈ {{ NULL ; &S___fc_inode_0_S___fc_stdout }} [0].__fc_inode ∈
{{ NULL ; &S___fc_inode_0_S___fc_stdout[0] }}
[1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈ [1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
[--..--] [--..--]
[1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }} [1].__fc_inode ∈
{{ NULL ; &S___fc_inode_1_S___fc_stdout[0] }}
S___fc_inode_0_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks} ∈ S___fc_inode_0_S___fc_stdout[0]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks} ∈
[--..--] [--..--]
[0].__fc_real_data ∈ [0].__fc_real_data ∈
{{ NULL ; {{ NULL ;
&S___fc_real_data_0_S___fc_inode_0_S___fc_stdout }} &S___fc_real_data_0_S___fc_inode_0_S___fc_stdout[0] }}
{[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks}} ∈ {[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks}} ∈
[--..--] [--..--]
[1].__fc_real_data ∈ [1].__fc_real_data ∈
{{ NULL ; {{ NULL ;
&S___fc_real_data_1_S___fc_inode_0_S___fc_stdout }} &S___fc_real_data_1_S___fc_inode_0_S___fc_stdout[0] }}
[1].__fc_real_data_max_size ∈ [--..--] [1].__fc_real_data_max_size ∈ [--..--]
S___fc_real_data_0_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--] S___fc_real_data_0_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
S___fc_real_data_1_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--] S___fc_real_data_1_S___fc_inode_0_S___fc_stdout[0..1] ∈ [--..--]
...@@ -43,12 +45,12 @@ ...@@ -43,12 +45,12 @@
[--..--] [--..--]
[0].__fc_real_data ∈ [0].__fc_real_data ∈
{{ NULL ; {{ NULL ;
&S___fc_real_data_0_S___fc_inode_1_S___fc_stdout }} &S___fc_real_data_0_S___fc_inode_1_S___fc_stdout[0] }}
{[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks}} ∈ {[0].__fc_real_data_max_size; [1]{.st_dev; .st_ino; .st_mode; .st_nlink; .st_uid; .st_gid; .st_rdev; .st_size; .st_atime; .st_mtime; .st_ctime; .st_blksize; .st_blocks}} ∈
[--..--] [--..--]
[1].__fc_real_data ∈ [1].__fc_real_data ∈
{{ NULL ; {{ NULL ;
&S___fc_real_data_1_S___fc_inode_1_S___fc_stdout }} &S___fc_real_data_1_S___fc_inode_1_S___fc_stdout[0] }}
[1].__fc_real_data_max_size ∈ [--..--] [1].__fc_real_data_max_size ∈ [--..--]
S___fc_real_data_0_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--] S___fc_real_data_0_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
S___fc_real_data_1_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--] S___fc_real_data_1_S___fc_inode_1_S___fc_stdout[0..1] ∈ [--..--]
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment