package frama-c
Install
dune-project
Dependency
Authors
-
MMichele Alberti
-
TThibaud Antignac
-
GGergö Barany
-
PPatrick Baudin
-
NNicolas Bellec
-
TThibaut Benjamin
-
AAllan Blanchard
-
LLionel Blatter
-
FFrançois Bobot
-
RRichard Bonichon
-
VVincent Botbol
-
QQuentin Bouillaguet
-
DDavid Bühler
-
ZZakaria Chihani
-
SSylvain Chiron
-
LLoïc Correnson
-
JJulien Crétin
-
PPascal Cuoq
-
ZZaynah Dargaye
-
BBasile Desloges
-
JJean-Christophe Filliâtre
-
PPhilippe Herrmann
-
JJordan Ischard
-
MMaxime Jacquemin
-
BBenjamin Jorge
-
FFlorent Kirchner
-
AAlexander Kogtenkov
-
RRemi Lazarini
-
TTristan Le Gall
-
KKilyan Le Gallic
-
JJean-Christophe Léchenet
-
MMatthieu Lemerre
-
DDara Ly
-
DDavid Maison
-
CClaude Marché
-
AAndré Maroneze
-
TThibault Martin
-
FFonenantsoa Maurica
-
MMelody Méaulle
-
BBenjamin Monate
-
NNicky Mouha
-
YYannick Moy
-
PPierre Nigron
-
AAnne Pacalet
-
VValentin Perrelle
-
GGuillaume Petiot
-
DDario Pinto
-
VVirgile Prevosto
-
AArmand Puccetti
-
FFélix Ridoux
-
VVirgile Robles
-
JJan Rochel
-
MMuriel Roger
-
CCécile Ruet-Cros
-
JJulien Signoles
-
FFabien Siron
-
NNicolas Stouls
-
HHugo Thievenaz
-
KKostyantyn Vorobyov
-
BBoris Yakobowski
Maintainers
Sources
sha256=9c1cbffd28bb33c17a668107e39c96e4ae7378a3d8249f69b47afc7ee964e9b8
doc/frama-c-callgraph.core/Callgraph/Cg/Graphviz_attributes/index.html
Module Cg.Graphviz_attributesSource
include Graph.Sig.G
with type t = G.t
with type V.t = Frama_c_kernel.Kernel_function.t
with type E.t = G.E.t
Graph structure
module V : Graph.Sig.VERTEX with type t = Frama_c_kernel.Kernel_function.tVertices have type V.t and are labeled with type V.label (note that an implementation may identify the vertex with its label)
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.
Is this an implementation of directed graphs?
Size functions
Degree of a vertex
Membership functions
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.
find_all_edges g v1 v2 returns all the edges from v1 to v2.
Successors and predecessors
You should better use iterators on successors/predecessors (see Section "Vertex iterators").
Labeled edges going from/to a vertex
Graph iterators
Iter on all edges of a graph. Edge label is ignored.
Fold on all edges of a graph. Edge label is ignored.
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.
iter/fold on all edges going from/to a vertex.
Vertex attributes
Edge attributes
The box (if exists) which the vertex belongs to. Boxes with same names are not distinguished and so they should have the same attributes.