sig
  type polarity = [ `Negative | `NoPolarity | `Positive ]
  module Make :
    functor (M : Sigs.Model->
      sig
        type value = M.loc Sigs.value
        type logic = M.loc Sigs.logic
        type result = M.loc Sigs.result
        type sigma = M.Sigma.t
        type chunk = M.Chunk.t
        type call
        type frame
        val pp_frame :
          Stdlib.Format.formatter -> LogicCompiler.Make.frame -> unit
        val local : descr:string -> LogicCompiler.Make.frame
        val frame : Cil_types.kernel_function -> LogicCompiler.Make.frame
        val call :
          ?result:M.loc ->
          Cil_types.kernel_function ->
          LogicCompiler.Make.value list -> LogicCompiler.Make.call
        val call_pre :
          LogicCompiler.Make.sigma ->
          LogicCompiler.Make.call ->
          LogicCompiler.Make.sigma -> LogicCompiler.Make.frame
        val call_post :
          LogicCompiler.Make.sigma ->
          LogicCompiler.Make.call ->
          LogicCompiler.Make.sigma Sigs.sequence -> LogicCompiler.Make.frame
        val mk_frame :
          ?kf:Cil_types.kernel_function ->
          ?result:LogicCompiler.Make.result ->
          ?status:Lang.F.var ->
          ?formals:LogicCompiler.Make.value Cil_datatype.Varinfo.Map.t ->
          ?labels:LogicCompiler.Make.sigma Clabels.LabelMap.t ->
          ?descr:string -> unit -> LogicCompiler.Make.frame
        val formal : Cil_types.varinfo -> LogicCompiler.Make.value option
        val return : unit -> Cil_types.typ
        val result : unit -> LogicCompiler.Make.result
        val status : unit -> Lang.F.var
        val trigger : Definitions.trigger -> unit
        val guards : LogicCompiler.Make.frame -> Lang.F.pred list
        val mem_frame : Clabels.c_label -> LogicCompiler.Make.sigma
        val has_at_frame :
          LogicCompiler.Make.frame -> Clabels.c_label -> bool
        val mem_at_frame :
          LogicCompiler.Make.frame ->
          Clabels.c_label -> LogicCompiler.Make.sigma
        val set_at_frame :
          LogicCompiler.Make.frame ->
          Clabels.c_label -> LogicCompiler.Make.sigma -> unit
        val in_frame : LogicCompiler.Make.frame -> ('-> 'b) -> '-> 'b
        val get_frame : unit -> LogicCompiler.Make.frame
        type env
        val mk_env :
          ?here:LogicCompiler.Make.sigma ->
          ?lvars:Cil_datatype.Logic_var.t list ->
          unit -> LogicCompiler.Make.env
        val current : LogicCompiler.Make.env -> LogicCompiler.Make.sigma
        val move_at :
          LogicCompiler.Make.env ->
          LogicCompiler.Make.sigma -> LogicCompiler.Make.env
        val env_at :
          LogicCompiler.Make.env -> Clabels.c_label -> LogicCompiler.Make.env
        val mem_at :
          LogicCompiler.Make.env ->
          Clabels.c_label -> LogicCompiler.Make.sigma
        val env_let :
          LogicCompiler.Make.env ->
          Cil_types.logic_var ->
          LogicCompiler.Make.logic -> LogicCompiler.Make.env
        val env_letp :
          LogicCompiler.Make.env ->
          Cil_types.logic_var -> Lang.F.pred -> LogicCompiler.Make.env
        val env_letval :
          LogicCompiler.Make.env ->
          Cil_types.logic_var ->
          LogicCompiler.Make.value -> LogicCompiler.Make.env
        val term : LogicCompiler.Make.env -> Cil_types.term -> Lang.F.term
        val pred :
          LogicCompiler.polarity ->
          LogicCompiler.Make.env -> Cil_types.predicate -> Lang.F.pred
        val logic :
          LogicCompiler.Make.env ->
          Cil_types.term -> LogicCompiler.Make.logic
        val region :
          LogicCompiler.Make.env ->
          unfold:bool -> Cil_types.term -> M.loc Sigs.region
        val bootstrap_term :
          (LogicCompiler.Make.env -> Cil_types.term -> Lang.F.term) -> unit
        val bootstrap_pred :
          (LogicCompiler.polarity ->
           LogicCompiler.Make.env -> Cil_types.predicate -> Lang.F.pred) ->
          unit
        val bootstrap_logic :
          (LogicCompiler.Make.env ->
           Cil_types.term -> LogicCompiler.Make.logic) ->
          unit
        val bootstrap_region :
          (LogicCompiler.Make.env ->
           unfold:bool -> Cil_types.term -> M.loc Sigs.region) ->
          unit
        val call_fun :
          LogicCompiler.Make.env ->
          Lang.F.tau ->
          Cil_types.logic_info ->
          Cil_types.logic_label list -> Lang.F.term list -> Lang.F.term
        val call_pred :
          LogicCompiler.Make.env ->
          Cil_types.logic_info ->
          Cil_types.logic_label list -> Lang.F.term list -> Lang.F.pred
        val logic_var :
          LogicCompiler.Make.env ->
          Cil_types.logic_var -> LogicCompiler.Make.logic
        val logic_info :
          LogicCompiler.Make.env ->
          Cil_types.logic_info -> Lang.F.pred option
        val has_ltype : Cil_types.logic_type -> Lang.F.term -> Lang.F.pred
        val lemma : LogicUsage.logic_lemma -> Definitions.dlemma
      end
end