From 915972a145ddcdcc770d7ccc6d5c7aef8033d0c2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 9 Oct 2018 09:39:21 +0200
Subject: [PATCH] Updates oracles: Value becomes Eva.
---
.../e-acsl/tests/bts/oracle/gen_bts1740.c | 2 +-
.../e-acsl/tests/bts/oracle/gen_bts1837.c | 2 +-
.../e-acsl/tests/bts/oracle/gen_bts2231.c | 2 +-
.../e-acsl/tests/bts/oracle/gen_bts2252.c | 2 +-
.../e-acsl/tests/format/oracle/gen_fprintf.c | 36 +++++++++----------
.../e-acsl/tests/gmp/oracle/gen_arith.c | 5 ++-
.../oracle/gen_at_on-purely-logic-variables.c | 18 +++++-----
.../tests/runtime/oracle/gen_block_valid.c | 4 +--
.../tests/runtime/oracle/gen_early_exit.c | 2 +-
.../tests/runtime/oracle/gen_local_init.c | 4 +--
.../tests/runtime/oracle/gen_mainargs.c | 4 +--
.../tests/runtime/oracle/gen_memalign.c | 4 +--
.../tests/temporal/oracle/gen_t_dpointer.c | 12 +++----
.../tests/temporal/oracle/gen_t_malloc-asan.c | 8 ++---
.../tests/temporal/oracle/gen_t_malloc.c | 2 +-
.../tests/temporal/oracle/gen_t_memcpy.c | 12 +++----
.../tests/temporal/oracle/gen_t_scope.c | 2 +-
.../tests/temporal/oracle/gen_t_while.c | 2 +-
18 files changed, 61 insertions(+), 62 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
index 0238773cf1d..23ebc578ded 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
@@ -42,7 +42,7 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_2;
- /*@ assert Value: dangling_pointer: ¬\dangling(&p); */
+ /*@ assert Eva: dangling_pointer: ¬\dangling(&p); */
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
(void *)(& p));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
index 479c1f71de9..cdb0aac13a7 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
@@ -92,7 +92,7 @@ int main(void)
while (1) {
int tmp;
tmp = i;
- /*@ assert Value: signed_overflow: -2147483648 ≤ i - 1; */
+ /*@ assert Eva: signed_overflow: -2147483648 ≤ i - 1; */
i --;
;
if (! tmp) break;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
index 109f7f7ba1c..34883c53204 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
@@ -23,7 +23,7 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl_A));
__gen_e_acsl__2 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_mul));
/*@ assert
- Value: signed_overflow: -9223372036854775808 ≤ __gen_e_acsl__2 - 1;
+ Eva: signed_overflow: -9223372036854775808 ≤ __gen_e_acsl__2 - 1;
*/
__gmpz_init_set_si(__gen_e_acsl__3,__gen_e_acsl__2 - 1L);
__gmpz_init(__gen_e_acsl_add);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
index dbe068e24e6..fbac950bb35 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
@@ -45,7 +45,7 @@ int main(void)
(char *)"main",(char *)"!\\valid_read(srcbuf + i)",
16);
}
- /*@ assert Value: mem_access: \valid_read(srcbuf + i); */
+ /*@ assert Eva: mem_access: \valid_read(srcbuf + i); */
if ((int)*(srcbuf + i) == (int)ch) loc = i;
i ++;
}
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
index 8c221966305..09448857900 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
@@ -239,7 +239,7 @@ int main(int argc, char const **argv)
int process_status;
__e_acsl_store_block((void *)(& process_status),(size_t)4);
waitpid(pid,& process_status,0);
- /*@ assert Value: initialization: \initialized(&process_status); */
+ /*@ assert Eva: initialization: \initialized(&process_status); */
signal_eval(process_status,0,__gen_e_acsl_literal_string_8);
__e_acsl_delete_block((void *)(& process_status));
}
@@ -257,7 +257,7 @@ int main(int argc, char const **argv)
int process_status_0;
__e_acsl_store_block((void *)(& process_status_0),(size_t)4);
waitpid(pid_0,& process_status_0,0);
- /*@ assert Value: initialization: \initialized(&process_status_0); */
+ /*@ assert Eva: initialization: \initialized(&process_status_0); */
signal_eval(process_status_0,1,__gen_e_acsl_literal_string_9);
__e_acsl_delete_block((void *)(& process_status_0));
}
@@ -280,7 +280,7 @@ int main(int argc, char const **argv)
int process_status_1;
__e_acsl_store_block((void *)(& process_status_1),(size_t)4);
waitpid(pid_1,& process_status_1,0);
- /*@ assert Value: initialization: \initialized(&process_status_1); */
+ /*@ assert Eva: initialization: \initialized(&process_status_1); */
signal_eval(process_status_1,0,__gen_e_acsl_literal_string_12);
__e_acsl_delete_block((void *)(& process_status_1));
}
@@ -300,7 +300,7 @@ int main(int argc, char const **argv)
int process_status_2;
__e_acsl_store_block((void *)(& process_status_2),(size_t)4);
waitpid(pid_2,& process_status_2,0);
- /*@ assert Value: initialization: \initialized(&process_status_2); */
+ /*@ assert Eva: initialization: \initialized(&process_status_2); */
signal_eval(process_status_2,1,__gen_e_acsl_literal_string_13);
__e_acsl_delete_block((void *)(& process_status_2));
}
@@ -320,7 +320,7 @@ int main(int argc, char const **argv)
int process_status_3;
__e_acsl_store_block((void *)(& process_status_3),(size_t)4);
waitpid(pid_3,& process_status_3,0);
- /*@ assert Value: initialization: \initialized(&process_status_3); */
+ /*@ assert Eva: initialization: \initialized(&process_status_3); */
signal_eval(process_status_3,1,__gen_e_acsl_literal_string_14);
__e_acsl_delete_block((void *)(& process_status_3));
}
@@ -339,7 +339,7 @@ int main(int argc, char const **argv)
int process_status_4;
__e_acsl_store_block((void *)(& process_status_4),(size_t)4);
waitpid(pid_4,& process_status_4,0);
- /*@ assert Value: initialization: \initialized(&process_status_4); */
+ /*@ assert Eva: initialization: \initialized(&process_status_4); */
signal_eval(process_status_4,0,__gen_e_acsl_literal_string_15);
__e_acsl_delete_block((void *)(& process_status_4));
}
@@ -357,7 +357,7 @@ int main(int argc, char const **argv)
int process_status_5;
__e_acsl_store_block((void *)(& process_status_5),(size_t)4);
waitpid(pid_5,& process_status_5,0);
- /*@ assert Value: initialization: \initialized(&process_status_5); */
+ /*@ assert Eva: initialization: \initialized(&process_status_5); */
signal_eval(process_status_5,1,__gen_e_acsl_literal_string_16);
__e_acsl_delete_block((void *)(& process_status_5));
}
@@ -376,7 +376,7 @@ int main(int argc, char const **argv)
int process_status_6;
__e_acsl_store_block((void *)(& process_status_6),(size_t)4);
waitpid(pid_6,& process_status_6,0);
- /*@ assert Value: initialization: \initialized(&process_status_6); */
+ /*@ assert Eva: initialization: \initialized(&process_status_6); */
signal_eval(process_status_6,0,__gen_e_acsl_literal_string_19);
__e_acsl_delete_block((void *)(& process_status_6));
}
@@ -395,7 +395,7 @@ int main(int argc, char const **argv)
int process_status_7;
__e_acsl_store_block((void *)(& process_status_7),(size_t)4);
waitpid(pid_7,& process_status_7,0);
- /*@ assert Value: initialization: \initialized(&process_status_7); */
+ /*@ assert Eva: initialization: \initialized(&process_status_7); */
signal_eval(process_status_7,0,__gen_e_acsl_literal_string_21);
__e_acsl_delete_block((void *)(& process_status_7));
}
@@ -414,7 +414,7 @@ int main(int argc, char const **argv)
int process_status_8;
__e_acsl_store_block((void *)(& process_status_8),(size_t)4);
waitpid(pid_8,& process_status_8,0);
- /*@ assert Value: initialization: \initialized(&process_status_8); */
+ /*@ assert Eva: initialization: \initialized(&process_status_8); */
signal_eval(process_status_8,1,__gen_e_acsl_literal_string_23);
__e_acsl_delete_block((void *)(& process_status_8));
}
@@ -433,7 +433,7 @@ int main(int argc, char const **argv)
int process_status_9;
__e_acsl_store_block((void *)(& process_status_9),(size_t)4);
waitpid(pid_9,& process_status_9,0);
- /*@ assert Value: initialization: \initialized(&process_status_9); */
+ /*@ assert Eva: initialization: \initialized(&process_status_9); */
signal_eval(process_status_9,1,__gen_e_acsl_literal_string_24);
__e_acsl_delete_block((void *)(& process_status_9));
}
@@ -452,7 +452,7 @@ int main(int argc, char const **argv)
int process_status_10;
__e_acsl_store_block((void *)(& process_status_10),(size_t)4);
waitpid(pid_10,& process_status_10,0);
- /*@ assert Value: initialization: \initialized(&process_status_10); */
+ /*@ assert Eva: initialization: \initialized(&process_status_10); */
signal_eval(process_status_10,1,__gen_e_acsl_literal_string_25);
__e_acsl_delete_block((void *)(& process_status_10));
}
@@ -472,7 +472,7 @@ int main(int argc, char const **argv)
int process_status_11;
__e_acsl_store_block((void *)(& process_status_11),(size_t)4);
waitpid(pid_11,& process_status_11,0);
- /*@ assert Value: initialization: \initialized(&process_status_11); */
+ /*@ assert Eva: initialization: \initialized(&process_status_11); */
signal_eval(process_status_11,0,__gen_e_acsl_literal_string_26);
__e_acsl_delete_block((void *)(& process_status_11));
}
@@ -492,7 +492,7 @@ int main(int argc, char const **argv)
int process_status_12;
__e_acsl_store_block((void *)(& process_status_12),(size_t)4);
waitpid(pid_12,& process_status_12,0);
- /*@ assert Value: initialization: \initialized(&process_status_12); */
+ /*@ assert Eva: initialization: \initialized(&process_status_12); */
signal_eval(process_status_12,0,__gen_e_acsl_literal_string_27);
__e_acsl_delete_block((void *)(& process_status_12));
}
@@ -512,7 +512,7 @@ int main(int argc, char const **argv)
int process_status_13;
__e_acsl_store_block((void *)(& process_status_13),(size_t)4);
waitpid(pid_13,& process_status_13,0);
- /*@ assert Value: initialization: \initialized(&process_status_13); */
+ /*@ assert Eva: initialization: \initialized(&process_status_13); */
signal_eval(process_status_13,1,__gen_e_acsl_literal_string_28);
__e_acsl_delete_block((void *)(& process_status_13));
}
@@ -532,7 +532,7 @@ int main(int argc, char const **argv)
int process_status_14;
__e_acsl_store_block((void *)(& process_status_14),(size_t)4);
waitpid(pid_14,& process_status_14,0);
- /*@ assert Value: initialization: \initialized(&process_status_14); */
+ /*@ assert Eva: initialization: \initialized(&process_status_14); */
signal_eval(process_status_14,1,__gen_e_acsl_literal_string_29);
__e_acsl_delete_block((void *)(& process_status_14));
}
@@ -552,7 +552,7 @@ int main(int argc, char const **argv)
int process_status_15;
__e_acsl_store_block((void *)(& process_status_15),(size_t)4);
waitpid(pid_15,& process_status_15,0);
- /*@ assert Value: initialization: \initialized(&process_status_15); */
+ /*@ assert Eva: initialization: \initialized(&process_status_15); */
signal_eval(process_status_15,1,__gen_e_acsl_literal_string_30);
__e_acsl_delete_block((void *)(& process_status_15));
}
@@ -572,7 +572,7 @@ int main(int argc, char const **argv)
int process_status_16;
__e_acsl_store_block((void *)(& process_status_16),(size_t)4);
waitpid(pid_16,& process_status_16,0);
- /*@ assert Value: initialization: \initialized(&process_status_16); */
+ /*@ assert Eva: initialization: \initialized(&process_status_16); */
signal_eval(process_status_16,0,__gen_e_acsl_literal_string_31);
__e_acsl_delete_block((void *)(& process_status_16));
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
index 19b540ee081..a3c67a7d24d 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
@@ -118,9 +118,8 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
__gen_e_acsl__7 = __gmpz_get_si((__e_acsl_mpz_struct const *)(__gen_e_acsl_div_2));
- /*@ assert Value: signed_overflow: -2147483648 ≤ 1 + __gen_e_acsl__7;
- */
- /*@ assert Value: signed_overflow: 1 + __gen_e_acsl__7 ≤ 2147483647; */
+ /*@ assert Eva: signed_overflow: -2147483648 ≤ 1 + __gen_e_acsl__7; */
+ /*@ assert Eva: signed_overflow: 1 + __gen_e_acsl__7 ≤ 2147483647; */
__e_acsl_assert(1 + __gen_e_acsl__7 == 1,(char *)"Assertion",
(char *)"main",
(char *)"1 + (z + 1) / (y - 123456789123456789) == 1",34);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c
index c6f65b06f7c..534b46472fb 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c
@@ -54,7 +54,7 @@ void g(void)
(char *)"mem_access: \\valid_read(__gen_e_acsl_at + (int)(__gen_e_acsl_w - 3))",
16);
/*@ assert
- Value: initialization:
+ Eva: initialization:
\initialized(__gen_e_acsl_at + (__gen_e_acsl_w - 3));
*/
if (! *(__gen_e_acsl_at + (__gen_e_acsl_w - 3))) ;
@@ -144,7 +144,7 @@ int main(void)
int __gen_e_acsl_u_7;
__gen_e_acsl_u_7 = 42;
/*@ assert
- Value: mem_access:
+ Eva: mem_access:
\valid(__gen_e_acsl_at_7 +
(int)((int)((int)(__gen_e_acsl_u_6 - 10) * 300) +
(int)((int)((int)((int)(__gen_e_acsl_v_6 -
@@ -251,7 +251,7 @@ int main(void)
(char *)"mem_access: \\valid_read(__gen_e_acsl_at_2 + (int)(__gen_e_acsl_j - 2))",
29);
/*@ assert
- Value: initialization:
+ Eva: initialization:
\initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2));
*/
if (! *(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2))) ;
@@ -304,7 +304,7 @@ int main(void)
(char *)"mem_access:\n \\valid_read(__gen_e_acsl_at_3 +\n (int)((int)((int)(__gen_e_acsl_u - 9) * 11) +\n (int)((int)(__gen_e_acsl_v - -5) - 1)))",
34);
/*@ assert
- Value: initialization:
+ Eva: initialization:
\initialized(__gen_e_acsl_at_3 +
((__gen_e_acsl_u - 9) * 11 +
((__gen_e_acsl_v - -5) - 1)));
@@ -385,7 +385,7 @@ int main(void)
(char *)"mem_access:\n \\valid_read(__gen_e_acsl_at_5 + (int)((int)(__gen_e_acsl_k_3 - -9) - 1))",
41);
/*@ assert
- Value: initialization:
+ Eva: initialization:
\initialized(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1));
*/
if (! (*(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1)) == 0L))
@@ -442,7 +442,7 @@ int main(void)
(char *)"mem_access:\n \\valid_read(__gen_e_acsl_at_6 +\n (int)((int)((int)(__gen_e_acsl_u_3 - 9) * 32) +\n (int)((int)(__gen_e_acsl_v_3 - -5) - 1)))",
45);
/*@ assert
- Value: initialization:
+ Eva: initialization:
\initialized(__gen_e_acsl_at_6 +
((__gen_e_acsl_u_3 - 9) * 32 +
((__gen_e_acsl_v_3 - -5) - 1)));
@@ -531,7 +531,7 @@ int main(void)
(char *)"mem_access:\n \\valid_read(__gen_e_acsl_at_7 +\n (int)((int)((int)(__gen_e_acsl_u_5 - 10) * 300) +\n (int)((int)((int)((int)(__gen_e_acsl_v_5 - -10) - 1) *\n 100)\n + (int)((int)(__gen_e_acsl_w - 100) - 1))))",
57);
/*@ assert
- Value: initialization:
+ Eva: initialization:
\initialized(__gen_e_acsl_at_7 +
((__gen_e_acsl_u_5 - 10) * 300 +
(((__gen_e_acsl_v_5 - -10) - 1) * 100 +
@@ -657,7 +657,7 @@ void __gen_e_acsl_f(int *t)
(char *)"mem_access:\n \\valid_read(__gen_e_acsl_at + (int)((int)(__gen_e_acsl_n - 1) - 1))",
7);
/*@ assert
- Value: initialization:
+ Eva: initialization:
\initialized(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1));
*/
if (*(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1))) {
@@ -673,7 +673,7 @@ void __gen_e_acsl_f(int *t)
(char *)"mem_access:\n \\valid_read(__gen_e_acsl_at_2 + (int)((int)(__gen_e_acsl_n - 1) - 1))",
7);
/*@ assert
- Value: initialization:
+ Eva: initialization:
\initialized(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
*/
__gen_e_acsl_and = *(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c
index 281b5e4f73a..1c80e61c845 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c
@@ -94,10 +94,10 @@ int main(int argc, char **argv)
__e_acsl_delete_block((void *)(& t));
}
__e_acsl_initialize((void *)pmin,sizeof(char));
- /*@ assert Value: mem_access: \valid(pmin); */
+ /*@ assert Eva: mem_access: \valid(pmin); */
*pmin = (char)'P';
__e_acsl_initialize((void *)pmax,sizeof(char));
- /*@ assert Value: mem_access: \valid(pmax); */
+ /*@ assert Eva: mem_access: \valid(pmax); */
*pmax = (char)'L';
int diff = (int)((unsigned long)pmax - (unsigned long)pmin);
/*@ assert \valid(pmin); */
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
index 97218423f4c..9283676c3db 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
@@ -41,7 +41,7 @@ int goto_bts(void)
sizeof(int *));
if (__gen_e_acsl_initialized_2) {
int __gen_e_acsl_valid_2;
- /*@ assert Value: dangling_pointer: ¬\dangling(&p); */
+ /*@ assert Eva: dangling_pointer: ¬\dangling(&p); */
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
(void *)(& p));
__gen_e_acsl_and_2 = __gen_e_acsl_valid_2;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_local_init.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_local_init.c
index 0d0a7af8168..4bf8407616c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_local_init.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_local_init.c
@@ -5,13 +5,13 @@ int X = 0;
int *p = & X;
int f(void)
{
- /*@ assert Value: mem_access: \valid_read(p); */
+ /*@ assert Eva: mem_access: \valid_read(p); */
{
int __gen_e_acsl_valid_read;
__gen_e_acsl_valid_read = __e_acsl_valid_read((void *)p,sizeof(int),
(void *)p,(void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"Assertion",(char *)"f",
- (char *)"Value: mem_access: \\valid_read(p)",12);
+ (char *)"Eva: mem_access: \\valid_read(p)",12);
}
int x = *p;
return x;
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
index 7b168a0908a..cc5634c8fbb 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
@@ -63,7 +63,7 @@ int __gen_e_acsl_main(int argc, char **argv)
(void *)(& argv));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(argv + argc)",15);
- /*@ assert Value: mem_access: \valid_read(argv + argc); */
+ /*@ assert Eva: mem_access: \valid_read(argv + argc); */
__e_acsl_assert(*(argv + argc) == (char *)0,(char *)"Assertion",
(char *)"main",(char *)"*(argv + argc) == \\null",15);
}
@@ -82,7 +82,7 @@ int __gen_e_acsl_main(int argc, char **argv)
(void *)(& argv));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(argv + argc)",16);
- /*@ assert Value: mem_access: \valid_read(argv + argc); */
+ /*@ assert Eva: mem_access: \valid_read(argv + argc); */
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)*(argv + argc),
sizeof(char),
(void *)*(argv + argc),
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
index 496f0208a15..2cb37870059 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
+++ b/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
@@ -12,8 +12,8 @@ int main(int argc, char const **argv)
__e_acsl_full_init((void *)(& memptr));
int res2 =
posix_memalign((void **)memptr,(unsigned long)256,(unsigned long)15);
- /*@ assert Value: initialization: \initialized(memptr); */
- /*@ assert Value: mem_access: \valid_read(memptr); */
+ /*@ assert Eva: initialization: \initialized(memptr); */
+ /*@ assert Eva: mem_access: \valid_read(memptr); */
char *p = *memptr;
__e_acsl_store_block((void *)(& p),(size_t)8);
__e_acsl_full_init((void *)(& p));
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c
index f1ba32d8da3..13d59a6a146 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c
@@ -24,9 +24,9 @@ int main(void)
__e_acsl_temporal_reset_parameters();
__e_acsl_temporal_reset_return();
__e_acsl_initialize((void *)(p + i),sizeof(int *));
- /*@ assert Value: mem_access: \valid(p + i); */
+ /*@ assert Eva: mem_access: \valid(p + i); */
*(p + i) = (int *)malloc(sizeof(int));
- /*@ assert Value: initialization: \initialized(p + i); */
+ /*@ assert Eva: initialization: \initialized(p + i); */
__e_acsl_temporal_store_nblock((void *)(p + i),(void *)*(p + i));
/*@ assert \valid(*(p + i)); */
{
@@ -43,7 +43,7 @@ int main(void)
(void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(p + i)",14);
- /*@ assert Value: initialization: \initialized(p + i); */
+ /*@ assert Eva: initialization: \initialized(p + i); */
__gen_e_acsl_valid_2 = __e_acsl_valid((void *)*(p + i),sizeof(int),
(void *)*(p + i),
(void *)(p + i));
@@ -58,8 +58,8 @@ int main(void)
__e_acsl_temporal_reset_parameters();
__e_acsl_temporal_reset_return();
__e_acsl_temporal_save_nreferent_parameter((void *)(p + 2),0U);
- /*@ assert Value: initialization: \initialized(p + 2); */
- /*@ assert Value: mem_access: \valid_read(p + 2); */
+ /*@ assert Eva: initialization: \initialized(p + 2); */
+ /*@ assert Eva: mem_access: \valid_read(p + 2); */
free((void *)*(p + 2));
__e_acsl_temporal_reset_parameters();
__e_acsl_temporal_reset_return();
@@ -79,7 +79,7 @@ int main(void)
(void *)(& p));
__e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(p + 2)",20);
- /*@ assert Value: dangling_pointer: ¬\dangling(p + 2); */
+ /*@ assert Eva: dangling_pointer: ¬\dangling(p + 2); */
__gen_e_acsl_valid_3 = __e_acsl_valid((void *)*(p + 2),sizeof(int),
(void *)*(p + 2),(void *)(
p + 2));
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc-asan.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc-asan.c
index 16284a8aa20..61977340a88 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc-asan.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc-asan.c
@@ -42,7 +42,7 @@ int main(void)
p = (int *)malloc((unsigned long)(1024 * 1024));
__e_acsl_temporal_store_nblock((void *)(& p),(void *)*(& p));
counter ++;
- /*@ assert Value: dangling_pointer: ¬\dangling(&q); */
+ /*@ assert Eva: dangling_pointer: ¬\dangling(&q); */
if (p != q) {
__e_acsl_temporal_reset_parameters();
__e_acsl_temporal_reset_return();
@@ -60,11 +60,11 @@ int main(void)
__e_acsl_full_init((void *)(& p));
p = (int *)0;
}
- /*@ assert Value: dangling_pointer: ¬\dangling(&p); */
+ /*@ assert Eva: dangling_pointer: ¬\dangling(&p); */
if (p) {
- /*@ assert Value: dangling_pointer: ¬\dangling(&q); */
+ /*@ assert Eva: dangling_pointer: ¬\dangling(&q); */
__e_acsl_initialize((void *)q,sizeof(int));
- /*@ assert Value: mem_access: \valid(q); */
+ /*@ assert Eva: mem_access: \valid(q); */
*q = 1;
__e_acsl_initialize((void *)p,sizeof(int));
*p = 2;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc.c
index 5798f68c74c..ce90dc8e2a7 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc.c
@@ -93,7 +93,7 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized_5) {
int __gen_e_acsl_valid_5;
- /*@ assert Value: dangling_pointer: ¬\dangling(&p); */
+ /*@ assert Eva: dangling_pointer: ¬\dangling(&p); */
__gen_e_acsl_valid_5 = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
(void *)(& p));
__gen_e_acsl_and_5 = __gen_e_acsl_valid_5;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
index db3449211e2..0e6ce723930 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
@@ -154,7 +154,7 @@ int main(void)
__e_acsl_temporal_store_nblock((void *)(& q),(void *)*(& q));
__e_acsl_temporal_store_nblock((void *)p,(void *)(& a));
__e_acsl_initialize((void *)p,sizeof(int *));
- /*@ assert Value: mem_access: \valid(p); */
+ /*@ assert Eva: mem_access: \valid(p); */
*p = & a;
__e_acsl_temporal_store_nblock((void *)(p + 1),(void *)(& a));
__e_acsl_initialize((void *)(p + 1),sizeof(int *));
@@ -237,8 +237,8 @@ int main(void)
else __gen_e_acsl_and_10 = 0;
__e_acsl_assert(__gen_e_acsl_and_10,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(q)",44);
- /*@ assert Value: initialization: \initialized(q); */
- /*@ assert Value: mem_access: \valid_read(q); */
+ /*@ assert Eva: initialization: \initialized(q); */
+ /*@ assert Eva: mem_access: \valid_read(q); */
__gen_e_acsl_valid_9 = __e_acsl_valid((void *)*q,sizeof(int),
(void *)*q,(void *)q);
__gen_e_acsl_and_11 = __gen_e_acsl_valid_9;
@@ -262,8 +262,8 @@ int main(void)
(void *)(& q));
__e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(q + 1)",45);
- /*@ assert Value: initialization: \initialized(q + 1); */
- /*@ assert Value: mem_access: \valid_read(q + 1); */
+ /*@ assert Eva: initialization: \initialized(q + 1); */
+ /*@ assert Eva: mem_access: \valid_read(q + 1); */
__gen_e_acsl_valid_10 = __e_acsl_valid((void *)*(q + 1),sizeof(int),
(void *)*(q + 1),
(void *)(q + 1));
@@ -278,7 +278,7 @@ int main(void)
tmp_1 = (int *)0;
__e_acsl_temporal_store_nreferent((void *)(q + 1),(void *)(& tmp_1));
__e_acsl_initialize((void *)(q + 1),sizeof(int *));
- /*@ assert Value: mem_access: \valid(q + 1); */
+ /*@ assert Eva: mem_access: \valid(q + 1); */
*(q + 1) = tmp_1;
__e_acsl_temporal_store_nreferent((void *)q,(void *)(& tmp_1));
__e_acsl_initialize((void *)q,sizeof(int *));
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c
index 5235e098e70..97a19425592 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c
@@ -33,7 +33,7 @@ int main(void)
sizeof(int *));
if (__gen_e_acsl_initialized) {
int __gen_e_acsl_valid;
- /*@ assert Value: dangling_pointer: ¬\dangling(&p); */
+ /*@ assert Eva: dangling_pointer: ¬\dangling(&p); */
__gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p,
(void *)(& p));
__gen_e_acsl_and = __gen_e_acsl_valid;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
index a22e34bc049..72a23b62f92 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
@@ -59,7 +59,7 @@ int main(void)
(char *)"!\\valid(q)",36);
}
__e_acsl_initialize((void *)q,sizeof(int));
- /*@ assert Value: mem_access: \valid(q); */
+ /*@ assert Eva: mem_access: \valid(q); */
*q = 1;
__retres = 0;
return_label: __e_acsl_store_block_duplicate((void *)(& q),(size_t)8);
--
GitLab