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 : string -> bool
val is_extension_block : string -> bool
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
val extension_from : string -> string

Return the plugin name of the extension

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
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:(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) -> extension_from:(string -> string) -> unit

Used to setup references related to the handling of ACSL extensions. If your name is not Acsl_extension, do not call this

  • since 21.0-Scandium
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