Commit 80c78d75 authored by MARCHE Claude's avatar MARCHE Claude

better cfg diagram

parent 6af319ea
digraph G {
graph [nodesep=0.5,
rankdir=TB,
ranksep=0.5
];
node [margin=0.05,shape=ellipse];
"entry" -> "L" [label=" i <- 0" ];
"L" -> "invariant" [label=" m <- a[i]"];
"invariant" -> "cond" [label=" i <- i+1"];
"cond" -> "do" [label=" i < n"];
"do" -> "L" [label=" a[i] > m"];
"do" -> "invariant" [label=" a[i] <= m"];
"cond" -> "exit" [label=" i >= n"];
}
......@@ -403,12 +403,14 @@ An example
return m;
}
The code can be viewed as a control-flow graph as follows.
The code can be viewed as a control-flow graph as shown in :numref:`fig.cfg.max_array`.
.. figure:: images/cfg.mps
.. graphviz:: images/max_array.dot
:caption: Control-Flow Graph of "max_array" example
:name: fig.cfg.max_array
Here is a version in the Why3-CFG language, where label L corresponds
to node X, label L1 to node 'inv', label L2 to node YY.
to node L, label L1 to node 'invariant', label L2 to node "do".
::
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment