sig
type value = M.loc Memory.value
type logic = M.loc Memory.logic
type sigma = M.Sigma.t
type chunk = M.Chunk.t
type frame = LogicCompiler.Make(M).frame
val pp_frame : Format.formatter -> frame -> unit
val frame : Cil_types.kernel_function -> frame
val frame_copy : frame -> frame
val call_pre : Cil_types.kernel_function -> value list -> sigma -> frame
val call_post :
Cil_types.kernel_function -> value list -> sigma Memory.sequence -> frame
val formal : Cil_types.varinfo -> value option
val return : unit -> Cil_types.typ
val result : unit -> Lang.F.var
val status : unit -> Lang.F.var
val trigger : Definitions.trigger -> unit
val guards : frame -> Lang.F.pred list
val mem_frame : Clabels.c_label -> sigma
val mem_at_frame : frame -> Clabels.c_label -> sigma
val in_frame : frame -> ('a -> 'b) -> 'a -> 'b
val get_frame : unit -> frame
type env = LogicCompiler.Make(M).env
val new_env : Cil_datatype.Logic_var.t list -> env
val move : env -> sigma -> env
val sigma : env -> sigma
val env_at : env -> Clabels.c_label -> env
val mem_at : env -> Clabels.c_label -> sigma
val env_let : env -> Cil_types.logic_var -> logic -> env
val env_letval : env -> Cil_types.logic_var -> value -> env
val term : env -> Cil_types.term -> Lang.F.term
val pred :
bool -> env -> Cil_types.predicate Cil_types.named -> Lang.F.pred
val logic : env -> Cil_types.term -> logic
val region : env -> Cil_types.term -> M.loc Memory.sloc list
val bootstrap_term : (env -> Cil_types.term -> Lang.F.term) -> unit
val bootstrap_pred :
(bool -> env -> Cil_types.predicate Cil_types.named -> Lang.F.pred) ->
unit
val bootstrap_logic : (env -> Cil_types.term -> logic) -> unit
val bootstrap_region :
(env -> Cil_types.term -> M.loc Memory.sloc list) -> unit
val call_fun :
env ->
Cil_types.logic_info ->
(Cil_types.logic_label * Cil_types.logic_label) list ->
Lang.F.term list -> Lang.F.term
val call_pred :
env ->
Cil_types.logic_info ->
(Cil_types.logic_label * Cil_types.logic_label) list ->
Lang.F.term list -> Lang.F.pred
val logic_var : env -> Cil_types.logic_var -> logic
val lemma : LogicUsage.logic_lemma -> Definitions.dlemma
end