module Logic_env:sig
..end
val is_extension : string -> bool
val extension_category : string -> Cil_types.ext_category
val preprocess_extension : string -> Logic_ptree.lexpr list -> Logic_ptree.lexpr list
module Logic_info:State_builder.Hashtbl
with type key = string and type data = Cil_types.logic_info list
module Logic_type_info:State_builder.Hashtbl
with type key = string and type data = Cil_types.logic_type_info
module Logic_ctor_info:State_builder.Hashtbl
with type key = string and type data = Cil_types.logic_ctor_info
module Model_info:State_builder.Hashtbl
with type key = string and type data = Cil_types.model_info
module Lemmas:State_builder.Hashtbl
with type key = string and type data = Cil_types.global_annotation
val builtin_states : State.t list
val prepare_tables : unit -> unit
val add_logic_function_gen : (Cil_types.logic_info -> Cil_types.logic_info -> bool) ->
Cil_types.logic_info -> unit
Logic_utils.add_logic_function
instead.val add_logic_type : string -> Cil_types.logic_type_info -> unit
val add_logic_ctor : string -> Cil_types.logic_ctor_info -> unit
val add_model_field : Cil_types.model_info -> unit
module Builtins:sig
..end
module Logic_builtin_used:sig
..end
val add_builtin_logic_function_gen : (Cil_types.builtin_logic_info -> Cil_types.builtin_logic_info -> bool) ->
Cil_types.builtin_logic_info -> unit
val add_builtin_logic_type : string -> Cil_types.logic_type_info -> unit
val add_builtin_logic_ctor : string -> Cil_types.logic_ctor_info -> unit
val is_builtin_logic_function : string -> bool
val is_builtin_logic_type : string -> bool
val is_builtin_logic_ctor : string -> bool
val iter_builtin_logic_function : (Cil_types.builtin_logic_info -> unit) -> unit
val iter_builtin_logic_type : (Cil_types.logic_type_info -> unit) -> unit
val iter_builtin_logic_ctor : (Cil_types.logic_ctor_info -> unit) -> unit
val find_all_logic_functions : string -> Cil_types.logic_info list
val find_all_model_fields : string -> Cil_types.model_info list
val find_model_field : string -> Cil_types.typ -> Cil_types.model_info
find_model_info field typ
returns the model field associated to field
in type typ
.Not_found
if no such type exists.val find_logic_cons : Cil_types.logic_var -> Cil_types.logic_info
Not_found
if the given varinfo is not associated to a global logic
constant.val find_logic_type : string -> Cil_types.logic_type_info
val find_logic_ctor : string -> Cil_types.logic_ctor_info
val is_logic_function : string -> bool
val is_logic_type : string -> bool
val is_logic_ctor : string -> bool
val is_model_field : string -> bool
val remove_logic_function : string -> unit
val remove_logic_info_gen : (Cil_types.logic_info -> Cil_types.logic_info -> bool) ->
Cil_types.logic_info -> unit
remove_logic_info_gen is_same_profile li
removes a specific logic info among all the overloaded ones.
If the name corresponds to built-ins, all overloaded functions are
removed at once (overloaded built-ins are always considered as a whole).
Otherwise, does nothing if no logic info with the same profile as li
is in the table.
See Logic_env.add_logic_info_gen
for more information about the
is_same_profile
argument.
Since Chlorine-20180501
val remove_logic_type : string -> unit
remove_logic_type s
removes the definition of logic type s
. If s
is
a sum type, also removes the associated constructors. Does nothing in case
s
is not a known logic type.val remove_logic_ctor : string -> unit
val remove_model_field : string -> unit
val add_typename : string -> unit
val hide_typename : string -> unit
val remove_typename : string -> unit
val reset_typenames : unit -> unit
val typename_status : string -> bool
val builtin_types_as_typenames : unit -> unit
val set_extension_handler : category:(string -> Cil_types.ext_category) ->
is_extension:(string -> bool) ->
preprocess:(string -> Logic_ptree.lexpr list -> Logic_ptree.lexpr list) ->
unit
Acsl_extension
, do not call thisval init_dependencies : State.t -> unit