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 0238773cf1dbde5283492d9e45aa5df8c395db78..23ebc578dedc86a9777417aabf541e019bd10fea 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 479c1f71de93530b93bc6539edaf6ea12471bc54..cdb0aac13a7e9955142419c501b83fee2b1893c0 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 109f7f7ba1c96d4eeac7cc0a25e4c4d47ff7abd6..34883c5320423d24ad61d9eadb9ff086aa364531 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 dbe068e24e6cf64cf28dfb2716b7ad150b321de0..fbac950bb35ba1de1b5c0cab828d301db3c447b2 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 8c22196630517dd819a4fdc6b268d8352c831d8c..094488579004d88251a40747c6ab0f01e3935fef 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 19b540ee081ce8d4e5ae7cb33e25e6f1ce01ca20..a3c67a7d24d396ed36195a55be80a2c265159870 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 c6f65b06f7c80ea452bdd467b56a65ec502f71f2..534b46472fb4b7d41af87833003a21ddb726fc7f 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 281b5e4f73a0e30e60ff32dee256229410cfb1c6..1c80e61c845a15ff6f973f96e61d18598b3fafe1 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 97218423f4cee8a0540340102120cfd704ee5ae3..9283676c3db0d7fb6ca941b96724f48062ea56e4 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 0d0a7af8168d0906951be0b6da1b9148af5dad7a..4bf8407616cef3965380916f316f05f8675f3f8e 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 7b168a0908a7a54a8e53523978a1a60875c89b09..cc5634c8fbb781ab5c9c22adc44dad4cc0153455 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 496f0208a15a54b0421b2c3378e20d39edbda3bb..2cb37870059b5b46414ff525c8e2c8115ef83c13 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 f1ba32d8da329e89f3bda89dffb8291b624f5cf8..13d59a6a146231814ede4cb1396e6323ee436107 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 16284a8aa203fc6642e4e44442cbec52c94ac629..61977340a88134d26ec809dccf4f9aeee11d9e83 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 5798f68c74c9e6698e6613de0563be14f913902b..ce90dc8e2a7ec6ef116969480608d37b58c0d3dd 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 db3449211e250fc288fea13ddad23c447bafd4c6..0e6ce7239309b553266e8db6f8fec55824628eeb 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 5235e098e70017a7f8e52871a0dc7b0db1c63c2c..97a194255926be1246726597a6e88f902ee2c3a7 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 a22e34bc0499957ab57151c0e770774e2c42913e..72a23b62f92da9f4f9cd65c045fa02942d1ef2db 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);