module Defs: sig
.. end
Find the statements that defines a given data at a program point,
ie. in each backward path starting from this point, find the statement
the the data has been assigned for the last time.
val debug1 : ('a, Format.formatter, unit) Pervasives.format -> 'a
module Interproc: Datascope.R.True
(
sig
val option_name : string
val help : string
end
)
module NSet: PdgTypes.Node.Set
val add_list_to_set : NSet.elt list -> NSet.t -> NSet.t
val _pp_list_node_underout : (unit, Format.formatter, unit, unit, unit, unit) format6 ->
Format.formatter -> (PdgTypes.Node.t * Locations.Zone.t option) list -> unit
val _pp_set : (unit, Format.formatter, unit, unit, unit, unit) format6 ->
Format.formatter -> NSet.t -> unit
val add_callee_nodes : Locations.Zone.t -> NSet.t -> NSet.t -> NSet.t
The nodes nodes
define the searched location z
. If those nodes are calls
to functions, go inside those calls, and find which nodes are relevant.
val add_caller_nodes : Locations.Zone.t ->
Cil_types.kernel_function ->
NSet.t -> Locations.Zone.t option * NSet.t -> NSet.t
kf
doesn't define all the data that we are looking for: the undef
zone must have been defined in its caller, let's find it. z
is the
initial zone that we are looking for, so that we do not look for more
than it.
val compute_aux : Kernel_function.t ->
Cil_types.stmt ->
Cil_types.lval -> (NSet.t * Locations.Zone.t option) option
val compute : Kernel_function.t ->
Cil_types.stmt ->
Cil_types.lval ->
(Cil_datatype.Stmt.Hptset.t * Locations.Zone.t option) option
val compute_with_def_type : Kernel_function.t ->
Cil_types.stmt ->
Cil_types.lval ->
((bool * bool) Cil_datatype.Stmt.Map.t * Locations.Zone.t option) option
module D: Datatype.Option
(
Datatype.Pair
(
Cil_datatype.Stmt.Hptset
)
(
Datatype.Option
(
Locations.Zone
)
)
)
module DT: Datatype.Option
(
Datatype.Pair
(
Cil_datatype.Stmt.Map.Make
(
Datatype.Pair
(
Datatype.Bool
)
(
Datatype.Bool
)
)
)
(
Datatype.Option
(
Locations.Zone
)
)
)