[kernel] export membership functions in Globals.Types

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)

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. *)

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
     | [] ->