module Defs: sig
.. end
val get_defs : Kernel_function.t ->
Cil_types.stmt ->
Cil_types.lval ->
(Cil_datatype.Stmt.Hptset.t * Locations.Zone.t option) option
Returns the set of statements that define lval
before stmt
in kf
.
Also returns the zone that is possibly not defined.
Can return None
when the information is not available (Pdg missing).
val get_defs_with_type : Kernel_function.t ->
Cil_types.stmt ->
Cil_types.lval ->
((bool * bool) Cil_datatype.Stmt.Map.t * Locations.Zone.t option) option
Returns a map from the statements that define lval
before stmt
in
kf
. The first boolean indicates the possibility of a direct
modification at this statement, ie. lval = ...
or lval = f()
.
The second boolean indicates a possible indirect modification through
a call.
Also returns the zone that is possibly not defined.
Can return None
when the information is not available (Pdg missing).