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