module Pdg_aux:sig
..end
Useful functions that are not directly accessible through the other Pdg modules.
typenode =
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.
typecall_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