Previous  Up  Next

Module Reason_graph

module Reason_graph: sig .. end
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 : Stdlib.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_formatter : ?in_kf:Cil_types.kernel_function ->
       reason -> Stdlib.Format.formatter -> unit
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