[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.

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

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);

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);