From 6e110768663cfb554e1604522082b40827ff5643 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 10 Jun 2014 10:42:22 +0200
Subject: [PATCH] update oracles
---
.../e-acsl-runtime/oracle/bts1398.1.res.oracle | 18 ++++++++++--------
.../e-acsl-runtime/oracle/bts1398.res.oracle | 18 ++++++++++--------
2 files changed, 20 insertions(+), 16 deletions(-)
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 73d3ac2b865..859f194de03 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
@@ -17,25 +17,27 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
- __fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
+ __fc_stdout ∈ {{ NULL ; &S___fc_stdout[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} ∈
[--..--]
- [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_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} ∈
[--..--]
[0].__fc_real_data ∈
{{ 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}} ∈
[--..--]
[1].__fc_real_data ∈
{{ 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 ∈ [--..--]
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] ∈ [--..--]
@@ -43,12 +45,12 @@
[--..--]
[0].__fc_real_data ∈
{{ 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}} ∈
[--..--]
[1].__fc_real_data ∈
{{ 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 ∈ [--..--]
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] ∈ [--..--]
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 73d3ac2b865..859f194de03 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
@@ -17,25 +17,27 @@
__e_acsl_init ∈ [--..--]
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
- __fc_stdout ∈ {{ NULL ; &S___fc_stdout }}
+ __fc_stdout ∈ {{ NULL ; &S___fc_stdout[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} ∈
[--..--]
- [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_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} ∈
[--..--]
[0].__fc_real_data ∈
{{ 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}} ∈
[--..--]
[1].__fc_real_data ∈
{{ 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 ∈ [--..--]
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] ∈ [--..--]
@@ -43,12 +45,12 @@
[--..--]
[0].__fc_real_data ∈
{{ 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}} ∈
[--..--]
[1].__fc_real_data ∈
{{ 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 ∈ [--..--]
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] ∈ [--..--]
--
GitLab