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 Dependency

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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-28.1-Nickel.tar.gz

sha256=0220bc743b7da2468ceb926f331edc7ddfaa7c603ba47962de3e33c8e1e3f593

doc/frama-c.kernel/Frama_c_kernel/Dotgraph/index.html

Module `Frama_c_kernel.Dotgraph`

Helper for Printing Dot-graphs.

This module provides smart-constructors for constructing Dot input files. Basically, a dot object is a buffer to a <file.dot> on disk where smart constructors write Dot statements.

Once the <file.dot> has been created, it is possible to layout it by running the dot command with various engines.

Typically, let say you have a graph with nodes of type M.elt with M : Map.S and assumes the graph is stored as a map graph : M.elt list M.t with roots : M.elt list then you can use:

  let module G = Dotgraph in
  let module N = G.Node(M) in
  begin
    let dot = G.open_dot ~name:"mygraph" () in
    (* For each generated node, declare it and link to its children. *)
    N.define dot
      (fun a na ->
         try
           List.iter
             (fun b -> G.edge dot na (N.get b) [])
             (M.find a graph)
         with Not_found -> ()) ;
    (* Starts by emitting some roots, or all nodes *)
    List.iter N.add roots ;
    (* Proceeds to the traversal *)
    G.pop_all dot ;
    (* You may then complete your graph
       with other decorations after the traversal... *)
    G.close dot ;
    (* Now call the layout engine, if installed. *)
    G.layout dot ~format:"pdf" () ;
  end

Attributes

type attr = [

| `LR
| `TB
| `Label of string
| `Color of string
| `Fillcolor of string
| `Shape of string
| `Style of string
| `Circle
| `Box
| `Oval
| `Point
| `Dotted
| `Filled
| `ArrowBoth
| `ArrowBack
| `ArrowForward
| `ArrowHead of string
| `ArrowTail of string
| `Attr of string * string

]

val pp_attr : Format.formatter -> attr -> unit

Dot Ouput

type dot

Buffer to a dot file with a graph environment (nodes, edges, etc.)

val open_dot : ?name:string -> ?attr:attr list -> ?file:string -> unit -> dot

val close : dot -> unit

val is_dot_installed : unit -> bool

Memoized

val layout : 
  ?force:bool ->
  ?target:string ->
  ?engine:string ->
  ?output:string ->
  dot ->
  string

Invoke dot command (if installed) with specified target and engine. Defaults are ~force:false, ~target:"pdf", ~engine:"dot".

The dot buffer must be closed before being laid out, although you can invoke several layouts.

Output is stored in ~output or in a filename derived from the one of dot. The function returns the generated output file.

raises Invalid_argument
if dot buffer is not closed, or when dot command fails and ~force:true (not by default).

val printf : dot -> ('a, Format.formatter, unit, unit) format4 -> 'a

Low-level routine to directly write material in the dot file

val println : dot -> ('a, Format.formatter, unit, unit) format4 -> 'a

Low-level routine to directly write material with an end-of-line ("\n") in the dot file

val flush : dot -> unit

Flushes the dot file buffer to disk.

Nodes and Edges

type node

val node_default : dot -> attr list -> unit

Set default node attributes

val edge_default : dot -> attr list -> unit

Set default edge attributes

val fresh : ?prefix:string -> dot -> node

Create a fresh node identifier

val pp_node : node Pretty_utils.formatter

val pp_edge : (node * node) Pretty_utils.formatter

a -> b

val node : dot -> node -> attr list -> unit

Set attributes to node

val edge : dot -> node -> node -> attr list -> unit

Create an edge with attributes

val link : dot -> node list -> attr list -> unit

Link the node sequence with attributed edges

val inode : dot -> ?prefix:string -> ?id:node -> attr list -> node

Combinaison of fresh and node

Clustering

val rank : dot -> node list -> unit

Layout nodes at the same rank

val subgraph : dot -> ?cluster:bool -> attr list -> (unit -> unit) -> unit

The continuation shall add the graph content in the dot file. Clustering is true by default

type record = [

| `Empty
| `Hbox of record list
| `Vbox of record list
| `Label of string
| `Port of string * link list * string
(*
Port with output edges to other nodes. Use Record.link and Record.label smart-constructors to create complex ports.
*)

]

and link = string * attr list * node

module Record : sig ... end

Complex node layout. Smart constructors to create records.

val port : node -> string -> node

Create a port to a node, and returns the associated pseudo-node so you can link an edge to it.

val record : dot -> node -> ?rounded:bool -> ?attr:attr list -> record -> unit

Define the node to be a record

val irecord : 
  dot ->
  ?prefix:string ->
  ?id:node ->
  ?rounded:bool ->
  ?attr:attr list ->
  record ->
  node

Create a new node from a record (combines fresh and record)

Node Indexing

module type Map = sig ... end

module Node (M : Map) : sig ... end

Lazily associates a node to any element.

val push : dot -> (unit -> unit) -> unit

val run : dot -> unit

Flushes all pending continuations.

Decorator

type buffer

A text buffer to compose labels and attributes. You can add text and attributes to the buffer, and finally flush it by calling attributes. A single `Label attribute is finally emitted with all the added text (if non-empty).

val buffer : attr list -> buffer

Create a buffer initialized with the given attributes.

val bprintf : buffer -> ('a, Format.formatter, unit, unit) format4 -> 'a

Add text material to buffer label.

val add_char : buffer -> char -> unit

val add_label : buffer -> string -> unit

val add_attr : buffer -> attr list -> unit

Add attributes to the buffer.

val add_options : buffer -> (bool * attr list) list -> unit

Only add attributes with a true boolean flag

val attributes : buffer -> attr list

Flushes the buffer into a list of attributes

val decorate : attr list -> (bool * attr list) list -> attr list

Concat the attributes with flagged ones

On This Page

Attributes
Dot Ouput
Nodes and Edges
Clustering
Node Indexing
Decorator