Module PdgTypes.Pdg

module Pdg: sig .. end

PDG for a function


exception Top

can be raised by most of the functions when called with a Top PDG. Top means that we were not able to compute the PDG for this function.

exception Bottom

exception raised when requiring the PDG of a function that is never called.

include Datatype.S
val top : Kernel_function.t -> t
val bottom : Kernel_function.t -> t
val is_top : t -> bool
val is_bottom : t -> bool
val get_kf : t -> Kernel_function.t
val iter_nodes : (PdgTypes.Node.t -> unit) -> t -> unit
val fold_call_nodes : ('a -> PdgTypes.Node.t -> 'a) -> 'a -> t -> Cil_types.stmt -> 'a
val iter_direct_dpds : t -> (PdgTypes.Node.t -> unit) -> PdgTypes.Node.t -> unit
val iter_direct_codpds : t -> (PdgTypes.Node.t -> unit) -> PdgTypes.Node.t -> unit
type dpd_info = PdgTypes.Node.t * Locations.Zone.t option 

a dependency to another node. The dependency can be restricted to a zone. (None means no restriction ie. total dependency)

val get_all_direct_dpds : t -> PdgTypes.Node.t -> dpd_info list
val get_x_direct_dpds : PdgTypes.Dpd.td -> t -> PdgTypes.Node.t -> dpd_info list
val get_all_direct_codpds : t -> PdgTypes.Node.t -> dpd_info list
val get_x_direct_codpds : PdgTypes.Dpd.td -> t -> PdgTypes.Node.t -> dpd_info list
val fold_direct_dpds : t ->
('a -> PdgTypes.Dpd.t * Locations.Zone.t option -> PdgTypes.Node.t -> 'a) ->
'a -> PdgTypes.Node.t -> 'a
val fold_direct_codpds : t ->
('a -> PdgTypes.Dpd.t * Locations.Zone.t option -> PdgTypes.Node.t -> 'a) ->
'a -> PdgTypes.Node.t -> 'a
val pretty_bw : ?bw:bool -> Format.formatter -> t -> unit
val pretty_graph : ?bw:bool -> Format.formatter -> PdgTypes.G.t -> unit
type fi = (PdgTypes.Node.t, unit) PdgIndex.FctIndex.t 

The nodes associated to each element. There is only one node for simple statements, but there are several for a call for instance.

val get_index : t -> fi
val make : Kernel_function.t ->
PdgTypes.G.t ->
PdgTypes.data_state Cil_datatype.Stmt.Hashtbl.t -> fi -> t

make fundec graph states index

val get_states : t -> PdgTypes.data_state Cil_datatype.Stmt.Hashtbl.t
val build_dot : string -> t -> unit

build the PDG .dot file and put it in filename.

module Printer: sig .. end