module Make: functor (
Value
:
Abstract_value.S
) ->
functor (
Loc
:
Abstract_location.S
with type value = Value.t
) ->
functor (
Domain
:
Abstract_domain.External
with type value = Value.t
and type location = Loc.location
) ->
functor (
Eva
:
Evaluation.S
with type state = Domain.state
and type value = Domain.value
and type origin = Domain.origin
and type loc = Domain.location
) ->
S
with type state := Domain.t
type
state
val initial_state : unit -> state Bottom.Type.or_bottom
val initial_state_with_formals : Cil_types.kernel_function -> state Bottom.Type.or_bottom