module Make: functor (
Value
:
Abstract_value.S
) ->
functor (
Location
:
Abstract_location.External
) ->
functor (
Domain
:
Domain
with type value = Value.t
and type location = Location.location
) ->
functor (
Eva
:
Evaluation.S
with type state = Domain.state
and type value = Domain.value
and type loc = Domain.location
and type Valuation.t = Domain.valuation
) ->
S
with type state = Domain.state
and type value = Domain.value
and type return = Domain.return
Parameters: |
Value |
: |
Abstract_value.S
|
Location |
: |
Abstract_location.External
|
Domain |
: |
Domain with type value = Value.t
and type location = Location.location
|
Eva |
: |
Evaluation.S with type state = Domain.state
and type value = Domain.value
and type loc = Domain.location
and type Valuation.t = Domain.valuation
|
|
type
state
type
value
type
return
val assign : with_alarms:CilE.warn_mode ->
state ->
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.lval -> Cil_types.exp -> state Eval.or_bottom
val assume : with_alarms:CilE.warn_mode ->
state ->
Cil_types.stmt ->
Cil_types.exp -> bool -> state Eval.or_bottom
val call : with_alarms:CilE.warn_mode ->
Cil_types.stmt ->
Cil_types.lval option ->
Cil_types.exp ->
Cil_types.exp list ->
state ->
state list Eval.or_bottom * Value_types.cacheable
val return : with_alarms:CilE.warn_mode ->
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.lval option ->
state ->
(state, return, value)
Eval.return_state Eval.or_bottom
val enter_loop : Cil_types.stmt -> state -> state
val incr_loop_counter : Cil_types.stmt -> state -> state
val leave_loop : Cil_types.stmt -> state -> state
val split_final_states : Cil_types.kernel_function ->
Cil_types.exp ->
Integer.t list ->
state list -> state list list
val check_unspecified_sequence : with_alarms:CilE.warn_mode ->
state ->
(Cil_types.stmt * Cil_types.lval list * Cil_types.lval list *
Cil_types.lval list * Cil_types.stmt Pervasives.ref list)
list -> unit Eval.or_bottom
type
res = (state, return, value)
Eval.call_result * Value_types.cacheable
val compute_call_ref : (Cil_types.kinstr ->
value Eval.call ->
state -> res)
Pervasives.ref