From c58cba8a1b391a5acaa91e34e8fd406a94ca088f Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 27 Aug 2020 09:42:43 +0200
Subject: [PATCH] [kernel] export membership functions in Globals.Types
---
src/kernel_services/ast_data/globals.ml | 8 ++++++++
src/kernel_services/ast_data/globals.mli | 10 ++++++++++
src/plugins/e-acsl/src/project_initializer/rtl.ml | 9 +--------
3 files changed, 19 insertions(+), 8 deletions(-)
diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml
index 9e7fc4010ab..8ca2727ea32 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -741,10 +741,18 @@ module Types = struct
TypeNameToGlobal.mark_as_computed ()
end
+ let mem_enum_tag x =
+ resolve_types ();
+ Enums.mem x
+
let find_enum_tag x =
resolve_types ();
Enums.find x
+ let mem_type namespace s =
+ resolve_types ();
+ Types.mem (s, namespace)
+
let find_type namespace s =
resolve_types ();
Types.find (s, namespace)
diff --git a/src/kernel_services/ast_data/globals.mli b/src/kernel_services/ast_data/globals.mli
index c9866e785bf..d61900ee900 100644
--- a/src/kernel_services/ast_data/globals.mli
+++ b/src/kernel_services/ast_data/globals.mli
@@ -219,10 +219,20 @@ module Types : sig
(** The two functions below are suitable for use in functor
{!Logic_typing.Make} *)
+ val mem_enum_tag: string -> bool
+ (** @return true iff there is an enum constant with the given name in the
+ AST.
+ @since Frama-C+dev *)
+
val find_enum_tag: string -> exp * typ
(** Find an enum constant from its name in the AST.
@raise Not_found when no such constant exists. *)
+ val mem_type: Logic_typing.type_namespace -> string -> bool
+ (** @return true iff there is a type with the given name in the given
+ namespace in the AST.
+ @since Frama-C+dev *)
+
val find_type: Logic_typing.type_namespace -> string -> typ
(** Find a type from its name in the AST.
@raise Not_found when no such type exists. *)
diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml
index 2a6e9673773..47f3c40f6cd 100644
--- a/src/plugins/e-acsl/src/project_initializer/rtl.ml
+++ b/src/plugins/e-acsl/src/project_initializer/rtl.ml
@@ -124,14 +124,7 @@ let lookup_rtl_globals rtl_ast =
end
(* [do_ty] is [do_it] for types *)
and do_ty acc l g kind tname =
- let mem _g =
- try
- ignore (Globals.Types.find_type kind tname);
- true
- with Not_found ->
- false
- in
- do_it mem acc l g
+ do_it (fun _ -> Globals.Types.mem_type kind tname) acc l g
and do_globals acc globs =
match globs with
| [] ->
--
GitLab