package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct