module Compute_impact:sig
..end
Computation of the PDG nodes that are impacted by the "execution"
of some initial PDG nodes. This is implemented as a forward
inter-procedural analysis on top of the PDG plugin.
typenodes =
Pdg_aux.NS.t
typeresult =
nodes Kernel_function.Map.t
val initial_nodes : skip:Locations.Zone.t ->
Cil_types.kernel_function -> Cil_types.stmt -> PdgTypes.Node.t list
val nodes_impacted_by_stmts : ?skip:Locations.Zone.t ->
?restrict:Locations.Zone.t ->
?reason:bool ->
Cil_types.kernel_function ->
Cil_types.stmt list ->
result * nodes Kernel_function.Map.t *
Reason_graph.reason
val nodes_impacted_by_nodes : ?skip:Locations.Zone.t ->
?restrict:Locations.Zone.t ->
?reason:bool ->
Cil_types.kernel_function ->
PdgTypes.Node.t list ->
result * nodes Kernel_function.Map.t *
Reason_graph.reason
val stmts_impacted : ?skip:Locations.Zone.t ->
reason:bool ->
Cil_types.kernel_function -> Cil_types.stmt list -> Cil_types.stmt list
val nodes_impacted : ?skip:Locations.Zone.t ->
reason:bool ->
Cil_types.kernel_function -> PdgTypes.Node.t list -> nodes
val result_to_nodes : result -> nodes
val nodes_to_stmts : nodes -> Cil_types.stmt list
val impact_in_kf : result -> Cil_types.kernel_function -> nodes
val skip : unit -> Locations.Zone.t
-impact-skip
Computation of the skip
field from the -impact-skip
option