sig
type state
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 start_call :
Cil_types.stmt ->
Abstract_domain.Transfer.value Eval.call ->
Abstract_domain.Transfer.valuation ->
Abstract_domain.Transfer.state ->
Abstract_domain.Transfer.state Eval.call_action
val finalize_call :
Cil_types.stmt ->
Abstract_domain.Transfer.value Eval.call ->
pre:Abstract_domain.Transfer.state ->
post:Abstract_domain.Transfer.state ->
Abstract_domain.Transfer.state Eval.or_bottom
val approximate_call :
Cil_types.stmt ->
Abstract_domain.Transfer.value Eval.call ->
Abstract_domain.Transfer.state ->
Abstract_domain.Transfer.state list Eval.or_bottom
val show_expr :
Abstract_domain.Transfer.valuation ->
Abstract_domain.Transfer.state ->
Format.formatter -> Cil_types.exp -> unit
end