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
    type state = t
    type value = value
    type location = location
    type valuation = Valuation.t
    val update : valuation -> state -> state
    val assign :
      Cil_types.kinstr ->
      location Eval.left_value ->
      Cil_types.exp ->
      value Eval.assigned -> valuation -> state -> state Eval.or_bottom
    val assume :
      Cil_types.stmt ->
      Cil_types.exp -> bool -> valuation -> state -> state Eval.or_bottom
    val start_call :
      Cil_types.stmt ->
      value Eval.call -> valuation -> state -> state Eval.call_action
    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
  end