sig
  type state
  type value
  type location
  type valuation
  val update :
    Abstract_domain.Transfer.valuation ->
    Abstract_domain.Transfer.state ->
    Abstract_domain.Transfer.state Eval.or_bottom
  val assign :
    Cil_types.kinstr ->
    Abstract_domain.Transfer.location Eval.left_value ->
    Cil_types.exp ->
    (Abstract_domain.Transfer.location, 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.location, Abstract_domain.Transfer.value)
    Eval.call ->
    Abstract_domain.Transfer.valuation ->
    Abstract_domain.Transfer.state ->
    Abstract_domain.Transfer.state Eval.or_bottom
  val finalize_call :
    Cil_types.stmt ->
    (Abstract_domain.Transfer.location, Abstract_domain.Transfer.value)
    Eval.call ->
    pre:Abstract_domain.Transfer.state ->
    post:Abstract_domain.Transfer.state ->
    Abstract_domain.Transfer.state Eval.or_bottom
  val show_expr :
    Abstract_domain.Transfer.valuation ->
    Abstract_domain.Transfer.state ->
    Stdlib.Format.formatter -> Cil_types.exp -> unit
end