Impact.Reason_graph
type reason_type =
| Intraprocedural of Pdg_types.PdgTypes.Dpd.t | (* The effect of |
| InterproceduralDownward | (* the effect of |
| InterproceduralUpward | (* the effect of |
Why is a node impacted. The reasons will be given as n is impacted
by the effect of [n'], and the impact is of type reason
.
module ReasonType : Frama_c_kernel.Datatype.S with type t = reason_type
module Reason :
Frama_c_kernel.Datatype.S_with_collections
with type t =
Pdg_types.PdgTypes.Node.t * Pdg_types.PdgTypes.Node.t * reason_type
type reason_graph = Reason.Set.t
type nodes_origin =
Frama_c_kernel.Cil_types.kernel_function Pdg_types.PdgTypes.Node.Map.t
Map from a node to the kernel_function it belongs to
type reason = {
reason_graph : reason_graph; |
nodes_origin : nodes_origin; |
initial_nodes : Pdg_aux.NS.t; |
}
module DatatypeReason : Frama_c_kernel.Datatype.S with type t = reason
val empty : reason
val to_dot_formatter :
?in_kf:Frama_c_kernel.Cil_types.kernel_function ->
reason ->
Stdlib.Format.formatter ->
unit
val print_dot_graph : reason -> unit