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