sig
  type value = Main_values.CVal.t
  type origin = Cvalue_transfer.value
  type location = Main_locations.PLoc.location
  val update :
    (value, location, origin) Abstract_domain.valuation ->
    Cvalue.Model.t -> Cvalue.Model.t Eval.or_bottom
  val assign :
    Cil_types.kinstr ->
    location Eval.left_value ->
    Cil_types.exp ->
    (location, value) Eval.assigned ->
    (value, location, origin) Abstract_domain.valuation ->
    Cvalue.Model.t -> Cvalue.Model.t Eval.or_bottom
  val assume :
    Cil_types.stmt ->
    Cil_types.exp ->
    bool ->
    (value, location, origin) Abstract_domain.valuation ->
    Cvalue.Model.t -> Cvalue.Model.t Eval.or_bottom
  val start_call :
    Cil_types.stmt ->
    (location, value) Eval.call ->
    (value, location, origin) Abstract_domain.valuation ->
    Cvalue.Model.t -> Cvalue.Model.t Eval.or_bottom
  val finalize_call :
    Cil_types.stmt ->
    (location, value) Eval.call ->
    pre:Cvalue.Model.t ->
    post:Cvalue.Model.t -> Cvalue.Model.t Eval.or_bottom
  val show_expr :
    (value, location, origin) Abstract_domain.valuation ->
    Cvalue.Model.t -> Format.formatter -> Cil_types.exp -> unit
end