package frama-c

  1. Overview
  2. Docs
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

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. N
    Nicolas Bellec
  6. T
    Thibaut Benjamin
  7. A
    Allan Blanchard
  8. L
    Lionel Blatter
  9. F
    François Bobot
  10. R
    Richard Bonichon
  11. V
    Vincent Botbol
  12. Q
    Quentin Bouillaguet
  13. D
    David Bühler
  14. Z
    Zakaria Chihani
  15. S
    Sylvain Chiron
  16. L
    Loïc Correnson
  17. J
    Julien Crétin
  18. P
    Pascal Cuoq
  19. Z
    Zaynah Dargaye
  20. B
    Basile Desloges
  21. J
    Jean-Christophe Filliâtre
  22. P
    Philippe Herrmann
  23. M
    Maxime Jacquemin
  24. B
    Benjamin Jorge
  25. F
    Florent Kirchner
  26. A
    Alexander Kogtenkov
  27. R
    Remi Lazarini
  28. T
    Tristan Le Gall
  29. K
    Kilyan Le Gallic
  30. J
    Jean-Christophe Léchenet
  31. M
    Matthieu Lemerre
  32. D
    Dara Ly
  33. D
    David Maison
  34. C
    Claude Marché
  35. A
    André Maroneze
  36. T
    Thibault Martin
  37. F
    Fonenantsoa Maurica
  38. M
    Melody Méaulle
  39. B
    Benjamin Monate
  40. Y
    Yannick Moy
  41. P
    Pierre Nigron
  42. A
    Anne Pacalet
  43. V
    Valentin Perrelle
  44. G
    Guillaume Petiot
  45. D
    Dario Pinto
  46. V
    Virgile Prevosto
  47. A
    Armand Puccetti
  48. F
    Félix Ridoux
  49. V
    Virgile Robles
  50. J
    Jan Rochel
  51. M
    Muriel Roger
  52. C
    Cécile Ruet-Cros
  53. J
    Julien Signoles
  54. N
    Nicolas Stouls
  55. K
    Kostyantyn Vorobyov
  56. B
    Boris Yakobowski

Maintainers

  1. F
    frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz
sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c-alias.core/Alias/API/G/index.html

Module API.GSource

Graph structure

Sourcetype t

Abstract type of graphs

module V : Graph.Sig.VERTEX with type t = int

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

Sourcetype vertex = V.t
module E : Graph.Sig.EDGE with type vertex = vertex with type label = EdgeLabel.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.

Sourcetype edge = E.t
Sourceval is_directed : bool

Is this an implementation of directed graphs?

Size functions

Sourceval is_empty : t -> bool
Sourceval nb_vertex : t -> int
Sourceval nb_edges : t -> int

Degree of a vertex

Sourceval out_degree : t -> vertex -> int

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

Sourceval in_degree : t -> vertex -> int

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

Membership functions

Sourceval mem_vertex : t -> vertex -> bool
Sourceval mem_edge : t -> vertex -> vertex -> bool
Sourceval mem_edge_e : t -> edge -> bool
Sourceval 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.

Sourceval 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").

Sourceval succ : t -> vertex -> vertex list

succ g v returns the successors of v in g.

Sourceval pred : t -> vertex -> vertex list

pred g v returns the predecessors of v in g.

Labeled edges going from/to a vertex

Sourceval succ_e : t -> vertex -> edge list

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

Sourceval pred_e : t -> vertex -> edge list

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

Graph iterators

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

Iter on all vertices of a graph.

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

Fold on all vertices of a graph.

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

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

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

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

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

Iter on all edges of a graph.

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

Fold on all edges of a graph.

Sourceval 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.

Sourceval iter_succ : (vertex -> unit) -> t -> vertex -> unit
Sourceval iter_pred : (vertex -> unit) -> t -> vertex -> unit
Sourceval fold_succ : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
Sourceval fold_pred : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a

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

Sourceval iter_succ_e : (edge -> unit) -> t -> vertex -> unit
Sourceval fold_succ_e : (edge -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
Sourceval iter_pred_e : (edge -> unit) -> t -> vertex -> unit
Sourceval fold_pred_e : (edge -> 'a -> 'a) -> t -> vertex -> 'a -> 'a