sig
type state
type summary
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 call_action :
Cil_types.stmt ->
Abstract_domain.Transfer.value Eval.call ->
Abstract_domain.Transfer.valuation ->
Abstract_domain.Transfer.state ->
(Abstract_domain.Transfer.state, Abstract_domain.Transfer.summary,
Abstract_domain.Transfer.value)
Eval.action
val summarize :
Cil_types.kernel_function ->
Cil_types.stmt ->
returned:(Abstract_domain.Transfer.location Eval.left_value *
Abstract_domain.Transfer.value Eval.copied)
option ->
Abstract_domain.Transfer.state ->
(Abstract_domain.Transfer.summary * Abstract_domain.Transfer.state)
Eval.or_bottom
val resolve_call :
Cil_types.stmt ->
Abstract_domain.Transfer.value Eval.call ->
assigned:(Abstract_domain.Transfer.location Eval.left_value *
Abstract_domain.Transfer.value Eval.copied)
option ->
Abstract_domain.Transfer.valuation ->
pre:Abstract_domain.Transfer.state ->
post:Abstract_domain.Transfer.summary * Abstract_domain.Transfer.state ->
Abstract_domain.Transfer.state Eval.or_bottom
val default_call :
Cil_types.stmt ->
Abstract_domain.Transfer.value Eval.call ->
Abstract_domain.Transfer.state ->
(Abstract_domain.Transfer.state, Abstract_domain.Transfer.summary,
Abstract_domain.Transfer.value)
Eval.call_result
end