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 cbe7c4de8e9885a56d45cdaf2669d4a6a1175259..ff60761947ba412e6652a8f0c7c68f3fd07f39be 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 6bf27aa86ccbd5e29bca87ef93b766e1005fd29b..fe353dc24020e6a6fd21637fab7c4a7f5135c554 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 773193133c3c3f969dce77f20497ea6710beb567..8b29d96a787032c285659cc7a2172fd62baca621 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);