diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml index 9e7fc4010aba93779273e9d65cb4fc7d625a29ac..8ca2727ea327d0a060d1e76dc95f36693696d668 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 c9866e785bfb78a40bbdb1777676d179c47a94c3..d61900ee900ab0114f9250493e18e60e0058b02c 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 2a6e96737732a5e5a0783c909d8b88d9d34cabaa..47f3c40f6cd15bd24db9f643c3e5b1fa2b7e14ea 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 | [] ->