diff --git a/src/plugins/e-acsl/src/code_generator/assert.ml b/src/plugins/e-acsl/src/code_generator/assert.ml
index a49425e216c0ed16091850cb5e88671c00e848a2..10512e24c50597ae8ac64f90aa98fe5185d52686 100644
--- a/src/plugins/e-acsl/src/code_generator/assert.ml
+++ b/src/plugins/e-acsl/src/code_generator/assert.ml
@@ -203,7 +203,10 @@ let register ~loc ?(force=false) name e adata =
adata
let register_term ~loc ?force t e adata =
- let name = Format.asprintf "@[%a@]" Printer.pp_term t in
+ let name =
+ Format.asprintf "@[%a@]"
+ Printer.pp_term (Logic_normalizer.get_orig_term t)
+ in
register ~loc name ?force e adata
let register_pred ~loc env ?force p e adata =
@@ -212,6 +215,7 @@ let register_pred ~loc env ?force p e adata =
because they should be the only predicate in an assertion clause. *)
adata
else
+ let p = Logic_normalizer.get_orig_pred p in
let name = Format.asprintf "@[%a@]" Printer.pp_predicate p in
register ~loc name ?force e adata
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c b/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
index 598514c5351e05f34baf16d146d26c670296530c..0b32c4d48181233546530db20fe2db07bdc31c08 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_extended_quantifiers.c
@@ -404,7 +404,7 @@ int main(void)
}
}
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_8,
- "\\sum(2, 10, \\lambda integer k; k - 2 >= 0? 1: 0)",
+ "\\numof(2, 10, \\lambda integer k; k - 2 >= 0)",
0,__gen_e_acsl_accumulator_8);
__gen_e_acsl_assert_data_8.blocking = 1;
__gen_e_acsl_assert_data_8.kind = "Assertion";
@@ -450,7 +450,7 @@ int main(void)
}
}
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_9,
- "\\sum(4294967295U - 5, 4294967295U, \\lambda integer k; k % 2 == 1? 1: 0)",
+ "\\numof(4294967295U - 5, 4294967295U, \\lambda integer k; k % 2 == 1)",
0,__gen_e_acsl_accumulator_9);
__gen_e_acsl_assert_data_9.blocking = 1;
__gen_e_acsl_assert_data_9.kind = "Assertion";
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
index fe353dc24020e6a6fd21637fab7c4a7f5135c554..9f9358add8a131caac5f6a515f64a5a15ecf2a75 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
@@ -464,9 +464,8 @@ int main(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_16 =
{.values = (void *)0};
__gen_e_acsl_p_here_here_2 = __gen_e_acsl_p_here_here(27);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_16,
- "__gen_e_acsl_p_here_here(27)",0,
- __gen_e_acsl_p_here_here_2);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_16,"p_here(27)",
+ 0,__gen_e_acsl_p_here_here_2);
__gen_e_acsl_assert_data_16.blocking = 1;
__gen_e_acsl_assert_data_16.kind = "Assertion";
__gen_e_acsl_assert_data_16.pred_txt = "p_here(27)";
@@ -482,9 +481,8 @@ int main(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_17 =
{.values = (void *)0};
__gen_e_acsl_f_here_here_2 = __gen_e_acsl_f_here_here(27);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_17,
- "__gen_e_acsl_f_here_here(27)",0,
- __gen_e_acsl_f_here_here_2);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_17,"f_here(27)",
+ 0,__gen_e_acsl_f_here_here_2);
__gen_e_acsl_assert_data_17.blocking = 1;
__gen_e_acsl_assert_data_17.kind = "Assertion";
__gen_e_acsl_assert_data_17.pred_txt = "f_here(27) == 27";
@@ -501,8 +499,7 @@ int main(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data_18 =
{.values = (void *)0};
__gen_e_acsl_f3_here_2 = __gen_e_acsl_f3_here(5);
- __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_18,
- "__gen_e_acsl_f3_here(5)",0,
+ __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_18,"f3(5)",0,
__gen_e_acsl_f3_here_2);
__gen_e_acsl_assert_data_18.blocking = 1;
__gen_e_acsl_assert_data_18.kind = "Assertion";
diff --git a/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c b/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c
index 8b29d96a787032c285659cc7a2172fd62baca621..6cf2e62d18034f544a77bfc71b60ed5ffafde688 100644
--- a/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c
+++ b/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c
@@ -61,8 +61,7 @@ int main(void)
__e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
__gen_e_acsl_length_here_2 = __gen_e_acsl_length_here(l);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"l",(void *)l);
- __e_acsl_assert_register_long(& __gen_e_acsl_assert_data,
- "__gen_e_acsl_length_here(l)",0,
+ __e_acsl_assert_register_long(& __gen_e_acsl_assert_data,"length(l)",0,
__gen_e_acsl_length_here_2);
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Assertion";
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c
index 80cf5b33238e1d610af6e7b8f916359b104e040f..82a6d17354d92e49547ed65be32b184ed6d4c54b 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_extended_quantifiers.c
@@ -212,7 +212,7 @@ int main(void)
__gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_3),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
__e_acsl_assert_register_mpz(& __gen_e_acsl_assert_data_3,
- "\\sum(2, 10, \\lambda integer k; k - 2 >= 0? 1: 0)",
+ "\\numof(2, 10, \\lambda integer k; k - 2 >= 0)",
0,
(__e_acsl_mpz_struct const *)(__gen_e_acsl_accumulator_3));
__gen_e_acsl_assert_data_3.blocking = 1;
diff --git a/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c b/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
index 62c4f08984c381d861bfa926cb998781ff613ca4..81522c937fe323622587aadf2e3d27d16dad21fc 100644
--- a/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
+++ b/src/plugins/e-acsl/tests/libc/oracle/gen_mem.c
@@ -420,8 +420,8 @@ void *__gen_e_acsl_memset(void *s, int c, size_t n)
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"n",0,n);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"s",s);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
- "valid_s: __gen_e_acsl_valid_or_empty_here(s, n)",
- 0,__gen_e_acsl_valid_or_empty_here_2);
+ "valid_s: valid_or_empty(s, n)",0,
+ __gen_e_acsl_valid_or_empty_here_2);
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Precondition";
__gen_e_acsl_assert_data.pred_txt = "valid_or_empty(s, n)";
@@ -484,8 +484,8 @@ void *__gen_e_acsl_memmove(void *dest, void const *src, size_t n)
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"n",0,n);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"dest",dest);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
- "valid_dest: __gen_e_acsl_valid_or_empty_here(dest, n)",
- 0,__gen_e_acsl_valid_or_empty_here_3);
+ "valid_dest: valid_or_empty(dest, n)",0,
+ __gen_e_acsl_valid_or_empty_here_3);
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Precondition";
__gen_e_acsl_assert_data.pred_txt = "valid_or_empty(dest, n)";
@@ -504,8 +504,8 @@ void *__gen_e_acsl_memmove(void *dest, void const *src, size_t n)
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"src",
(void *)src);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
- "valid_src: __gen_e_acsl_valid_read_or_empty_here(src, n)",
- 0,__gen_e_acsl_valid_read_or_empty_here_2);
+ "valid_src: valid_read_or_empty(src, n)",0,
+ __gen_e_acsl_valid_read_or_empty_here_2);
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "Precondition";
__gen_e_acsl_assert_data_2.pred_txt = "valid_read_or_empty(src, n)";
@@ -594,8 +594,8 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"n",0,n);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"dest",dest);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
- "valid_dest: __gen_e_acsl_valid_or_empty_here(dest, n)",
- 0,__gen_e_acsl_valid_or_empty_here_4);
+ "valid_dest: valid_or_empty(dest, n)",0,
+ __gen_e_acsl_valid_or_empty_here_4);
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Precondition";
__gen_e_acsl_assert_data.pred_txt = "valid_or_empty(dest, n)";
@@ -614,8 +614,8 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"src",
(void *)src);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
- "valid_src: __gen_e_acsl_valid_read_or_empty_here(src, n)",
- 0,__gen_e_acsl_valid_read_or_empty_here_3);
+ "valid_src: valid_read_or_empty(src, n)",0,
+ __gen_e_acsl_valid_read_or_empty_here_3);
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "Precondition";
__gen_e_acsl_assert_data_2.pred_txt = "valid_read_or_empty(src, n)";
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 2ee59ac21428c963a95e43ed214b48f2ec3dd711..e03df15a615064ed5a156a094c597055581026d7 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
@@ -756,8 +756,8 @@ void *__gen_e_acsl_memset(void *s, int c, size_t n)
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"n",0,n);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"s",s);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
- "valid_s: __gen_e_acsl_valid_or_empty_here(s, n)",
- 0,__gen_e_acsl_valid_or_empty_here_2);
+ "valid_s: valid_or_empty(s, n)",0,
+ __gen_e_acsl_valid_or_empty_here_2);
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Precondition";
__gen_e_acsl_assert_data.pred_txt = "valid_or_empty(s, n)";
@@ -851,8 +851,8 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
__e_acsl_assert_register_ulong(& __gen_e_acsl_assert_data,"n",0,n);
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data,"dest",dest);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data,
- "valid_dest: __gen_e_acsl_valid_or_empty_here(dest, n)",
- 0,__gen_e_acsl_valid_or_empty_here_3);
+ "valid_dest: valid_or_empty(dest, n)",0,
+ __gen_e_acsl_valid_or_empty_here_3);
__gen_e_acsl_assert_data.blocking = 1;
__gen_e_acsl_assert_data.kind = "Precondition";
__gen_e_acsl_assert_data.pred_txt = "valid_or_empty(dest, n)";
@@ -871,8 +871,8 @@ void *__gen_e_acsl_memcpy(void * restrict dest, void const * restrict src,
__e_acsl_assert_register_ptr(& __gen_e_acsl_assert_data_2,"src",
(void *)src);
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
- "valid_src: __gen_e_acsl_valid_read_or_empty_here(src, n)",
- 0,__gen_e_acsl_valid_read_or_empty_here_2);
+ "valid_src: valid_read_or_empty(src, n)",0,
+ __gen_e_acsl_valid_read_or_empty_here_2);
__gen_e_acsl_assert_data_2.blocking = 1;
__gen_e_acsl_assert_data_2.kind = "Precondition";
__gen_e_acsl_assert_data_2.pred_txt = "valid_read_or_empty(src, n)";