Module Pdg_aux

module Pdg_aux: sig .. end

Useful functions that are not directly accessible through the other Pdg modules.

find_call_input_nodes pdg_caller s ?z input find all the nodes of pdg_caller that define the pdg input input above the call statement s. If input is an implicit input, its value is refined according to z.

Useful functions that are not directly accessible through the other Pdg modules.

type node = PdgTypes.Node.t * Locations.Zone.t

Refinement of a PDG node: we add an indication of which zone is really impacted

val pretty_node : node Pretty_utils.formatter

module NS: sig .. end

Sets of pairs Node.t * Zone.t, with a special semantics for zones: add n z (add n z' empty) results in (n, Zone.join z z') instead of a set with two different elements.

type call_interface = (PdgTypes.Node.t * NS.t) list

Abstract view of a call frontier. An element n, S of the list is such that n is impacted if one of the nodes of S is impacted.

val all_call_input_nodes : caller:Db.Pdg.t ->
       callee:Cil_types.kernel_function * Db.Pdg.t ->
       Cil_types.stmt -> call_interface

all_call_input_nodes caller callee call_stmt find all the nodes above call_stmt in the pdg of caller that define the inputs of callee. Each input node in callee is returned with the set of nodes that define it in caller.

val all_call_out_nodes : callee:Db.Pdg.t ->
       caller:Db.Pdg.t -> Cil_types.stmt -> call_interface

all_call_out_nodes ~callee ~caller stmt find all the nodes of callee that define the Call/Out nodes of caller for the call to callee that occurs at stmt. Each such out node is returned, with the set of nodes that define it in callee