Module Compute_impact

module Compute_impact: sig .. end

Initial

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.

type nodes = Pdg_aux.NS.t

type result = nodes Kernel_function.Map.t

val initial_nodes : skip:Locations.Zone.t ->
       Cil_types.kernel_function -> Cil_types.stmt -> PdgTypes.Node.t list

To compute the impact of a statement, find the initial PDG nodes that must be put in the worklist. The only subtlety consists in skipping input nodes on statements that are calls; otherwise, we would get an impact in the callees of the call.

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

Impact of a list stmts coming from the same function

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

Impact of a list of PDG nodes coming from the same function

val stmts_impacted : ?skip:Locations.Zone.t ->
       reason:bool ->
       Cil_types.kernel_function -> Cil_types.stmt list -> Cil_types.stmt list

Impact of a list of statements as a set of statements

val nodes_impacted : ?skip:Locations.Zone.t ->
       reason:bool ->
       Cil_types.kernel_function -> PdgTypes.Node.t list -> nodes

Impact of a list of PDG nodes as a set of nodes

val result_to_nodes : result -> nodes

Transform the result of an analysis into a set of PDG nodes

val nodes_to_stmts : nodes -> Cil_types.stmt list

Transform a set of PDG nodes into a set of statements

val impact_in_kf : result -> Cil_types.kernel_function -> nodes

Nodes impacted in a given function

val skip : unit -> Locations.Zone.t

computed from the option -impact-skip

Computation of the skip field from the -impact-skip option