Functor Initialization.Make

module Make: 
functor (Domain : Abstract_domain.External-> 
functor (Eva : Evaluation.S with type state = Domain.state and type loc = Domain.location-> 
functor (Transfer : Transfer_stmt.S with type state = Domain.t-> S with type state := Domain.t
Parameters:
Domain : Abstract_domain.External
Eva : Evaluation.S with type state = Domain.state and type loc = Domain.location
Transfer : Transfer_stmt.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_local_variable : Cil_types.stmt ->
Cil_types.varinfo ->
Cil_types.init ->
state -> state Bottom.Type.or_bottom

Initializes a local variable in the current state.