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-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c.kernel/Frama_c_kernel/Interpreted_automata/UnrollUnnatural/index.html

Module `Interpreted_automata.UnrollUnnatural`

Control flow graphs where unnatural loops are modified such that all paths entering a loop enters it by its head.

module Vertex_Set : Datatype.S_with_collections with type t = Vertex.Set.t

module Version : 
  Datatype.S_with_collections with type t = Vertex.t * Vertex.Set.t

include Graph
  with type V.t = Version.t
   and type E.t = Version.t * Version.t edge * Version.t
   and type V.label = Version.t
   and type E.label = Version.t edge

include Graph.Sig.I
  with type V.t = Version.t
  with type E.t = Version.t * Version.t edge * Version.t
  with type V.label = Version.t
  with type E.label = Version.t edge

An imperative graph is a graph.

include Graph.Sig.G
  with type V.t = Version.t
  with type E.t = Version.t * Version.t edge * Version.t
  with type V.label = Version.t
  with type E.label = Version.t edge

Graph structure

type t

Abstract type of graphs

module V : Graph.Sig.VERTEX with type t = Version.t with type label = Version.t

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 = Version.t * Version.t edge * Version.t
    with type label = Version.t edge

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 create : ?size:int -> unit -> t

create () returns an empty graph. Optionally, a size can be given, which should be on the order of the expected number of vertices that will be in the graph (for hash tables-based implementations). The graph grows as needed, so size is just an initial guess.

val clear : t -> unit

Remove all vertices and edges from the given graph.

since ocamlgraph 1.4

val copy : t -> t

copy g returns a copy of g. Vertices and edges (and eventually marks, see module Mark) are duplicated.

val add_vertex : t -> vertex -> unit

add_vertex g v adds the vertex v to the graph g. Do nothing if v is already in g.

val remove_vertex : t -> vertex -> unit

remove g v removes the vertex v from the graph g (and all the edges going from v in g). Do nothing if v is not in g.

<b>Time complexity for ocamlgraph implementations:</b> O(|V|*ln(D)) for unlabeled graphs and O(|V|*D) for labeled graphs. D is the maximal degree of the graph.

val add_edge : t -> vertex -> vertex -> unit

add_edge g v1 v2 adds an edge from the vertex v1 to the vertex v2 in the graph g. Add also v1 (resp. v2) in g if v1 (resp. v2) is not in g. Do nothing if this edge is already in g.

val add_edge_e : t -> edge -> unit

add_edge_e g e adds the edge e in the graph g. Add also E.src e (resp. E.dst e) in g if E.src e (resp. E.dst e) is not in g. Do nothing if e is already in g.

val remove_edge : t -> vertex -> vertex -> unit

remove_edge g v1 v2 removes the edge going from v1 to v2 from the graph g. If the graph is labelled, all the edges going from v1 to v2 are removed from g. Do nothing if this edge is not in g.

raises Invalid_argument
if v1 or v2 are not in g.

val remove_edge_e : t -> edge -> unit

remove_edge_e g e removes the edge e from the graph g. Do nothing if e is not in g.

raises Invalid_argument
if E.src e or E.dst e are not in g.

module VTable : FCHashtbl.S with type key = vertex

type wto = vertex Wto.partition

module WTO : Wto.S with type node = vertex

val pretty : t Pretty_utils.formatter

val build_wto : pref:WTO.pref -> t -> V.t -> wto

Build a wto for the given automaton. The pref function is a comparison function used to determine what is the best vertex to use as a Wto component head. See Wto.Make for more details.

val output_to_dot : 
  ?pp_vertex:V.t Pretty_utils.formatter ->
  ?pp_edge:E.label Pretty_utils.formatter ->
  ?wto:wto ->
  out_channel ->
  t ->
  unit

Output the automaton in dot format

val exit_strategy : t -> V.t Wto.component -> wto

Extract an exit strategy from a component, i.e. a sub-wto where all vertices lead outside the wto without passing through the head.

type 'a widening =

| Fixpoint
| Widening of 'a

Widening for abstract domains

module type Domain = sig ... end

Abstract domains

module ForwardAnalysis (D : Domain) : sig ... end

Forward dataflow analysis

module BackwardAnalysis (D : Domain) : sig ... end