sig
  type value = Main_values.CVal.t
  type location = Main_locations.PLoc.location
  val find_right_value :
    Cil_types.typ ->
    Cvalue.V_Offsetmap.t ->
    Cvalue_transfer.value Eval.or_bottom Eval.flagged_value
  module Transfer :
    functor
      (Valuation : sig
                     type t
                     type value = value
                     type origin = bool
                     type loc = location
                     val find :
                       t ->
                       Cil_types.exp ->
                       (value, origin) Eval.record_val Eval.or_top
                     val fold :
                       (Cil_types.exp ->
                        (value, origin) Eval.record_val -> '-> 'a) ->
                       t -> '-> 'a
                     val find_loc :
                       t -> Cil_types.lval -> loc Eval.record_loc Eval.or_top
                   end->
      sig
        type state = Cvalue.Model.t
        type summary = Cvalue.V_Offsetmap.t option
        val update : Valuation.t -> state -> state
        val assign :
          Cil_types.kinstr ->
          location Eval.left_value ->
          Cil_types.exp ->
          value Eval.assigned -> Valuation.t -> state -> state Eval.or_bottom
        val assume :
          Cil_types.stmt ->
          Cil_types.exp ->
          bool -> Valuation.t -> state -> state Eval.or_bottom
        val summarize :
          Cil_types.kernel_function ->
          Cil_types.stmt ->
          returned:(location Eval.left_value * value Eval.copied) option ->
          state -> (summary * state) Eval.or_bottom
        val resolve_call :
          Cil_types.stmt ->
          value Eval.call ->
          assigned:(location Eval.left_value * value Eval.copied) option ->
          Valuation.t ->
          pre:state -> post:summary * state -> state Eval.or_bottom
        val default_call :
          Cil_types.stmt ->
          value Eval.call ->
          state -> (state, summary, value) Eval.call_result
        val call_action :
          Cil_types.stmt ->
          Cvalue_transfer.value Eval.call ->
          Valuation.t ->
          state ->
          (state, summary, Cvalue_transfer.value) Eval.action *
          Base.SetLattice.t
      end
end