From 93fc8ec7a331b5dd5e58cf4f9e78dd780ec0d1c7 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 27 Aug 2020 09:50:37 +0200
Subject: [PATCH] [kernel] export membership functions from Globals.Functions
---
src/kernel_services/ast_data/globals.ml | 21 +++++++++++++++++++
src/kernel_services/ast_data/globals.mli | 14 +++++++++++++
.../e-acsl/src/project_initializer/rtl.ml | 11 +++-------
3 files changed, 38 insertions(+), 8 deletions(-)
diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml
index 8ca2727ea32..cae5f59e1f5 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 d61900ee900..59c9a4875aa 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 47f3c40f6cd..38f3fb5809f 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
--
GitLab