From 1bd59cd42fd4d5bec61c1c3af5dec02f9f81bf71 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 2 Aug 2022 16:29:26 +0200
Subject: [PATCH] [Doc] update ViewCfg tutorial
---
doc/developer/Makefile | 9 +
doc/developer/tutorial.tex | 488 +++++++++---------
doc/developer/tutorial/viewcfg/pdfs/bogue.pdf | Bin 0 -> 13321 bytes
.../viewcfg/{v1 => v1-simple}/ViewCfg.ml | 0
doc/developer/tutorial/viewcfg/v1-simple/dune | 10 +
.../tutorial/viewcfg/v1-simple/dune-project | 5 +
.../viewcfg/v1-simple/tests/ptests_config | 1 +
.../viewcfg/v1-simple/tests/test_config | 1 +
.../v1-simple/tests/viewcfg/oracle/cfg.dot | 32 ++
.../tests/viewcfg/oracle/test.res.oracle | 1 +
.../{v1 => v1-simple/tests/viewcfg}/test.c | 6 +-
.../viewcfg/{v1 => v1-simple}/view_cfg.ml | 24 +-
doc/developer/tutorial/viewcfg/v1/dune | 34 --
.../tutorial/viewcfg/v1/dune-project | 27 -
.../tutorial/viewcfg/v2-options/ViewCfg.ml | 3 +
.../tutorial/viewcfg/v2-options/dune | 10 +
.../tutorial/viewcfg/v2-options/dune-project | 5 +
.../tutorial/viewcfg/v2-options/view_cfg.ml | 74 +++
.../tutorial/viewcfg/v3-eva/ViewCfg.ml | 3 +
doc/developer/tutorial/viewcfg/v3-eva/dune | 10 +
.../tutorial/viewcfg/v3-eva/dune-project | 5 +
.../viewcfg/v3-eva/tests/ptests_config | 1 +
.../tutorial/viewcfg/v3-eva/tests/test_config | 1 +
.../v3-eva/tests/viewcfg/oracle/cfg.dot | 32 ++
.../tests/viewcfg/oracle/test.res.oracle | 23 +
.../viewcfg/v3-eva/tests/viewcfg/test.c | 24 +
.../tutorial/viewcfg/v3-eva/view_cfg.ml | 82 +++
.../tutorial/viewcfg/v4-bogue/ViewCfg.ml | 3 +
.../tutorial/viewcfg/v4-bogue/dump.ml | 9 +
doc/developer/tutorial/viewcfg/v4-bogue/dune | 11 +
.../tutorial/viewcfg/v4-bogue/dune-project | 5 +
.../tutorial/viewcfg/v4-bogue/gui.ml | 37 ++
.../tutorial/viewcfg/v4-bogue/options.ml | 11 +
.../tutorial/viewcfg/v4-bogue/run.ml | 5 +
.../tutorial/viewcfg/v4-bogue/test.c | 24 +
.../tutorial/viewcfg/v4-bogue/visit.ml | 47 ++
.../tutorial/viewcfg/v5-state/ViewCfg.ml | 3 +
.../tutorial/viewcfg/v5-state/dump.ml | 24 +
doc/developer/tutorial/viewcfg/v5-state/dune | 11 +
.../tutorial/viewcfg/v5-state/dune-project | 5 +
.../tutorial/viewcfg/v5-state/gui.ml | 37 ++
.../tutorial/viewcfg/v5-state/options.ml | 11 +
.../tutorial/viewcfg/v5-state/run.ml | 5 +
.../tutorial/viewcfg/v5-state/test.c | 24 +
.../tutorial/viewcfg/v5-state/visit.ml | 47 ++
.../viewcfg/v6-state-clear/ViewCfg.ml | 3 +
.../tutorial/viewcfg/v6-state-clear/dump.ml | 37 ++
.../tutorial/viewcfg/v6-state-clear/dune | 11 +
.../viewcfg/v6-state-clear/dune-project | 5 +
.../tutorial/viewcfg/v6-state-clear/gui.ml | 37 ++
.../viewcfg/v6-state-clear/options.ml | 11 +
.../tutorial/viewcfg/v6-state-clear/run.ml | 5 +
.../tutorial/viewcfg/v6-state-clear/test.c | 24 +
.../tutorial/viewcfg/v6-state-clear/visit.ml | 47 ++
doc/frama-c-book.cls | 4 +-
55 files changed, 1091 insertions(+), 323 deletions(-)
create mode 100644 doc/developer/tutorial/viewcfg/pdfs/bogue.pdf
rename doc/developer/tutorial/viewcfg/{v1 => v1-simple}/ViewCfg.ml (100%)
create mode 100644 doc/developer/tutorial/viewcfg/v1-simple/dune
create mode 100644 doc/developer/tutorial/viewcfg/v1-simple/dune-project
create mode 100644 doc/developer/tutorial/viewcfg/v1-simple/tests/ptests_config
create mode 100644 doc/developer/tutorial/viewcfg/v1-simple/tests/test_config
create mode 100644 doc/developer/tutorial/viewcfg/v1-simple/tests/viewcfg/oracle/cfg.dot
create mode 100644 doc/developer/tutorial/viewcfg/v1-simple/tests/viewcfg/oracle/test.res.oracle
rename doc/developer/tutorial/viewcfg/{v1 => v1-simple/tests/viewcfg}/test.c (80%)
rename doc/developer/tutorial/viewcfg/{v1 => v1-simple}/view_cfg.ml (52%)
delete mode 100644 doc/developer/tutorial/viewcfg/v1/dune
delete mode 100644 doc/developer/tutorial/viewcfg/v1/dune-project
create mode 100644 doc/developer/tutorial/viewcfg/v2-options/ViewCfg.ml
create mode 100644 doc/developer/tutorial/viewcfg/v2-options/dune
create mode 100644 doc/developer/tutorial/viewcfg/v2-options/dune-project
create mode 100644 doc/developer/tutorial/viewcfg/v2-options/view_cfg.ml
create mode 100644 doc/developer/tutorial/viewcfg/v3-eva/ViewCfg.ml
create mode 100644 doc/developer/tutorial/viewcfg/v3-eva/dune
create mode 100644 doc/developer/tutorial/viewcfg/v3-eva/dune-project
create mode 100644 doc/developer/tutorial/viewcfg/v3-eva/tests/ptests_config
create mode 100644 doc/developer/tutorial/viewcfg/v3-eva/tests/test_config
create mode 100644 doc/developer/tutorial/viewcfg/v3-eva/tests/viewcfg/oracle/cfg.dot
create mode 100644 doc/developer/tutorial/viewcfg/v3-eva/tests/viewcfg/oracle/test.res.oracle
create mode 100644 doc/developer/tutorial/viewcfg/v3-eva/tests/viewcfg/test.c
create mode 100644 doc/developer/tutorial/viewcfg/v3-eva/view_cfg.ml
create mode 100644 doc/developer/tutorial/viewcfg/v4-bogue/ViewCfg.ml
create mode 100644 doc/developer/tutorial/viewcfg/v4-bogue/dump.ml
create mode 100644 doc/developer/tutorial/viewcfg/v4-bogue/dune
create mode 100644 doc/developer/tutorial/viewcfg/v4-bogue/dune-project
create mode 100644 doc/developer/tutorial/viewcfg/v4-bogue/gui.ml
create mode 100644 doc/developer/tutorial/viewcfg/v4-bogue/options.ml
create mode 100644 doc/developer/tutorial/viewcfg/v4-bogue/run.ml
create mode 100644 doc/developer/tutorial/viewcfg/v4-bogue/test.c
create mode 100644 doc/developer/tutorial/viewcfg/v4-bogue/visit.ml
create mode 100644 doc/developer/tutorial/viewcfg/v5-state/ViewCfg.ml
create mode 100644 doc/developer/tutorial/viewcfg/v5-state/dump.ml
create mode 100644 doc/developer/tutorial/viewcfg/v5-state/dune
create mode 100644 doc/developer/tutorial/viewcfg/v5-state/dune-project
create mode 100644 doc/developer/tutorial/viewcfg/v5-state/gui.ml
create mode 100644 doc/developer/tutorial/viewcfg/v5-state/options.ml
create mode 100644 doc/developer/tutorial/viewcfg/v5-state/run.ml
create mode 100644 doc/developer/tutorial/viewcfg/v5-state/test.c
create mode 100644 doc/developer/tutorial/viewcfg/v5-state/visit.ml
create mode 100644 doc/developer/tutorial/viewcfg/v6-state-clear/ViewCfg.ml
create mode 100644 doc/developer/tutorial/viewcfg/v6-state-clear/dump.ml
create mode 100644 doc/developer/tutorial/viewcfg/v6-state-clear/dune
create mode 100644 doc/developer/tutorial/viewcfg/v6-state-clear/dune-project
create mode 100644 doc/developer/tutorial/viewcfg/v6-state-clear/gui.ml
create mode 100644 doc/developer/tutorial/viewcfg/v6-state-clear/options.ml
create mode 100644 doc/developer/tutorial/viewcfg/v6-state-clear/run.ml
create mode 100644 doc/developer/tutorial/viewcfg/v6-state-clear/test.c
create mode 100644 doc/developer/tutorial/viewcfg/v6-state-clear/visit.ml
diff --git a/doc/developer/Makefile b/doc/developer/Makefile
index 7825f1cba79..c5016b3524f 100644
--- a/doc/developer/Makefile
+++ b/doc/developer/Makefile
@@ -154,6 +154,15 @@ install:
rm -f ../manuals/plugin-development-guide.pdf
cp developer.pdf ../manuals/plugin-development-guide.pdf
+viewcfg: viewcfg-clean viewcfg-v1
+
+viewcfg-clean:
+ $(ECHO) Cleaning ViewCfg files...
+ rm -rf tutorial/viewcfg/v*/_build
+
+viewcfg-v1:
+ cd tutorial/viewcfg/v1 && $(duneb) @install && $(duneb) @ptests
+
tutorial/viewcfg/generated:
cd tutorial/viewcfg && make
diff --git a/doc/developer/tutorial.tex b/doc/developer/tutorial.tex
index bbc2322f6b2..fddcbad4b78 100644
--- a/doc/developer/tutorial.tex
+++ b/doc/developer/tutorial.tex
@@ -212,7 +212,8 @@ afterwards. In case of success, there will be no visible output at the end.
so make sure that your Hello directory is not inside another one containing
a Dune project (\eg if you are running this directly from the \framac source
archive), otherwise \verb|dune build| may fail. You can always add option
- ``\verb|--root .|'' to force Dune to ignore parent directories.
+ ``\verb|--root .|'', or create an empty \texttt{dune-workspace} file in
+ the current directory to force Dune to ignore parent directories.
\end{important}
Note a few details about the naming conventions:
@@ -784,9 +785,8 @@ In this section, we create a new ViewCfg plug-in that computes the control
flow graph of a function and outputs it in the \dottool format. Through its
implementation, we explain some of \framac APIs such as how to visit
an AST\footnote{Abstract Syntax Tree}, how to hook a plug-in, how to interface
-a plug-in with other plug-ins, how to extend the
-GUI\footnote{Graphical User Interface}, how to make a plug-in usable by
-others, and how to make a plug-in usable in a multi-project setting.
+a plug-in with other plug-ins, and how to make a plug-in usable in a
+multi-project setting (which also allows it to save/load data).
This section assumes the reader is already familiar with the basics of plug-ins
for \framac as covered by the Hello plug-in in the previous
@@ -815,7 +815,7 @@ suitable for us, as it will recursively print substatements of compound
statements (blocks, if, while, ...), while we only want to pretty-print
the node representing the current statement: substatements will be represented
by other nodes. Thus we will use the following small function:
-\ocamlinput[firstline=29,lastline=43]{./tutorial/viewcfg/v1/view_cfg.ml}
+\ocamlinput[linerange={7-21}]{./tutorial/viewcfg/v1-simple/view_cfg.ml}
\sscodeidx{Cil\_types}{stmtkind}{Instr}
\sscodeidx{Cil\_types}{stmtkind}{Return}
\sscodeidx{Cil\_types}{stmtkind}{Goto}
@@ -852,7 +852,7 @@ children. By inheriting from the visitor, and redefining some of the
methods, one can perform actions on selected parts of the AST, without
the need to traverse the AST explicitly.
-\ocamlinput[firstline=45,lastline=46]{./tutorial/viewcfg/v1/view_cfg.ml}
+\ocamlinput[linerange={23-24}]{./tutorial/viewcfg/v1-simple/view_cfg.ml}
\scodeidx{Visitor}{frama\_c\_inplace}
Here we used the so-called ``in place'' visitor, which should be used for
@@ -866,7 +866,7 @@ at the file level, we create the whole graph structure.
%in the code below, the fancy 'at'-terms such as ``\texttt{@[<hov 2>}'' are
% related to OCaml's Format module, and can be ignored for now.}.
-\ocamlinput[firstline=48,lastline=50]{./tutorial/viewcfg/v1/view_cfg.ml}
+\ocamlinput[linerange={26-28}]{./tutorial/viewcfg/v1-simple/view_cfg.ml}
\sscodeidx{Cil}{visitAction}{DoChildrenPost}
\sscodeidx{Cil}{cilVisitor}{vfile}
@@ -880,7 +880,7 @@ in the file.
Then, for each function, we encapsulate the CFG in a subgraph, and do
nothing for the other globals.
-\ocamlinput[firstline=52,lastline=58]{./tutorial/viewcfg/v1/view_cfg.ml}
+\ocamlinput[linerange={30-36}]{./tutorial/viewcfg/v1-simple/view_cfg.ml}
\sscodeidx{Cil}{visitAction}{DoChildrenPost}
\sscodeidx{Cil}{visitAction}{SkipChildren}
\sscodeidx{Visitor}{frama\_c\_visitor}{vglob\_aux}
@@ -895,7 +895,7 @@ should have been used instead.}.
Last, for each statement, we create a node in the graph, and create
the edges toward its successors:
-\ocamlinput[firstline=60,lastline=65]{./tutorial/viewcfg/v1/view_cfg.ml}
+\ocamlinput[linerange={38-43}]{./tutorial/viewcfg/v1-simple/view_cfg.ml}
\sscodeidx{Cil}{visitAction}{DoChildren}
\sscodeidx{Visitor}{frama\_c\_visitor}{vstmt\_aux}
@@ -905,7 +905,7 @@ cannot contain other statements, like \texttt{Instr}, and avoid
visiting the expressions.
Finally, we close the \texttt{object} definition:
-\ocamlinput[firstline=67,lastline=67]{./tutorial/viewcfg/v1/view_cfg.ml}
+\ocamlinput[linerange={45-45}]{./tutorial/viewcfg/v1-simple/view_cfg.ml}
\subsubsection*{Hooking into \framac}
@@ -916,7 +916,7 @@ will not have had the time to parse the sources and produce its AST
(used by \verb|Ast.get ()|). For more details about initialization issues,
see Section~\ref{adv:init}.
-\ocamlinput[firstline=69,lastline=75]{./tutorial/viewcfg/v1/view_cfg.ml}
+\ocamlinput[linerange={47-53}]{./tutorial/viewcfg/v1-simple/view_cfg.ml}
Now, since \framac uses Dune, this code needs to be integrated as a Dune
project, as has been done in the Hello tutorial. We need to create a new
@@ -925,10 +925,10 @@ file. We will then add the corresponding \texttt{dune} and
\texttt{dune-project} files:
\listingname{dune}
-\duneinput[linerange={23-999}]{./tutorial/viewcfg/v1/dune}
+\duneinput{./tutorial/viewcfg/v1-simple/dune}
\listingname{dune-project}
-\duneinput[linerange={1-1,24-999}]{./tutorial/viewcfg/v1/dune-project}
+\duneinput{./tutorial/viewcfg/v1-simple/dune-project}
Finally, we need an (empty) interface file, called \texttt{ViewCfg.ml}, in
the same directory.
@@ -948,7 +948,7 @@ And run it as a \framac plugin:
And the graph can be visualized with an external tool, such as {\em dotty} or
{\em xdot}.
\begin{shell}
- dotty cfg.out
+ dotty cfg.dot
\end{shell}
This produces a graph like in Figure~\ref{fig:tut:basiccfg}
@@ -957,7 +957,7 @@ This produces a graph like in Figure~\ref{fig:tut:basiccfg}
\centering
\begin{minipage}[h]{0.45\linewidth}
\listingname{test.c}
- \cinput{./tutorial/viewcfg/tests/test.c}
+ \cinput[linerange={5-999}]{./tutorial/viewcfg/v1-simple/tests/viewcfg/test.c}
\end{minipage}%
\begin{minipage}[h]{0.4\linewidth}
\includegraphics[width=\textwidth]{./tutorial/viewcfg/pdfs/cfg.pdf}
@@ -995,9 +995,9 @@ for our plug-in.
We have already seen how to register options in the previous ``Hello'' tutorial.
We now apply these principles to the ViewCfg plug-in.
-\ocamlinput{./tutorial/viewcfg/src/register_and_options.ml}
+\ocamlinput[linerange={9-26}]{./tutorial/viewcfg/v2-options/view_cfg.ml}
\scodeidx{Plugin}{Register}
-\ocamlinput{./tutorial/viewcfg/src/extend_with_run_with_options.ml}
+\ocamlinput[linerange={66-74}]{./tutorial/viewcfg/v2-options/view_cfg.ml}
\scodeidx{Visitor}{visitFramacFileSameGlobals}
\scodeidx{Ast}{get}
@@ -1025,44 +1025,62 @@ section~\ref{adv:project} of this manual should help you understand the
underlying notion of states).
With these command-line options, we can properly interface our ViewCfg plug-in
-with the \texttt{value} plug-in.
+with the \texttt{eva} plug-in.
-\subsection{Interfacing with a kernel-integrated plug-in}
+\subsection{Interfacing with other plug-ins}
-Kernel-integrated plug-ins, such as \texttt{value}, use a special mechanism
-to statically register their APIs for other plug-ins that wish to access them.
-This mechanism is the \texttt{Db} module of the \framac kernel,
-the entry point for all kernel-integrated plug-ins. By using the functions
-exported through the \texttt{Db.Value} module, our plug-in will obtain
-reachability information computed by \texttt{value}.
+Plug-ins can use functions specified in the public interfaces of other
+plug-ins, as long as they are declared as dependencies. To do so, you only
+need to add them to the \texttt{libraries} stanza\footnote{A stanza is,
+roughly speaking, a ``term'' in \texttt{dune} parlance: a parenthesized
+expression.} in the \texttt{dune} file.
+We will use a function from the \textsf{Eva} plug-in in our example,
+so we will add \texttt{frama-c-eva.core} to the \texttt{dune} file:
+\duneinput[linerange={5-5}]{./tutorial/viewcfg/v3-eva/dune-project}
+
+Now our plug-in can call all functions and access all types declared in
+\textsf{Eva}'s public interface.
+
+For historical reasons, several kernel-integrated plug-ins, such as
+\textsf{From}, \textsf{InOut} and \textsf{Slicing}, had their API exposed
+via the \texttt{Db} module of the \framac kernel. This has been deprecated
+for \textsf{Eva}, and newer plug-ins expose their public interface directly.
+
+In our example, we will use \textsf{Eva}'s new API to obtain reachability
+information computed by the value analysis.
The code modification we propose is to color in pink the nodes guaranteed to
be unreachable by the value analysis. For this purpose, we change the
\texttt{vstmt\_aux} method in the visitor:
-\ocamlinput{./tutorial/viewcfg/src/print_cfg_vstmt_aux_value.ml}
-\sscodeidx{Db}{Value}{is\_computed}
-\sscodeidx{Db}{Value}{get\_stmt\_state}
-\sscodeidx{Db}{Value}{is\_reachable}
+\ocamlinput[linerange={57-70}]{./tutorial/viewcfg/v3-eva/view_cfg.ml}
+\sscodeidx{Eva}{Analysis}{is\_computed}
+\sscodeidx{Eva}{Results}{is\_reachable}
\sscodeidx{Cil}{visitAction}{DoChildren}
\sscodeidx{Visitor}{frama\_c\_visitor}{vstmt\_aux}
This code fills the nodes with green if the node may be
reachable, and in pink if the node is guaranteed not to be
-reachable; but only if the value analysis was previously computed.
+reachable; but only if the value analysis was previously computed.
-To test this code, frama-c should be launched with:
+To test this code, we recompile the plug-in with the modified \texttt{dune}
+file to take into account the dependency on \textsf{Eva}, as well as the
+modified \texttt{vstmt\_aux}. We run \verb|dune build @install| and then
+we run \textsf{Eva}, and then our plug-in:
\begin{shell}
- frama-c test.c -load-script cfg_print.ml -val -then -cfg && dotty cfg.out
+ dune exec -- frama-c test.c -eva -then -cfg && dotty cfg.dot
\end{shell}
-Note that the relative order of the parameters \texttt{-load-script} and
-\texttt{-val} in this example is not relevant
-(see Section~\ref{adv:init} for details).
-However, it is important to ensure that \texttt{-cfg} is separated from
-\texttt{-val} by a \texttt{-then}; otherwise, it is not guaranteed that
-the \texttt{value} plug-in will run before the ViewCfg plug-in, which might
-lead to a non-colored graph in some cases, and colored in others.
+The relative order of most options and file names is not important
+{\em between} occurrences of \texttt{-then}, but it {\em is} important
+whether they are before or after \texttt{-then}-related options
+(\texttt{-then}, \texttt{-then-on}, \texttt{-then-last});
+see Section~\ref{adv:init} for details. Here, we want to ensure that
+\textsf{Eva} is run {\em before} our plug-in, so we order it as
+\verb|-eva -then -cfg|. Without \texttt{-then}, even if \texttt{-eva}
+is before \texttt{-cfg} in the command line, it is {\em not} guaranteed
+that it will run before; options in the same ``block'' can be thought of as
+{\em concurrent}: there is no specified order between them.
The resulting graph is shown in Figure~\ref{fig:tut:coloredcfg}.
@@ -1070,7 +1088,7 @@ The resulting graph is shown in Figure~\ref{fig:tut:coloredcfg}.
\centering
\begin{minipage}[h]{0.45\linewidth}
\listingname{test.c}
- \cinput{./tutorial/viewcfg/tests/test.c}
+ \cinput[linerange={5-999}]{./tutorial/viewcfg/v3-eva/tests/viewcfg/test.c}
\end{minipage}%
\begin{minipage}[h]{0.4\linewidth}
\includegraphics[width=\textwidth]{./tutorial/viewcfg/pdfs/cfg_colored.pdf}
@@ -1079,168 +1097,124 @@ The resulting graph is shown in Figure~\ref{fig:tut:coloredcfg}.
\label{fig:tut:coloredcfg}
\end{figure}
-\subsection{Extending the Frama-C GUI}
-\label{tut2:gui}
-\index{Plug-in!GUI}
+\subsection{Splitting files and providing a mini-GUI for testing}
+\label{tut2:split-and-gui}
-In this section, we will extend our plug-in so that the control flow
-graph can be displayed interactively. For that, we will extend the \framac GUI
-so that when you right-click on a function in the code, a new ``Show
-CFG'' item appears, that displays the control flow graph of the
-function in a dialog box. This is achieved just by appending the following
-pieces of code at the end of the \texttt{cfg\_print.ml} file.
+Our plug-in is starting to amass enough code that we should envisage to split
+it into several modules, for better organizing it. Dune automatically compiles
+all source files it finds, unless specified otherwise, and it handles
+dependencies between them, so it is essentially free to do so. As we did in the
+{\em Hello} tutorial, we will split our \verb|view_cfg.ml| file into smaller
+modules.
-\begin{important}
-Frama-C's GUI can be compiled against two versions of lablgtk (the OCaml
-bindings to the Gtk toolkit). The actual rendering of the control flow graph
-is actually done by the external OCamlgraph library, and only available
-when compiling against lablgtk2. If you're using lablgtk3,
-you will only see a pop-up window indicating that there's no support for
-displaying graphs.
-\end{important}
+We will create the following files:
-Currently, we used a visitor that outputs a \dottool file with the CFG of
-all functions of all files. We use \texttt{dump\_function} to output
-the CFG of a single function instead.
+\begin{description}
+\item[options.ml]: will contain the module registration (\verb|Self|) and
+ command-line options (\verb|Enabled| and \verb|OutputFile|);
+\item[visit.ml]: will contain the \verb|print_stmt| function and the visitor;
+\item[run.ml]: will contain the definition of function \verb|run| and the
+ call to \verb|Db.Main.extend|.
+\end{description}
-\ocamlinput{./tutorial/viewcfg/src/dump_function.ml}
+Note that a few changes are needed to the code: functions from other files
+need to include that file name as module, \eg
+\verb|Enabled.get| becomes \verb|Options.Enabled.get|.
-We reused the \texttt{print\_cfg} visitor, but we selected a different
-starting point. The argument \texttt{fundec} gets type
-\texttt{Cil\_types.fundec}\scodeidx{Cil\_types}{fundec}, which is the CIL type
-representing a function definition.
+For simplicity's sake, we will remove options \verb|-cfg| and \verb|-cfg-output|
+and replace them with a single boolean option, \verb|-cfg-gui|, to launch the
+GUI (this prevents unsuitable combinations of \verb|-cfg| and \verb|-cfg-gui|).
+The new option is defined as below:
-Now we write the GUI extension code:
+\ocamlinput[linerange={7-11}]{./tutorial/viewcfg/v4-bogue/options.ml}
-\ocamlinput{./tutorial/viewcfg/src/gui.ml}
-\sscodeidx{Pretty\_source}{localizable}{PVDecl}
-\sscodeidx{Globals}{Functions}{get}
-\scodeidx{Kernel\_function}{get\_definition}
-\scodeidx{Dgraph\_helper}{graph\_window}
-\scodeidx{Design}{register\_extension}
-\sscodeidx{Design}{main\_window\_extension\_points}{register\_source\_selector}
-
-Let us explain this code from the end. \texttt{Design.register\_extension} is
-the entry point for extending the GUI. Its argument is a function which takes as
-argument an object corresponding to the main window of the \framac GUI. This
-object provides access to the main widgets of the window, and several
-extension points.
-
-Here we have implemented a single extension, the ``source selector'',
-that allows to add entries to menu obtained when right-clicking on the
-source. This is implemented by the \texttt{cfg\_selector} function.
-
-This function takes a \texttt{localizable} argument, which gives information on
-where the user clicks on the source. Here we do something only if the user
-clicks on the declaration of a variable whose type is a function (\ie when the
-user clicked on a function declaration or definition). In that case, we add an
-item to the popup menu, that calls the \texttt{callback} function if
-clicked. The \texttt{callback} function calls a \framac GUI function that
-displays a graph from \dottool printing functions. It uses several important \framac
-APIs: \texttt{Globals} and \texttt{Kernel\_function}, which contain several
-functions for manipulating globals and functions.
-
-Note that this GUI extension could also have been done through a script
-(instead of a plug-in), but it would have been less than ideal.
-In particular, the GUI \ocaml modules are available only when a script
-is loaded with \texttt{frama-c-gui}, and not when loaded with
-\texttt{frama-c}. When the user wants to view the CFG from the GUI,
-outputting the CFG of all functions in \texttt{cfg.out} is useless.
-A better architectural solution is to split our plug-in in several files,
-with its own Makefile, to better manage its functionalities.
-
-\subsection{Splitting files and writing a Makefile}\label{tut2:makefile}
-\index{Plug-in!Makefile}
-
-The \framac plug-in development environment allows to split GUI-related
-and non-GUI related modules, so that GUI-related modules are loaded
-and run only if \framac is executed with \texttt{frama-c-gui}. This
-requires splitting the module into several files. We choose the
-following architecture:
+And the \verb|run| function in \verb|run.ml| becomes simply:
-\begin{itemize}
-\item \texttt{cfg\_options.ml} implements plug-in registration and
- configuration options;
-\item \texttt{cfg\_core.ml} implements the main functions for
- computing the CFG;
-\item \texttt{cfg\_register.ml} implements ``global'' computation of
- the CFG using the \texttt{-cfg} option, and hooking into the \framac
- main loop;
-\item \texttt{cfg\_gui.ml} implements GUI registration.
-\end{itemize}
+\ocamlinput[linerange={1-3}]{./tutorial/viewcfg/v4-bogue/run.ml}
-Dependencies between the modules\footnote{This graphic is generated in
- file \texttt{doc/code/modules.dot} after running \texttt{make doc}.}
-is presented on Figure \ref{fig:tut:cfgarchitecture}.
+We can now erase \verb|view_cfg.ml| and re-run \verb|dune build @install| to
+compile the plug-in.
-\begin{figure}[htbp]
- \centering
- \includegraphics[width=0.5\textwidth]{./tutorial/viewcfg/pdfs/modules.pdf}
- \caption{CFG plug-in architecture}
- \label{fig:tut:cfgarchitecture}
-\end{figure}
+\subsubsection{Mini-GUI for testing}
-To break recursive dependencies between \ocaml modules, it is typical
-that plug-in registration is done at the bottom of the module
-hierarchy, while definition of the \texttt{run} function is at the
-top. The GUI is also at the top of the hierarchy: the \framac
-\texttt{Makefile} requires that normal plug-in modules do not depend on
-GUI modules. Note that currently, the dependency from
-\texttt{Cfg\_core} and \texttt{Cfg\_gui} to \texttt{Cfg\_register} is
-artificial, but in future evolutions the GUI could depend on
-configuration options.
+Extending \framac's Ivette graphical user interface is a task too large for
+this tutorial; Ivette being a desktop Electron application, written in
+TypeScript and using React, there is a substantial amount of explaining to
+do before one can show how to integrate a \framac plug-in in it.
-\listingname{Makefile}
-\codeidx{Makefile.dynamic}
-\codeidx{FRAMAC\_SHARE}
-\codeidx{PLUGIN\_CMO}
-\codeidx{PLUGIN\_GUI\_CMO}
-\codeidx{PLUGIN\_NAME}
-\makefileinput{./tutorial/viewcfg/generated/split/Makefile}
+Instead, for this tutorial, we will use a lightweight OCaml GUI library,
+BOGUE\footnote{\url{http://sanette.github.io/bogue/Principles.html}}.
+You can install it through opam:
-In the \texttt{Makefile}, the \texttt{PLUGIN\_CMO} variable must
-contain the list of file names of the ml files, in the correct \ocaml
-build order. Modules in \texttt{PLUGIN\_CMO} must not depend on modules in
-\texttt{PLUGIN\_GUI\_CMO}.
+\begin{shell}
+\$ opam install bogue
+\end{shell}
+
+It is based on SDL2, which means you may need to install non-OCaml
+dependencies\footnote{With opam $< 2.1$, you may need to install and
+run \texttt{depext}. With opam $\geq 2.1$, depext is already included.}.
+
+Since we will be using BOGUE in our plug-in, we need to declare it in the
+\texttt{dune} file:
+
+\duneinput[linerange={5-5}]{./tutorial/viewcfg/v4-bogue/dune}
-We also need to add an interface for the whole plug-in:
-\listingname{ViewCfg.mli}
-\ocamlinput{./tutorial/viewcfg/generated/split/ViewCfg.mli}
+We also need a way to print an individual function as a standalone graph,
+without having to call the file visitor (\verb|Visit.vfile|). We will call
+it \verb|dump_function| and put it in a separate file, \verb|dump.ml|:
-Here is the listing for the different modules:
+\listingname{./dump.ml}
+\ocamlinput{./tutorial/viewcfg/v4-bogue/dump.ml}
+\scodeidx{Visitor}{visitFramacFunction}
-\listingname{cfg\_options.ml}
-\ocamlinput{./tutorial/viewcfg/generated/split/cfg_options.ml}
+The code prints a feedback message, then the header, calls the visitor,
+and prints the footer. This function will be called by our ``mini-GUI'',
+and the output will be sent to \texttt{dotty}, which will open a window
+with our graph.
-\listingname{cfg\_core.ml}
-\ocamlinput{./tutorial/viewcfg/generated/split/cfg_core.ml}
+The actual GUI code is put inside a file appropriately named \texttt{gui.ml}:
-\listingname{cfg\_register.ml}
-\ocamlinput{./tutorial/viewcfg/generated/split/cfg_register.ml}
+\listingname{./gui.ml}
+\ocamlinput{./tutorial/viewcfg/v4-bogue/gui.ml}
+\sscodeidx{Globals}{Functions}{find\_by\_name}
+\scodeidx{Kernel\_function}{get\_definition}
-\listingname{cfg\_gui.ml}
-\ocamlinput{./tutorial/viewcfg/generated/split/cfg_gui.ml}
+Most of the code is boilerplate for Bogue. The only \framac-related part is
+the checking of the function name: \verb|Globals.Functions.find_by_name| raises
+exception \verb|Not_found| if the name input by the user does not exist. But
+even if it does, since we need a function {\em definition}, we must check that
+it is not simply {\em declared}. Besides that, we simply call
+\verb|dump_function|. Figure~\ref{fig:tut:bogue} shows what this mini-GUI looks
+like.
-\subsection{Getting your Plug-in Usable by Others}\label{tut2:api}
-\index{Plug-in!API}
-\todo
+\begin{figure}[htbp]
+ \centering
+ \includegraphics[width=0.35\textwidth]{./tutorial/viewcfg/pdfs/bogue.pdf}
+ \caption{Mini-GUI with Bogue for testing our plug-in.}
+ \label{fig:tut:bogue}
+\end{figure}
-% TODO: A script that uses "dump_function" of the CFG plug-in
+Whenever we click the ``Show CFG'' button, a new \texttt{dotty} window is
+opened. After we close it, we can repeat the operation as we like.
-% Detect \dottool at compile time.
-% Link to section 5.3: plug-in specific configure.in
+Note that the feedback message ``Computing CFG for function'' is emitted
+each time we click the button, which means we perform a new visit.
+For large computations and programs, this is wasteful,
+and we should be able to easily cache the result.
+The next section will show how to do it using {\em states}.
-\subsection{Getting your plug-in Usable in a Multi Projects Setting}
+\subsection{Saving/Loading Data, and Usability in a Multi-Project Setting}
\label{tut2:project-and-state}
\index{Project}
\subsubsection{Registering and using state}
In this section, we will learn how to register state into \framac. A
-\emph{state} is a piece of information kept by a plug-in. For instance,
-the \texttt{value} plug-in computes, for each statement, a table associating to
-each AST's variable a set of values the program may have at runtime: this
-association table is a state.
+\emph{state} is a piece of information kept by a plug-in. For instance, we can
+use a boolean state to store whether an expensive analysis has been executed,
+to avoid recomputing it. Another example of state: the \textsf{Eva} plug-in
+computes, for each statement, a table associating to each AST variable a set of
+values the program may have at runtime; this association table is a state.
State registration provides several features:
\begin{itemize}
@@ -1251,99 +1225,143 @@ State registration provides several features:
parameters of the analysis of the different plug-ins.
\end{itemize}
-In this tutorial, we will store the file representing the \dottool
-output of the control flow graph of a function (as needed by
-\texttt{dump\_function}) as a string, by using a hashtable from \texttt{fundec}
-to \texttt{string}. Storing this string will allow us to memoize~\cite{michie68}
+We will modify our \verb|Dump| module to output the \dottool graph as a string,
+and store it in a hash table from \texttt{fundec} to \texttt{string}.
+Storing this string will allow us to memoize~\cite{michie68}
our computation: the string is computed the first time the CFG of a
function is displayed, while the following requests will reuse the result of
-the computation. Registering the hashtable as a \framac state is
+the computation. Registering the hash table as a \framac state is
\emph{mandatory} to ensure \framac consistency: for instance, by using a
-standard \caml hashtable, a user that would have loaded several session through
-the GUI could observe the CFG of function of a previous session instead of the
+standard \caml hash table, a user that would have loaded several sessions through
+a GUI could observe the CFG of function of a previous session instead of the
one he wants to observe.
Registering a state is done by a functor application:
-\ocamlinput{./tutorial/viewcfg/src/register_cfg_graph_state.ml}
+\ocamlinput[linerange={10-17}]{./tutorial/viewcfg/v5-state/dump.ml}
\scodeidx{State\_builder}{Hashtbl}
\scodeidx{Cil\_datatype}{Fundec}
\scodeidx{Datatype}{String}
\scodeidx{Ast}{self}
-\sscodeidx{Db}{Value}{self}
+\sscodeidx{Eva}{Analysis}{self}
The \texttt{State\_builder} module provides several functors that help
registering states. \texttt{State\_builder.Hashtbl} allows the developer to
-create a hashtable. It is parameterized by a module describing the hashtable
+create a hash table. It is parameterized by a module describing the hash table
and its key, a module describing the data associated to keys, and
-other informations.
+other information.
The \texttt{Datatype} and \texttt{Cil\_datatype} modules describe the
-hashtable and its associated data, and explain for instance how the
+hash table and its associated data, and explain for instance how the
datatype should be copied, printed, or marshalled to the disk. They
are part of the \texttt{Type} library~\cite{signoles:jfla11}, described in
Section~\ref{adv:datatype}. \texttt{Datatype} provides
descriptions for standard \caml types, and \texttt{Cil\_datatype} for
the CIL types (in the \texttt{Cil\_types} module).
-The last module argument describes the initial size of the hashtable, a name
-(mainly used for internal debugging), and a list of \emph{dependencies}. Here we
-expressed that our hashtable depends on the Ast and the results of the
-\texttt{Value} plug-in. For instance, whenever the \framac kernel updates one of these
-states, it will automatically reset our hashtable. This ensures consistency of
-the analysis: if the Ast of a function changes, or the value analysis is
-executed with a different entry point, this potentially affects the display of
-the control flow graph, that we must recompute.
+The last module argument describes the initial size of the hash table%
+\footnote{This initial size is an optimization feature; the table automatically
+grows when needed.}, a name (mainly used for internal debugging),
+and a list of \emph{dependencies}.
+Here we expressed that our hash table depends on the AST and the results of the
+\textsf{Eva} plug-in. For instance, whenever the \framac kernel updates one of
+these states, it will automatically reset our hash table.
+This ensures consistency of the analysis: if the AST of a function changes,
+or the value analysis is executed with a different entry point,
+this potentially affects the display of the control flow graph,
+that we must recompute.
Once the module has been declared, it is fairly easy to use it.
-\ocamlinput{./tutorial/viewcfg/src/dump_to_string_memoized.ml}
+\ocamlinput[linerange={3-8}]{./tutorial/viewcfg/v5-state/dump.ml}
\scodeidx{Visitor}{visitFramacFunction}
-\ocamlinput{./tutorial/viewcfg/src/dump_function_memo_no_clear_cache.ml}
+\ocamlinput[linerange={19-24}]{./tutorial/viewcfg/v5-state/dump.ml}
\texttt{dump\_function} now takes two steps: first the CFG is printed
to a string, then the string is printed to the \texttt{fmt}
argument. This allows the \texttt{dump\_to\_string} part to be
\emph{memoized}, \ie the results of \texttt{dump\_to\_string} are
saved so that later calls to \texttt{dump\_function} with the same
-\texttt{fundec} argument reuse that result.
+\texttt{fundec} argument reuse that result.
-If you launch \texttt{frama-c-gui} with the above code, click on
-functions to view their CFG, and inspect the console, you will observe
-that the string ``Computing CFG for function ...'' is displayed only
-once per function.
+To check this, we re-run our mini-GUI with:
-One can see the effects of the dependency on the \texttt{Value} plug-in
-by first launching the value analysis, inspecting the CFG for the
-\texttt{f} function, then changing the entry point to \texttt{f} in the
-CFG and re-running the value analysis. The console indicates that the
-\texttt{CFG} have been recomputed. Indeed the state of the
-\texttt{Value} plug-in, and of its dependencies, was reset when the
-entry point was changed.
+\begin{shell}
+\$ dune exec -- frama-c <file> -cfg-gui
+\end{shell}
+
+The first graph for each function will show the message
+``Computing CFG for function ...'', but subsequent calls will no longer do it.
+
+Also, we can see the effects of the dependency on the \textsf{Eva} plug-in
+by first launching the value analysis and then our plug-in:
+
+\begin{shell}
+\$ dune exec -- frama-c <file> -eva -then -cfg-gui
+\end{shell}
+
+In this case, the graphs will be colored.
+
+Finally, to check that the state dependency on \textsf{Eva} works, we will use
+a more complex command line:
+
+\begin{shell}
+\$ dune exec -- frama-c <file> -eva -then -cfg-gui -then -main f
+\end{shell}
+
+We have three stages: first run \textsf{Eva}, then open the mini-GUI, then
+change the entry point (\verb|-main f| means that the program will start
+executing from function \verb|f|) {\em and} re-open the mini-GUI.
+Remember that most \framac options {\em persist} from one stage to the next:
+the same way that we do not have to repeat \verb|-eva| after the first
+\verb|-then|, we do not have to repeat \verb|-cfg-gui| after the second
+\verb|-then|. If we want to avoid re-running the mini-GUI in future stages,
+we need to use \texttt{apply\_once}, as mentioned in Section~\ref{tut2:options}.
+
+What we observe is the following: when the mini-GUI opens, we click
+{\em Show CFG}, see a ``Computing CFG for function ...'' message, and get a
+mostly-green CFG. Then, we close the mini-GUI, and it opens again. Clicking
+{\em Show CFG} will show the same ``Computing CFG'' message, but the graph will
+be entirely pink: with \verb|f| as the entry point, function \verb|main| is
+never called, therefore entirely unreachable. Because the entry point changed,
+and \textsf{Eva} depends on its state, it is automatically recomputed.
+Because our plug-in depends on \textsf{Eva}'s state, it recomputes the graph
+when we ask again for the CFG.
Another way to observe how \framac automatically handles states is to display a
-CFG, save the session, close and restart \framac,
-and then reload the session: the control flow graph is not recomputed,
-which means that \framac has automatically saved the
-\texttt{Cfg\_graph\_state} with the rest of the session. Everything
-should also work properly when loading several sessions.
+CFG, save the session (option \verb|-save <file>|), and then load it again:
+
+\begin{shell}
+\$ dune exec -- frama-c <file> -eva -then -cfg-gui -save session.sav
+\end{shell}
+
+Then click on the ``Show CFG'' (see the feedback message), then close the CFG
+and the mini-GUI. Reload the session:
+
+\begin{shell}
+\$ dune exec -- frama-c -load session.sav
+\end{shell}
+
+Click ``Show CFG'' and you will {\em not} see the ``Computing CFG'' message:
+the state \texttt{Cfg\_graph\_state} had beem automatically saved by \framac
+and has just been loaded from the session.
\subsubsection{Clearing states, selection and projects}
There is one caveat though: if the user computes the CFG before
-running the \texttt{Value} analysis, and then runs \texttt{Value}, he
-will not see a colored graph (unless he re-launch the \texttt{Value}
-analysis with different parameters). This is because the state of the
-CFG is reset when the state of \texttt{Value} is reset, not when it is
+running the \textsf{Eva} analysis, and then runs \textsf{Eva}, they
+will not see a colored graph (unless they re-launch \textsf{Eva}
+with different parameters). This is because the state of the
+CFG is reset when the state of \textsf{Eva} is reset, not when it is
first computed.
To solve this problem, we will manually reset the
-\texttt{Cfg\_graph\_state} if we detect that the \texttt{Value}
-analysis has been run since the last time we computed the CFG. For
+\texttt{Cfg\_graph\_state} if we detect that \textsf{Eva}
+has been run since the last time we computed the CFG. For
that, we have to remember the previous value of
-\texttt{Db.Value.is\_computed ()}, \ie to register another state:
+\texttt{Eva.Analysis.is\_computed ()}, \ie to register another state:
-\ocamlinput{./tutorial/viewcfg/src/register_value_computed_state.ml}
+\ocamlinput[linerange={19-25}]{./tutorial/viewcfg/v6-state-clear/dump.ml}
\scodeidx{State\_builder}{Ref}
\scodeidx{Datatype}{Bool}
@@ -1352,29 +1370,29 @@ This new state only consists of a reference to a boolean value.
Then we just replace \texttt{dump\_function} in the code above by the
following.
-\ocamlinput{./tutorial/viewcfg/src/dump_function_memo_clear_cache.ml}
-\sscodeidx{Db}{Value}{is\_computed}
+\ocamlinput[linerange={29-37}]{./tutorial/viewcfg/v6-state-clear/dump.ml}
+\sscodeidx{Eva}{Analysis}{is\_computed}
\sscodeidx{State\_selection}{S}{with\_dependencies}
\scodeidx{Project}{clear}
-The only part that need to be explained is the notion of
+The only parts that need to be explained are the notions of
\emph{selection} and \emph{project}. A selection is just a set of
states; here we selected the state \texttt{Cfg\_graph\_state} with all
-its dependencies, as resetting this state would also impact states
-that would depend on it (even if there is none for now). We use
+of its dependencies, as resetting this state would also impact states
+that would depend on it (even if there are none for now). We use
\texttt{Project.clear} to reset the selection.
\subsubsection{Project explanation}
A \emph{project}~\cite{project} is a consistent version of all the \emph{states}
of \framac. \framac is multi-AST, \ie \framac plug-ins can change the AST of the
-program, or perform incompatible analysis (\eg with different entry
-points). Projects consistently groups a version of the AST of the program, with
-the states related to this AST.
+program, or perform incompatible analyses (\eg with different entry
+points). Projects consistently group a version of the program's AST with
+the states related to it.
-The \texttt{Project.clear} function has type :
+The \texttt{Project.clear} function has type:
\begin{ocamlcode}
-val clear: ?selection:State_selection.t -> ?project:t -> unit -> unit
+val clear: ?selection:State_selection.t -> ?project:t -> unit -> unit
\end{ocamlcode}
\scodeidxdef{Project}{clear}
\scodeidx{State\_selection}{t}
@@ -1406,16 +1424,16 @@ To summarize:
\item As a plug-in developer, you have to remember that is up to you to preserve
consistency between your states and their dependencies by clearing the latter
when the former is modified in an incompatible way. For instance, it would
- have been incorrect to not call
+ have been incorrect not to call
\texttt{State\_selection.with\_dependencies}
- \sscodeidx{State\_selection}{S}{with\_dependencies} in the last code snippet of
- this tutorial.
+ \sscodeidx{State\_selection}{S}{with\_dependencies}
+ in the last code snippet of this tutorial.
\end{itemize}
Projects are generally created using copy visitors. We encourage the reader to
-experiment with multiple projects development by using them. An interesting
+experiment with multi-project development by using them. An interesting
exercise would be to change the AST so that execution of each instruction is
-logged to a file, and then re-read that file to print in the CFG how much time
+logged to a file, and then re-read that file to print in the CFG how many times
each instruction has been executed. Another interesting exercise would be
to use the \texttt{apply\_once} function so that the ViewCfg plug-in is executed
only once, as explained in section~\ref{tut2:options} of this tutorial.
diff --git a/doc/developer/tutorial/viewcfg/pdfs/bogue.pdf b/doc/developer/tutorial/viewcfg/pdfs/bogue.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..a965650b1995fdad3e13a04b2da4ec7ed9b6bd84
GIT binary patch
literal 13321
zcmb_@1yo(Vwl41O?o!-cT3kwT*~Oj0#@$_u6lifTPSN7-?(S~IrMUI2_Wb9Zd*8X^
z+Iws4u_Vb(GQZ4ZeltR=EGf;x!ODk3TYFOeh{R37PGM(kg(NIY!KPqlYvKHXf(Hmv
zMWUdfV3W4Ab~bYap4LXrW|C$mcBW=XqM}Gn&W>hAHc0O2T<Yu);(8JkMjxySEG!FR
z(}y(%aEp`&VB^_2VIrAu@)?7fb^=0Ba6V4qUSXr+Ohp>WUqwZ+WG|tL$xr*!5d<cP
z%Vx)6pdvlsnj^8^>ju0*fOrxij6yQAHT|m;;O%$)epl-E6R4H|$M5LhA6);a{GaMd
zxjW0KIRjOt5ElL&09<TF?7#;Fn}iqz2L+pn5pV|t03!Z&X9Fo2TbY?S|4HM{OTqhF
z^xtv7@2@g`2mLPV-vA`=JJp{O|095Ym#XezZ$|O=%>SfRb1`=Q6DV!xX!9pTT-?r`
zLI=o-or05tgMx#Hk3#QHgsPd7or|N1nG*&7pMrq8`~z{O9VGQvJB&M=oZJ&!oGO3d
zSK|_S%SC}aBs;b{rNpf)%ceO|!OpF0Ke&$sBMxCgj3WE5aQ+tIFF1L4|1Rq9;{GP;
zpL+bi!pXr-0sQ_2&_7}S7ovdt{|}JL*%(=v{i(8+r757moC2JGzGTfTEj~B{=<@&h
zl(4h5b5yf8G69-K(#+M;#7tF2{7;OWEuiN1cE7cp!r9T~Z+VGZIy)(wIZD{s*xT8f
z**a73|2y43$$$rGXw8LkeU_v)%q{9!V<J_7VUkkMTfi0jh;z^?2QLK+SsX~gsG1+y
znoWiDig&^vR*k!ln`?07$&%}Z+)Zh01p<nZB;oyfHF>7jxQIno>%9J%J~$)ta?Ohd
zD*`<_gZ)DDIio=7b)j^$_AQTbG!c(4QI&Kw(d#maxkFpNL^1(ltjx-x0n53TS;wKb
zxCLyp`leeOSYPVcDoXa2h_j%0tj;9CVYSV-X^II3H|LS6)9hp-aynKEr7uBWdU|$y
zdd%SE8Bj=z8FMS$ceTTwQ(&*%h}Q2Ui&VUZmm@*VUcZc_*Q$2u+H%dV9?>&c1Z8pG
zDOeR01%LhV#$z(T@hi01qx=9mSx(8<Iw}g&`LbnHJ8#yRqSn!}cXOvaKHB!>=GS|7
z9FZiw33DIcX)_ACs;o~6`pA6vh^C1hr+z@4!%S8FijkF#F=xiEatH@jZ$s0q@S?MO
zeC;j@sD+SDTB%;iV~@~drL^pKbNi1a;GN{_HS!AkggK`#+J=itmeD_8Rz<t<uHsZr
zs0Ab>tqQ{P9M?Oi%@VF}%yCxi9<HLt!-;C^t82|q###&VO!h}r(NgmF(rETs*Ah#r
zd3s;54l}cQsTgkI98JW5Tk`OiBfb%$$Lg%vZDC<rx=1#?1Zg;<ma*wK$v3ppo_y}}
zvOIuS%o3R&{8?p>n~=n(ZDaK&=cNGt*BtLc!KLGM?^}(s*G;-Uu>D3i_<GB!wIw>J
zFDWv7bojRNEDIP(jg-900<ANTZ&Kc>o~FjGmMCI=cU>-AI!!jk6gH3UmxcC1yuLOz
z!H25P$+hUGH`~y(TcOZfAUYG__joAH2&#^3F8tP<6qa;0_Cqg0gXfk^*pyzksD&h{
zVR?CeeYTs4#u_Z9BDZ>?6r2QiqqLH-b%Y;2yeixh)Llo$_)7e{o`%!x;H=)=&e9QI
zz4fxg)6M~L{h?bgt)O6YV}r-{I(n9j<sPeY{m6)S18mGjb{z3#%hdLp8KKR`1C!f@
zuG0O91`X~{JA~;ggDGFLa{HBH()f38=tZ97<{Oa{cK6wgE%i6Gv%hF5n;vaAw|!N;
zyX$>Bd#c~|h;Cl{Q?{K4jO%jyRi5#QQz`jmsA?gB*#5l1O*=x%%E5Yaai9fTF#^_n
zGOUKL@YS-7&IXy$26@?c2Gj6@d<3K>u_5V#@_J(Zf$Qc4!{wm&0*)W2A=SONPW2oR
z(~e16`5vL+y^(^v9v|+l(H01?BR`4PTSMa)d)>|=ui!#{ZO9wJwt#_?Is0gl6cm`=
z;_dHrsBo|TKIGfH?bG~aLee#g*0E4*1nHD@Zf$W0uI-SvgC(IBvWWrgJm`H(UuT+2
z{XX+Vx`<M4$sW=+hqp{#S&-8{H4)ej7rd}liJ#N@Bbcdn-YDNSP&N(qM!>*faHMO<
zJ?K8pgx(=3iIku;SnBrjV%ZdZg_R=+nww9FycFSP(DlK3RQr0B?XrYORZ-tXp4CBC
zlqAt<&c!VbycFkSQ9-*$%6Ac=v)?Ym_R6PR?Te2>fuCp9&EDO`5g)ob7k*qO&pWyL
zFp*f(($Qp|X1R@pN>kO#%=^@(5mbnzvR3RZoG0vW_Kgo#_CN3}_&$Bl?Z04XA&m^Q
zcRlW5NcSH;TeWNQt$ukJZ5per6QL>@rGzYB2&Q>9V{#a7z9q*?_`)(ZYtS-7A#{uJ
zLwX!flh;V6K8xWsdef&Y!JyvJk-_DpxW?Di$o=)fcH;vheFVw-x+NtM(MnyF)UMKn
z`Df%pMw}+7DxB0@^vvE~%0DzEXH%Kx*<Yr<=MugbNH+gWA=uMLzeQqBYyZ)=>2Q<a
zG&9Kn;YdTj-16B{;~mRX&@*8QyVU+;kLkExL-@6$y`xmOE6j>MrIGnFg_M|<yNb$t
z*r5f+`gI-f9OId&sP?a-<A?6#_{gzh8B(=R3p5F(Z(mi*GIP|R5*IgE4H<`pq^Vs&
zPg!pvjbLBy-_sQd$|x>iFbm2{7%z;Zxn#8*Z>;alrPekCuMTULO54Kuf!Z8VSM=R`
zG5urhsi1p4c1XQbV39{7w_H6rstmnmW)=BbWsk`VLK%O}4kLPSL>~MhGA>&}Bxv`?
z&T%6$lV-)+wd(o@d6ub39%;H9o%#^FPgmzRwJ!Dw@7C98!qKwFr<U+u$AvEm2s)LX
z$SuR$NlK!jA=j^&wlj%h(o>rXHGA%mG5Ry8-k#3uHV}wx7u<bVj*(>|ZZ0>D&OcRT
zJtbR9t0G453qF7evF?<Sq74%wpRXjb7}wZftU<<SgETUwcGq*g>iM<_x4rEMPtRv~
z^kd7nbTzzB8$9R8#+R4g{8@hzL&bZLyUzZdbEboLj+k}TSY4?=olfDQz+f8OQRpdO
z%!ppoNw!#z@A6$K?&c$13S2}?G80|CdoKNVx^LMegsn_eR$2pz_D*k)?($4cBRbx_
zwUAS^71e6yL3FQjb3{a1h5EEwXR;4h9qn>G3I~}S_K8G-K2D|C*mzs0d+7mnZ*-sf
zQ9-^hlR=m<y|HhApFsfExBQ!3a+*Q-j{=JZ5`3s&4e&hmP`2U@sCvmXYz>WE1g)O&
zwLt(54#)^4y#4KUQV<bIyYIKP)#0$Jxe0glN5nv)P<UiX$=+n0C7eVOQHR5*plT*p
z;=GAv>Rb#Zy_Ht^;g}pHdM$LCDZLLK4Xn2CYgL~O^`ndzg!!GnwdTGRb70WQa$R6=
z=Gw)_h#*N{#Rvs$xfLHGl~_lSA6<TL{O}o~KJcrm)NTsrrM%aznX@^2*?VNRrUr*`
zxudIUVzrnf+wsZB0d0K00h-1hntW@Q70TA|AVJK<;oQr4>HUh2gRAKd{2%-xLVqeE
z_To~he#Dw$6yYp?_gU@g>Y|%0QiGSbb|E7kE-aWluy&;d%4m*Nzr4=P5fugPTk~qA
zi%xKH2rV);VAW%{J5wAa9Uex^=f+$+Qadj-8W@NMSY9z=lHrzLUZdB5S%=2Hji!7G
z#;Bj3datXljfa7Q^ko8fNYH4G7aoSouVc`EpvRi}#)&34btw`giWoLBHf(Xdl<;ld
zykt~N(i|P*4eP{O^J{3|Kn9qQV9J6GX@s}|_A26y5tpNPpGbrzYy0|FF;_8MeV(8K
zq^}de2%~d#Xd%69n3EHT;==y5PR?SI*e?i^qtjm1&4o&fRY{Sy{Ivp{53t6_oa-Ng
zc*OhGHoFt&N?~_1^l(xtNZ;4cZHD{q<mAT*FuCnkM6rPIbPNe}vWYX=?Pb>DN$(@6
zFQc|DNk3oigTmw)nDOIOF>#a93bLoGk9b;E$p~9biz!JOF4lknPK%!I4AVC;91BAD
zG-}P|b}cA4&y*Tl%^mrc0T0J4yd@r~2@2T|bu!GWBU~1~4b9ZNK1<>&WLWDX8uP@I
z*!PeAy`FFG{Xr%T#u^INQ0JDNL{yx}s0ea8U2X(vsV1ziw%)wDf!zCyfEQJpx^%>4
zG1?b8UWch*R2GNmYS*%cNr?Ij=0(5F*8?`>)ncp>UE!%->lkPOO>dUnU(I67hP_@A
zMSKo^T^h!(m_7KwFiGOOL)(_>k&+SZReGYYzsT|7PHbf^l}mpSd)?(vd`$07(wo+s
z>4CY@e3JGWK~_Hp(@e{$&Dw0{y;viKm#*;i5TWnRxsKPlKT*F%Cidb~gp1Y~I&Jmr
z+CtN@;>D#?aw_L!<vn?-B?*aK2+;Hs9Y?vOh`2%8cVK?u8neyJ52S&~>guL;?aK}x
zWMl3tTsW~gCaL^o(4s!730Z2kOJZEQ8Q+Lp<9a67tm5|Aw!u;f%P%`CXo_l|A?l@Q
zRzT#azLShXg`;MUr%Awg8naw$$l^TA>&ntkBt4S(je_W_1O|Kz2rXhb>5vUthMy4S
zbg|hkceX$xP|nPJztO|9LL0nuL=I6uI5Z|PiA3Gtaqm2hWoSJBp;gYosar)P;j?&&
z<kT5Dx5sB(sxhnETbMB-yEvWK5zA63EZyrWFk`#$gZB}BQ&woQj0e15v5Gb*WSOD*
zp}Ejh!n^H#7v*w|@sWCsYO{|_20Gd8n5bErZqZRKct!jO(xgTba}tg*94(fR*Gkja
zQR&e)x~d>s7@9}rG^Z<SWaXV}Om@Vs-T+B#${j2Wb^FlRXqZ#io=Wr9!Za4hMM+yQ
zUiu5cqr+~FxIf-^vt?mao4NbBlek3Qx(*h4w%5-cV!F*PUNCP=N{yIo+lsS|Fm;4o
zi`qO<Ra_DubZ6v`bBB4fYVlb08)WfiQelK#A4{v8bXSB`woMEPQx@xPe);eQzRy1F
zze6|Q7i?@YF-!=wz}aV2|H?hBUjw5-zee`jqt7~bRyD|sq4;362_u{cfvV#COWW`>
zByLr4BW<Go9sfw+m(2V{wx&8BaQ&Ic07J!6q94_(+hnD^h>aC&j<9h_GEq`Zcg~uP
zFG}W%p&5@eEKgyKWjN2ERzhwEk4eaBIN6~CR-SJyE7QJqFp-h!R<Jh?*lIPkNAG~)
zfRR<hfrn`8tt_aaIAm7PL~Ww#tV1kx(=X~?&O~le#i0F-br3(~`+hpF{__*eW3}V_
zh-Ni=m`ppPTEq|~mr)IWHLquL`vpx?v*UsfLb)b71bB!#>Ix)Qgi*oW6SLi3ksATh
zpEn4pzvoK8O3mA@K<P4A9;}3f`$Kl-j8-?VJ2ySGge6r(6o=$S5`XmB804&3Ms;)R
zrGLM?1Wh~R_6lMV;*@(WGUDx<4<@sOry=zXH@dyOd~KkoJLs<qjmS0%c%7K!wb<m#
zPd)>w524V7Ou6V;5hA{uhEnf*U2KL@kbaeR7sMS{5krR+m12?#YDuc@zHavwHq`b*
zOtEy-CWJq@r7TwQG6H|*iS=l@(VUt5NhTm8QvIpnlu5tdWn2L}%ZO|4inQ^Kq*Z89
zaQwg<kGO#EP!pzw10UdEWU4B_>woi`mLp%DiKfC^J~AB{qbYFSeonQZ<8`pi`m}#T
z$gL)+S}c%=`UR7ez4olbGF}2_Cjk#WRC4_#uiC&>IrpZ0ap~S|5fz;*QF8`#CY$j7
zlvCE%tbOxmuX2Xmt8lr2o1`xZ4<O5~FZZELrJU7~h}>2)g4U!je$;%Y+<Rm~`)y|R
zi8;@bjkMkUqlA1?5<YA4#E+u~kLY^Et&<wmInreod=Gv#MJn5cnBbYBi|KG4tC>5?
z9wHvAC+@%bx+W)ScJ0q0l2k5*1Yp0%<@L<ZvU#UCRnk-!)W*@0TQWUF5j~&6d9WhL
zF~Kxguc_u_X?!J1<7A)0LDX?~nE#E0MM5A6yDXoZ#n->?$NhdiuInwF=oFFrJze}9
zf89Us_k3hPni=I}_*v!?84nN7YP%mf-NW<kdh?KE`_tv{XL=<vQSb1~*UwkezaHCv
z9bNSK?az>w($do_rSn&{w2+`pgsirO42_JaYif>-jlJ~0ewlnpIrpY`ud7>{lf&V0
zxigt7GoC5(7)I{v?n5;J{i?jQl$)FTOI#cwm-$E(Ay>I>;}qdjvwZu@!;#y%&+YZR
z!LOTTyO!0fjA^FI(B9tAC>A2EPMu5<FF3X?>5si;ncHV)>+OEOfa<+G{TyHAJ+BuR
zayumvbpGJ!=^0kqNzBB^7>YvpH9voLVd3t!{a0&F4y3vFGe^hXy7$k~^Udzv-CYOd
zQiLt@ux$@BBPu{Z>_nZrjSL|-%`$D+zO%K~<#)Fyke;w}8<gkRc6N5}-@liWlXGxz
zAQ0f^ClDg8x}oy9p4Ebcgq)h1l8GTXSmL1gl2=f0bGj<T!h(w6X0u<Wp{W^qLdDFi
zaJNC9<^A3DL>s`^xQw(F3ap`_@pFG%rW}i${MXgN^jZ6_m#6!mr>CcUwkw7n$W?RN
zML8p*qd>+UKwZj7p`oHHD$agmc(Enba=J98gZw#z+cN&sr%&f%iHH84j9AN)!{0-(
zjynRN!_Ce~vU@J22?!ZzwGObsWg#uLt4%JirpaFWuGE@97yvD0c(POr7XI?q=DYM^
zlzt-5Mv$&qhd-pNt1FveSXJnfftVQNCNQ~hz)zK~m)*w1!Xg#=iCJAm1(OX43CW-F
zyE5}ugTpqfLEFeltfr=>)BadlMTLdk>t9blQHgm82ni`$>KfQSB9N>!IOIk}p&a5j
z1lQHoB_-iAMKUrm*;re%mmp%(ZQ#w#&DGnj_mKj(@{$rk->16>Z2H5aBMS?QYGW8F
zj3=vusr>1Jcf=gVFp8iS_luY3$Esy}6O&Q~CMJ^@lm3`q-IbM<a)b7@CAz5E+jT#`
z^Nr2{8VB5XR_Px}2EK$uL?z|rXyB1l9%L~j2Etp@?dow+i5GvPfx*E|Joer;pT}UY
zJ<#X)_;@^7EiHVt<ytU)-{+*H{)~wEpL?Uoh=`p>^h%jD^z_>b3rLfA!@(mM)!1kX
zvf73uE10(#f-Z*z@6y<L`cjjV37Y5A1)Llm9WhF)6b4-F5u5S0e{Dsw#h!HVH^7?L
zn+@ZUY(BKR9O1<u!Xo2k^PxaIr=_H12snjuCFSH$mN$9)+>2Z}&X^wl4yU8nU=PU}
zKvdS$)HLcu00tF&)2aXfla`k5+CW1?E4n;qAYrDYglufh$}-T?BUOBJiOyJWyZX@)
zTI^@;C()1L;f7<O)b`i<t)3bD4uQ0?g^C$aL_bb8yTiKpr0PRLLgeM;?cdHw+Vh&$
z5zs#coZNuGEio}MeMOZM{`l2!nh5Z?xVW<ZN?D?#h9g5mUH9kY*x1<aT^HN^n@>Mb
zA0Y?=OiU^a`OHc^+}(AXoDrXC=;*q*qNAfPnnK<YfV)Fcp)YS?#QnQTAcZhOvrK+=
zx;h^(aNM;A1VBcOunN1Ku22QU(i@Htctl1xmFB>M2t>N`t7yAQ2#C)&$9j$!)CxL&
zT@dL(x_Wqc5ZsJq2m#%9LD-0VA#0J4-I#!pk&%OgW1-W^$|^S3SjVumQ`s7CAlgWJ
z!J_vgE{H+*`U!oavOrK!FnQql@isCtvTCamVlD&~E;3}6gNH||J{iY4W*Jf>lvn|B
zqO#qnO7I}Xu3bMz|M8$OYvcU<RRb-rX{mZ7HUaq6*Emqu_@-jGWHtm`f8jYHDk^I7
zb7v4d^I-p4t?#qv@iIu+9l2cZyD1{FbT&jYRo4e~bsQ+vn2p|@!Oz=UTiV_^5ayT(
z7zP_R4Qz>zM-}aJGc!GCBOvId=ZEVcu4-p|vTL>gUpxevbL>rARwFPt@+U`p0+ZI3
zzBOOp$%f^E7pCYN@<^Yk+Am*lCc?;ok#X<fAmY5nVmuR%chgbUnaZ0)1uhOP2lB0d
zv!Qiyad9PXgYVUkNvF;=C|}Hn_J>2Js2je3V6P33#02I`k<Z-5+PTefKm#%t)E@F&
zB{u=IA_5v(pN<0R?Xw1j0^xIgibS0ust`@+Ora9FweoSAC`o5x<Ot*>FjTkq3N$u0
z`cKZz;+{fIcNVid<dLkct&PJTU?WJ?uim~%@M~S-@?(Zq2w=f1|5{iWb}Y`H3s$Mv
z^iGEpqQ36|FOV>hQ0$UGvo?9%+TO8?LMbooTs%CUwf7HhZf*iP-#2DwX}P$t5RNO8
z5&nGsV=}jE5ltW3G>^(Zl?kh=V1QDm5^f&1oN5!1pfEBL846yN0tW0ZiqY-RN0k2g
ze%z_kHJTwZJe)$M=RC8%WS%`LFOMcqB3TbPw|0<7Ft~lw`&dhNDtsOp);K4+s?L0r
zXzy#;wP2|c7)suH=NxhcVHzIa9a+sVOU&Q)LPRgDwCaokqqAxs!7m_u(@3b->bs+V
zRp=Lp{Ypqf%F02*0vp9@_#X-F!=Vlvv9gpKHv`hK))ZkLlTNa4VE7~s!>Nm8Vt-Mu
zZZ&m@=|;XKAtkMvus3u^yL{u0*05Y>LyYy>6lb6<)`@Dgva+&c3ke<WC6v*8AeORA
zbb@eh!#CWAf}5HenuPK!q?=i%F3RWEY#@&U;ZLbB{s3IMvaIM09^IPj+#uff-R3b1
z0YvirEIp#=?IH7>bmIm=JUb&97AK9_;eB=Yo$%y_>d7xfD!H-sHNK(il;Cqn5aM<x
z+MqZM_7uu_<U>pX84JjZbs*7VEIs1eQo1?%1o&kQf%^1#vD)YH1{RHZ)^3yt>op81
zjjw%ZN5`86k`jn=Y<|X}n*eBdPY;hxm<Grv!YV9cigIy6*dFCQY7PmwKrHCznmZ~)
zxdEU9Rnh0dpBjdh8a=|AEzm*`y@hgM<A+ubYzNxMTM6hxUdY1x9y+Cv9t~g5*^`${
zQ9TX-OTKA%_eCfi`wgU(YF_hixsL5B$>QIfM*5?@@5a1?-irw^dL3*AieO=$Lj+-u
zF=_YkC_qZ_-C!8aiT-+W$}0t7Y6jMtqaxBP1o*G*aeMje|8lEIwxOk^Rne#-Dj}V-
zzg%neQVFC)-G0JG#=*ewFNN;egdrejf~uE%Z4XEDt;6H~a+jFTw&#*^I_R<Xjtt%o
zQ-5;@<Z#*vn~rT%MLMS(Ugb&R1uGO-hHDq{-sGC-5r_S|3?G8uh;hXrQD`(IL_L#M
zxqY%BN)cgnRFr@B&v`>siC$TZRg71Qabwk?0SAYN##X?%$I@0kJU%Wn(tC;c>rfVX
zP8o-Sj%u{Sv=Ij<0_hL|B>~pKxJ;r`1=9?$(`3T#{(8uEaqJLO4czjXXxmFpom}u>
zFj!elT|M}^3kx3)udBHd#2g3#a%W42&pg=J=n%mQFro1Lnu-?#mCjB^Pfw3Ce{pef
zPClb1ARw?&Pdc}uesgmJK`w^p)@fO`O~feEz~l}0Sqdw10o5%;t2(8P4vc{{57>up
z=&F2wGwYXRSY0%+bQ_|I5u&H8SsybqvmZ#+ii(PT3xeHCPLOH{Hb?Un@V4x9Scu00
z8&E281_tCh<em_kKk)GD+<60o!q7+q(G8KMpdeN%1%Dt3&|sP19WPm+<}Nk4FpVs1
z<s1o>C7Gdy23}M(WOo4c2C$JsLr95ye0*VL`sx*k)o|+#?iW<N(tzp053pxxDk&;5
zq|g1$dyR5bgh)ialTWe$?$zP?@emHC_RdV0Zsl7^$xvUPw2Vyu$OsDc)zuY@XLuc(
zF=}~WBZY2P|2g&wrGTk{l3{98tymCT4tW%wNOd7MKonPA8@c<;*;8V$^YTiMp&%J5
zNpce$0-VEyzJ(LK@ST&3ORG#fWVWiNMsnN`#!K7U`uL|}W$40}FJFR(jj##ek%PsF
zFYrGAe9~A*{2@9d6gC#O#xR<eUdZ*hW0#%IKk#}29i`XtY@f6$RF^dF!tW{NwI()&
zA)hoO0Vye}nu%0p#45mR)}ci3g^OhJI%0aBZEfDY8$DfZ2AY3S$NdrDy5Fm-H`Ngl
z5#0l(6z)9mzqKnnRO($c`a8HQYHJg9{fO)fb(%nTq(?!?6<?7Y5nt;PKJN-aCctII
ze~C7@c_wOxaq4v6Ko2))2(Aj<l~xUVG-gkRTEKbPXH3>IHl~6SN&2wKql=kTLqM#H
z{|M)4n90n{FR+3ef_sW~YN#`k+6+5_(9~!@p`ARI!ev24MU^S)v$T~$Y5OrQ+X5w1
zhv9}4)i%Hx>OHO2ec(G1G0zd76sU@h-DI@#kb_Dp=G+d~08m7PNzEI$1!MA8tgLu1
zAqt_ySYGL&9!4na8RsT)8xcN;@Qr2Y9Hb#!kC&uzIK$E38jKs^i~65*RG109AvPi6
zpw=$$E=-hz7_k@@zdZ~399dA)OdS>VSB93=0)~Q}-TvDfQBl!>j95>~d+%C<aN0Rp
zy>DdQM3>m6#@Q&e5XOWciLTJ7(*z+&%AmYg%*>_m1YuXaKn~JWt-JpV*X_UU<NX&2
zJ(od`yGaJD`Yp)`3D>J`>#a+_P!*|KGk!;GhLJO~u)w1dIdAtxYdxmn(@ZTF*GJd3
z|9U<Hd>x=y+5x2M0zXDJ&rREo7)+z8G<#GXs&IBNUFhQCq6PSFG!vs~d@42~zE1@3
z-+-&61mNy~JLAQw_zZ9ZrA*;Q*ApVqChz;p>!bPhyDj8Ij;-9s+p}EkQzfLWuF%lX
zr6uk3i0y{qAb51`CmT<!gOhon5b*Z)c0xkJ?99x$n!diio}LID9UVWv`}N^0e-Uuy
z<iw?>4n0550q!gZ6BBsyt5iuz3BYCn#_r_iX5m+jb)6a=JqkEYcjucDedc0f0WmRX
zW9gzkO@V=dA3uI9E<Pw$D{Oe3_Liy@+tX+6O)Nl%0S5mVdEySXu$Zs611R<C(2%^L
z%XS~Ch=_=QKx0>zI9>@zSHiuk&^<0Wncw%x9UcACzD*S#5fLLLWtHEr7l4HsrAtXk
zZH#qvKp2&Oi+V$KkzH<FX3*|C08J=AKpBQgY;JDe_Z)Ej;|IWGWMrhIs@j>Nr(>yn
zA5ZEHeD8O2Wj+lJ57*Yzn2#hwHt6?g%gG@=e!gnJQ&-Fs{_PR!vHM{~u(`m4iz?qF
zwzY{evbl}{hPFU4<6|k-D-ryi*!=wbW489UZ{L0*;DF-ZgdsVL<v|!xOyx$jJUmj&
zl-yET?Ig-30DSPR-pI4n=Kit4!9g*!gQKIzQNHz!biieUq3ZzY=|z7(I-LEsw6vsF
zpwP)K*sZOrOY*P|j4j}CAQvU??|a+ZKWpCrzAGmuCxYuQJfLNa0DIU&RBUk+UAecn
zN5{tYDd<?uIQpuc;^qA#Fu$Ots!FGjTxrxD+U#})`27`tG662m@4rO)&DoCuo_+l1
z&w%`ZKuAB%)igC-0d8Eh8qV`a0e^E&5znh1Hz&*C%27P*Q-GHbF!kS)0mmd5FsE$*
zzfFJAJ^x0>KQ%Msyg!!l@Zk9*=`TUwfI<F8Q~mCD@#mJO3zZz8qz9gt2J6>-BVQWr
z`sDK5#IGJ>|97)3|3y#y?+gO1IN;suPb{CuRE|uS4b~P`hh;p&u2f4C^gW75Ri(>5
zvy@z!yRnfUkYa&|l}a(ed8hcGH1WS)K4-CC$QVb1s9mZ%Ql}*Uyft^Ea#l%~#x)uA
z0J|%;WDIQ>MTjZqWLMc9e1Vh~)N7!$?L^l0F~3lk8uK@k#D)GqDBBuHjU9=AU*7x}
zDi=2G=NdmOFdOCPf(zE}466;4pUsHJeJ8#%cQ;Ue6>osg-Ysa=rWB)T&!8Clev^{d
zbmoV^w>1QCYCx|Qnw&hb_^#&TKzY}~lLj;OzNh&IxP+1G0p%qOy6Uc0sctdd-ciNw
zcI8=C{Yie1YeM}oqtbn?@6g_|d2?PZc0mMBd}UKqZ8layG-me~e7Se(gu)s&6JOp>
zeg7#_LR17g2~KJgoAV!pS{Lr%@eV!3ND&|)2&HG?v+Ge13Aq+qK!VulP?`3;{ft3Q
zP0wRVH_xt)+V0&sBfsxK3X>y|Py??7J~f&!o$XY!K-ZW{sT*<0bi=Cxrbe2AdG5H<
zT{k`~qI*UvOjc*@dtfv_ThF(KqaoOgn5-j!2?&g_!!a<E$b>aWJ&uJd6ryZm9(`Lh
zIafKynIfxrC0$RM!}9PISiGi;zllP_$qkQc@gl=F68XX=lPYU~$obcW(tswD*6Yz`
z@IGs8f6C9gT7XSMuk}DPu_?OjI>1}TJnqO&?Y6~uD1_Kas@O{w?iM7<8e6FW$2^J#
zza_~!a)5xpP~)l$&OiaF^Yw0p-}tHaV5JLBo8z<pa;jm;Fw0tKKI?#_E*NoLjI1w%
zpA!W`s9AO=uKD!R_A#=akM<f0DhXCeV`*wt@%FPk2Z<UR2g&e2W37a~<(lh(i~d4T
zxZt<Y<15imjh$xxBZ|FKN*YHksBn~wUtZd~rnCnXf>{DrQg?x%pms$9AWc$e$*JX!
z^*~-|#7xEE+$D}2iq2S3^>aQ#9#tmemA6`6Mea<Z5q9kRgB(odg}ses3sin|jj8)e
zC4=C~r09|!A~}$rMup`aepIsA#9Ql)9;w7b*5YtwmT;3&RJA!3x22$kuq{PxSN(NL
z6J_|S;obQMpBV!z4P0b$#>6;78Ski;rk|N9X~tp~v6j_@Xg_^^hBC4|4I8YJ7ngj3
zL6=dt*$!1mgO;65R}HrNNPL|@_PA!SE<@t2B5PclGosFoCa!K~QwLsxYTtv1p8pyo
zeRIlo{nh<lX`Em&t2bIPrZV??H*9a>DmnA~ee0we^Q{-zW$ig|XP6kF@w7dzo-T5d
zGzB&>xA>h(H;vx%tyiRizLn6r5b~t5^+eIZ-m?8A%C{m)PAABMnib)lME=03;`RRR
z*NO8V;%LWiN1v7RUPIXmNl}@cRFK~s(h6p~y+)kt=^tQ74c?f3?~3>X5*qA78M>4{
zH{~R&x<9kKUSSD`GgNV57O^EsIxJxOnEb2Wm-nkF){@_k;7+yK_c)K0p9u7k-SYPu
z9wjDUBuw`x*hq!ei`)zlouSq<tu}%iZmI(5uwJL&p7L{g6lWCeR1Uu7ttC+40)Ks8
zKf6{D%GZ1ppaC7xE|GhQ9}VZz6=lar_|whFW~lJ_B$eT+bBZmuBqj5A;X&!9l`^E+
zLW1M53&3!RuWS$`5QuqwCbMKO#tvzDAuiAeGroH?ENsM4TM%Z~W0pKnt6xu0LJ)Gf
zp&D=5C(v$~g}zgWG@`gTy1n2Z!L+nV(=ZJy&2gGZHY~ZW_5n<a>LKe~AUYT>feQOE
zTgf0Xs<u0oqWna%fX{s?Yl|qI{GRyL8{O$Ewl5?V!uC7dDQ32+pUo9OA2{ZZHe`7u
zzF5lY_R0+VmKF{AT#wZ5Sx_GiuX&xZeZD?c!D@p7kB&=!fgP8Qf(qvW2;rlz3^GhW
z%&ph87{@Fn*h+CQemg-jKlE3zzK->C+Xk|bZlF^iIOPU2Njmv+D!ZQVs5wcejI1Vn
zRC*wl!^bv>BX0C6g;j>#pih#MKdtAlcqMe;$Dg1hm1%s>;}$wF)wom1@1Ab)dWa74
zXL!b+f>PTJhy~Q_n%>_DpB?Y9MT*=gfj+D?XTjL3)kcG}YWE;;l#2{WqJD-ku%w@*
zK__LlImnP-P-1O=nc(_qe>LrQm)HJu?PIxkUpjt(CzMB5vVq_mI9JyVHjG%YBH#H6
zEv?ua*_fF^1S#bt!kOA0!He`};qbiKdd5>NaVa+)hnzZ+2)nx*X5Yh%D)|PBSoV+p
zn~d6=6)iH+^fBd>98$kHtas*ae$3r3*Q|}SP&!<)C|k_u+h-tvN6jo*)ACe!eNY7*
zszjFGrn_p1F5muIT;bxJut`=v?#*|_y+_mSf{hQyPcEr`>2pMQrk@5>WJYG7ZK>kB
zC22&ZNl3WmaC0gp=3Y8jlopx2i{f2>8DUG&gnkTvn+xy%DMRdee4P^moQGfh4QL^X
zk!#_i(-wF#p<z+6QA)&$G(Sql%4Dhh`?f~=;l@nD6_a~d-+O*|qqhVf7i|w3>KX-T
zw;j`&)9Wb7a{P8un2CD|8;Vo6ZPOPOd58IX%Q*bs-$YouSL;prGsdu;3+0{03-;R>
z2q~SV(Jzpoq8qB~q7$@iXua3QivU>6yUBLklQzKW21@~^`S+^L|K<+Z{aMjF!Ill8
zTE#l*+ANpb%eXa4fFjUf9VAHoj~0UdKTwl@u0dUWFBS2+DFxWJZ1&dHmRg~rUb}DW
z4|Gz1lg*XsgrSq0+YJv5l>>9mmpgJdc>Qd8P0lY*9yfJ0HCHQ*PP4PKx_10O`=W`v
zT31^<urusi^%@;v-F7^`m6nzQj=9}id3k{Uf~~9?))dqE13K+nNd+8XGPddGi4{ei
z_E7keBcU8xGeo@bg7!Uy01mFFmtk+0d{<@C->}AxsoQlO8ertEYuBJ+W5ePmz*<^S
z(eF@R51udI#9Ns$G$jZ-IsqKnBsPORIH!jz%XBvDS5c^i4ndu*!J{$YkkOcV7QCw3
z#Snbp#*vAiLVDY~dy+=Fz3&OOaa}3*sWu7D;1jA3PhXt05i;+0Ug8!4Vs6&`eziV=
zz}D6%C@3>n9{`sGpufP}w6@=e*%A$40SQ>2IzIVsHtc%5P-WB&ccW=wus%LMzPOmu
z3ZUZR?2LklXk-UG72drA=87BEG|P2UVq*<Id>FXKBO{9u`d;4<2`u_FHw$?+n+{?L
z2{p6m)Y-QZ5);$Y(K)u3fvTu@dGTH^>NpeQ;hCG6^<MAMVt6&XUl<b;r`asmRn;To
zv+CB{>dDI^>D#v&Z2^<3=60wkDC}|X(s--t-zKs4c6j^vG_Kj_hKD2EXzJ*Aji&N=
z-5hs1xS9gA9$0AO=H%S+42nBBIT4U(Y-qT9d~`CeudED@iP`fET68;Gi%vsITkYuy
z<`OD*adgDu^|H5Tw|K?H#RZaHIIbk_>$rv!LP#V1>FDCJI}+p26%Vu&o94R)zETFd
zffQ13jl;IIQMH$+r(^5l(voq4Ky^1=a_Tu1QW|M%NNA{We()$-#m0!OjSZ@reQTLs
zGcOMhF5J!t87^)}!tMwe4h{_4mS;CN(2hpi-bU5Hn$-AeKT(9FC(l2%_<y#N`oHKv
zxwo=3SOyP%vq{S*|GG*2&#v&lcByl4@UnCLeWN<xKQ^lWeXG5av6Y(h-}cr2b&7$5
z^B-Hv6)8CWZ1a}3baZm2;Qs6VKR?<aGRlG6#f}5B(b~R+H_uyKOA(A#rc448VY{V#
znComQ9{=(AmM)Het-slg7DNa0@v#80*CiQ2=o|&1b7HHblY(0J2M>DL!^UPr&JHsh
z)44<jIaqjGt`KkkE#7SVEOD(B0;c#tdwx-bt^Q~wh!n4%<$`dm^o#0#h2mAFOuP?q
zrRA2NoMxFhO{CAt)e~$;95>;A0Mc(c{|*w*KOo}x=h=w=1fxIa9sb~<NWt}QFyi3*
zZ-K-U(~1<tjuYaRwPme=w6~UB7T)k<PD;Lhit<CaI0x4DM7>?Kvq1OelQ+soeu<Z9
zl5{6^4UA9YUnvF6u81Hp>McPR!7!UKT9ri2qhutrE+3r7&~z$DxAfnQ1*)|b;P>R-
z4r?P}>Tb_)Dn6%bTg2}qJ80hzj+I>!Iq1m8$0H3TGkoq%*@<{{pG5+SzC5&fR|GG4
zK2{snhV9Ao>OX+%@8>yyV;UU1|AgybRSKkPX8s3-zZ8n^?*RR);`~1Hp=Rl6M)B84
z11$<24hl{R&cDuc*x5M)$2<O^j&io<b`%`H58kN$yAuVt!#SA#Z!lmw8?m$7><QxC
zDa5xZA+X+14Fs~s=uI1!z!k|8(NM#DN*SU38tEIUJ7S1duU1-d|HSJOSCz0N+Ks+Y
fiiGvAGCMgNIXb&L0^)FRvGegG(b7sONhAFq<C@9L
literal 0
HcmV?d00001
diff --git a/doc/developer/tutorial/viewcfg/v1/ViewCfg.ml b/doc/developer/tutorial/viewcfg/v1-simple/ViewCfg.ml
similarity index 100%
rename from doc/developer/tutorial/viewcfg/v1/ViewCfg.ml
rename to doc/developer/tutorial/viewcfg/v1-simple/ViewCfg.ml
diff --git a/doc/developer/tutorial/viewcfg/v1-simple/dune b/doc/developer/tutorial/viewcfg/v1-simple/dune
new file mode 100644
index 00000000000..5d8c9ca6e63
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v1-simple/dune
@@ -0,0 +1,10 @@
+(library
+ (name ViewCfg)
+ (public_name frama-c-view-cfg.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel))
+
+(plugin
+ (name view-cfg)
+ (libraries frama-c-view-cfg.core)
+ (site (frama-c plugins)))
diff --git a/doc/developer/tutorial/viewcfg/v1-simple/dune-project b/doc/developer/tutorial/viewcfg/v1-simple/dune-project
new file mode 100644
index 00000000000..78c9ebfe3fd
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v1-simple/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(name frama-c-view-cfg)
+(package (name frama-c-view-cfg))
diff --git a/doc/developer/tutorial/viewcfg/v1-simple/tests/ptests_config b/doc/developer/tutorial/viewcfg/v1-simple/tests/ptests_config
new file mode 100644
index 00000000000..c286d4b312b
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v1-simple/tests/ptests_config
@@ -0,0 +1 @@
+DEFAULT_SUITES= viewcfg
diff --git a/doc/developer/tutorial/viewcfg/v1-simple/tests/test_config b/doc/developer/tutorial/viewcfg/v1-simple/tests/test_config
new file mode 100644
index 00000000000..f02f756a6e5
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v1-simple/tests/test_config
@@ -0,0 +1 @@
+PLUGIN: view-cfg
diff --git a/doc/developer/tutorial/viewcfg/v1-simple/tests/viewcfg/oracle/cfg.dot b/doc/developer/tutorial/viewcfg/v1-simple/tests/viewcfg/oracle/cfg.dot
new file mode 100644
index 00000000000..6d18d21ac40
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v1-simple/tests/viewcfg/oracle/cfg.dot
@@ -0,0 +1,32 @@
+digraph cfg {
+ subgraph cluster_f {
+ graph [label="f"];
+ s1 [label="g ++;"];
+ s1 -> s2;
+ s2 [label="g --;"];
+ s2 -> s16;
+ s16 [label="<return>"];
+ }
+ subgraph cluster_main {
+ graph [label="main"];
+ s5 [label="int i = 3;"];
+ s5 -> s7;
+ s7 [label="if i > 0"];
+ s7 -> s8;
+ s7 -> s13;
+ s8 [label="<loop>"];
+ s8 -> s9;
+ s9 [label="i --;"];
+ s9 -> s10;
+ s10 [label="if i"];
+ s10 -> s8;
+ s10 -> s11;
+ s11 [label="<break>"];
+ s11 -> s14;
+ s13 [label="f(3);"];
+ s13 -> s14;
+ s14 [label="__retres = 0;"];
+ s14 -> s18;
+ s18 [label="<return>"];
+ }
+}
diff --git a/doc/developer/tutorial/viewcfg/v1-simple/tests/viewcfg/oracle/test.res.oracle b/doc/developer/tutorial/viewcfg/v1-simple/tests/viewcfg/oracle/test.res.oracle
new file mode 100644
index 00000000000..ccfd0298d17
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v1-simple/tests/viewcfg/oracle/test.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing test.c (with preprocessing)
diff --git a/doc/developer/tutorial/viewcfg/v1/test.c b/doc/developer/tutorial/viewcfg/v1-simple/tests/viewcfg/test.c
similarity index 80%
rename from doc/developer/tutorial/viewcfg/v1/test.c
rename to doc/developer/tutorial/viewcfg/v1-simple/tests/viewcfg/test.c
index 727f15d69fd..78b057cb38e 100644
--- a/doc/developer/tutorial/viewcfg/v1/test.c
+++ b/doc/developer/tutorial/viewcfg/v1-simple/tests/viewcfg/test.c
@@ -1,8 +1,11 @@
+/* run.config
+ LOG: cfg.dot
+ OPT:
+ */
void f(int g)
{
g++;
g--;
-
}
int main(int argc, char **argv)
@@ -17,6 +20,5 @@ int main(int argc, char **argv)
{
f(3);
}
-
return 0;
}
diff --git a/doc/developer/tutorial/viewcfg/v1/view_cfg.ml b/doc/developer/tutorial/viewcfg/v1-simple/view_cfg.ml
similarity index 52%
rename from doc/developer/tutorial/viewcfg/v1/view_cfg.ml
rename to doc/developer/tutorial/viewcfg/v1-simple/view_cfg.ml
index a208d9f1bbb..0841af991e9 100644
--- a/doc/developer/tutorial/viewcfg/v1/view_cfg.ml
+++ b/doc/developer/tutorial/viewcfg/v1-simple/view_cfg.ml
@@ -1,25 +1,3 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2022 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
(*
This file is used by the ViewCfg tutorial.
NOTE: any modifications changing line numbers will impact the
@@ -67,7 +45,7 @@ class print_cfg out = object
end
let run () =
- let chan = open_out "cfg.out" in
+ let chan = open_out "cfg.dot" in
let fmt = Format.formatter_of_out_channel chan in
Visitor.visitFramacFileSameGlobals (new print_cfg fmt) (Ast.get ());
close_out chan
diff --git a/doc/developer/tutorial/viewcfg/v1/dune b/doc/developer/tutorial/viewcfg/v1/dune
deleted file mode 100644
index abc1f859c79..00000000000
--- a/doc/developer/tutorial/viewcfg/v1/dune
+++ /dev/null
@@ -1,34 +0,0 @@
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; ;;
-;; This file is part of Frama-C. ;;
-;; ;;
-;; Copyright (C) 2007-2022 ;;
-;; CEA (Commissariat à l'énergie atomique et aux énergies ;;
-;; alternatives) ;;
-;; ;;
-;; you can redistribute it and/or modify it under the terms of the GNU ;;
-;; Lesser General Public License as published by the Free Software ;;
-;; Foundation, version 2.1. ;;
-;; ;;
-;; It is distributed in the hope that it will be useful, ;;
-;; but WITHOUT ANY WARRANTY; without even the implied warranty of ;;
-;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ;;
-;; GNU Lesser General Public License for more details. ;;
-;; ;;
-;; See the GNU Lesser General Public License version 2.1 ;;
-;; for more details (enclosed in the file licenses/LGPLv2.1). ;;
-;; ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(library
- (name ViewCfg)
- (public_name frama-c-view-cfg.core)
- (flags -open Frama_c_kernel :standard)
- (libraries frama-c.kernel)
-)
-
-(plugin
- (name view-cfg)
- (libraries frama-c-view-cfg.core)
- (site (frama-c plugins))
-)
diff --git a/doc/developer/tutorial/viewcfg/v1/dune-project b/doc/developer/tutorial/viewcfg/v1/dune-project
deleted file mode 100644
index 4e3c156be6c..00000000000
--- a/doc/developer/tutorial/viewcfg/v1/dune-project
+++ /dev/null
@@ -1,27 +0,0 @@
-(lang dune 3.0)
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; ;;
-;; This file is part of Frama-C. ;;
-;; ;;
-;; Copyright (C) 2007-2022 ;;
-;; CEA (Commissariat à l'énergie atomique et aux énergies ;;
-;; alternatives) ;;
-;; ;;
-;; you can redistribute it and/or modify it under the terms of the GNU ;;
-;; Lesser General Public License as published by the Free Software ;;
-;; Foundation, version 2.1. ;;
-;; ;;
-;; It is distributed in the hope that it will be useful, ;;
-;; but WITHOUT ANY WARRANTY; without even the implied warranty of ;;
-;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ;;
-;; GNU Lesser General Public License for more details. ;;
-;; ;;
-;; See the GNU Lesser General Public License version 2.1 ;;
-;; for more details (enclosed in the file licenses/LGPLv2.1). ;;
-;; ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(using dune_site 0.1)
-
-(name frama-c-view-cfg)
-(package (name frama-c-view-cfg))
diff --git a/doc/developer/tutorial/viewcfg/v2-options/ViewCfg.ml b/doc/developer/tutorial/viewcfg/v2-options/ViewCfg.ml
new file mode 100644
index 00000000000..9107a4fed90
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v2-options/ViewCfg.ml
@@ -0,0 +1,3 @@
+(** ViewCfg plug-in.
+
+ No function is exported. *)
diff --git a/doc/developer/tutorial/viewcfg/v2-options/dune b/doc/developer/tutorial/viewcfg/v2-options/dune
new file mode 100644
index 00000000000..9351560d08d
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v2-options/dune
@@ -0,0 +1,10 @@
+(library
+ (name ViewCfg)
+ (public_name frama-c-view-cfg.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel frama-c-eva.core))
+
+(plugin
+ (name view-cfg)
+ (libraries frama-c-view-cfg.core)
+ (site (frama-c plugins)))
diff --git a/doc/developer/tutorial/viewcfg/v2-options/dune-project b/doc/developer/tutorial/viewcfg/v2-options/dune-project
new file mode 100644
index 00000000000..78c9ebfe3fd
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v2-options/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(name frama-c-view-cfg)
+(package (name frama-c-view-cfg))
diff --git a/doc/developer/tutorial/viewcfg/v2-options/view_cfg.ml b/doc/developer/tutorial/viewcfg/v2-options/view_cfg.ml
new file mode 100644
index 00000000000..8fa8244e8d4
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v2-options/view_cfg.ml
@@ -0,0 +1,74 @@
+(*
+ This file is used by the ViewCfg tutorial.
+ NOTE: any modifications changing line numbers will impact the
+ generated PDF for the development guide!
+*)
+
+open Cil_types
+
+module Self = Plugin.Register(struct
+ let name = "control flow graph"
+ let shortname = "viewcfg"
+ let help = "control flow graph computation and display"
+ end)
+
+module Enabled = Self.False(struct
+ let option_name = "-cfg"
+ let help =
+ "when on (off by default), computes the CFG of all functions."
+ end)
+
+module OutputFile = Self.String(struct
+ let option_name = "-cfg-output"
+ let default = "cfg.dot"
+ let arg_name = "output-file"
+ let help = "file where the graph is output, in dot format."
+ end)
+
+let print_stmt out = function
+ | Instr i -> Printer.pp_instr out i
+ | Return _ -> Format.pp_print_string out "<return>"
+ | Goto _ -> Format.pp_print_string out "<goto>"
+ | Break _ -> Format.pp_print_string out "<break>"
+ | Continue _ -> Format.pp_print_string out "<continue>"
+ | If (e,_,_,_) -> Format.fprintf out "if %a" Printer.pp_exp e
+ | Switch(e,_,_,_) -> Format.fprintf out "switch %a" Printer.pp_exp e
+ | Loop _ -> Format.fprintf out "<loop>"
+ | Block _ -> Format.fprintf out "<block>"
+ | UnspecifiedSequence _ -> Format.fprintf out "<unspecified sequence>"
+ | TryFinally _ | TryExcept _ | TryCatch _ -> Format.fprintf out "<try>"
+ | Throw _ -> Format.fprintf out "<throw>"
+
+class print_cfg out = object
+ inherit Visitor.frama_c_inplace
+
+ method! vfile _ =
+ Format.fprintf out "digraph cfg {\n";
+ Cil.DoChildrenPost (fun f -> Format.fprintf out "}\n%!"; f)
+
+ method! vglob_aux g =
+ match g with
+ | GFun(f,_) ->
+ Format.fprintf out " subgraph cluster_%a {\n" Printer.pp_varinfo f.svar;
+ Format.fprintf out " graph [label=\"%a\"];\n" Printer.pp_varinfo f.svar;
+ Cil.DoChildrenPost (fun g -> Format.fprintf out " }\n"; g)
+ | _ -> Cil.SkipChildren
+
+ method! vstmt_aux s =
+ Format.fprintf out " s%d [label=%S];\n"
+ s.sid (Pretty_utils.to_string print_stmt s.skind);
+ List.iter (fun succ -> Format.fprintf out " s%d -> s%d;\n" s.sid succ.sid)
+ s.succs;
+ Cil.DoChildren
+
+end
+
+let run () =
+ if Enabled.get() then
+ let filename = OutputFile.get () in
+ let chan = open_out filename in
+ let fmt = Format.formatter_of_out_channel chan in
+ Visitor.visitFramacFileSameGlobals (new print_cfg fmt) (Ast.get ());
+ close_out chan
+
+let () = Db.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/v3-eva/ViewCfg.ml b/doc/developer/tutorial/viewcfg/v3-eva/ViewCfg.ml
new file mode 100644
index 00000000000..9107a4fed90
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v3-eva/ViewCfg.ml
@@ -0,0 +1,3 @@
+(** ViewCfg plug-in.
+
+ No function is exported. *)
diff --git a/doc/developer/tutorial/viewcfg/v3-eva/dune b/doc/developer/tutorial/viewcfg/v3-eva/dune
new file mode 100644
index 00000000000..9351560d08d
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v3-eva/dune
@@ -0,0 +1,10 @@
+(library
+ (name ViewCfg)
+ (public_name frama-c-view-cfg.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel frama-c-eva.core))
+
+(plugin
+ (name view-cfg)
+ (libraries frama-c-view-cfg.core)
+ (site (frama-c plugins)))
diff --git a/doc/developer/tutorial/viewcfg/v3-eva/dune-project b/doc/developer/tutorial/viewcfg/v3-eva/dune-project
new file mode 100644
index 00000000000..78c9ebfe3fd
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v3-eva/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(name frama-c-view-cfg)
+(package (name frama-c-view-cfg))
diff --git a/doc/developer/tutorial/viewcfg/v3-eva/tests/ptests_config b/doc/developer/tutorial/viewcfg/v3-eva/tests/ptests_config
new file mode 100644
index 00000000000..c286d4b312b
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v3-eva/tests/ptests_config
@@ -0,0 +1 @@
+DEFAULT_SUITES= viewcfg
diff --git a/doc/developer/tutorial/viewcfg/v3-eva/tests/test_config b/doc/developer/tutorial/viewcfg/v3-eva/tests/test_config
new file mode 100644
index 00000000000..f02f756a6e5
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v3-eva/tests/test_config
@@ -0,0 +1 @@
+PLUGIN: view-cfg
diff --git a/doc/developer/tutorial/viewcfg/v3-eva/tests/viewcfg/oracle/cfg.dot b/doc/developer/tutorial/viewcfg/v3-eva/tests/viewcfg/oracle/cfg.dot
new file mode 100644
index 00000000000..6d604ab84c8
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v3-eva/tests/viewcfg/oracle/cfg.dot
@@ -0,0 +1,32 @@
+digraph cfg {
+ subgraph cluster_f {
+ graph [label="f"];
+ s1 [label="g ++;" fillcolor=pink style=filled]
+ s1 -> s2;
+ s2 [label="g --;" fillcolor=pink style=filled]
+ s2 -> s16;
+ s16 [label="<return>" fillcolor=pink style=filled]
+ }
+ subgraph cluster_main {
+ graph [label="main"];
+ s5 [label="int i = 3;" fillcolor="#ccffcc" style=filled]
+ s5 -> s7;
+ s7 [label="if i > 0" fillcolor="#ccffcc" style=filled]
+ s7 -> s8;
+ s7 -> s13;
+ s8 [label="<loop>" fillcolor="#ccffcc" style=filled]
+ s8 -> s9;
+ s9 [label="i --;" fillcolor="#ccffcc" style=filled]
+ s9 -> s10;
+ s10 [label="if i" fillcolor="#ccffcc" style=filled]
+ s10 -> s8;
+ s10 -> s11;
+ s11 [label="<break>" fillcolor="#ccffcc" style=filled]
+ s11 -> s14;
+ s13 [label="f(3);" fillcolor=pink style=filled]
+ s13 -> s14;
+ s14 [label="__retres = 0;" fillcolor="#ccffcc" style=filled]
+ s14 -> s18;
+ s18 [label="<return>" fillcolor="#ccffcc" style=filled]
+ }
+}
diff --git a/doc/developer/tutorial/viewcfg/v3-eva/tests/viewcfg/oracle/test.res.oracle b/doc/developer/tutorial/viewcfg/v3-eva/tests/viewcfg/oracle/test.res.oracle
new file mode 100644
index 00000000000..911280d1b80
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v3-eva/tests/viewcfg/oracle/test.res.oracle
@@ -0,0 +1,23 @@
+[kernel] Parsing test.c (with preprocessing)
+[eva] Warning: The inout plugin is missing: some features are disabled, and the analysis may have degraded precision and performance.
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva] test.c:17: starting to merge loop iterations
+[eva] done for function main
+[eva] Warning: The scope plugin is missing: cannot remove redundant alarms.
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 2): 50% coverage.
+ In this function, 8 statements reached (out of 9): 88% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 2 warnings
+ by the Frama-C kernel: 0 errors 0 warnings
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
diff --git a/doc/developer/tutorial/viewcfg/v3-eva/tests/viewcfg/test.c b/doc/developer/tutorial/viewcfg/v3-eva/tests/viewcfg/test.c
new file mode 100644
index 00000000000..cf5d86680d7
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v3-eva/tests/viewcfg/test.c
@@ -0,0 +1,24 @@
+/* run.config
+ LOG: cfg.dot
+ OPT: -eva -then -cfg
+ */
+void f(int g)
+{
+ g++;
+ g--;
+}
+
+int main(int argc, char **argv)
+{
+ int i = 3;
+
+ if( i > 0)
+ {
+ while(--i);
+ }
+ else
+ {
+ f(3);
+ }
+ return 0;
+}
diff --git a/doc/developer/tutorial/viewcfg/v3-eva/view_cfg.ml b/doc/developer/tutorial/viewcfg/v3-eva/view_cfg.ml
new file mode 100644
index 00000000000..1eefd2a6aaf
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v3-eva/view_cfg.ml
@@ -0,0 +1,82 @@
+(*
+ This file is used by the ViewCfg tutorial.
+ NOTE: any modifications changing line numbers will impact the
+ generated PDF for the development guide!
+*)
+
+open Cil_types
+
+module Self = Plugin.Register(struct
+ let name = "control flow graph"
+ let shortname = "viewcfg"
+ let help = "control flow graph computation and display"
+ end)
+
+module Enabled = Self.False(struct
+ let option_name = "-cfg"
+ let help =
+ "when on (off by default), computes the CFG of all functions."
+ end)
+
+module OutputFile = Self.String(struct
+ let option_name = "-cfg-output"
+ let default = "cfg.dot"
+ let arg_name = "output-file"
+ let help = "file where the graph is output, in dot format."
+ end)
+
+let print_stmt out = function
+ | Instr i -> Printer.pp_instr out i
+ | Return _ -> Format.pp_print_string out "<return>"
+ | Goto _ -> Format.pp_print_string out "<goto>"
+ | Break _ -> Format.pp_print_string out "<break>"
+ | Continue _ -> Format.pp_print_string out "<continue>"
+ | If (e,_,_,_) -> Format.fprintf out "if %a" Printer.pp_exp e
+ | Switch(e,_,_,_) -> Format.fprintf out "switch %a" Printer.pp_exp e
+ | Loop _ -> Format.fprintf out "<loop>"
+ | Block _ -> Format.fprintf out "<block>"
+ | UnspecifiedSequence _ -> Format.fprintf out "<unspecified sequence>"
+ | TryFinally _ | TryExcept _ | TryCatch _ -> Format.fprintf out "<try>"
+ | Throw _ -> Format.fprintf out "<throw>"
+
+class print_cfg out = object
+ inherit Visitor.frama_c_inplace
+
+ method! vfile _ =
+ Format.fprintf out "digraph cfg {\n";
+ Cil.DoChildrenPost (fun f -> Format.fprintf out "}\n%!"; f)
+
+ method! vglob_aux g =
+ match g with
+ | GFun(f,_) ->
+ Format.fprintf out " subgraph cluster_%a {\n" Printer.pp_varinfo f.svar;
+ Format.fprintf out " graph [label=\"%a\"];\n" Printer.pp_varinfo f.svar;
+ Cil.DoChildrenPost (fun g -> Format.fprintf out " }\n"; g)
+ | _ -> Cil.SkipChildren
+
+ method! vstmt_aux s =
+ let color =
+ if Eva.Analysis.is_computed () then
+ if Eva.Results.is_reachable s
+ then "fillcolor=\"#ccffcc\" style=filled"
+ else "fillcolor=pink style=filled"
+ else ""
+ in
+ Format.fprintf out " s%d [label=%S %s]\n"
+ s.sid (Pretty_utils.to_string print_stmt s.skind) color;
+ List.iter
+ (fun succ -> Format.fprintf out " s%d -> s%d;\n" s.sid succ.sid)
+ s.succs;
+ Cil.DoChildren
+
+end
+
+let run () =
+ if Enabled.get() then
+ let filename = OutputFile.get () in
+ let chan = open_out filename in
+ let fmt = Format.formatter_of_out_channel chan in
+ Visitor.visitFramacFileSameGlobals (new print_cfg fmt) (Ast.get ());
+ close_out chan
+
+let () = Db.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/v4-bogue/ViewCfg.ml b/doc/developer/tutorial/viewcfg/v4-bogue/ViewCfg.ml
new file mode 100644
index 00000000000..9107a4fed90
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v4-bogue/ViewCfg.ml
@@ -0,0 +1,3 @@
+(** ViewCfg plug-in.
+
+ No function is exported. *)
diff --git a/doc/developer/tutorial/viewcfg/v4-bogue/dump.ml b/doc/developer/tutorial/viewcfg/v4-bogue/dump.ml
new file mode 100644
index 00000000000..a83309c18d9
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v4-bogue/dump.ml
@@ -0,0 +1,9 @@
+open Cil_types
+
+let dump_function fundec fmt =
+ Options.Self.feedback "Computing CFG for function %s"
+ (fundec.svar.vorig_name);
+ Format.fprintf fmt "digraph %s {\n" fundec.svar.vorig_name;
+ ignore
+ (Visitor.visitFramacFunction (new Visit.print_cfg fmt) fundec);
+ Format.fprintf fmt "\n}\n"
diff --git a/doc/developer/tutorial/viewcfg/v4-bogue/dune b/doc/developer/tutorial/viewcfg/v4-bogue/dune
new file mode 100644
index 00000000000..bc08d2353b4
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v4-bogue/dune
@@ -0,0 +1,11 @@
+(library
+ (name ViewCfg)
+ (public_name frama-c-view-cfg.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel frama-c-eva.core bogue))
+
+(plugin
+ (name view-cfg)
+ (libraries frama-c-view-cfg.core)
+ (site (frama-c plugins))
+)
diff --git a/doc/developer/tutorial/viewcfg/v4-bogue/dune-project b/doc/developer/tutorial/viewcfg/v4-bogue/dune-project
new file mode 100644
index 00000000000..78c9ebfe3fd
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v4-bogue/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(name frama-c-view-cfg)
+(package (name frama-c-view-cfg))
diff --git a/doc/developer/tutorial/viewcfg/v4-bogue/gui.ml b/doc/developer/tutorial/viewcfg/v4-bogue/gui.ml
new file mode 100644
index 00000000000..ea90922dcb0
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v4-bogue/gui.ml
@@ -0,0 +1,37 @@
+open Bogue
+module W = Widget
+module L = Layout
+
+let show () =
+ (* Create a few widgets for our GUI: a label, a text input with the function
+ to be displayed, and a button to show it. *)
+ let l = W.label "Show graph for function:" in
+ let t = W.text_input ~text:"main" () in
+ let b = W.button "Show CFG" in
+ let status = W.label (String.make 50 '-') in (* used for error messages *)
+ let layout = L.tower_of_w [l;t;b;status] in
+ let show_graph _button =
+ let name = W.get_text t in
+ try
+ (* Check the function name exists and is defined (not just declared). *)
+ let kf = Globals.Functions.find_by_name name in
+ let fd = Kernel_function.get_definition kf in
+ W.set_text status "";
+
+ (* Create a temporary file with the graph and pass it to 'dotty'. *)
+ let (tmpname, oc) = Filename.open_temp_file "cfg_view" ".dot" in
+ Dump.dump_function fd (Format.formatter_of_out_channel oc);
+ close_out oc;
+ let cmd = Format.asprintf "dotty %S" tmpname in
+ ignore (Sys.command cmd);
+ W.set_text status (String.make 50 '-');
+ Unix.unlink tmpname
+ with
+ | Not_found ->
+ W.set_text status ("Error: function " ^ name ^ " not found.")
+ | Kernel_function.No_Definition ->
+ W.set_text status ("Error: function " ^ name ^ " is not defined.")
+ in
+ W.on_release ~release:show_graph b;
+ let board = Bogue.make [] [layout] in
+ Bogue.run board
diff --git a/doc/developer/tutorial/viewcfg/v4-bogue/options.ml b/doc/developer/tutorial/viewcfg/v4-bogue/options.ml
new file mode 100644
index 00000000000..be309367bc4
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v4-bogue/options.ml
@@ -0,0 +1,11 @@
+module Self = Plugin.Register(struct
+ let name = "control flow graph"
+ let shortname = "viewcfg"
+ let help = "control flow graph computation and display"
+ end)
+
+module Gui = Self.False(struct
+ let option_name = "-cfg-gui"
+ let help =
+ "when on (off by default), displays a mini-GUI for showing graphs."
+ end)
diff --git a/doc/developer/tutorial/viewcfg/v4-bogue/run.ml b/doc/developer/tutorial/viewcfg/v4-bogue/run.ml
new file mode 100644
index 00000000000..adc46ac9afe
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v4-bogue/run.ml
@@ -0,0 +1,5 @@
+let run () =
+ if Options.Gui.get() then
+ Gui.show ()
+
+let () = Db.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/v4-bogue/test.c b/doc/developer/tutorial/viewcfg/v4-bogue/test.c
new file mode 100644
index 00000000000..cf5d86680d7
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v4-bogue/test.c
@@ -0,0 +1,24 @@
+/* run.config
+ LOG: cfg.dot
+ OPT: -eva -then -cfg
+ */
+void f(int g)
+{
+ g++;
+ g--;
+}
+
+int main(int argc, char **argv)
+{
+ int i = 3;
+
+ if( i > 0)
+ {
+ while(--i);
+ }
+ else
+ {
+ f(3);
+ }
+ return 0;
+}
diff --git a/doc/developer/tutorial/viewcfg/v4-bogue/visit.ml b/doc/developer/tutorial/viewcfg/v4-bogue/visit.ml
new file mode 100644
index 00000000000..48f6a28b0c5
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v4-bogue/visit.ml
@@ -0,0 +1,47 @@
+open Cil_types
+
+let print_stmt out = function
+ | Instr i -> Printer.pp_instr out i
+ | Return _ -> Format.pp_print_string out "<return>"
+ | Goto _ -> Format.pp_print_string out "<goto>"
+ | Break _ -> Format.pp_print_string out "<break>"
+ | Continue _ -> Format.pp_print_string out "<continue>"
+ | If (e,_,_,_) -> Format.fprintf out "if %a" Printer.pp_exp e
+ | Switch(e,_,_,_) -> Format.fprintf out "switch %a" Printer.pp_exp e
+ | Loop _ -> Format.fprintf out "<loop>"
+ | Block _ -> Format.fprintf out "<block>"
+ | UnspecifiedSequence _ -> Format.fprintf out "<unspecified sequence>"
+ | TryFinally _ | TryExcept _ | TryCatch _ -> Format.fprintf out "<try>"
+ | Throw _ -> Format.fprintf out "<throw>"
+
+class print_cfg out = object
+ inherit Visitor.frama_c_inplace
+
+ method! vfile _ =
+ Format.fprintf out "digraph cfg {\n";
+ Cil.DoChildrenPost (fun f -> Format.fprintf out "}\n%!"; f)
+
+ method! vglob_aux g =
+ match g with
+ | GFun(f,_) ->
+ Format.fprintf out " subgraph cluster_%a {\n" Printer.pp_varinfo f.svar;
+ Format.fprintf out " graph [label=\"%a\"];\n" Printer.pp_varinfo f.svar;
+ Cil.DoChildrenPost (fun g -> Format.fprintf out " }\n"; g)
+ | _ -> Cil.SkipChildren
+
+ method! vstmt_aux s =
+ let color =
+ if Eva.Analysis.is_computed () then
+ if Eva.Results.is_reachable s
+ then "fillcolor=\"#ccffcc\" style=filled"
+ else "fillcolor=pink style=filled"
+ else ""
+ in
+ Format.fprintf out " s%d [label=%S %s]\n"
+ s.sid (Pretty_utils.to_string print_stmt s.skind) color;
+ List.iter
+ (fun succ -> Format.fprintf out " s%d -> s%d;\n" s.sid succ.sid)
+ s.succs;
+ Cil.DoChildren
+
+end
diff --git a/doc/developer/tutorial/viewcfg/v5-state/ViewCfg.ml b/doc/developer/tutorial/viewcfg/v5-state/ViewCfg.ml
new file mode 100644
index 00000000000..9107a4fed90
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v5-state/ViewCfg.ml
@@ -0,0 +1,3 @@
+(** ViewCfg plug-in.
+
+ No function is exported. *)
diff --git a/doc/developer/tutorial/viewcfg/v5-state/dump.ml b/doc/developer/tutorial/viewcfg/v5-state/dump.ml
new file mode 100644
index 00000000000..bccac711ae0
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v5-state/dump.ml
@@ -0,0 +1,24 @@
+open Cil_types
+
+let dump_to_string fundec =
+ Options.Self.feedback "Computing CFG for function %s"
+ (fundec.svar.vorig_name);
+ ignore
+ (Visitor.visitFramacFunction (new Visit.print_cfg Format.str_formatter) fundec);
+ Format.flush_str_formatter ()
+
+module Cfg_graph_state = State_builder.Hashtbl
+ (Cil_datatype.Fundec.Hashtbl)
+ (Datatype.String)
+ (struct
+ let name = "Dump.Cfg_graph_state"
+ let dependencies = [ Ast.self; Eva.Analysis.self ]
+ let size = 17
+ end)
+
+let dump_to_string_memoized = Cfg_graph_state.memo dump_to_string
+
+let dump_function fundec fmt =
+ Format.fprintf fmt "digraph %s {\n%s\n}\n"
+ fundec.svar.vorig_name
+ (dump_to_string_memoized fundec)
diff --git a/doc/developer/tutorial/viewcfg/v5-state/dune b/doc/developer/tutorial/viewcfg/v5-state/dune
new file mode 100644
index 00000000000..bc08d2353b4
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v5-state/dune
@@ -0,0 +1,11 @@
+(library
+ (name ViewCfg)
+ (public_name frama-c-view-cfg.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel frama-c-eva.core bogue))
+
+(plugin
+ (name view-cfg)
+ (libraries frama-c-view-cfg.core)
+ (site (frama-c plugins))
+)
diff --git a/doc/developer/tutorial/viewcfg/v5-state/dune-project b/doc/developer/tutorial/viewcfg/v5-state/dune-project
new file mode 100644
index 00000000000..78c9ebfe3fd
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v5-state/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(name frama-c-view-cfg)
+(package (name frama-c-view-cfg))
diff --git a/doc/developer/tutorial/viewcfg/v5-state/gui.ml b/doc/developer/tutorial/viewcfg/v5-state/gui.ml
new file mode 100644
index 00000000000..ea90922dcb0
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v5-state/gui.ml
@@ -0,0 +1,37 @@
+open Bogue
+module W = Widget
+module L = Layout
+
+let show () =
+ (* Create a few widgets for our GUI: a label, a text input with the function
+ to be displayed, and a button to show it. *)
+ let l = W.label "Show graph for function:" in
+ let t = W.text_input ~text:"main" () in
+ let b = W.button "Show CFG" in
+ let status = W.label (String.make 50 '-') in (* used for error messages *)
+ let layout = L.tower_of_w [l;t;b;status] in
+ let show_graph _button =
+ let name = W.get_text t in
+ try
+ (* Check the function name exists and is defined (not just declared). *)
+ let kf = Globals.Functions.find_by_name name in
+ let fd = Kernel_function.get_definition kf in
+ W.set_text status "";
+
+ (* Create a temporary file with the graph and pass it to 'dotty'. *)
+ let (tmpname, oc) = Filename.open_temp_file "cfg_view" ".dot" in
+ Dump.dump_function fd (Format.formatter_of_out_channel oc);
+ close_out oc;
+ let cmd = Format.asprintf "dotty %S" tmpname in
+ ignore (Sys.command cmd);
+ W.set_text status (String.make 50 '-');
+ Unix.unlink tmpname
+ with
+ | Not_found ->
+ W.set_text status ("Error: function " ^ name ^ " not found.")
+ | Kernel_function.No_Definition ->
+ W.set_text status ("Error: function " ^ name ^ " is not defined.")
+ in
+ W.on_release ~release:show_graph b;
+ let board = Bogue.make [] [layout] in
+ Bogue.run board
diff --git a/doc/developer/tutorial/viewcfg/v5-state/options.ml b/doc/developer/tutorial/viewcfg/v5-state/options.ml
new file mode 100644
index 00000000000..be309367bc4
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v5-state/options.ml
@@ -0,0 +1,11 @@
+module Self = Plugin.Register(struct
+ let name = "control flow graph"
+ let shortname = "viewcfg"
+ let help = "control flow graph computation and display"
+ end)
+
+module Gui = Self.False(struct
+ let option_name = "-cfg-gui"
+ let help =
+ "when on (off by default), displays a mini-GUI for showing graphs."
+ end)
diff --git a/doc/developer/tutorial/viewcfg/v5-state/run.ml b/doc/developer/tutorial/viewcfg/v5-state/run.ml
new file mode 100644
index 00000000000..adc46ac9afe
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v5-state/run.ml
@@ -0,0 +1,5 @@
+let run () =
+ if Options.Gui.get() then
+ Gui.show ()
+
+let () = Db.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/v5-state/test.c b/doc/developer/tutorial/viewcfg/v5-state/test.c
new file mode 100644
index 00000000000..cf5d86680d7
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v5-state/test.c
@@ -0,0 +1,24 @@
+/* run.config
+ LOG: cfg.dot
+ OPT: -eva -then -cfg
+ */
+void f(int g)
+{
+ g++;
+ g--;
+}
+
+int main(int argc, char **argv)
+{
+ int i = 3;
+
+ if( i > 0)
+ {
+ while(--i);
+ }
+ else
+ {
+ f(3);
+ }
+ return 0;
+}
diff --git a/doc/developer/tutorial/viewcfg/v5-state/visit.ml b/doc/developer/tutorial/viewcfg/v5-state/visit.ml
new file mode 100644
index 00000000000..48f6a28b0c5
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v5-state/visit.ml
@@ -0,0 +1,47 @@
+open Cil_types
+
+let print_stmt out = function
+ | Instr i -> Printer.pp_instr out i
+ | Return _ -> Format.pp_print_string out "<return>"
+ | Goto _ -> Format.pp_print_string out "<goto>"
+ | Break _ -> Format.pp_print_string out "<break>"
+ | Continue _ -> Format.pp_print_string out "<continue>"
+ | If (e,_,_,_) -> Format.fprintf out "if %a" Printer.pp_exp e
+ | Switch(e,_,_,_) -> Format.fprintf out "switch %a" Printer.pp_exp e
+ | Loop _ -> Format.fprintf out "<loop>"
+ | Block _ -> Format.fprintf out "<block>"
+ | UnspecifiedSequence _ -> Format.fprintf out "<unspecified sequence>"
+ | TryFinally _ | TryExcept _ | TryCatch _ -> Format.fprintf out "<try>"
+ | Throw _ -> Format.fprintf out "<throw>"
+
+class print_cfg out = object
+ inherit Visitor.frama_c_inplace
+
+ method! vfile _ =
+ Format.fprintf out "digraph cfg {\n";
+ Cil.DoChildrenPost (fun f -> Format.fprintf out "}\n%!"; f)
+
+ method! vglob_aux g =
+ match g with
+ | GFun(f,_) ->
+ Format.fprintf out " subgraph cluster_%a {\n" Printer.pp_varinfo f.svar;
+ Format.fprintf out " graph [label=\"%a\"];\n" Printer.pp_varinfo f.svar;
+ Cil.DoChildrenPost (fun g -> Format.fprintf out " }\n"; g)
+ | _ -> Cil.SkipChildren
+
+ method! vstmt_aux s =
+ let color =
+ if Eva.Analysis.is_computed () then
+ if Eva.Results.is_reachable s
+ then "fillcolor=\"#ccffcc\" style=filled"
+ else "fillcolor=pink style=filled"
+ else ""
+ in
+ Format.fprintf out " s%d [label=%S %s]\n"
+ s.sid (Pretty_utils.to_string print_stmt s.skind) color;
+ List.iter
+ (fun succ -> Format.fprintf out " s%d -> s%d;\n" s.sid succ.sid)
+ s.succs;
+ Cil.DoChildren
+
+end
diff --git a/doc/developer/tutorial/viewcfg/v6-state-clear/ViewCfg.ml b/doc/developer/tutorial/viewcfg/v6-state-clear/ViewCfg.ml
new file mode 100644
index 00000000000..9107a4fed90
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v6-state-clear/ViewCfg.ml
@@ -0,0 +1,3 @@
+(** ViewCfg plug-in.
+
+ No function is exported. *)
diff --git a/doc/developer/tutorial/viewcfg/v6-state-clear/dump.ml b/doc/developer/tutorial/viewcfg/v6-state-clear/dump.ml
new file mode 100644
index 00000000000..f3e8600ecca
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v6-state-clear/dump.ml
@@ -0,0 +1,37 @@
+open Cil_types
+
+let dump_to_string fundec =
+ Options.Self.feedback "Computing CFG for function %s"
+ (fundec.svar.vorig_name);
+ ignore
+ (Visitor.visitFramacFunction (new Visit.print_cfg Format.str_formatter) fundec);
+ Format.flush_str_formatter ()
+
+module Cfg_graph_state = State_builder.Hashtbl
+ (Cil_datatype.Fundec.Hashtbl)
+ (Datatype.String)
+ (struct
+ let name = "Dump.Cfg_graph_state"
+ let dependencies = [ Ast.self; Eva.Analysis.self ]
+ let size = 17
+ end)
+
+module Eva_is_computed = State_builder.Ref
+ (Datatype.Bool)
+ (struct
+ let name = "Dump.Eva_is_computed"
+ let dependencies = []
+ let default () = false
+ end)
+
+let dump_to_string_memoized = Cfg_graph_state.memo dump_to_string
+
+let dump_function fundec fmt =
+ if not (Eva_is_computed.get ()) && Eva.Analysis.is_computed () then begin
+ Eva_is_computed.set true;
+ let selection = State_selection.with_dependencies Cfg_graph_state.self in
+ Project.clear ~selection ();
+ end;
+ Format.fprintf fmt "digraph %s {\n%s\n}\n"
+ fundec.svar.vorig_name
+ (dump_to_string_memoized fundec)
diff --git a/doc/developer/tutorial/viewcfg/v6-state-clear/dune b/doc/developer/tutorial/viewcfg/v6-state-clear/dune
new file mode 100644
index 00000000000..bc08d2353b4
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v6-state-clear/dune
@@ -0,0 +1,11 @@
+(library
+ (name ViewCfg)
+ (public_name frama-c-view-cfg.core)
+ (flags -open Frama_c_kernel :standard)
+ (libraries frama-c.kernel frama-c-eva.core bogue))
+
+(plugin
+ (name view-cfg)
+ (libraries frama-c-view-cfg.core)
+ (site (frama-c plugins))
+)
diff --git a/doc/developer/tutorial/viewcfg/v6-state-clear/dune-project b/doc/developer/tutorial/viewcfg/v6-state-clear/dune-project
new file mode 100644
index 00000000000..78c9ebfe3fd
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v6-state-clear/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(name frama-c-view-cfg)
+(package (name frama-c-view-cfg))
diff --git a/doc/developer/tutorial/viewcfg/v6-state-clear/gui.ml b/doc/developer/tutorial/viewcfg/v6-state-clear/gui.ml
new file mode 100644
index 00000000000..ea90922dcb0
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v6-state-clear/gui.ml
@@ -0,0 +1,37 @@
+open Bogue
+module W = Widget
+module L = Layout
+
+let show () =
+ (* Create a few widgets for our GUI: a label, a text input with the function
+ to be displayed, and a button to show it. *)
+ let l = W.label "Show graph for function:" in
+ let t = W.text_input ~text:"main" () in
+ let b = W.button "Show CFG" in
+ let status = W.label (String.make 50 '-') in (* used for error messages *)
+ let layout = L.tower_of_w [l;t;b;status] in
+ let show_graph _button =
+ let name = W.get_text t in
+ try
+ (* Check the function name exists and is defined (not just declared). *)
+ let kf = Globals.Functions.find_by_name name in
+ let fd = Kernel_function.get_definition kf in
+ W.set_text status "";
+
+ (* Create a temporary file with the graph and pass it to 'dotty'. *)
+ let (tmpname, oc) = Filename.open_temp_file "cfg_view" ".dot" in
+ Dump.dump_function fd (Format.formatter_of_out_channel oc);
+ close_out oc;
+ let cmd = Format.asprintf "dotty %S" tmpname in
+ ignore (Sys.command cmd);
+ W.set_text status (String.make 50 '-');
+ Unix.unlink tmpname
+ with
+ | Not_found ->
+ W.set_text status ("Error: function " ^ name ^ " not found.")
+ | Kernel_function.No_Definition ->
+ W.set_text status ("Error: function " ^ name ^ " is not defined.")
+ in
+ W.on_release ~release:show_graph b;
+ let board = Bogue.make [] [layout] in
+ Bogue.run board
diff --git a/doc/developer/tutorial/viewcfg/v6-state-clear/options.ml b/doc/developer/tutorial/viewcfg/v6-state-clear/options.ml
new file mode 100644
index 00000000000..be309367bc4
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v6-state-clear/options.ml
@@ -0,0 +1,11 @@
+module Self = Plugin.Register(struct
+ let name = "control flow graph"
+ let shortname = "viewcfg"
+ let help = "control flow graph computation and display"
+ end)
+
+module Gui = Self.False(struct
+ let option_name = "-cfg-gui"
+ let help =
+ "when on (off by default), displays a mini-GUI for showing graphs."
+ end)
diff --git a/doc/developer/tutorial/viewcfg/v6-state-clear/run.ml b/doc/developer/tutorial/viewcfg/v6-state-clear/run.ml
new file mode 100644
index 00000000000..adc46ac9afe
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v6-state-clear/run.ml
@@ -0,0 +1,5 @@
+let run () =
+ if Options.Gui.get() then
+ Gui.show ()
+
+let () = Db.Main.extend run
diff --git a/doc/developer/tutorial/viewcfg/v6-state-clear/test.c b/doc/developer/tutorial/viewcfg/v6-state-clear/test.c
new file mode 100644
index 00000000000..cf5d86680d7
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v6-state-clear/test.c
@@ -0,0 +1,24 @@
+/* run.config
+ LOG: cfg.dot
+ OPT: -eva -then -cfg
+ */
+void f(int g)
+{
+ g++;
+ g--;
+}
+
+int main(int argc, char **argv)
+{
+ int i = 3;
+
+ if( i > 0)
+ {
+ while(--i);
+ }
+ else
+ {
+ f(3);
+ }
+ return 0;
+}
diff --git a/doc/developer/tutorial/viewcfg/v6-state-clear/visit.ml b/doc/developer/tutorial/viewcfg/v6-state-clear/visit.ml
new file mode 100644
index 00000000000..48f6a28b0c5
--- /dev/null
+++ b/doc/developer/tutorial/viewcfg/v6-state-clear/visit.ml
@@ -0,0 +1,47 @@
+open Cil_types
+
+let print_stmt out = function
+ | Instr i -> Printer.pp_instr out i
+ | Return _ -> Format.pp_print_string out "<return>"
+ | Goto _ -> Format.pp_print_string out "<goto>"
+ | Break _ -> Format.pp_print_string out "<break>"
+ | Continue _ -> Format.pp_print_string out "<continue>"
+ | If (e,_,_,_) -> Format.fprintf out "if %a" Printer.pp_exp e
+ | Switch(e,_,_,_) -> Format.fprintf out "switch %a" Printer.pp_exp e
+ | Loop _ -> Format.fprintf out "<loop>"
+ | Block _ -> Format.fprintf out "<block>"
+ | UnspecifiedSequence _ -> Format.fprintf out "<unspecified sequence>"
+ | TryFinally _ | TryExcept _ | TryCatch _ -> Format.fprintf out "<try>"
+ | Throw _ -> Format.fprintf out "<throw>"
+
+class print_cfg out = object
+ inherit Visitor.frama_c_inplace
+
+ method! vfile _ =
+ Format.fprintf out "digraph cfg {\n";
+ Cil.DoChildrenPost (fun f -> Format.fprintf out "}\n%!"; f)
+
+ method! vglob_aux g =
+ match g with
+ | GFun(f,_) ->
+ Format.fprintf out " subgraph cluster_%a {\n" Printer.pp_varinfo f.svar;
+ Format.fprintf out " graph [label=\"%a\"];\n" Printer.pp_varinfo f.svar;
+ Cil.DoChildrenPost (fun g -> Format.fprintf out " }\n"; g)
+ | _ -> Cil.SkipChildren
+
+ method! vstmt_aux s =
+ let color =
+ if Eva.Analysis.is_computed () then
+ if Eva.Results.is_reachable s
+ then "fillcolor=\"#ccffcc\" style=filled"
+ else "fillcolor=pink style=filled"
+ else ""
+ in
+ Format.fprintf out " s%d [label=%S %s]\n"
+ s.sid (Pretty_utils.to_string print_stmt s.skind) color;
+ List.iter
+ (fun succ -> Format.fprintf out " s%d -> s%d;\n" s.sid succ.sid)
+ s.succs;
+ Cil.DoChildren
+
+end
diff --git a/doc/frama-c-book.cls b/doc/frama-c-book.cls
index ef5703754df..cb6f16df585 100644
--- a/doc/frama-c-book.cls
+++ b/doc/frama-c-book.cls
@@ -335,8 +335,8 @@ morekeywords={include},%
{language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic}
\lstnewenvironment{ccode}[1][]%
{\lstset{language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic,#1}}{}
-\newcommand{\cinput}[1]%
-{\lstinputlisting[language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic]{#1}}
+\newcommand{\cinput}[2][]%
+{\lstinputlisting[language={[ANSI]C},alsolanguage=ACSL,style=framac-code-style,basicstyle=\lp@basic,#1]{#2}}
\newcommand{\cinline}[1]%
{\lstinline[style=framac-code]{#1}}
% --- Ocaml ----------------------------------------------------------------
--
GitLab