sig
type state
type value
type location
type origin
val update :
(Abstract_domain.Transfer.value, Abstract_domain.Transfer.location,
Abstract_domain.Transfer.origin)
Abstract_domain.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.value, Abstract_domain.Transfer.location,
Abstract_domain.Transfer.origin)
Abstract_domain.valuation ->
Abstract_domain.Transfer.state ->
Abstract_domain.Transfer.state Eval.or_bottom
val assume :
Cil_types.stmt ->
Cil_types.exp ->
bool ->
(Abstract_domain.Transfer.value, Abstract_domain.Transfer.location,
Abstract_domain.Transfer.origin)
Abstract_domain.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 ->
Eval.recursion option ->
(Abstract_domain.Transfer.value, Abstract_domain.Transfer.location,
Abstract_domain.Transfer.origin)
Abstract_domain.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 ->
Eval.recursion option ->
pre:Abstract_domain.Transfer.state ->
post:Abstract_domain.Transfer.state ->
Abstract_domain.Transfer.state Eval.or_bottom
val show_expr :
(Abstract_domain.Transfer.value, Abstract_domain.Transfer.location,
Abstract_domain.Transfer.origin)
Abstract_domain.valuation ->
Abstract_domain.Transfer.state ->
Stdlib.Format.formatter -> Cil_types.exp -> unit
end