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 summary = summary
    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 call_action :
      Cil_types.stmt ->
      value Eval.call ->
      valuation -> state -> (state, summary, value) Eval.action
    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 -> 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
  end