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 -> ('-> 'b) -> '-> '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