From e6752985c5f93b9645252a9abb1902f950a3fe95 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 4 Mar 2022 17:31:25 +0100
Subject: [PATCH] [e-acsl] update tests
---
.../e-acsl/tests/arith/oracle/gen_at.c | 12 ++++--
.../oracle/gen_at_on-purely-logic-variables.c | 37 +++++++++++--------
.../e-acsl/tests/bts/oracle/gen_bts1307.c | 6 +--
.../e-acsl/tests/bts/oracle/gen_bts1326.c | 12 +++---
.../tests/bts/oracle/gen_issue-eacsl-139.c | 3 +-
.../tests/bts/oracle/gen_issue-eacsl-40.c | 1 +
.../constructs/oracle/gen_function_contract.c | 4 ++
.../e-acsl/tests/format/oracle/gen_printf.c | 1 +
.../e-acsl/tests/libc/oracle/gen_file.c | 1 +
.../e-acsl/tests/libc/oracle/gen_str.c | 1 +
.../memory/oracle/gen_valid_in_contract.c | 1 +
.../special/oracle/gen_e-acsl-functions.c | 6 ++-
12 files changed, 54 insertions(+), 31 deletions(-)
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_at.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
index 9f178a13837..fc16d53dd1f 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
@@ -170,10 +170,11 @@ void g(int *p, int *q)
(void *)q,(void *)(& q));
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "RTE";
- __gen_e_acsl_assert_data.pred_txt = "mem_access: \\valid_read(q)";
+ __gen_e_acsl_assert_data.pred_txt = "\\valid_read(q)";
__gen_e_acsl_assert_data.file = "at.i";
__gen_e_acsl_assert_data.fct = "g";
__gen_e_acsl_assert_data.line = 39;
+ __gen_e_acsl_assert_data.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
__gen_e_acsl_at = *q;
@@ -199,10 +200,11 @@ void g(int *p, int *q)
(void *)(& p));
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "RTE";
- __gen_e_acsl_assert_data_2.pred_txt = "mem_access: \\valid_read(p + __gen_e_acsl_at)";
+ __gen_e_acsl_assert_data_2.pred_txt = "\\valid_read(p + __gen_e_acsl_at)";
__gen_e_acsl_assert_data_2.file = "at.i";
__gen_e_acsl_assert_data_2.fct = "g";
__gen_e_acsl_assert_data_2.line = 39;
+ __gen_e_acsl_assert_data_2.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read_2,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
__gen_e_acsl_at_2 = *(p + __gen_e_acsl_at);
@@ -240,10 +242,11 @@ void g(int *p, int *q)
(void *)(& p));
__gen_e_acsl_assert_data_4.blocking = 1;
__gen_e_acsl_assert_data_4.kind = "RTE";
- __gen_e_acsl_assert_data_4.pred_txt = "mem_access: \\valid_read(p + __gen_e_acsl_at)";
+ __gen_e_acsl_assert_data_4.pred_txt = "\\valid_read(p + __gen_e_acsl_at)";
__gen_e_acsl_assert_data_4.file = "at.i";
__gen_e_acsl_assert_data_4.fct = "g";
__gen_e_acsl_assert_data_4.line = 43;
+ __gen_e_acsl_assert_data_4.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read_3,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
__gen_e_acsl_at_3 = *(p + __gen_e_acsl_at);
@@ -264,10 +267,11 @@ void g(int *p, int *q)
(void *)(& p));
__gen_e_acsl_assert_data_6.blocking = 1;
__gen_e_acsl_assert_data_6.kind = "RTE";
- __gen_e_acsl_assert_data_6.pred_txt = "mem_access: \\valid_read(p + __gen_e_acsl_at)";
+ __gen_e_acsl_assert_data_6.pred_txt = "\\valid_read(p + __gen_e_acsl_at)";
__gen_e_acsl_assert_data_6.file = "at.i";
__gen_e_acsl_assert_data_6.fct = "g";
__gen_e_acsl_assert_data_6.line = 41;
+ __gen_e_acsl_assert_data_6.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read_4,& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
__gen_e_acsl_assert_data_5.blocking = 1;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
index 1e9af602313..cae72156516 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
@@ -66,7 +66,7 @@ void g(void)
(void *)(& __gen_e_acsl_at));
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "RTE";
- __gen_e_acsl_assert_data_2.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at + (int)(__gen_e_acsl_w_2 - 3))";
+ __gen_e_acsl_assert_data_2.pred_txt = "\\valid_read(__gen_e_acsl_at + (int)(__gen_e_acsl_w_2 - 3))";
__gen_e_acsl_assert_data_2.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_2.fct = "g";
__gen_e_acsl_assert_data_2.line = 16;
@@ -288,7 +288,7 @@ int main(void)
(void *)(& __gen_e_acsl_at_3));
__gen_e_acsl_assert_data_4.blocking = 1;
__gen_e_acsl_assert_data_4.kind = "RTE";
- __gen_e_acsl_assert_data_4.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at_3 + (int)(__gen_e_acsl_j_2 - 2))";
+ __gen_e_acsl_assert_data_4.pred_txt = "\\valid_read(__gen_e_acsl_at_3 + (int)(__gen_e_acsl_j_2 - 2))";
__gen_e_acsl_assert_data_4.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_4.fct = "main";
__gen_e_acsl_assert_data_4.line = 29;
@@ -362,7 +362,7 @@ int main(void)
(void *)(& __gen_e_acsl_at_5));
__gen_e_acsl_assert_data_6.blocking = 1;
__gen_e_acsl_assert_data_6.kind = "RTE";
- __gen_e_acsl_assert_data_6.pred_txt = "mem_access:\n \\valid_read(__gen_e_acsl_at_5 +\n (int)((int)((int)(__gen_e_acsl_u_6 - 9) * 11) +\n (int)(__gen_e_acsl_v_4 - -4)))";
+ __gen_e_acsl_assert_data_6.pred_txt = "\\valid_read(__gen_e_acsl_at_5 +\n (int)((int)((int)(__gen_e_acsl_u_6 - 9) * 11) +\n (int)(__gen_e_acsl_v_4 - -4)))";
__gen_e_acsl_assert_data_6.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_6.fct = "main";
__gen_e_acsl_assert_data_6.line = 34;
@@ -429,7 +429,7 @@ int main(void)
(void *)(& __gen_e_acsl_at_2));
__gen_e_acsl_assert_data_8.blocking = 1;
__gen_e_acsl_assert_data_8.kind = "RTE";
- __gen_e_acsl_assert_data_8.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at_2 + 0)";
+ __gen_e_acsl_assert_data_8.pred_txt = "\\valid_read(__gen_e_acsl_at_2 + 0)";
__gen_e_acsl_assert_data_8.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_8.fct = "main";
__gen_e_acsl_assert_data_8.line = 38;
@@ -487,7 +487,7 @@ int main(void)
(void *)(& __gen_e_acsl_at_8));
__gen_e_acsl_assert_data_10.blocking = 1;
__gen_e_acsl_assert_data_10.kind = "RTE";
- __gen_e_acsl_assert_data_10.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at_8 + (int)(__gen_e_acsl_k_4 - -8))";
+ __gen_e_acsl_assert_data_10.pred_txt = "\\valid_read(__gen_e_acsl_at_8 + (int)(__gen_e_acsl_k_4 - -8))";
__gen_e_acsl_assert_data_10.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_10.fct = "main";
__gen_e_acsl_assert_data_10.line = 42;
@@ -565,7 +565,7 @@ int main(void)
(void *)(& __gen_e_acsl_at_6));
__gen_e_acsl_assert_data_12.blocking = 1;
__gen_e_acsl_assert_data_12.kind = "RTE";
- __gen_e_acsl_assert_data_12.pred_txt = "mem_access:\n \\valid_read(__gen_e_acsl_at_6 +\n (int)((int)((int)(__gen_e_acsl_u_7 - 9) * 32) +\n (int)(__gen_e_acsl_v_5 - -4)))";
+ __gen_e_acsl_assert_data_12.pred_txt = "\\valid_read(__gen_e_acsl_at_6 +\n (int)((int)((int)(__gen_e_acsl_u_7 - 9) * 32) +\n (int)(__gen_e_acsl_v_5 - -4)))";
__gen_e_acsl_assert_data_12.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_12.fct = "main";
__gen_e_acsl_assert_data_12.line = 46;
@@ -683,7 +683,7 @@ int main(void)
(void *)(& __gen_e_acsl_at_7));
__gen_e_acsl_assert_data_14.blocking = 1;
__gen_e_acsl_assert_data_14.kind = "RTE";
- __gen_e_acsl_assert_data_14.pred_txt = "mem_access:\n \\valid_read(__gen_e_acsl_at_7 +\n (int)((int)((int)(__gen_e_acsl_u_8 - 10) * 300) +\n (int)((int)((int)(__gen_e_acsl_v_6 - -9) * 100) +\n (int)(__gen_e_acsl_w_2 - 101))))";
+ __gen_e_acsl_assert_data_14.pred_txt = "\\valid_read(__gen_e_acsl_at_7 +\n (int)((int)((int)(__gen_e_acsl_u_8 - 10) * 300) +\n (int)((int)((int)(__gen_e_acsl_v_6 - -9) * 100) +\n (int)(__gen_e_acsl_w_2 - 101))))";
__gen_e_acsl_assert_data_14.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_14.fct = "main";
__gen_e_acsl_assert_data_14.line = 59;
@@ -795,10 +795,11 @@ void __gen_e_acsl_f(int *t)
(void *)(& t));
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "RTE";
- __gen_e_acsl_assert_data.pred_txt = "mem_access: \\valid_read(t + __gen_e_acsl_m)";
+ __gen_e_acsl_assert_data.pred_txt = "\\valid_read(t + __gen_e_acsl_m)";
__gen_e_acsl_assert_data.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data.fct = "f";
__gen_e_acsl_assert_data.line = 8;
+ __gen_e_acsl_assert_data.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
*(__gen_e_acsl_at + 0) = *(t + __gen_e_acsl_m) == -4;
@@ -823,10 +824,11 @@ void __gen_e_acsl_f(int *t)
(void *)(& t));
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "RTE";
- __gen_e_acsl_assert_data_2.pred_txt = "mem_access: \\valid_read(t + (int)(__gen_e_acsl_m_2 - 4))";
+ __gen_e_acsl_assert_data_2.pred_txt = "\\valid_read(t + (int)(__gen_e_acsl_m_2 - 4))";
__gen_e_acsl_assert_data_2.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_2.fct = "f";
__gen_e_acsl_assert_data_2.line = 8;
+ __gen_e_acsl_assert_data_2.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read_2,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
*(__gen_e_acsl_at_2 + 0) = *(t + (__gen_e_acsl_m_2 - 4));
@@ -854,10 +856,11 @@ void __gen_e_acsl_f(int *t)
(void *)(& t));
__gen_e_acsl_assert_data_3.blocking = 1;
__gen_e_acsl_assert_data_3.kind = "RTE";
- __gen_e_acsl_assert_data_3.pred_txt = "mem_access: \\valid_read(t + (int)(__gen_e_acsl_n - 1))";
+ __gen_e_acsl_assert_data_3.pred_txt = "\\valid_read(t + (int)(__gen_e_acsl_n - 1))";
__gen_e_acsl_assert_data_3.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_3.fct = "f";
__gen_e_acsl_assert_data_3.line = 7;
+ __gen_e_acsl_assert_data_3.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read_3,
& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
@@ -887,10 +890,11 @@ void __gen_e_acsl_f(int *t)
(void *)(& t));
__gen_e_acsl_assert_data_4.blocking = 1;
__gen_e_acsl_assert_data_4.kind = "RTE";
- __gen_e_acsl_assert_data_4.pred_txt = "mem_access: \\valid_read(t + __gen_e_acsl_n_2)";
+ __gen_e_acsl_assert_data_4.pred_txt = "\\valid_read(t + __gen_e_acsl_n_2)";
__gen_e_acsl_assert_data_4.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_4.fct = "f";
__gen_e_acsl_assert_data_4.line = 7;
+ __gen_e_acsl_assert_data_4.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read_4,
& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
@@ -931,10 +935,11 @@ void __gen_e_acsl_f(int *t)
(void *)(& __gen_e_acsl_at_4));
__gen_e_acsl_assert_data_6.blocking = 1;
__gen_e_acsl_assert_data_6.kind = "RTE";
- __gen_e_acsl_assert_data_6.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at_4 + (int)(__gen_e_acsl_n_3 - 2))";
+ __gen_e_acsl_assert_data_6.pred_txt = "\\valid_read(__gen_e_acsl_at_4 + (int)(__gen_e_acsl_n_3 - 2))";
__gen_e_acsl_assert_data_6.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_6.fct = "f";
__gen_e_acsl_assert_data_6.line = 7;
+ __gen_e_acsl_assert_data_6.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read_5,
& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
@@ -956,10 +961,11 @@ void __gen_e_acsl_f(int *t)
(void *)(& __gen_e_acsl_at_3));
__gen_e_acsl_assert_data_7.blocking = 1;
__gen_e_acsl_assert_data_7.kind = "RTE";
- __gen_e_acsl_assert_data_7.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at_3 + (int)(__gen_e_acsl_n_3 - 2))";
+ __gen_e_acsl_assert_data_7.pred_txt = "\\valid_read(__gen_e_acsl_at_3 + (int)(__gen_e_acsl_n_3 - 2))";
__gen_e_acsl_assert_data_7.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_7.fct = "f";
__gen_e_acsl_assert_data_7.line = 7;
+ __gen_e_acsl_assert_data_7.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read_6,
& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
@@ -1004,10 +1010,11 @@ void __gen_e_acsl_f(int *t)
(void *)(& __gen_e_acsl_at));
__gen_e_acsl_assert_data_9.blocking = 1;
__gen_e_acsl_assert_data_9.kind = "RTE";
- __gen_e_acsl_assert_data_9.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at + 0)";
+ __gen_e_acsl_assert_data_9.pred_txt = "\\valid_read(__gen_e_acsl_at + 0)";
__gen_e_acsl_assert_data_9.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_9.fct = "f";
__gen_e_acsl_assert_data_9.line = 8;
+ __gen_e_acsl_assert_data_9.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read_7,& __gen_e_acsl_assert_data_9);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_9);
if (*(__gen_e_acsl_at + 0)) {
@@ -1028,7 +1035,7 @@ void __gen_e_acsl_f(int *t)
(void *)(& __gen_e_acsl_at_2));
__gen_e_acsl_assert_data_10.blocking = 1;
__gen_e_acsl_assert_data_10.kind = "RTE";
- __gen_e_acsl_assert_data_10.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at_2 + 0)";
+ __gen_e_acsl_assert_data_10.pred_txt = "\\valid_read(__gen_e_acsl_at_2 + 0)";
__gen_e_acsl_assert_data_10.file = "at_on-purely-logic-variables.c";
__gen_e_acsl_assert_data_10.fct = "f";
__gen_e_acsl_assert_data_10.line = 8;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index 91b3577515f..d88f9586db8 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -195,7 +195,7 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
(void *)(& __gen_e_acsl_at));
__gen_e_acsl_assert_data_5.blocking = 1;
__gen_e_acsl_assert_data_5.kind = "RTE";
- __gen_e_acsl_assert_data_5.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at)";
+ __gen_e_acsl_assert_data_5.pred_txt = "\\valid_read(__gen_e_acsl_at)";
__gen_e_acsl_assert_data_5.file = "bts1307.i";
__gen_e_acsl_assert_data_5.fct = "bar";
__gen_e_acsl_assert_data_5.line = 26;
@@ -215,7 +215,7 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
(void *)(& __gen_e_acsl_at_3));
__gen_e_acsl_assert_data_6.blocking = 1;
__gen_e_acsl_assert_data_6.kind = "RTE";
- __gen_e_acsl_assert_data_6.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at_3)";
+ __gen_e_acsl_assert_data_6.pred_txt = "\\valid_read(__gen_e_acsl_at_3)";
__gen_e_acsl_assert_data_6.file = "bts1307.i";
__gen_e_acsl_assert_data_6.fct = "bar";
__gen_e_acsl_assert_data_6.line = 26;
@@ -268,7 +268,7 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
(void *)(& __gen_e_acsl_at));
__gen_e_acsl_assert_data_7.blocking = 1;
__gen_e_acsl_assert_data_7.kind = "RTE";
- __gen_e_acsl_assert_data_7.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at)";
+ __gen_e_acsl_assert_data_7.pred_txt = "\\valid_read(__gen_e_acsl_at)";
__gen_e_acsl_assert_data_7.file = "bts1307.i";
__gen_e_acsl_assert_data_7.fct = "bar";
__gen_e_acsl_assert_data_7.line = 26;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
index eb58dccf2f5..0e739191004 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
@@ -102,7 +102,7 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
(void *)0);
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "RTE";
- __gen_e_acsl_assert_data_2.pred_txt = "mem_access: \\valid_read((int *)*__gen_e_acsl_at)";
+ __gen_e_acsl_assert_data_2.pred_txt = "\\valid_read((int *)*__gen_e_acsl_at)";
__gen_e_acsl_assert_data_2.file = "bts1326.i";
__gen_e_acsl_assert_data_2.fct = "atp_NORMAL_computeAverageAccel";
__gen_e_acsl_assert_data_2.line = 8;
@@ -122,7 +122,7 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
(void *)0);
__gen_e_acsl_assert_data_3.blocking = 1;
__gen_e_acsl_assert_data_3.kind = "RTE";
- __gen_e_acsl_assert_data_3.pred_txt = "mem_access: \\valid_read(&(*__gen_e_acsl_at)[1])";
+ __gen_e_acsl_assert_data_3.pred_txt = "\\valid_read(&(*__gen_e_acsl_at)[1])";
__gen_e_acsl_assert_data_3.file = "bts1326.i";
__gen_e_acsl_assert_data_3.fct = "atp_NORMAL_computeAverageAccel";
__gen_e_acsl_assert_data_3.line = 8;
@@ -142,7 +142,7 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
(void *)0);
__gen_e_acsl_assert_data_4.blocking = 1;
__gen_e_acsl_assert_data_4.kind = "RTE";
- __gen_e_acsl_assert_data_4.pred_txt = "mem_access: \\valid_read(&(*__gen_e_acsl_at)[2])";
+ __gen_e_acsl_assert_data_4.pred_txt = "\\valid_read(&(*__gen_e_acsl_at)[2])";
__gen_e_acsl_assert_data_4.file = "bts1326.i";
__gen_e_acsl_assert_data_4.fct = "atp_NORMAL_computeAverageAccel";
__gen_e_acsl_assert_data_4.line = 8;
@@ -162,7 +162,7 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
(void *)0);
__gen_e_acsl_assert_data_5.blocking = 1;
__gen_e_acsl_assert_data_5.kind = "RTE";
- __gen_e_acsl_assert_data_5.pred_txt = "mem_access: \\valid_read(&(*__gen_e_acsl_at)[3])";
+ __gen_e_acsl_assert_data_5.pred_txt = "\\valid_read(&(*__gen_e_acsl_at)[3])";
__gen_e_acsl_assert_data_5.file = "bts1326.i";
__gen_e_acsl_assert_data_5.fct = "atp_NORMAL_computeAverageAccel";
__gen_e_acsl_assert_data_5.line = 8;
@@ -182,7 +182,7 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
(void *)0);
__gen_e_acsl_assert_data_6.blocking = 1;
__gen_e_acsl_assert_data_6.kind = "RTE";
- __gen_e_acsl_assert_data_6.pred_txt = "mem_access: \\valid_read(&(*__gen_e_acsl_at)[4])";
+ __gen_e_acsl_assert_data_6.pred_txt = "\\valid_read(&(*__gen_e_acsl_at)[4])";
__gen_e_acsl_assert_data_6.file = "bts1326.i";
__gen_e_acsl_assert_data_6.fct = "atp_NORMAL_computeAverageAccel";
__gen_e_acsl_assert_data_6.line = 8;
@@ -202,7 +202,7 @@ void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
(void *)(& __gen_e_acsl_at_2));
__gen_e_acsl_assert_data_7.blocking = 1;
__gen_e_acsl_assert_data_7.kind = "RTE";
- __gen_e_acsl_assert_data_7.pred_txt = "mem_access: \\valid_read(__gen_e_acsl_at_2)";
+ __gen_e_acsl_assert_data_7.pred_txt = "\\valid_read(__gen_e_acsl_at_2)";
__gen_e_acsl_assert_data_7.file = "bts1326.i";
__gen_e_acsl_assert_data_7.fct = "atp_NORMAL_computeAverageAccel";
__gen_e_acsl_assert_data_7.line = 8;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c
index 213b4d9f74e..7bccd9add24 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c
@@ -55,10 +55,11 @@ void __gen_e_acsl_f(struct X *item)
(void *)(& item));
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "RTE";
- __gen_e_acsl_assert_data.pred_txt = "mem_access: \\valid_read(item)";
+ __gen_e_acsl_assert_data.pred_txt = "\\valid_read(item)";
__gen_e_acsl_assert_data.file = "issue-eacsl-139.c";
__gen_e_acsl_assert_data.fct = "f";
__gen_e_acsl_assert_data.line = 9;
+ __gen_e_acsl_assert_data.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
__gen_e_acsl_at_2 = *item;
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c
index 0c097d165c8..aecdee5351d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-40.c
@@ -277,6 +277,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data_5.file = "FRAMAC_SHARE/libc/stdio.h";
__gen_e_acsl_assert_data_5.fct = "fread";
__gen_e_acsl_assert_data_5.line = 356;
+ __gen_e_acsl_assert_data_5.name = "size_read";
__e_acsl_assert(__retres <= __gen_e_acsl_at_3,
& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c
index a969672a927..501806c4f43 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c
@@ -433,6 +433,7 @@ void __gen_e_acsl_o(void)
__gen_e_acsl_assert_data_13.file = "function_contract.i";
__gen_e_acsl_assert_data_13.fct = "o";
__gen_e_acsl_assert_data_13.line = 99;
+ __gen_e_acsl_assert_data_13.name = "neg";
__e_acsl_assert(X == __gen_e_acsl_at,& __gen_e_acsl_assert_data_13);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_13);
}
@@ -450,6 +451,7 @@ void __gen_e_acsl_o(void)
__gen_e_acsl_assert_data_14.file = "function_contract.i";
__gen_e_acsl_assert_data_14.fct = "o";
__gen_e_acsl_assert_data_14.line = 104;
+ __gen_e_acsl_assert_data_14.name = "pos";
__e_acsl_assert(X == __gen_e_acsl_at,& __gen_e_acsl_assert_data_14);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_14);
}
@@ -467,6 +469,7 @@ void __gen_e_acsl_o(void)
__gen_e_acsl_assert_data_15.file = "function_contract.i";
__gen_e_acsl_assert_data_15.fct = "o";
__gen_e_acsl_assert_data_15.line = 109;
+ __gen_e_acsl_assert_data_15.name = "odd";
__e_acsl_assert(X == __gen_e_acsl_at,& __gen_e_acsl_assert_data_15);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_15);
}
@@ -484,6 +487,7 @@ void __gen_e_acsl_o(void)
__gen_e_acsl_assert_data_16.file = "function_contract.i";
__gen_e_acsl_assert_data_16.fct = "o";
__gen_e_acsl_assert_data_16.line = 114;
+ __gen_e_acsl_assert_data_16.name = "even";
__e_acsl_assert(X == __gen_e_acsl_at,& __gen_e_acsl_assert_data_16);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_16);
}
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
index 4fcfca74865..3cc0a9f2184 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
@@ -912,6 +912,7 @@ char *__gen_e_acsl_strchr(char const *s, int c)
__gen_e_acsl_assert_data_2.file = "FRAMAC_SHARE/libc/string.h";
__gen_e_acsl_assert_data_2.fct = "strchr";
__gen_e_acsl_assert_data_2.line = 177;
+ __gen_e_acsl_assert_data_2.name = "found/result_char";
__e_acsl_assert((int)*__retres == (int)((char)__gen_e_acsl_at_2),
& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_file.c b/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
index c6e10b5b0c5..f4e8c5310d9 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_file.c
@@ -277,6 +277,7 @@ size_t __gen_e_acsl_fread(void * restrict ptr, size_t size, size_t nmemb,
__gen_e_acsl_assert_data_5.file = "FRAMAC_SHARE/libc/stdio.h";
__gen_e_acsl_assert_data_5.fct = "fread";
__gen_e_acsl_assert_data_5.line = 356;
+ __gen_e_acsl_assert_data_5.name = "size_read";
__e_acsl_assert(__retres <= __gen_e_acsl_at_3,
& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_str.c b/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
index 23add5a82f4..a920841927e 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_str.c
@@ -329,6 +329,7 @@ char *__gen_e_acsl_strcat(char * restrict dest, char const * restrict src)
__gen_e_acsl_assert_data_8.file = "FRAMAC_SHARE/libc/string.h";
__gen_e_acsl_assert_data_8.fct = "strcat";
__gen_e_acsl_assert_data_8.line = 434;
+ __gen_e_acsl_assert_data_8.name = "result_ptr";
__e_acsl_assert(__retres == __gen_e_acsl_at,& __gen_e_acsl_assert_data_8);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_8);
__e_acsl_delete_block((void *)(& dest));
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
index e2ed7604f62..af84a51e13b 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
@@ -159,6 +159,7 @@ struct list *__gen_e_acsl_f(struct list *l)
__gen_e_acsl_assert_data_3.file = "valid_in_contract.c";
__gen_e_acsl_assert_data_3.fct = "f";
__gen_e_acsl_assert_data_3.line = 18;
+ __gen_e_acsl_assert_data_3.name = "B2";
__e_acsl_assert(__retres == __gen_e_acsl_at,
& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c
index 660f9ccf3bb..fae8de90730 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c
+++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c
@@ -116,10 +116,11 @@ int __gen_e_acsl_f(int *p)
(void *)p,(void *)(& p));
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "RTE";
- __gen_e_acsl_assert_data.pred_txt = "mem_access: \\valid_read(p)";
+ __gen_e_acsl_assert_data.pred_txt = "\\valid_read(p)";
__gen_e_acsl_assert_data.file = "e-acsl-functions.c";
__gen_e_acsl_assert_data.fct = "f";
__gen_e_acsl_assert_data.line = 11;
+ __gen_e_acsl_assert_data.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
__gen_e_acsl_at = *p;
@@ -152,10 +153,11 @@ int __gen_e_acsl_f(int *p)
(void *)p,(void *)(& p));
__gen_e_acsl_assert_data_4.blocking = 1;
__gen_e_acsl_assert_data_4.kind = "RTE";
- __gen_e_acsl_assert_data_4.pred_txt = "mem_access: \\valid_read(p)";
+ __gen_e_acsl_assert_data_4.pred_txt = "\\valid_read(p)";
__gen_e_acsl_assert_data_4.file = "e-acsl-functions.c";
__gen_e_acsl_assert_data_4.fct = "f";
__gen_e_acsl_assert_data_4.line = 10;
+ __gen_e_acsl_assert_data_4.name = "mem_access";
__e_acsl_assert(__gen_e_acsl_valid_read_2,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
__gen_e_acsl_assert_data_3.blocking = 1;
--
GitLab