module Reason_graph:sig
..end
module NodeSet: PdgTypes.NodeSet
type
reason_type =
| |
Intraprocedural of |
(* | 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:Datatype.Make
(
sig
typet =
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)
typereason_graph =
Reason.Set.t
Map from a node to the kernel_function it belongs to
typenodes_origin =
Cil_types.kernel_function PdgTypes.Node.Map.t
type
reason = {
|
reason_graph : |
|
nodes_origin : |
|
initial_nodes : |
val empty : reason
module DatatypeReason:Datatype.Make
(
sig
include Datatype.Serializable_undefined
typet =
Reason_graph.reason
val name : string
val reprs : Reason_graph.reason list
end
)
module type AdditionalInfo =sig
..end
module Printer:
module Dot:
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