module Make:functor (
Value
:
Abstract_value.External
) ->
functor (
Location
:
Abstract_location.External
) ->
functor (
Domain
:
Abstract_domain.External
with type value = Value.t and type location = Location.location
) ->
functor (
States
:
Powerset.S
with type state = Domain.t
) ->
functor (
Logic
:
Transfer_logic.S
with type state = Domain.t and type states = States.t
) ->
sig
..end
Parameters: |
|
val treat_statement_assigns : Cil_types.assigns -> Domain.t -> Domain.t
val compute_using_specification : Cil_types.kinstr ->
Value.t Eval.call ->
Cil_types.spec -> Domain.t -> Domain.t list Eval.or_bottom