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 : lib_entry:bool -> state Bottom.Type.or_bottom
Compute the initial state for an analysis. The initial state is generated
according to the options of Value governing the shape of this state.
All global variables are bound in the resulting abstract state.
val initial_state_with_formals : lib_entry:bool ->
Cil_types.kernel_function -> state Bottom.Type.or_bottom
Compute the initial state for an analysis (as in
Initialization.S.initial_state
),
but also bind the formal parameters of the function given as argument.
val initialize_var : with_alarms:CilE.warn_mode ->
Cil_types.stmt ->
Cil_types.varinfo ->
Cil_types.init ->
state -> state Bottom.Type.or_bottom
add to the current state a varinfo with its initialization. Also used
for initializing locals.
Since Phosphorus-20170501-beta1