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