sig
  type value = Main_values.CVal.t
  type location = Main_locations.PLoc.location
  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
        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 finalize_call :
          Cil_types.stmt ->
          value Eval.call -> pre:state -> post:state -> state Eval.or_bottom
        val approximate_call :
          Cil_types.stmt ->
          value Eval.call -> state -> state list Eval.or_bottom
        val show_expr :
          Valuation.t -> state -> Format.formatter -> Cil_types.exp -> unit
        val start_call :
          Cil_types.stmt ->
          Cvalue_transfer.value Eval.call ->
          Valuation.t -> state -> state Eval.call_action * Base.SetLattice.t
      end
end