module Computer: functor (
Abstract
:
Abstractions.Eva
) ->
functor (
States
:
Powerset.S
with type state = Abstract.Dom.t
) ->
functor (
Transfer
:
Transfer_stmt.S
with type state = Abstract.Dom.t
and type value = Abstract.Val.t
) ->
functor (
Init
:
Initialization.S
with type state := Abstract.Dom.t
) ->
functor (
Logic
:
Transfer_logic.S
with type state = Abstract.Dom.t
and type states = States.t
) ->
functor (
Spec
:
sig
end
) ->
sig
.. end
Parameters: |
Abstract |
: |
Abstractions.Eva
|
States |
: |
Powerset.S with type state = Abstract.Dom.t
|
Transfer |
: |
Transfer_stmt.S with type state = Abstract.Dom.t
and type value = Abstract.Val.t
|
Init |
: |
Initialization.S with type state := Abstract.Dom.t
|
Logic |
: |
Transfer_logic.S with type state = Abstract.Dom.t
and type states = States.t
|
Spec |
: |
sig
val treat_statement_assigns: assigns -> Abstract.Dom.t -> Abstract.Dom.t
end
|
|
val compute : Cil_types.kernel_function ->
Cil_types.kinstr ->
Abstract.Dom.t -> Abstract.Dom.t list Eval.or_bottom * Value_types.cacheable