sig
type t
val dummy : Env.t
val empty : Visitor.frama_c_visitor -> Env.t
val has_no_new_stmt : Env.t -> bool
type localized_scope =
LGlobal
| LFunction of Cil_types.kernel_function
| LLocal_block of Cil_types.kernel_function
val new_var :
loc:Cil_types.location ->
?scope:Varname.scope ->
?name:string ->
Env.t ->
Cil_types.term option ->
Cil_types.typ ->
(Cil_types.varinfo -> Cil_types.exp -> Cil_types.stmt list) ->
Cil_types.varinfo * Cil_types.exp * Env.t
val new_var_and_mpz_init :
loc:Cil_types.location ->
?scope:Varname.scope ->
?name:string ->
Env.t ->
Cil_types.term option ->
(Cil_types.varinfo -> Cil_types.exp -> Cil_types.stmt list) ->
Cil_types.varinfo * Cil_types.exp * Env.t
module Logic_binding :
sig
val add :
?ty:Cil_types.typ ->
Env.t ->
Cil_types.logic_var -> Cil_types.varinfo * Cil_types.exp * Env.t
val add_binding :
Env.t -> Cil_types.logic_var -> Cil_types.varinfo -> Env.t
val get : Env.t -> Cil_types.logic_var -> Cil_types.varinfo
val remove : Env.t -> Cil_types.logic_var -> unit
end
val add_assert : Env.t -> Cil_types.stmt -> Cil_types.predicate -> unit
val add_stmt :
?post:bool -> ?before:Cil_types.stmt -> Env.t -> Cil_types.stmt -> Env.t
val extend_stmt_in_place :
Env.t ->
Cil_types.stmt -> label:Cil_types.logic_label -> Cil_types.block -> Env.t
val push : Env.t -> Env.t
type where = Before | Middle | After
val pop_and_get :
?split:bool ->
Env.t ->
Cil_types.stmt ->
global_clear:bool -> Env.where -> Cil_types.block * Env.t
val pop : Env.t -> Env.t
val transfer : from:Env.t -> Env.t -> Env.t
val get_generated_variables :
Env.t -> (Cil_types.varinfo * Env.localized_scope) list
val get_visitor : Env.t -> Visitor.generic_frama_c_visitor
val get_behavior : Env.t -> Visitor_behavior.t
val current_kf : Env.t -> Cil_types.kernel_function option
module Logic_scope :
sig
val get : Env.t -> Lscope.t
val extend : Env.t -> Lscope.lscope_var -> Env.t
val reset : Env.t -> Env.t
val set_reset : Env.t -> bool -> Env.t
val get_reset : Env.t -> bool
end
val set_current_kf : Env.t -> Cil_types.kernel_function -> unit
val annotation_kind : Env.t -> Misc.annotation_kind
val set_annotation_kind : Env.t -> Misc.annotation_kind -> Env.t
val push_loop : Env.t -> Env.t
val add_loop_invariant : Env.t -> Cil_types.predicate -> Env.t
val pop_loop : Env.t -> Cil_types.predicate list * Env.t
val rte : Env.t -> bool -> Env.t
val generate_rte : Env.t -> bool
module Context :
sig val save : Env.t -> unit val restore : Env.t -> Env.t end
val pretty : Format.formatter -> Env.t -> unit
end