Frama-C API - `Logic_env`

Global Logic Environment

registered ACSL extensions

val is_extension : plugin:string -> string -> bool

Return true if an extension is registered for the given plugin.

before Frama-C+def
the function took one less argument, plugin, which is now used to avoid ambiguity if plugins use the same name for an extension

val is_extension_block : plugin:string -> string -> bool

Return true if an extension block is registered for the given plugin.

before Frama-C+def
the function took one less argument, plugin, which is now used to avoid ambiguity if plugins use the same name for an extension

val is_importer : plugin:string -> string -> bool

Return true if a module importer is registered for the given name and plugin.

since 30.0-Zinc

val extension_category : plugin:string -> string -> Cil_types.ext_category

Return the extension category.

raises Not_Found
if the extension is not registered

before Frama-C+def
the function took one less argument, plugin, which is now used to avoid ambiguity if plugins use the same name for an extension

val preprocess_extension : plugin:string -> string -> Logic_ptree.lexpr list -> Logic_ptree.lexpr list

Return the extension preprocessor.

before Frama-C+def
the function took one less argument, plugin, which is now used to avoid ambiguity if plugins use the same name for an extension

val preprocess_extension_block : plugin:string -> string -> (string * Logic_ptree.extended_decl list) -> string * Logic_ptree.extended_decl list

Return the extension block preprocessor.

before Frama-C+def
the function took one less argument, plugin, which is now used to avoid ambiguity if plugins use the same name for an extension

val extension_from : ?plugin:string -> string -> string

Return the plugin name of the ACSL extension. If ~plugin is None, we try to find an extension with this name in our tables (can crash in case of ambiguity), if it is Some we check that this extension exists.

raises Not_Found
If the extension does not exist

raises Log.AbortFatal
If ~plugin is None and two or more extensions have the same name

before 30.0-Zinc
The ~plugin parameter did not exist and the function only performed the None case.

alert acsl_extension_from extension_from is for internal uses only to disambiguate usages of acsl extensions during the lexing phase.

val importer_from : ?plugin:string -> string -> string

Return the plugin name of the module importer extension. If ~plugin is None we try to find an extension with this name in our tables, if it is Some we check that this extension exists.

raises Not_Found
If the importer does not exist

raises Log.AbortFatal
If ~plugin is None and two or more extensions have the same name

since 30.0-Zinc

alert acsl_extension_from importer_from is for internal uses only to disambiguate usages of module importer extensions during the lexing phase.

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

module Modules : State_builder.Hashtbl with type key = string and type data = (string * string) option * Cil_types.location

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.

raises Not_found
if no such type exists.

since Oxygen-20120901

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

removing

val remove_logic_function : string -> unit

removes all overloaded bindings to a given symbol.

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.

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

removes the given logic constructor. Does nothing if no such constructor exists.

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 set_extension_handler : category:(plugin:string -> string -> Cil_types.ext_category) -> is_extension:(plugin:string -> string -> bool) -> is_importer:(plugin:string -> string -> bool) -> preprocess: (plugin:string -> string -> Logic_ptree.lexpr list -> Logic_ptree.lexpr list) -> is_extension_block:(plugin:string -> string -> bool) -> preprocess_block: (plugin:string -> string -> (string * Logic_ptree.extended_decl list) -> string * Logic_ptree.extended_decl list) -> extension_from:(?plugin:string -> string -> string) -> importer_from:(?plugin:string -> string -> string) -> unit

alert acsl_extension_handler This function can only be called by Acsl_extension

val init_dependencies : State.t -> unit

Used to postpone dependency of Lenv global tables wrt Cil_state, which is initialized afterwards.

Frama-C API - Logic_env