Previous  Up  Next

Module Reason_graph

module Reason_graph: sig .. end
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 NodeSet: PdgTypes.NodeSet
type reason_type =
| Intraprocedural of PdgTypes.Dpd.t (*The effect of n' in f impact n, which is also in f.*)
| InterproceduralDownward (*the effect of n' in f has an effect on a callee f' of f, in which n is located.*)
| InterproceduralUpward (*the effect of n' in f has an effect on a caller f' of f (once the call to f has ended), n being in f'.*)
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: Datatype.Make(sig


type t = Reason_graph.reason_type 




val name : string


val reprs : Reason_graph.reason_type list
include Datatype.Serializable_undefined



val compare : t -> t -> int


val hash : t -> int


val equal : t -> t -> bool


val pretty : Format.formatter -> Reason_graph.reason_type -> unit
end)
module Reason: Datatype.Triple_with_collections(PdgTypes.Node)(PdgTypes.Node)(ReasonType)(sig


val module_name : string
end)
Reasons for impact are expressed as sets (n', n, reason) 
type reason_graph = Reason.Set.t

Map from a node to the kernel_function it belongs to
type nodes_origin = Cil_types.kernel_function PdgTypes.Node.Map.t 
type reason = {
   reason_graph : reason_graph;
   nodes_origin : nodes_origin;
   initial_nodes : Pdg_aux.NS.t;
} 
val empty : reason
module DatatypeReason: Datatype.Make(sig
include Datatype.Serializable_undefined



type t = Reason_graph.reason 




val name : string


val reprs : Reason_graph.reason list
end)
module type AdditionalInfo = sig .. end
module Printer: 
functor (X : AdditionalInfo) -> sig .. end
module Dot: 
functor (X : AdditionalInfo) -> Graph.Graphviz.Dot(Printer(X))
val to_dot_file : temp:bool ->
       ?in_kf:Cil_types.kernel_function -> reason -> string
val print_dot_graph : reason -> unit
val print_reason : Reason.Set.t -> unit