sig
  type loc = M.loc
  type sigma = M.Sigma.t
  type value = M.loc Memory.value
  type logic = M.loc Memory.logic
  type region = M.loc Memory.sloc list
  val pp_logic : Format.formatter -> logic -> unit
  val pp_sloc : Format.formatter -> loc Memory.sloc -> unit
  val pp_region : Format.formatter -> region -> unit
  type frame = LogicSemantics.Make(M).frame
  val pp_frame : Format.formatter -> frame -> unit
  val get_frame : unit -> frame
  val in_frame : frame -> ('-> 'b) -> '-> 'b
  val mem_frame : Clabels.c_label -> sigma
  val mem_at_frame : frame -> Clabels.c_label -> sigma
  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 return : unit -> Cil_types.typ
  val result : unit -> Lang.F.var
  val status : unit -> Lang.F.var
  val guards : frame -> Lang.F.pred list
  type env = LogicSemantics.Make(M).env
  val new_env : Cil_types.logic_var list -> env
  val move : env -> sigma -> env
  val sigma : env -> sigma
  val mem_at : env -> Clabels.c_label -> sigma
  val call : sigma -> env
  val term : env -> Cil_types.term -> Lang.F.term
  val pred :
    positive:bool ->
    env -> Cil_types.predicate Cil_types.named -> Lang.F.pred
  val region : env -> Cil_types.term -> region
  val assigns :
    env ->
    Cil_types.identified_term Cil_types.assigns ->
    (Ctypes.c_object * region) list option
  val assigns_from :
    env ->
    Cil_types.identified_term Cil_types.from list ->
    (Ctypes.c_object * region) list
  val val_of_term : env -> Cil_types.term -> Lang.F.term
  val loc_of_term : env -> Cil_types.term -> loc
  val lemma : LogicUsage.logic_lemma -> Definitions.dlemma
  val vars : region -> Lang.F.Vars.t
  val occurs : Lang.F.var -> region -> bool
  val valid : sigma -> Memory.acs -> Ctypes.c_object -> region -> Lang.F.pred
  val included :
    Ctypes.c_object -> region -> Ctypes.c_object -> region -> Lang.F.pred
  val separated : (Ctypes.c_object * region) list -> Lang.F.pred
end