Previous  Up  Next

Module Service_graph

module Service_graph: sig .. end

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.

type 'a vertex = private {
   node : 'a;
   mutable is_root : bool;
   mutable root : 'a vertex;
} 
type edge = private
| Inter_services
| Inter_functions
| Both 
module type S = sig .. end

Output signature for services.

module Make: 
functor (G : sig
type t 
module V: sig .. end
val iter_vertex : (V.t -> unit) -> t -> unit
val iter_succ : (V.t -> unit) ->
       t -> V.t -> unit
val iter_pred : (V.t -> unit) ->
       t -> V.t -> unit
val fold_pred : (V.t -> 'a -> 'a) ->
       t -> V.t -> 'a -> 'a
val datatype_name : string
end) -> S  with type node = G.V.t and type graph = G.t

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