sig
type t
val dummy : Env.t
val empty : Visitor.frama_c_visitor -> Env.t
val has_no_new_stmt : Env.t -> bool
type scope = Global | Function | Local_block
val new_var :
loc:Cil_types.location ->
?init:bool ->
?scope:Env.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 ->
?init:bool ->
?scope:Env.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 get : Env.t -> Cil_types.logic_var -> Cil_types.varinfo
val remove : Env.t -> Cil_types.logic_var -> Env.t
end
val add_assert : Env.t -> Cil_types.stmt -> Cil_types.predicate -> unit
val add_stmt :
?init:bool -> ?before:Cil_types.stmt -> Env.t -> Cil_types.stmt -> Env.t
val extend_stmt_in_place :
Env.t -> Cil_types.stmt -> pre:bool -> 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.scope) list
val get_visitor : Env.t -> Visitor.generic_frama_c_visitor
val get_behavior : Env.t -> Cil.visitor_behavior
val current_kf : Env.t -> Cil_types.kernel_function option
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