sig
  type kind = CPtr | Ptr | Data of Cil_types.typ
  type action = Strip | Id
  type param = string * Mem_utils.kind * Mem_utils.action
  type proto = Mem_utils.kind * Mem_utils.param list
  module type Function =
    sig
      val name : string
      val prototype : unit -> Mem_utils.proto
      val well_typed : Cil_types.typ option -> Cil_types.typ list -> bool
    end
  module Make :
    functor (F : Function->
      sig
        val generate_function_type : Cil_types.typ -> Cil_types.typ
        val generate_prototype : Cil_types.typ -> string * Cil_types.typ
        val well_typed_call :
          Cil_types.lval option ->
          Cil_types.varinfo -> Cil_types.exp list -> bool
        val retype_args :
          Cil_types.typ -> Cil_types.exp list -> Cil_types.exp list
        val key_from_call :
          Cil_types.lval option ->
          Cil_types.varinfo -> Cil_types.exp list -> Cil_types.typ
      end
  type 'a spec_gen =
      Cil_types.location ->
      Cil_types.typ ->
      Cil_types.term -> Cil_types.term -> Cil_types.term -> 'a
  val mem2s_spec :
    requires:Cil_types.identified_predicate list Mem_utils.spec_gen ->
    assigns:Cil_types.assigns Mem_utils.spec_gen ->
    ensures:(Cil_types.termination_kind * Cil_types.identified_predicate)
            list Mem_utils.spec_gen ->
    Cil_types.typ ->
    Cil_types.location -> Cil_types.fundec -> Cil_types.funspec
  val mem2s_typing : Cil_types.typ option -> Cil_types.typ list -> bool
  val memcpy_memmove_common_requires :
    Cil_types.identified_predicate list Mem_utils.spec_gen
  val memcpy_memmove_common_assigns : Cil_types.assigns Mem_utils.spec_gen
  val memcpy_memmove_common_ensures :
    string ->
    (Cil_types.termination_kind * Cil_types.identified_predicate) list
    Mem_utils.spec_gen
  type pointed_expr_type =
      Of_null of Cil_types.typ
    | Value_of of Cil_types.typ
    | No_pointed
  val exp_type_of_pointed : Cil_types.exp -> Mem_utils.pointed_expr_type
end