diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_safe_locations.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_safe_locations.c
index 2bb83096a37b444aaa320e4fa64a095c8e1e3c56..7b343fbdcb26a9859682feae9336e38cafbfffb3 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_safe_locations.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_safe_locations.c
@@ -126,20 +126,21 @@ void *thread_start(void *arg)
}
/*@ assert \valid(__fc_stderr) && \initialized(__fc_stderr); */ ;
{
- int __gen_e_acsl_valid_3;
+ int __gen_e_acsl_valid_read;
int __gen_e_acsl_and_3;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
- __gen_e_acsl_valid_3 = __e_acsl_valid((void *)stdin,sizeof(FILE),
- (void *)stdin,(void *)(& stdin));
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)stdin,sizeof(FILE),
+ (void *)stdin,
+ (void *)(& stdin));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"__fc_stdin",
(void *)stdin);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_3,
"sizeof(FILE)",0,sizeof(FILE));
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
- "\\valid(__fc_stdin)",0,
- __gen_e_acsl_valid_3);
- if (__gen_e_acsl_valid_3) {
+ "\\valid_read(__fc_stdin)",0,
+ __gen_e_acsl_valid_read);
+ if (__gen_e_acsl_valid_read) {
int __gen_e_acsl_initialized_3;
__gen_e_acsl_initialized_3 = __e_acsl_initialized((void *)stdin,
sizeof(FILE));
@@ -155,14 +156,14 @@ void *thread_start(void *arg)
else __gen_e_acsl_and_3 = 0;
__gen_e_acsl_assert_data_3.blocking = 1;
__gen_e_acsl_assert_data_3.kind = "Assertion";
- __gen_e_acsl_assert_data_3.pred_txt = "\\valid(__fc_stdin) && \\initialized(__fc_stdin)";
+ __gen_e_acsl_assert_data_3.pred_txt = "\\valid_read(__fc_stdin) && \\initialized(__fc_stdin)";
__gen_e_acsl_assert_data_3.file = "threads_safe_locations.c";
__gen_e_acsl_assert_data_3.fct = "thread_start";
__gen_e_acsl_assert_data_3.line = 8;
__e_acsl_assert(__gen_e_acsl_and_3,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
}
- /*@ assert \valid(__fc_stdin) && \initialized(__fc_stdin); */ ;
+ /*@ assert \valid_read(__fc_stdin) && \initialized(__fc_stdin); */ ;
int *addrof_errno = & errno;
__e_acsl_store_block((void *)(& addrof_errno),8UL);
__e_acsl_full_init((void *)(& addrof_errno));
@@ -182,8 +183,8 @@ void *thread_start(void *arg)
"\\initialized(&addrof_errno)",0,
__gen_e_acsl_initialized_4);
if (__gen_e_acsl_initialized_4) {
- int __gen_e_acsl_valid_4;
- __gen_e_acsl_valid_4 = __e_acsl_valid((void *)addrof_errno,sizeof(int),
+ int __gen_e_acsl_valid_3;
+ __gen_e_acsl_valid_3 = __e_acsl_valid((void *)addrof_errno,sizeof(int),
(void *)addrof_errno,
(void *)(& addrof_errno));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_4,
@@ -192,8 +193,8 @@ void *thread_start(void *arg)
"sizeof(int)",0,sizeof(int));
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_4,
"\\valid(addrof_errno)",0,
- __gen_e_acsl_valid_4);
- __gen_e_acsl_and_4 = __gen_e_acsl_valid_4;
+ __gen_e_acsl_valid_3);
+ __gen_e_acsl_and_4 = __gen_e_acsl_valid_3;
}
else __gen_e_acsl_and_4 = 0;
if (__gen_e_acsl_and_4) {
diff --git a/src/plugins/e-acsl/tests/concurrency/threads_safe_locations.c b/src/plugins/e-acsl/tests/concurrency/threads_safe_locations.c
index 52850ca6aedd650e196d879c1f91c2ee1e79a809..c9d8f8541438855d91714da1fdadb736fe0de4fa 100644
--- a/src/plugins/e-acsl/tests/concurrency/threads_safe_locations.c
+++ b/src/plugins/e-acsl/tests/concurrency/threads_safe_locations.c
@@ -5,7 +5,7 @@
void *thread_start(void *arg) {
//@ assert \valid(stdout) && \initialized(stdout);
//@ assert \valid(stderr) && \initialized(stderr);
- //@ assert \valid(stdin) && \initialized(stdin);
+ //@ assert \valid_read(stdin) && \initialized(stdin);
int *addrof_errno = &errno;
//@ assert \valid(addrof_errno) && \initialized(addrof_errno);
return NULL;
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c
index 850c8d6d027c4ec2d45439c17d90bb796f99c57f..07f3bc147ab6946873b871aee042604f92bf743e 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c
@@ -58,33 +58,34 @@ int main(void)
}
/*@ assert \valid(__fc_stderr); */ ;
{
- int __gen_e_acsl_valid_2;
+ int __gen_e_acsl_valid_read;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
{.values = (void *)0};
- __gen_e_acsl_valid_2 = __e_acsl_valid((void *)stdin,sizeof(FILE),
- (void *)stdin,(void *)(& stdin));
+ __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)stdin,sizeof(FILE),
+ (void *)stdin,
+ (void *)(& stdin));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"__fc_stdin",
(void *)stdin);
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data_2,
"sizeof(FILE)",0,sizeof(FILE));
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
- "\\valid(__fc_stdin)",0,
- __gen_e_acsl_valid_2);
+ "\\valid_read(__fc_stdin)",0,
+ __gen_e_acsl_valid_read);
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "Assertion";
- __gen_e_acsl_assert_data_2.pred_txt = "\\valid(__fc_stdin)";
+ __gen_e_acsl_assert_data_2.pred_txt = "\\valid_read(__fc_stdin)";
__gen_e_acsl_assert_data_2.file = "stdout.c";
__gen_e_acsl_assert_data_2.fct = "main";
__gen_e_acsl_assert_data_2.line = 9;
- __e_acsl_assert(__gen_e_acsl_valid_2,& __gen_e_acsl_assert_data_2);
+ __e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
- /*@ assert \valid(__fc_stdin); */ ;
+ /*@ assert \valid_read(__fc_stdin); */ ;
{
- int __gen_e_acsl_valid_3;
+ int __gen_e_acsl_valid_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
{.values = (void *)0};
- __gen_e_acsl_valid_3 = __e_acsl_valid((void *)stdout,sizeof(FILE),
+ __gen_e_acsl_valid_2 = __e_acsl_valid((void *)stdout,sizeof(FILE),
(void *)stdout,(void *)(& stdout));
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_3,"__fc_stdout",
(void *)stdout);
@@ -92,14 +93,14 @@ int main(void)
"sizeof(FILE)",0,sizeof(FILE));
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,
"\\valid(__fc_stdout)",0,
- __gen_e_acsl_valid_3);
+ __gen_e_acsl_valid_2);
__gen_e_acsl_assert_data_3.blocking = 1;
__gen_e_acsl_assert_data_3.kind = "Assertion";
__gen_e_acsl_assert_data_3.pred_txt = "\\valid(__fc_stdout)";
__gen_e_acsl_assert_data_3.file = "stdout.c";
__gen_e_acsl_assert_data_3.fct = "main";
__gen_e_acsl_assert_data_3.line = 10;
- __e_acsl_assert(__gen_e_acsl_valid_3,& __gen_e_acsl_assert_data_3);
+ __e_acsl_assert(__gen_e_acsl_valid_2,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
}
/*@ assert \valid(__fc_stdout); */ ;
diff --git a/src/plugins/e-acsl/tests/memory/stdout.c b/src/plugins/e-acsl/tests/memory/stdout.c
index 0238e9d99a5bc81c1c2720f928cf98a4fd2d0465..ab6d02c8f6efbbc178a486ce5048b28cfef40317 100644
--- a/src/plugins/e-acsl/tests/memory/stdout.c
+++ b/src/plugins/e-acsl/tests/memory/stdout.c
@@ -6,7 +6,7 @@
int main(void) {
/*@assert \valid(stderr); */
- /*@assert \valid(stdin); */
+ /*@assert \valid_read(stdin); */
/*@assert \valid(stdout); */
return 0;
}