module Pdg_aux:sig
..end
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
.
typenode =
PdgTypes.Node.t * Locations.Zone.t
val pretty_node : node Pretty_utils.formatter
module NS:sig
..end
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
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