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