From 534eeaa552ff2aa67b66365653c23cc04210fbd4 Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Tue, 10 Sep 2024 20:50:51 +0200
Subject: [PATCH] [e-acsl] add annotation for generated logic_info
Add the code of generated predicates and logic functions as a global
annotation above their declaration in the generated C code.
---
.../e-acsl/src/code_generator/logic_functions.ml | 14 +++++++++++---
.../e-acsl/tests/arith/oracle/gen_functions.c | 6 ++++++
.../tests/examples/oracle/gen_functions_contiki.c | 10 ++++++++++
3 files changed, 27 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index cbe7c4de8e9..ff60761947b 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -374,13 +374,21 @@ end
let reset () = Gen_functions.clear ()
let add_generated_functions_to_file file =
- let rec decls_of_li ?(loc = Location.unknown) li =
+ let rec decls_of_li ?(generated = false) ?(loc = Location.unknown) li =
let dependencies =
- List.concat_map (decls_of_li ~loc)
+ List.concat_map (decls_of_li ~generated:true ~loc)
(Logic_normalizer.Logic_infos.generated_of li)
in
+ let add_generated_annot =
+ if generated
+ then fun decls -> GAnnot(Dfun_or_pred(li, loc), loc) :: decls
+ else fun decls -> decls
+ in
let kfs = Gen_functions.kernel_functions_of_logic_info li in
- dependencies @ List.map (fun kf -> GFunDecl (Cil.empty_funspec (), kf, loc)) kfs
+ let decls =
+ List.map (fun kf -> GFunDecl (Cil.empty_funspec (), kf, loc)) kfs
+ in
+ dependencies @ add_generated_annot @@ decls
in
let generated_decls_of_global = function
| GAnnot(Dfun_or_pred(li, loc), _) -> decls_of_li ~loc li
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 6bf27aa86cc..fe353dc2402 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
@@ -85,10 +85,14 @@ double __gen_e_acsl_f2(double x);
/*@ predicate p_here{L}(integer x) = x > 0;
*/
+/*@ predicate __gen_e_acsl_p_here_here(integer x) = x > 0;
+ */
int __gen_e_acsl_p_here_here(int x);
/*@ logic integer f_here{L}(integer x) = x;
*/
+/*@ logic integer __gen_e_acsl_f_here_here(integer x) = x;
+ */
int __gen_e_acsl_f_here_here(int x);
/*@ logic integer f_sum(integer x) = \sum(1, x, \lambda integer y; 1);
@@ -111,6 +115,8 @@ int __gen_e_acsl_signum_5(double x);
int z = 8;
/*@ logic integer f3{L}(integer y) = \at(z + y,L);
+ */
+/*@ logic integer __gen_e_acsl_f3_here(integer y) = z + y;
*/
long __gen_e_acsl_f3_here(int y);
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 773193133c3..8b29d96a787 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
@@ -20,9 +20,19 @@ logic integer length_aux{L}(struct list *l, integer n) =
(n < 2147483647? length_aux(l->next, n + 1): -1)),
L);
*/
+/*@
+logic integer __gen_e_acsl_length_aux_here(struct list *l, integer n) =
+ n < 0? -1:
+ (l == (struct list *)0? n:
+ (n < 2147483647? __gen_e_acsl_length_aux_here(l->next, n + 1): -1));
+ */
long __gen_e_acsl_length_aux_here(struct list *l, unsigned int n);
/*@ logic integer length{L}(struct list *l) = \at(length_aux(l, 0),L);
+ */
+/*@
+logic integer __gen_e_acsl_length_here(struct list *l) =
+ __gen_e_acsl_length_aux_here(l, 0);
*/
long __gen_e_acsl_length_here(struct list *l);
--
GitLab