Module Defs

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) Pervasives.format6 ->
Format.formatter -> (PdgTypes.Node.t * Locations.Zone.t option) list -> unit
val _pp_set : (unit, Format.formatter, unit, unit, unit, unit) Pervasives.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)))