sig
  module M : Model
  type loc = M.loc
  type nonrec value = M.loc Wp.Sigs.value
  type nonrec logic = M.loc Wp.Sigs.logic
  type nonrec region = M.loc Wp.Sigs.region
  type nonrec result = M.loc Wp.Sigs.result
  type sigma = M.Sigma.t
  type frame
  val pp_frame :
    Stdlib.Format.formatter -> Wp.Sigs.LogicSemantics.frame -> unit
  val get_frame : unit -> Wp.Sigs.LogicSemantics.frame
  val in_frame : Wp.Sigs.LogicSemantics.frame -> ('-> 'b) -> '-> 'b
  val mem_at_frame :
    Wp.Sigs.LogicSemantics.frame ->
    Wp.Clabels.c_label -> Wp.Sigs.LogicSemantics.sigma
  val set_at_frame :
    Wp.Sigs.LogicSemantics.frame ->
    Wp.Clabels.c_label -> Wp.Sigs.LogicSemantics.sigma -> unit
  val has_at_frame :
    Wp.Sigs.LogicSemantics.frame -> Wp.Clabels.c_label -> bool
  val mem_frame : Wp.Clabels.c_label -> Wp.Sigs.LogicSemantics.sigma
  val mk_frame :
    ?kf:Cil_types.kernel_function ->
    ?result:Wp.Sigs.LogicSemantics.result ->
    ?status:Wp.Lang.F.var ->
    ?formals:Wp.Sigs.LogicSemantics.value Cil_datatype.Varinfo.Map.t ->
    ?labels:Wp.Sigs.LogicSemantics.sigma Wp.Clabels.LabelMap.t ->
    ?descr:string -> unit -> Wp.Sigs.LogicSemantics.frame
  val local : descr:string -> Wp.Sigs.LogicSemantics.frame
  val frame : Cil_types.kernel_function -> Wp.Sigs.LogicSemantics.frame
  type call
  val call :
    ?result:M.loc ->
    Cil_types.kernel_function ->
    Wp.Sigs.LogicSemantics.value list -> Wp.Sigs.LogicSemantics.call
  val call_pre :
    Wp.Sigs.LogicSemantics.sigma ->
    Wp.Sigs.LogicSemantics.call ->
    Wp.Sigs.LogicSemantics.sigma -> Wp.Sigs.LogicSemantics.frame
  val call_post :
    Wp.Sigs.LogicSemantics.sigma ->
    Wp.Sigs.LogicSemantics.call ->
    Wp.Sigs.LogicSemantics.sigma Wp.Sigs.sequence ->
    Wp.Sigs.LogicSemantics.frame
  val return : unit -> Cil_types.typ
  val result : unit -> Wp.Sigs.LogicSemantics.result
  val status : unit -> Wp.Lang.F.var
  val guards : Wp.Sigs.LogicSemantics.frame -> Wp.Lang.F.pred list
  type env
  val mk_env :
    ?here:Wp.Sigs.LogicSemantics.sigma ->
    ?lvars:Cil_types.logic_var list -> unit -> Wp.Sigs.LogicSemantics.env
  val current : Wp.Sigs.LogicSemantics.env -> Wp.Sigs.LogicSemantics.sigma
  val move_at :
    Wp.Sigs.LogicSemantics.env ->
    Wp.Sigs.LogicSemantics.sigma -> Wp.Sigs.LogicSemantics.env
  val mem_at :
    Wp.Sigs.LogicSemantics.env ->
    Wp.Clabels.c_label -> Wp.Sigs.LogicSemantics.sigma
  val env_at :
    Wp.Sigs.LogicSemantics.env ->
    Wp.Clabels.c_label -> Wp.Sigs.LogicSemantics.env
  val lval :
    Wp.Sigs.LogicSemantics.env ->
    Cil_types.term_lval -> Cil_types.typ * M.loc
  val term : Wp.Sigs.LogicSemantics.env -> Cil_types.term -> Wp.Lang.F.term
  val pred :
    Wp.Sigs.polarity ->
    Wp.Sigs.LogicSemantics.env -> Cil_types.predicate -> Wp.Lang.F.pred
  val call_pred :
    Wp.Sigs.LogicSemantics.env ->
    Cil_types.logic_info ->
    Cil_types.logic_label list -> Wp.Lang.F.term list -> Wp.Lang.F.pred
  val region :
    Wp.Sigs.LogicSemantics.env ->
    Cil_types.term -> Wp.Sigs.LogicSemantics.region
  val assigned_of_lval :
    Wp.Sigs.LogicSemantics.env ->
    Cil_types.lval -> Wp.Sigs.LogicSemantics.region
  val assigned_of_froms :
    Wp.Sigs.LogicSemantics.env ->
    Cil_types.from list -> Wp.Sigs.LogicSemantics.region
  val assigned_of_assigns :
    Wp.Sigs.LogicSemantics.env ->
    Cil_types.assigns -> Wp.Sigs.LogicSemantics.region option
  val val_of_term :
    Wp.Sigs.LogicSemantics.env -> Cil_types.term -> Wp.Lang.F.term
  val loc_of_term :
    Wp.Sigs.LogicSemantics.env ->
    Cil_types.term -> Wp.Sigs.LogicSemantics.loc
  val lemma : Wp.LogicUsage.logic_lemma -> Wp.Definitions.dlemma
  val vars : Wp.Sigs.LogicSemantics.region -> Wp.Lang.F.Vars.t
  val occurs : Wp.Lang.F.var -> Wp.Sigs.LogicSemantics.region -> bool
  val check_assigns :
    unfold:int ->
    Wp.Sigs.LogicSemantics.sigma ->
    written:Wp.Sigs.LogicSemantics.region ->
    assignable:Wp.Sigs.LogicSemantics.region -> Wp.Lang.F.pred
end