sig
  type state
  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 start_call :
    Cil_types.stmt ->
    Abstract_domain.Transfer.value Eval.call ->
    Abstract_domain.Transfer.valuation ->
    Abstract_domain.Transfer.state ->
    Abstract_domain.Transfer.state Eval.call_action
  val finalize_call :
    Cil_types.stmt ->
    Abstract_domain.Transfer.value Eval.call ->
    pre:Abstract_domain.Transfer.state ->
    post:Abstract_domain.Transfer.state ->
    Abstract_domain.Transfer.state Eval.or_bottom
  val approximate_call :
    Cil_types.stmt ->
    Abstract_domain.Transfer.value Eval.call ->
    Abstract_domain.Transfer.state ->
    Abstract_domain.Transfer.state list Eval.or_bottom
  val show_expr :
    Abstract_domain.Transfer.valuation ->
    Abstract_domain.Transfer.state ->
    Format.formatter -> Cil_types.exp -> unit
end