sig
  module Make :
    functor
      (Abstract : Abstractions.Eva) (Transfer : sig
                                                  type state = Abstract.Dom.t
                                                  type value
                                                  type location
                                                  val assign :
                                                    state ->
                                                    Cil_types.kinstr ->
                                                    Cil_types.lval ->
                                                    Cil_types.exp ->
                                                    state Eval.or_bottom
                                                  val assume :
                                                    state ->
                                                    Cil_types.stmt ->
                                                    Cil_types.exp ->
                                                    bool ->
                                                    state Eval.or_bottom
                                                  val call :
                                                    Cil_types.stmt ->
                                                    Cil_types.lval option ->
                                                    Cil_types.exp ->
                                                    Cil_types.exp list ->
                                                    state ->
                                                    state list Eval.or_bottom *
                                                    Value_types.cacheable
                                                  val check_unspecified_sequence :
                                                    Cil_types.stmt ->
                                                    state ->
                                                    (Cil_types.stmt *
                                                     Cil_types.lval list *
                                                     Cil_types.lval list *
                                                     Cil_types.lval list *
                                                     Cil_types.stmt ref list)
                                                    list ->
                                                    unit Eval.or_bottom
                                                  val enter_scope :
                                                    Cil_types.kernel_function ->
                                                    Cil_types.varinfo list ->
                                                    state -> state
                                                  type call_result = {
                                                    states :
                                                      state list
                                                      Eval.or_bottom;
                                                    cacheable :
                                                      Value_types.cacheable;
                                                    builtin : bool;
                                                  }
                                                  val compute_call_ref :
                                                    (Cil_types.stmt ->
                                                     (location, value)
                                                     Eval.call ->
                                                     state -> call_result)
                                                    ref
                                                end) (Kf : sig
                                                             val kf :
                                                               Cil_types.kernel_function
                                                           end->
      sig
        type state = Abstract.Dom.t
        type store
        type tank
        type flow
        type widening
        val empty_store :
          stmt:Cil_types.stmt option -> Trace_partitioning.Make.store
        val empty_flow : Trace_partitioning.Make.flow
        val empty_tank : unit -> Trace_partitioning.Make.tank
        val empty_widening :
          stmt:Cil_types.stmt option -> Trace_partitioning.Make.widening
        val initial_tank :
          Trace_partitioning.Make.state list -> Trace_partitioning.Make.tank
        val pretty_store :
          Format.formatter -> Trace_partitioning.Make.store -> unit
        val pretty_flow :
          Format.formatter -> Trace_partitioning.Make.flow -> unit
        val expanded :
          Trace_partitioning.Make.store -> Trace_partitioning.Make.state list
        val smashed :
          Trace_partitioning.Make.store ->
          Trace_partitioning.Make.state Bottom.Type.or_bottom
        val contents :
          Trace_partitioning.Make.flow -> Trace_partitioning.Make.state list
        val is_empty_store : Trace_partitioning.Make.store -> bool
        val is_empty_flow : Trace_partitioning.Make.flow -> bool
        val is_empty_tank : Trace_partitioning.Make.tank -> bool
        val store_size : Trace_partitioning.Make.store -> int
        val flow_size : Trace_partitioning.Make.flow -> int
        val tank_size : Trace_partitioning.Make.tank -> int
        val reset_store : Trace_partitioning.Make.store -> unit
        val reset_tank : Trace_partitioning.Make.tank -> unit
        val reset_widening : Trace_partitioning.Make.widening -> unit
        val reset_widening_counter : Trace_partitioning.Make.widening -> unit
        val enter_loop :
          Trace_partitioning.Make.flow ->
          Cil_types.stmt -> Trace_partitioning.Make.flow
        val leave_loop :
          Trace_partitioning.Make.flow ->
          Cil_types.stmt -> Trace_partitioning.Make.flow
        val next_loop_iteration :
          Trace_partitioning.Make.flow ->
          Cil_types.stmt -> Trace_partitioning.Make.flow
        val split_return :
          Trace_partitioning.Make.flow ->
          Cil_types.exp option -> Trace_partitioning.Make.flow
        val drain :
          Trace_partitioning.Make.tank -> Trace_partitioning.Make.flow
        val fill :
          into:Trace_partitioning.Make.tank ->
          Trace_partitioning.Make.flow -> unit
        val transfer :
          (Trace_partitioning.Make.state ->
           Trace_partitioning.Make.state list) ->
          Trace_partitioning.Make.flow -> Trace_partitioning.Make.flow
        val join :
          (Partition.branch * Trace_partitioning.Make.flow) list ->
          Trace_partitioning.Make.store -> Trace_partitioning.Make.flow
        val widen :
          Trace_partitioning.Make.widening ->
          Trace_partitioning.Make.flow -> Trace_partitioning.Make.flow
      end
end