sig
type t
val empty : 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.kernel_function ->
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.kernel_function ->
Cil_types.term option ->
(Cil_types.varinfo -> Cil_types.exp -> Cil_types.stmt list) ->
Cil_types.varinfo * Cil_types.exp * Env.t
val rtl_call_to_new_var :
loc:Cil_types.location ->
?scope:Varname.scope ->
?name:string ->
Env.t ->
Cil_types.kernel_function ->
Cil_types.term option ->
Cil_types.typ -> string -> Cil_types.exp list -> Cil_types.exp * Env.t
module Logic_binding :
sig
val add :
?ty:Cil_types.typ ->
Env.t ->
Cil_types.kernel_function ->
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 :
Cil_types.kernel_function ->
Cil_types.stmt -> Cil_types.predicate -> unit
val add_stmt :
?post:bool ->
?before:Cil_types.stmt ->
Env.t -> Cil_types.kernel_function -> 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
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 annotation_kind : Env.t -> Smart_stmt.annotation_kind
val set_annotation_kind : Env.t -> Smart_stmt.annotation_kind -> Env.t
val push_loop : Env.t -> Env.t
val set_loop_variant :
?measure:Cil_types.logic_info -> Env.t -> Cil_types.term -> Env.t
val add_loop_invariant : Env.t -> Cil_types.toplevel_predicate -> Env.t
val top_loop_variant :
Env.t -> (Cil_types.term * Cil_types.logic_info option) option
val top_loop_invariants : Env.t -> Cil_types.toplevel_predicate list
val pop_loop : Env.t -> Env.t
val rte : Env.t -> bool -> Env.t
val generate_rte : Env.t -> bool
val with_rte : f:(Env.t -> Env.t) -> Env.t -> bool -> Env.t
val with_rte_and_result :
f:(Env.t -> 'a * Env.t) -> Env.t -> bool -> 'a * Env.t
module Context :
sig val save : Env.t -> unit val restore : Env.t -> Env.t end
val handle_error : (Env.t -> Env.t) -> Env.t -> Env.t
val handle_error_with_args :
(Env.t * 'a -> Env.t * 'a) -> Env.t * 'a -> Env.t * 'a
val not_yet : Env.t -> string -> 'a
val untypable : Env.t -> string -> 'a
val push_contract : Env.t -> Contract_types.contract -> Env.t
val top_contract :
Env.t -> Contract_types.contract * Contract_types.contract list
val pop_and_get_contract : Env.t -> Contract_types.contract * Env.t
val pop_contract : Env.t -> Env.t
val pretty : Stdlib.Format.formatter -> Env.t -> unit
end