sig
  type state
  type summary
  type value
  type location
  type valuation
  val update :
    Abstract_domain.Transfer.valuation ->
    Abstract_domain.Transfer.state -> Abstract_domain.Transfer.state
  val assign :
    Cil_types.kinstr ->
    Abstract_domain.Transfer.location Eval.left_value ->
    Cil_types.exp ->
    Abstract_domain.Transfer.value Eval.assigned ->
    Abstract_domain.Transfer.valuation ->
    Abstract_domain.Transfer.state ->
    Abstract_domain.Transfer.state Eval.or_bottom
  val assume :
    Cil_types.stmt ->
    Cil_types.exp ->
    bool ->
    Abstract_domain.Transfer.valuation ->
    Abstract_domain.Transfer.state ->
    Abstract_domain.Transfer.state Eval.or_bottom
  val call_action :
    Cil_types.stmt ->
    Abstract_domain.Transfer.value Eval.call ->
    Abstract_domain.Transfer.valuation ->
    Abstract_domain.Transfer.state ->
    (Abstract_domain.Transfer.state, Abstract_domain.Transfer.summary,
     Abstract_domain.Transfer.value)
    Eval.action
  val summarize :
    Cil_types.kernel_function ->
    Cil_types.stmt ->
    returned:(Abstract_domain.Transfer.location Eval.left_value *
              Abstract_domain.Transfer.value Eval.copied)
             option ->
    Abstract_domain.Transfer.state ->
    (Abstract_domain.Transfer.summary * Abstract_domain.Transfer.state)
    Eval.or_bottom
  val resolve_call :
    Cil_types.stmt ->
    Abstract_domain.Transfer.value Eval.call ->
    assigned:(Abstract_domain.Transfer.location Eval.left_value *
              Abstract_domain.Transfer.value Eval.copied)
             option ->
    Abstract_domain.Transfer.valuation ->
    pre:Abstract_domain.Transfer.state ->
    post:Abstract_domain.Transfer.summary * Abstract_domain.Transfer.state ->
    Abstract_domain.Transfer.state Eval.or_bottom
  val default_call :
    Cil_types.stmt ->
    Abstract_domain.Transfer.value Eval.call ->
    Abstract_domain.Transfer.state ->
    (Abstract_domain.Transfer.state, Abstract_domain.Transfer.summary,
     Abstract_domain.Transfer.value)
    Eval.call_result
end