sig
type state
type return
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, Abstract_domain.Transfer.return,
Abstract_domain.Transfer.value)
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 make_return :
Cil_types.kernel_function ->
Cil_types.stmt ->
Abstract_domain.Transfer.value Eval.assigned ->
Abstract_domain.Transfer.valuation ->
Abstract_domain.Transfer.state -> Abstract_domain.Transfer.return
val assign_return :
Cil_types.stmt ->
Abstract_domain.Transfer.location Eval.left_value ->
Cil_types.kernel_function ->
Abstract_domain.Transfer.return ->
Abstract_domain.Transfer.value Eval.assigned ->
Abstract_domain.Transfer.valuation ->
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.return,
Abstract_domain.Transfer.value)
Eval.call_result
val enter_loop :
Cil_types.stmt ->
Abstract_domain.Transfer.state -> Abstract_domain.Transfer.state
val incr_loop_counter :
Cil_types.stmt ->
Abstract_domain.Transfer.state -> Abstract_domain.Transfer.state
val leave_loop :
Cil_types.stmt ->
Abstract_domain.Transfer.state -> Abstract_domain.Transfer.state
end