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 9f178a13837c806c0575135acd2c7013ce7fd34c..fc16d53dd1fc412895d4b1ea4afbe73552f7f2b7 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 1e9af6023135f12963514b9fcbd469d275a408d4..cae72156516869acc9f2964bf479d16baafaa71a 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 91b3577515f914de25c8b42d016d2b5bbdeeca51..d88f9586db8b11110e08dd704a21edac2a41f861 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 eb58dccf2f55da9a1211ad762c48191f56b73a15..0e7391910046bb16db211d8452a20138dcd04a7c 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 213b4d9f74eac564bebdd0059d7b93532bd5c786..7bccd9add2462a018e73403d29cc190b08992e8a 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 0c097d165c898e577807b108df86ae1b9f1af4cd..aecdee5351dadcd56fe95c8c4748633747def547 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 a969672a927d878c2756178fede4fa29a88554d7..501806c4f435ef09594846b2a8a7e66d2bf84847 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 4fcfca74865f84b46d21f3289bb4d2857120ad17..3cc0a9f218434ee686c775f66611fcde9a72ee1c 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 c6e10b5b0c544ee932324fbc8badc71f04621b8b..f4e8c5310d990d1a47034b19a3fd5758e5a50a3b 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 23add5a82f4db755be7a6a45211e12d7aa452294..a920841927e7a495fe70d277d47f50922257f2c0 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 e2ed7604f622ceb4eedcefe8c3fb0c6bf8cf9ad0..af84a51e13bced58dbfedafa5657fa3ad9c16c42 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 660f9ccf3bb7eea28c2838193af92523cb57823b..fae8de9073015154e66d4a745e8aef0e23f0387b 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;