functor
  (Valuation : sig
                 type t
                 type value = value
                 type origin = origin
                 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
    val update : Valuation.t -> t -> t Eval.or_bottom
    val assign :
      Cil_types.kinstr ->
      location Eval.left_value ->
      Cil_types.exp ->
      (location, value) Eval.assigned -> Valuation.t -> t -> t Eval.or_bottom
    val assume :
      Cil_types.stmt ->
      Cil_types.exp -> bool -> Valuation.t -> t -> t Eval.or_bottom
    val start_call :
      Cil_types.stmt ->
      (location, value) Eval.call -> Valuation.t -> t -> t Eval.or_bottom
    val finalize_call :
      Cil_types.stmt ->
      (location, value) Eval.call -> pre:t -> post:t -> t Eval.or_bottom
    val show_expr :
      Valuation.t -> t -> Format.formatter -> Cil_types.exp -> unit
  end