package frama-c

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Program dependence graph main part : the nodes of the graph represent computations, and the edges represent the dependencies between these computations. Only a few functions are exported, to build the graph in pdg/build.ml. Iterating over the PDG should be done using the functions in module Pdg below

type t
module E : sig ... end
val create : unit -> t
val add_elem : t -> PdgIndex.Key.t -> Node.t
val add_dpd : t -> Node.t -> Dpd.td -> Frama_c_kernel.Locations.Zone.t option -> Node.t -> unit