Module Logic_env

module Logic_env: sig .. end

Global Logic Environment



module Logic_info: State_builder.Hashtbl 
  with type key = string and type data = Cil_types.logic_info
Global Tables
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

Shortcuts to the functions of the modules above


val prepare_tables : unit -> unit
Prepare all internal tables before their uses: clear all tables except builtins.

Add an user-defined object


val add_logic_function_gen : (Cil_types.logic_info -> Cil_types.logic_info -> bool) ->
Cil_types.logic_info -> unit
add_logic_function_gen takes as argument a function eq_logic_info which decides whether two logic_info are identical. It is intended to be Logic_utils.is_same_logic_profile, but this one can not be called from here since it will cause a circular dependency Logic_env <- Logic_utils <- Cil <- Logic_env. Do not use this function directly unless you're really sure about what you're doing. Use 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
Since Oxygen-20120901

Add a builtin object


module Builtins: sig .. end
module Logic_builtin_used: sig .. end
logic function/predicates that are effectively used in current project.
val add_builtin_logic_function_gen : (Cil_types.builtin_logic_info -> Cil_types.builtin_logic_info -> bool) ->
Cil_types.builtin_logic_info -> unit
see add_logic_function_gen above
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

searching the environment


val find_all_logic_functions : string -> Cil_types.logic_info list
val find_all_model_fields : string -> Cil_types.model_info list
returns all model fields of the same name.
Since Oxygen-20120901
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.
Since Oxygen-20120901
Raises Not_found if no such type exists.
val find_logic_cons : Cil_types.logic_var -> Cil_types.logic_info
cons is a logic function with no argument. It is used as a variable, but may occasionally need to find associated logic_info.
Raises 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

tests of existence


val is_logic_type : string -> bool
val is_logic_ctor : string -> bool
val is_model_field : string -> bool
Since Oxygen-20120901
val remove_logic_function : string -> unit

removing


val remove_logic_type : string -> unit
val remove_logic_ctor : string -> unit
val remove_model_field : string -> unit
Since Oxygen-20120901

Typename table


val add_typename : string -> unit
marks an identifier as being a typename in the logic
val hide_typename : string -> unit
marks temporarily a typename as being a normal identifier in the logic
val remove_typename : string -> unit
removes latest typename status associated to a given identifier
val reset_typenames : unit -> unit
erases all the typename status
val typename_status : string -> bool
returns the typename status of the given identifier.
val builtin_types_as_typenames : unit -> unit
marks builtin logical types as logical typenames for the logic lexer.

Internal use


val init_dependencies : State.t -> unit
Used to postpone dependency of Lenv global tables wrt Cil_state, which is initialized afterwards.