Frama-C:
Plug-ins:
Libraries:

Frama-C API - Lenv

Local logic environment

type t
val empty : unit -> t

Note that empty still contains the label Init since it is always available.

  • before 31.0-Gallium

    Init was not available in the environment.

val add_var : string -> Cil_types.logic_var -> t -> t
val add_type_var : string -> Cil_types.logic_type -> t -> t
val add_logic_info : string -> Cil_types.logic_info -> t -> t
val add_logic_label : string -> Cil_types.logic_label -> t -> t
val find_var : string -> t -> Cil_types.logic_var
val find_type_var : string -> t -> Cil_types.logic_type
val find_logic_info : string -> t -> Cil_types.logic_info
val find_logic_label : string -> t -> Cil_types.logic_label