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 :
      Stdlib.Format.formatter -> Trace_partitioning.Make.store -> unit
    val pretty_flow :
      Stdlib.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