[kernel] export membership functions from Globals.Functions

src/kernel_services/ast_data/globals.ml

@@ -359,6 +359,27 @@ module Functions = struct
     else
       res
 
+  let mem_name fct_name =
+    try
+      ignore (find_by_name fct_name);
+      true
+    with Not_found ->
+      false
+
+  let mem_def_name fct_name =
+    try
+      ignore (find_def_by_name fct_name);
+      true
+    with Not_found ->
+      false
+
+  let mem_decl_name fct_name =
+    try
+      ignore (find_decl_by_name fct_name);
+      true
+    with Not_found ->
+      false
+
   let () =
     Parameter_builder.find_kf_by_name := find_by_name;
     Parameter_builder.find_kf_def_by_name := find_def_by_name;

src/kernel_services/ast_data/globals.mli

@@ -103,6 +103,20 @@ module Functions: sig
   val get_params: kernel_function -> varinfo list
   val get_vi: kernel_function -> varinfo
 
+  (** {2 Membership} *)
+
+  val mem_name: string -> bool
+  (** @return true iff there is a function with such a name
+      @since Frama-C+dev *)
+
+  val mem_def_name: string -> bool
+  (** @return true iff there is a function definition with such a name
+      @since Frama-C+dev *)
+
+  val mem_decl_name: string -> bool
+  (** @return true iff there is a function declaration with such a name
+      @since Frama-C+dev *)
+
   (** {2 Searching} *)
 
   val find_by_name : string -> kernel_function

src/plugins/e-acsl/src/project_initializer/rtl.ml

@@ -139,9 +139,8 @@ let lookup_rtl_globals rtl_ast =
     | GVarDecl(vi, (pos, _)) | GVar(vi, _, (pos, _)) as g :: l  ->
       let tunit = Translation_unit pos.Filepath.pos_path in
       let mem _g =
-        match Globals.Syntactic_search.find_in_scope vi.vorig_name tunit with
-        | None -> false
-        | Some _ -> true
+        let g = Globals.Syntactic_search.find_in_scope vi.vorig_name tunit in
+        Option.is_some g
       in
       let add g =
         Symbols.add_vi vi.vname vi;
@@ -152,16 +151,12 @@ let lookup_rtl_globals rtl_ast =
       in
       do_it ~add mem acc l g
     | GFunDecl(_, vi, _loc) | GFun({ svar = vi }, _loc) as g :: l ->
-      let mem _g =
-        try ignore (Globals.Functions.find_by_name vi.vname); true
-        with Not_found -> false
-      in
       let add _g =
         Symbols.add_vi vi.vname vi;
         (* functions will be registered in kernel's table after substitution of
            RTL's symbols inside them *)
       in
-      do_it ~add mem acc l g
+      do_it ~add (fun _ -> Globals.Functions.mem_name vi.vname) acc l g
     | GAnnot _ :: l ->
       (* ignoring annotations from the AST *)
       do_globals acc l