Frama_c_kernel.Logic_env
val extension_category : string -> Cil_types.ext_category
val preprocess_extension :
string ->
Logic_ptree.lexpr list ->
Logic_ptree.lexpr list
val preprocess_extension_block :
string ->
(string * Logic_ptree.extended_decl list) ->
string * Logic_ptree.extended_decl 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
module Axiomatics :
State_builder.Hashtbl
with type key = string
and type data = Cil_types.location
val builtin_states : State.t list
Prepare all internal tables before their uses: clear all tables except builtins.
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
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 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
returns all model fields of the same name.
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
.
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.
val find_logic_type : string -> Cil_types.logic_type_info
val find_logic_ctor : string -> Cil_types.logic_ctor_info
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_function_gen
for more information about the is_same_profile
argument.
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.
removes the given logic constructor. Does nothing if no such constructor exists.
marks temporarily a typename as being a normal identifier in the logic
marks builtin logical types as logical typenames for the logic lexer.
val set_extension_handler :
category:(string -> Cil_types.ext_category) ->
is_extension:(string -> bool) ->
preprocess:(string -> Logic_ptree.lexpr list -> Logic_ptree.lexpr list) ->
is_extension_block:(string -> bool) ->
preprocess_block:
(string ->
(string * Logic_ptree.extended_decl list) ->
string * Logic_ptree.extended_decl list) ->
unit
Used to setup references related to the handling of ACSL extensions. If your name is not Acsl_extension
, do not call this
val init_dependencies : State.t -> unit
Used to postpone dependency of Lenv global tables wrt Cil_state, which is initialized afterwards.