functor (M : Memory.Model->
  sig
    type loc = M.loc
    type value = LogicSemantics.Make.loc Memory.value
    type logic = LogicSemantics.Make.loc Memory.logic
    type region = LogicSemantics.Make.loc Memory.sloc list
    type sigma = M.Sigma.t
    module L :
      sig
        type logic = M.loc Memory.logic
        val value : logic -> Lang.F.term
        val loc : logic -> M.loc
        val vset : logic -> Vset.set
        val sloc : logic -> M.loc Memory.sloc list
        val rdescr :
          M.loc Memory.sloc -> Lang.F.var list * M.loc * Lang.F.pred
        val map : Lang.F.unop -> logic -> logic
        val map_opp : logic -> logic
        val map_loc : (M.loc -> M.loc) -> logic -> logic
        val map_l2t : (M.loc -> Lang.F.term) -> logic -> logic
        val map_t2l : (Lang.F.term -> M.loc) -> logic -> logic
        val apply : Lang.F.binop -> logic -> logic -> logic
        val apply_add : logic -> logic -> logic
        val apply_sub : logic -> logic -> logic
        val field : logic -> Cil_types.fieldinfo -> logic
        val shift : logic -> Ctypes.c_object -> ?size:int -> logic -> logic
        val load : M.Sigma.t -> Ctypes.c_object -> logic -> logic
        val union : Cil_types.logic_type -> logic list -> logic
        val inter : Cil_types.logic_type -> logic list -> logic
        type region = M.loc Memory.sloc list
        val separated : (Ctypes.c_object * region) list -> Lang.F.pred
        val included :
          Ctypes.c_object ->
          region -> Ctypes.c_object -> region -> Lang.F.pred
        val valid :
          M.Sigma.t -> Memory.acs -> Ctypes.c_object -> region -> Lang.F.pred
      end
    module C :
      sig
        type value = M.loc Memory.value
        type logic = M.loc Memory.logic
        type sigma = M.Sigma.t
        type chunk = M.Chunk.t
        type frame = LogicCompiler.Make(M).frame
        val pp_frame : Format.formatter -> frame -> unit
        val frame : Cil_types.kernel_function -> frame
        val frame_copy : frame -> frame
        val call_pre :
          Cil_types.kernel_function -> value list -> sigma -> frame
        val call_post :
          Cil_types.kernel_function ->
          value list -> sigma Memory.sequence -> frame
        val formal : Cil_types.varinfo -> value option
        val return : unit -> Cil_types.typ
        val result : unit -> Lang.F.var
        val status : unit -> Lang.F.var
        val trigger : Definitions.trigger -> unit
        val guards : frame -> Lang.F.pred list
        val mem_frame : Clabels.c_label -> sigma
        val mem_at_frame : frame -> Clabels.c_label -> sigma
        val in_frame : frame -> ('-> 'b) -> '-> 'b
        val get_frame : unit -> frame
        type env = LogicCompiler.Make(M).env
        val new_env : Cil_datatype.Logic_var.t list -> env
        val move : env -> sigma -> env
        val sigma : env -> sigma
        val env_at : env -> Clabels.c_label -> env
        val mem_at : env -> Clabels.c_label -> sigma
        val env_let : env -> Cil_types.logic_var -> logic -> env
        val env_letval : env -> Cil_types.logic_var -> value -> env
        val term : env -> Cil_types.term -> Lang.F.term
        val pred :
          bool -> env -> Cil_types.predicate Cil_types.named -> Lang.F.pred
        val logic : env -> Cil_types.term -> logic
        val region : env -> Cil_types.term -> M.loc Memory.sloc list
        val bootstrap_term : (env -> Cil_types.term -> Lang.F.term) -> unit
        val bootstrap_pred :
          (bool -> env -> Cil_types.predicate Cil_types.named -> Lang.F.pred) ->
          unit
        val bootstrap_logic : (env -> Cil_types.term -> logic) -> unit
        val bootstrap_region :
          (env -> Cil_types.term -> M.loc Memory.sloc list) -> unit
        val call_fun :
          env ->
          Cil_types.logic_info ->
          (Cil_types.logic_label * Cil_types.logic_label) list ->
          Lang.F.term list -> Lang.F.term
        val call_pred :
          env ->
          Cil_types.logic_info ->
          (Cil_types.logic_label * Cil_types.logic_label) list ->
          Lang.F.term list -> Lang.F.pred
        val logic_var : env -> Cil_types.logic_var -> logic
        val lemma : LogicUsage.logic_lemma -> Definitions.dlemma
      end
    type frame = LogicSemantics.Make.C.frame
    val pp_frame : Format.formatter -> LogicSemantics.Make.C.frame -> unit
    val get_frame : unit -> LogicSemantics.Make.C.frame
    val in_frame : LogicSemantics.Make.C.frame -> ('-> 'b) -> '-> 'b
    val mem_frame : Clabels.c_label -> LogicSemantics.Make.C.sigma
    val mem_at_frame :
      LogicSemantics.Make.C.frame ->
      Clabels.c_label -> LogicSemantics.Make.C.sigma
    val mem_at :
      LogicSemantics.Make.C.env ->
      Clabels.c_label -> LogicSemantics.Make.C.sigma
    val frame : Cil_types.kernel_function -> LogicSemantics.Make.C.frame
    val frame_copy :
      LogicSemantics.Make.C.frame -> LogicSemantics.Make.C.frame
    val call_pre :
      Cil_types.kernel_function ->
      LogicSemantics.Make.C.value list ->
      LogicSemantics.Make.C.sigma -> LogicSemantics.Make.C.frame
    val call_post :
      Cil_types.kernel_function ->
      LogicSemantics.Make.C.value list ->
      LogicSemantics.Make.C.sigma Memory.sequence ->
      LogicSemantics.Make.C.frame
    val return : unit -> Cil_types.typ
    val result : unit -> Lang.F.var
    val status : unit -> Lang.F.var
    val guards : LogicSemantics.Make.C.frame -> Lang.F.pred list
    val pp_logic : Format.formatter -> M.loc Memory.logic -> unit
    val pp_bound : Format.formatter -> Lang.F.term option -> unit
    val pp_sloc : Format.formatter -> M.loc Memory.sloc -> unit
    val pp_region : Format.formatter -> M.loc Memory.sloc list -> unit
    type env = LogicSemantics.Make.C.env
    val new_env : Cil_datatype.Logic_var.t list -> LogicSemantics.Make.C.env
    val move :
      LogicSemantics.Make.C.env ->
      LogicSemantics.Make.C.sigma -> LogicSemantics.Make.C.env
    val sigma : LogicSemantics.Make.C.env -> LogicSemantics.Make.C.sigma
    val call : LogicSemantics.Make.C.sigma -> LogicSemantics.Make.C.env
    val logic_of_value : 'Memory.value -> 'Memory.logic
    val loc_of_term : LogicSemantics.Make.C.env -> Cil_types.term -> M.loc
    val val_of_term :
      LogicSemantics.Make.C.env -> Cil_types.term -> Lang.F.term
    val set_of_term : LogicSemantics.Make.C.env -> Cil_types.term -> Vset.set
    val collection_of_term :
      LogicSemantics.Make.C.env ->
      Cil_types.term -> LogicSemantics.Make.C.logic
    val term : LogicSemantics.Make.C.env -> Cil_types.term -> Lang.F.term
    val access_offset :
      LogicSemantics.Make.C.env ->
      LogicSemantics.Make.logic ->
      Cil_types.term_offset -> LogicSemantics.Make.logic
    val update_offset :
      LogicSemantics.Make.C.env ->
      Lang.F.term -> Cil_types.term_offset -> Lang.F.term -> Lang.F.term
    val shift_offset :
      LogicSemantics.Make.C.env ->
      Cil_types.typ ->
      LogicSemantics.Make.logic ->
      Cil_types.term_offset -> Cil_types.typ * LogicSemantics.Make.logic
    type lv_value =
        VAL of LogicSemantics.Make.logic
      | VAR of Cil_types.varinfo
    val logic_var :
      LogicSemantics.Make.C.env ->
      Cil_types.logic_var -> LogicSemantics.Make.lv_value
    val load_loc :
      LogicSemantics.Make.C.env ->
      Cil_types.typ ->
      LogicSemantics.Make.loc ->
      Cil_types.term_offset -> LogicSemantics.Make.L.logic
    val term_lval :
      LogicSemantics.Make.C.env ->
      Cil_types.term_lhost * Cil_types.term_offset ->
      LogicSemantics.Make.logic
    val addr_lval :
      LogicSemantics.Make.C.env ->
      Cil_types.term_lhost * Cil_types.term_offset ->
      LogicSemantics.Make.logic
    val term_unop :
      Cil_types.unop ->
      LogicSemantics.Make.L.logic -> LogicSemantics.Make.L.logic
    type eqsort =
        EQ_set
      | EQ_loc
      | EQ_plain
      | EQ_array of Matrix.matrix
      | EQ_comp of Cil_types.compinfo
      | EQ_incomparable
    val eqsort_of_type : Cil_types.logic_type -> LogicSemantics.Make.eqsort
    val eqsort_of_comparison :
      Cil_types.term -> Cil_types.term -> LogicSemantics.Make.eqsort
    val use_equal : bool -> bool
    val term_equal :
      bool ->
      LogicSemantics.Make.C.env ->
      Cil_types.term -> Cil_types.term -> Lang.F.pred
    val term_diff :
      bool ->
      LogicSemantics.Make.C.env ->
      Cil_types.term -> Cil_types.term -> Lang.F.pred
    val compare_term :
      LogicSemantics.Make.C.env ->
      (Lang.F.term -> Lang.F.term -> 'a) ->
      (M.loc -> M.loc -> 'a) -> Cil_types.term -> Cil_types.term -> 'a
    val exp_equal :
      LogicSemantics.Make.C.env ->
      Cil_types.term -> Cil_types.term -> 'Memory.logic
    val exp_diff :
      LogicSemantics.Make.C.env ->
      Cil_types.term -> Cil_types.term -> 'Memory.logic
    val exp_compare :
      LogicSemantics.Make.C.env ->
      (Lang.F.term -> Lang.F.term -> Lang.F.pred) ->
      (M.loc -> M.loc -> Lang.F.pred) ->
      Cil_types.term -> Cil_types.term -> 'Memory.logic
    val toreal :
      bool -> LogicSemantics.Make.L.logic -> LogicSemantics.Make.L.logic
    val arith :
      LogicSemantics.Make.C.env ->
      (LogicSemantics.Make.C.logic -> LogicSemantics.Make.C.logic -> 'a) ->
      (LogicSemantics.Make.L.logic -> LogicSemantics.Make.L.logic -> 'a) ->
      Cil_types.term -> Cil_types.term -> 'a
    val term_binop :
      LogicSemantics.Make.C.env ->
      Cil_types.binop ->
      Cil_types.term -> Cil_types.term -> LogicSemantics.Make.L.logic
    type cvsort =
        L_real
      | L_integer
      | L_cint of Ctypes.c_int
      | L_cfloat of Ctypes.c_float
      | L_pointer of Cil_types.typ
    val cvsort_of_type : Cil_types.logic_type -> LogicSemantics.Make.cvsort
    val term_cast :
      LogicSemantics.Make.C.env ->
      Cil_types.typ -> Cil_types.term -> LogicSemantics.Make.C.logic
    val bind_quantifiers :
      LogicSemantics.Make.env ->
      Cil_types.logic_var list ->
      Lang.F.var list * LogicSemantics.Make.C.env * Lang.F.pred list
    val term_node :
      LogicSemantics.Make.env -> Cil_types.term -> LogicSemantics.Make.logic
    val separated_terms :
      LogicSemantics.Make.C.env -> Cil_types.term list -> Lang.F.pred
    val relation :
      bool ->
      LogicSemantics.Make.C.env ->
      Cil_types.relation -> Cil_types.term -> Cil_types.term -> Lang.F.pred
    val valid :
      C.env ->
      Memory.acs -> Cil_types.logic_label -> Cil_types.term -> Lang.F.pred
    val predicate :
      bool ->
      LogicSemantics.Make.C.env ->
      Cil_types.predicate Cil_types.named -> Lang.F.pred
    val assignable_lval :
      LogicSemantics.Make.C.env ->
      Cil_types.term_lhost * Cil_types.term_offset -> M.loc Memory.sloc list
    val assignable :
      LogicSemantics.Make.C.env -> Cil_types.term -> M.loc Memory.sloc list
    val term_trigger :
      LogicSemantics.Make.env -> Cil_types.term -> LogicSemantics.Make.logic
    val pred_trigger :
      bool ->
      LogicSemantics.Make.C.env ->
      Cil_types.predicate Cil_types.named -> Lang.F.pred
    val pred :
      positive:bool ->
      LogicSemantics.Make.C.env ->
      Cil_types.predicate Cil_types.named -> Lang.F.pred
    val logic :
      LogicSemantics.Make.env -> Cil_types.term -> LogicSemantics.Make.logic
    val region :
      LogicSemantics.Make.C.env -> Cil_types.term -> M.loc Memory.sloc list
    val lemma : LogicUsage.logic_lemma -> Definitions.dlemma
    val assigns_from :
      LogicSemantics.Make.C.env ->
      (Cil_types.identified_term * 'a) list ->
      (Ctypes.c_object * M.loc Memory.sloc list) list
    val assigns :
      LogicSemantics.Make.C.env ->
      Cil_types.identified_term Cil_types.assigns ->
      (Ctypes.c_object * M.loc Memory.sloc list) list option
    val valid :
      M.Sigma.t ->
      Memory.acs ->
      Ctypes.c_object -> LogicSemantics.Make.L.region -> Lang.F.pred
    val included :
      Ctypes.c_object ->
      LogicSemantics.Make.L.region ->
      Ctypes.c_object -> LogicSemantics.Make.L.region -> Lang.F.pred
    val separated :
      (Ctypes.c_object * LogicSemantics.Make.L.region) list -> Lang.F.pred
    val occurs_opt : Lang.F.var -> Lang.F.term option -> bool
    val occurs_sloc : Lang.F.var -> M.loc Memory.sloc -> bool
    val occurs : Lang.F.var -> M.loc Memory.sloc list -> bool
    val vars_opt : Lang.F.term option -> Lang.F.Vars.t
    val vars_sloc : M.loc Memory.sloc -> Lang.F.Vars.t
    val vars : M.loc Memory.sloc list -> Lang.F.Vars.t
  end