package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Global Logic Environment

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-28.0-Nickel.tar.gz

sha256=29612882330ecb6eddd0b4ca3afc0492b70d0feb3379a1b8e893194c6e173983

doc/frama-c.kernel/Frama_c_kernel/Logic_env/index.html

Module `Frama_c_kernel.Logic_env`

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

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

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