diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml index 8ca2727ea327d0a060d1e76dc95f36693696d668..cae5f59e1f52990ea1df0ee8aa9ecab4caddfe69 100644 --- a/src/kernel_services/ast_data/globals.ml +++ b/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; diff --git a/src/kernel_services/ast_data/globals.mli b/src/kernel_services/ast_data/globals.mli index d61900ee900ab0114f9250493e18e60e0058b02c..59c9a4875aab1acb22ed4e6e8fae6e52b4f2af11 100644 --- a/src/kernel_services/ast_data/globals.mli +++ b/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 diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml index 47f3c40f6cd15bd24db9f643c3e5b1fa2b7e14ea..38f3fb5809f3adc1a37e721dbb726d3a46f31393 100644 --- a/src/plugins/e-acsl/src/project_initializer/rtl.ml +++ b/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