Module Frama_c_kernel.Service_graph

Compute services from a callgraph.

val frama_c_display : bool -> unit

must be set to false before output the graph in dot format and must be set to true in order to display the graph in the Frama-C GUI.

  • since Oxygen-20120901
type 'a vertex = private {
  1. node : 'a;
  2. mutable is_root : bool;
  3. mutable root : 'a vertex;
}
type edge = private
  1. | Inter_services
  2. | Inter_functions
  3. | Both
module type S = sig ... end

Output signature for services.

module Make (G : sig ... end) : S with type node = G.V.t and type graph = G.t

Generic functor implementing the services algorithm according to a graph implementation.