package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c.kernel/Frama_c_kernel/Service_graph/Make/TP/index.html

Module `Make.TP`

since Beryllium-20090902

include Graph.Sig.G
  with type t = Service_graph.t
  with type V.t = node vertex
  with type E.t = Service_graph.E.t

Graph structure

type t = Service_graph.t

Abstract type of graphs

module V : Graph.Sig.VERTEX with type t = node vertex

Vertices have type V.t and are labeled with type V.label (note that an implementation may identify the vertex with its label)

type vertex = V.t

module E : 
  Graph.Sig.EDGE with type vertex = vertex with type t = Service_graph.E.t

Edges have type E.t and are labeled with type E.label. src (resp. dst) returns the origin (resp. the destination) of a given edge.

type edge = E.t

val is_directed : bool

Is this an implementation of directed graphs?

Size functions

val is_empty : t -> bool

val nb_vertex : t -> int

val nb_edges : t -> int

Degree of a vertex

val out_degree : t -> vertex -> int

out_degree g v returns the out-degree of v in g.

raises Invalid_argument
if v is not in g.

val in_degree : t -> vertex -> int

in_degree g v returns the in-degree of v in g.

raises Invalid_argument
if v is not in g.

Membership functions

val mem_vertex : t -> vertex -> bool

val mem_edge : t -> vertex -> vertex -> bool

val mem_edge_e : t -> edge -> bool

val find_edge : t -> vertex -> vertex -> edge

find_edge g v1 v2 returns the edge from v1 to v2 if it exists. Unspecified behaviour if g has several edges from v1 to v2.

raises Not_found
if no such edge exists.

val find_all_edges : t -> vertex -> vertex -> edge list

find_all_edges g v1 v2 returns all the edges from v1 to v2.

since ocamlgraph 1.8

Successors and predecessors

You should better use iterators on successors/predecessors (see Section "Vertex iterators").

val succ : t -> vertex -> vertex list

succ g v returns the successors of v in g.

raises Invalid_argument
if v is not in g.

val pred : t -> vertex -> vertex list

pred g v returns the predecessors of v in g.

raises Invalid_argument
if v is not in g.

Labeled edges going from/to a vertex

val succ_e : t -> vertex -> edge list

succ_e g v returns the edges going from v in g.

raises Invalid_argument
if v is not in g.

val pred_e : t -> vertex -> edge list

pred_e g v returns the edges going to v in g.

raises Invalid_argument
if v is not in g.

Graph iterators

val iter_vertex : (vertex -> unit) -> t -> unit

Iter on all vertices of a graph.

val fold_vertex : (vertex -> 'a -> 'a) -> t -> 'a -> 'a

Fold on all vertices of a graph.

val iter_edges : (vertex -> vertex -> unit) -> t -> unit

Iter on all edges of a graph. Edge label is ignored.

val fold_edges : (vertex -> vertex -> 'a -> 'a) -> t -> 'a -> 'a

Fold on all edges of a graph. Edge label is ignored.

val iter_edges_e : (edge -> unit) -> t -> unit

Iter on all edges of a graph.

val fold_edges_e : (edge -> 'a -> 'a) -> t -> 'a -> 'a

Fold on all edges of a graph.

val map_vertex : (vertex -> vertex) -> t -> t

Map on all vertices of a graph.

The current implementation requires the supplied function to be injective. Said otherwise, map_vertex cannot be used to contract a graph by mapping several vertices to the same vertex. To contract a graph, use instead create, add_vertex, and add_edge.

Vertex iterators

Each iterator iterator f v g iters f to the successors/predecessors of v in the graph g and raises Invalid_argument if v is not in g. It is the same for functions fold_* which use an additional accumulator.

<b>Time complexity for ocamlgraph implementations:</b> operations on successors are in O(1) amortized for imperative graphs and in O(ln(|V|)) for persistent graphs while operations on predecessors are in O(max(|V|,|E|)) for imperative graphs and in O(max(|V|,|E|)*ln|V|) for persistent graphs.

iter/fold on all successors/predecessors of a vertex.

val iter_succ : (vertex -> unit) -> t -> vertex -> unit

val iter_pred : (vertex -> unit) -> t -> vertex -> unit

val fold_succ : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a

val fold_pred : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a

iter/fold on all edges going from/to a vertex.

val iter_succ_e : (edge -> unit) -> t -> vertex -> unit

val fold_succ_e : (edge -> 'a -> 'a) -> t -> vertex -> 'a -> 'a

val iter_pred_e : (edge -> unit) -> t -> vertex -> unit

val fold_pred_e : (edge -> 'a -> 'a) -> t -> vertex -> 'a -> 'a

val graph_attributes : t -> Graph.Graphviz.DotAttributes.graph list

Vertex attributes

val default_vertex_attributes : t -> Graph.Graphviz.DotAttributes.vertex list

val vertex_name : V.t -> string

val vertex_attributes : V.t -> Graph.Graphviz.DotAttributes.vertex list

Edge attributes

val default_edge_attributes : t -> Graph.Graphviz.DotAttributes.edge list

val edge_attributes : E.t -> Graph.Graphviz.DotAttributes.edge list

val get_subgraph : V.t -> Graph.Graphviz.DotAttributes.subgraph option

The box (if exists) which the vertex belongs to. Boxes with same names are not distinguished and so they should have the same attributes.