diff --git a/doc/aorai/.gitignore b/doc/aorai/.gitignore
index 6a221921fab276e8a0562d04cb7d688a80d69827..2bc720799abbe79ef5af31c9b5b52293bcf71364 100644
--- a/doc/aorai/.gitignore
+++ b/doc/aorai/.gitignore
@@ -1,2 +1,8 @@
/transf.cm*
/transf
+/frama-c-book.cls
+/fc-macros.tex
+/logos
+/anr-logo.png
+/eu-flag.jpg
+/frama-c-guy.png
diff --git a/doc/aorai/Makefile b/doc/aorai/Makefile
index 4b28a27814427ee7c44d6158b311b0fed5c16f37..a05e3b73fc55fb225ac2ed61d48957451285dada 100644
--- a/doc/aorai/Makefile
+++ b/doc/aorai/Makefile
@@ -32,11 +32,14 @@ EXAMPLES=example.c example.ya \
example_loop.c example_loop.ya \
README.md
-BNF=ya_file.bnf basic_ya.bnf extended_ya.bnf ya_variables.bnf
-
all: main.pdf $(ARCHIVENAME).tar.gz
+include ../MakeLaTeXModern
+
+BNF=ya_file.bnf basic_ya.bnf extended_ya.bnf ya_variables.bnf
+
main.pdf: main.tex $(BNF:.bnf=.tex) macros.tex
+ $(MAKE) $(FRAMAC_MODERN)
touch main.aux #work around latexmk bug
latexmk -pdf main.tex
diff --git a/doc/aorai/main.tex b/doc/aorai/main.tex
index b2739cff1da393a8c148c43c2116a7bf22e48972..bcdb2d0309e4aeec8d9b3e6da35057b8a93f4d9b 100644
--- a/doc/aorai/main.tex
+++ b/doc/aorai/main.tex
@@ -1,4 +1,4 @@
-\documentclass{report}
+\documentclass{frama-c-book}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
@@ -25,22 +25,6 @@
%\setboolean{extension}{true}
-\lstdefinelanguage{ACSL}{%
- morekeywords={assert,assigns,assumes,axiom,axiomatic,behavior,behaviors,
- boolean,breaks,complete,continues,data,decreases,disjoint,ensures,
- exit_behavior,ghost,global,inductive,integer,invariant,lemma,logic,loop,
- model,predicate,reads,real,requires,returns,sizeof,strong,struct,terminates,type,
- union,variant},
-% otherkeywords={\\at,\\base_addr,\\block_length,\\false,\\fresh,\\from,
-% \\initialized,\\lambda,\\let,\\match,\\max,\\nothing,\\null,
-% \\numof,\\old,\\result,\\specified,\\strlen,\\sum,\\true,
-% \\valid,\\valid_range},
- keywordsprefix={\\},
- alsoletter={\\},
- morecomment=[l]{//},
- moredelim=*[s]{/*@}{*/}
-}
-
\lstdefinelanguage{ya}{
alsoletter={\\,\%,\$},
morekeywords={CALL,RETURN,COR,return,true,false,transitions,\\result,other},
@@ -51,19 +35,29 @@
\lstset{
basicstyle=\ttfamily,
keywordstyle=\bfseries,
+mathescape=false
}
+\newcommand{\framacversion}%
+ {\input{../../VERSION} (\input{../../VERSION_CODENAME}\unskip)}
+
\title{\aorai\ Plugin Tutorial\\\textit{\normalsize (A.k.a. LTL to ACSL)}}
\author{Nicolas Stouls and Virgile Prevosto\\
\small\textit{Nicolas.Stouls@insa-lyon.fr},\textit{virgile.prevosto@cea.fr}}
-\date{\today}
+
+\fcversion{\framacversion}
+
+\cclicence{by-sa}
+\copyrightstarts{2009}
\begin{document}
+\sloppy
+\emergencystretch 3em
\maketitle
\section*{Foreword}
-\aorai is a Frama-C plugin that provides a method to automatically annotate a
+\aorai is a Frama-C plugin that provides a method to automatically annotate a
C program according to an automaton $F$ such that, if the annotations
are verified, we ensure that the program respects $F$. A classical method to
validate annotations then is to use Eva or WP.
@@ -75,16 +69,16 @@ in particular the notions of {\it plug-ins} and {\it project}.
\vspace*{20pt}
\noindent \textbf{Notes:}
\begin{itemize}
- \item to the question "Why this name: \textit{\aorai} ?"
- my answer is: why not~? \aorai is the name of the tallest reachable
+ \item to the question "Why this name: \textit{\aorai}?"
+ my answer is: why not? \aorai is the name of the tallest reachable
mount in the Tahiti island and its reachability is not always obvious.
\end{itemize}
\vspace*{20pt}
-\noindent \textbf{Official web site for the original version:}
+\noindent \textbf{Official website for the original version:}
\begin{center}
- \url{http://amazones.gforge.inria.fr/aorai/index.html}
+ \url{https://www.frama-c.com/fc-plugins/aorai.html}
\end{center}
\tableofcontents
@@ -99,7 +93,7 @@ in particular the notions of {\it plug-ins} and {\it project}.
with Frama-C. Installation instructions for Frama-C are available at
\url{https://frama-c.com/html/get-frama-c.html}.
-\section{Interest of \aorai }
+\section{Interest of \aorai}
As explained before, \aorai 's goal is to prove that the C program
works like a given automaton. The approach used by \aorai has two
@@ -123,7 +117,7 @@ This document is divided into four parts:
software.
\item The second part defines the \aorai input language with which it is
possible to describe a given property.
-\item The third part explains how to prove a program annotated with \aorai
+\item The third part explains how to prove a program annotated with \aorai
using the WP plug-in.
\item Finally, the last part details \aorai's underlying theory, and its
internal architecture in order to help people who would like to contribute to
@@ -136,7 +130,7 @@ the plug-in itself.
\chapter{Quick overview}
In this chapter we will see how to use Frama-C and the couple
-WP-\aorai to prove that a C program has the same behavior than
+WP-\aorai to prove that a C program has the same behavior as
an automaton.
\section{First use}
@@ -148,10 +142,10 @@ an automaton.
that we have already written the file which describes the automaton.
WP verification\footnote{For more information about WP
- and code verification,please refer to
+ and code verification, please refer to
\url{http://frama-c.com/wp.html}} can only be done on C
- code augmented with ACSL annotations. Thus,
- \aorai creates a new C file where the automaton is encoded into ACSL
+ code augmented with ACSL annotations. Thus,
+ \aorai creates a new C file where the automaton is encoded into ACSL
annotations. Section~\ref{generated_annotated_file} will give more
information about the annotations generated by \aorai
@@ -165,32 +159,32 @@ an automaton.
With these two files (automaton's description and C file), we can create an
annotated file. This
is done by the following command:
-\begin{lstlisting}
-$ frama-c example.c -aorai-automata example.ya \
+\begin{frama-c-commands}
+\$ frama-c example.c -aorai-automata example.ya \
-then-last -ocode example_annot.c -print
-\end{lstlisting} %$
+\end{frama-c-commands} %$
This generates a new C file \texttt{example\_annot.c}.
In order to decide if the original program is correct with respect to
the automaton, it is sufficient to establish that the generated C code and
its associated ACSL annotations are valid. For instance, the following command
uses the WP plugin over the generated file:
-\begin{lstlisting}[language=sh]
-$ frama-c example_annot.c -wp -wp-rte
-\end{lstlisting} %$
+\begin{frama-c-commands}
+\$ frama-c example_annot.c -wp -wp-rte
+\end{frama-c-commands} %$
Of course, any option of WP itself can be used, notably \texttt{-wp-rte} to
check for the absence of runtime error.
Finally, it is possible to instruct Frama-C to do a
-sequence of analyses over various projects, {\it via} the \texttt{-then-on}
+sequence of analyzes over various projects, {\it via} the \texttt{-then-on}
options and \texttt{-then-last} options.
Thus, we do not need to use an intermediate file and to run Frama-C
twice. Instead, we just instruct WP to operate on the \texttt{aorai}
project that contains the code annotated by \aorai:
-\begin{lstlisting}
-$ frama-c example.c -aorai-automata example.ya \
+\begin{frama-c-commands}
+\$ frama-c example.c -aorai-automata example.ya \
-then-last -wp -wp-rte
-\end{lstlisting} %$
+\end{frama-c-commands} %$
\subsection{Automata and verification}
The main interest of \aorai is to prove that the program can be
@@ -232,11 +226,11 @@ write automata in \aorai are listed in the next chapter.
\end{tabular}
}
-Finally, the C-code which will be checked is given in
+Finally, the C-code which will be checked is given in
figure~\ref{example_c_file}.
\begin{figure}[ht]
-\lstinputlisting[language=C,alsolanguage=ACSL]{example/example.c}
+\lstinputlisting[style=c]{example/example.c}
\caption{Example of C File}
\label{example_c_file}
\end{figure}
@@ -262,7 +256,7 @@ information about that, please read section \ref{collaboration}.
The \texttt{frama-c -aorai-help} command returns the list of options for the
\aorai plug-in. Here are the most common ones:
- \begin{itemize}
+ \begin{description}
\item[-aorai-automata <f>] considers the property described by the ya
automata (in Ya language) from file \texttt{<f>}
\item[-aorai-verbose <n>] gives some information during computation,
@@ -271,8 +265,8 @@ information about that, please read section \ref{collaboration}.
\item[-aorai-dot] generates a dot file of the automata.
Dot is a graph format used by the
GraphViz tools\footnote{\url{http://www.graphviz.org}}.
-
- \end{itemize}
+
+ \end{description}
\section{Known Restrictions}
@@ -311,7 +305,7 @@ A YA file follows the grammar described in Fig.~\ref{ya-file}.
\end{figure}
The directives specify the initial and accepting state(s). There must be at
least one initial state (exactly one if the automaton is supposed to be
-deterministic. All initial and accepting state must appear in the list of
+deterministic). All initial and accepting state must appear in the list of
states afterwards.
A state is simply described by its name and the list of transitions
@@ -323,7 +317,7 @@ Conditions that can occur in guards are described in the next section.
\begin{new}
By default, \aorai considers that all functions calls and returns trigger
-a transition of the automaton. In order to have transitions only for the
+a transition of the automaton. In order to have transitions only for the
functions that explicitly appear in the description of the automaton, the
following directive must be used:
\begin{lstlisting}[language=ya]
@@ -343,24 +337,24 @@ figure~\ref{fig:basic_ya}.
Basically, a condition is a logical expression obtained from the following
atoms:
\begin{itemize}
-\item \lstinline|CALL|, \lstinline|RETURN| or \lstinline|COR| event, indicating
+\item \lstinline|CALL|, \lstinline|RETURN| or \lstinline|COR| event, indicating
respectively the call, the return, the call or the return
of the corresponding function;
\item A relation over the variables of the programs. In addition to global
-variables, that are directly accessed through their \lstinline|id|,
+variables, that are directly accessed through their \lstinline|id|,
it is possible to consider the value returned by a function or the value of
-its formal parameters. This is done through
+its formal parameters. This is done through
\lstinline|f().return| and \lstinline|f().a| respectively.
-In order to be closer to ACSL's syntax,
-\lstinline|f().\result| is accepted as a synonym
-of \lstinline|f().return|.
+In order to be closer to ACSL's syntax,
+\lstinline|f().\result| is accepted as a synonym
+of \lstinline|f().return|.
\end{itemize}
Whenever \lstinline|f().prm| appears in a relation, the
-related guard has an implicit \lstinline|CALL(f)| event, while
+related guard has an implicit \lstinline|CALL(f)| event, while
\lstinline|f().return|
-and \lstinline|f().\result| trigger a \lstinline|RETURN(f)| event.
-Note that this might result in an always-false guard if several such
+and \lstinline|f().\result| trigger a \lstinline|RETURN(f)| event.
+Note that this might result in an always-false guard if several such
expressions occur in the same guard, as in
\begin{lstlisting}[language=ya]
f().x <= g().y
@@ -371,11 +365,11 @@ a negative occurrence, that is under a negation, as in
\begin{lstlisting}[language=ya]
! f().x <= 4
\end{lstlisting}
-the related \lstinline|CALL(f)| event itself is {\it not} negated.
-In other words,
+the related \lstinline|CALL(f)| event itself is {\it not} negated.
+In other words,
the guard above is true if and only if we call \lstinline|f| with an argument
greater than \lstinline|4|. Usage of these expressions might be deprecated in
-future versions of \aorai in favor of the less ambiguous constructions
+future versions of \aorai in favor of the less ambiguous constructions
presented in the next subsection.
For instance, the automaton used in the chapter~\ref{first_use} contains the
@@ -418,13 +412,13 @@ A guard can now be the succession of several atomic events, possibly optional
or on the contrary repeated more than one time. The repetition modifier
follows the syntax and semantics of POSIX regexps: the most general are
\lstinline|{e1,e2}| that indicates at least \lstinline|e1| repetitions and at
-most \lstinline|e2| and \lstinline|{e1,}| that indicates at least
+most \lstinline|e2| and \lstinline|{e1,}| that indicates at least
\texttt{e1} repetitions without upper bound. There are then shortcuts for the
most common patterns:
\begin{itemize}
\item no modifier indicates exactly one execution (equivalent to
\lstinline|{1,1}|)
-\item \lstinline|+| indicates 1 or more repetitions
+\item \lstinline|+| indicates 1 or more repetitions
(equivalent to \lstinline|{1,}|)
\item \lstinline|*| indicates any number of repetitions, including 0
(equivalent to \lstinline|{0,}|)
@@ -437,31 +431,31 @@ Note that a repetition modifier that allows a non-fixed number of
repetitions prevents the automaton to be \lstinline|%deterministic|.
\lstinline|id(seq)| indicates that we have a \lstinline|CALL(id)| event,
-followed by the internal \texttt{seq}uence of event, and a
+followed by the internal \texttt{seq}uence of event, and a
\lstinline|RETURN(id)|,
\textit{i.e.} it describes a complete call to \texttt{id}, including the calls
-that \lstinline|id| itself performs. In particular, \lstinline|f()| indicates
+that \lstinline|id| itself performs. In particular, \lstinline|f()| indicates
that \lstinline|f| does not perform any call.
When in a sequence internal to a call to \lstinline|f|, the identifiers found in
-the expressions are first searched among the formals of \lstinline|f|,
+the expressions are first searched among the formals of \lstinline|f|,
starting with the innermost call and then among globals. It is still possible
-to use \lstinline|f().x| to refer to parameter \lstinline|x| of \lstinline|f|,
-but if \lstinline|f| is already in the call stack, this will not trigger a new
-\lstinline|CALL(f)| event at this point.
+to use \lstinline|f().x| to refer to parameter \lstinline|x| of \lstinline|f|,
+but if \lstinline|f| is already in the call stack, this will not trigger a new
+\lstinline|CALL(f)| event at this point.
Instead, the value of \lstinline|x| for the
last call to \lstinline|f| will be used.
-In addition, the \lstinline|CALL(id)| event may be further guarded by a
-pre-condition, that is either the name of an ACSL behavior of \lstinline|id|,
+In addition, the \lstinline|CALL(id)| event may be further guarded by a
+pre-condition, that is either the name of an ACSL behavior of \lstinline|id|,
or a basic YA condition (in which we have access to the formals of
- \lstinline|id| as explained above). Similarly, the final
-\lstinline|RETURN(id)| event can come with a
+ \lstinline|id| as explained above). Similarly, the final
+\lstinline|RETURN(id)| event can come with a
post-condition, in which one can access the \lstinline|\result|
returned by \lstinline|id|.
For instance, the following automaton describes a function main that does not
call anything when called in behavior \lstinline|bhv| and performs a single call
-to \lstinline|f|, when called with a parameter \lstinline|c| less than or
+to \lstinline|f|, when called with a parameter \lstinline|c| less than or
equal to \lstinline|0|, returning \lstinline|0| in this latter case:
\begin{lstlisting}[language=ya]
%init: S0;
@@ -474,7 +468,7 @@ Sf: -> Sf;
\end{lstlisting}
\subsubsection{YA variables}
-Extended guards do not allow to specify relations between the parameters of
+Extended guards do not allow specifying relations between the parameters of
distinct, non-nested calls. In order to be more flexible, it is possible to declare
variables in a Ya file, to assign them values when crossing a transition, and to use
them in guards. The syntax for that is described in Fig.~\ref{fig:ya-variables}.
@@ -572,12 +566,12 @@ These annotations are detailed in the rest of this section.
\lstset{language=C}
We have to represent the current state of the automaton.
-It can take two forms. First, if the automaton is marked as
+It can take two forms. First, if the automaton is marked as
{\lstset{language=ya}\lstinline|%deterministic|},
an \lstinline|enum| type representing the states of the automaton is
generated. It makes it easier to read the generated annotations when they
-come from a Ya file with explicitly named states.
-We use then a single variable,
+come from a Ya file with explicitly named states.
+We use then a single variable,
\curStates which is simply a value of the \lstinline|enum| type corresponding
to the current (unique) active state of the automaton.
Otherwise, we use a set of boolean variables, whose value is
@@ -588,11 +582,11 @@ Furthermore, the use of extended YA constructions
(section~\ref{sec:ya-extensions}) might introduce additional variables:
\begin{itemize}
\item Repetitions introduce a counter, \lstinline|aorai_counter| (with a numeric
-suffix if needed), except if their lower bound is \lstinline|0| or
-\lstinline|1| and they don't have an upper bound or their upper bound is
+suffix if needed), except if their lower bound is \lstinline|0| or
+\lstinline|1| and they don't have an upper bound or their upper bound is
\lstinline|0| or \lstinline|1| (in these cases, there is no need to
test the number of repetition done so far at the end of the sequence).
-\item The value of a parameter \lstinline|prm| of function \lstinline|f|
+\item The value of a parameter \lstinline|prm| of function \lstinline|f|
that is accessed in another event than \lstinline|CALL(f)| is stored in a global
variable \lstinline|aorai_prm| in order to be accessible in the remainder of the
sequence.
@@ -620,8 +614,8 @@ sequence.
\subsection{Deterministic lemmas}
\lstset{language=ya}
-When a YA automaton is marked as \lstinline|%deterministic|, some lemmas are
-generated whose verification will ensure that the automaton is indeed
+When a YA automaton is marked as \lstinline|%deterministic|, some lemmas are
+generated whose verification will ensure that the automaton is indeed
deterministic. Namely, for each state of the automaton, a lemma states that
at any given event, there is at most one transition exiting from this state
that is active.
@@ -634,38 +628,38 @@ is then called when entering \texttt{f}, while \texttt{f\_post\_func} is called
just before \texttt{f} returns. Both come with a specification that indicates
what actions may occur for the automaton at the corresponding event.
For instance, we can have a look at the specification generated for
-\texttt{opa\_pre\_func} in our running example, presented in
+\texttt{opa\_pre\_func} in our running example, presented in
figure~\ref{fig:pre-func}. Similarly, the corresponding body is shown in figure~\ref{fig:pre-func-body}.
\begin{figure}[htbp]
-\begin{lstlisting}[language=C,alsolanguage=ACSL]
+\begin{lstlisting}[style=c]
/*@ ensures aorai_CurOpStatus == aorai_Called;
ensures aorai_CurOperation == op_opa;
assigns aorai_CurOpStatus, aorai_CurOperation,
S1, S2, S3, S4, S5, S6, S7;
-
+
behavior buch_state_S1_out:
ensures 0 == S1;
-
+
behavior buch_state_S2_out:
ensures 0 == S2;
-
+
behavior buch_state_S3_in:
assumes 1 == S2 && r >= 0;
ensures 1 == S3;
-
+
behavior buch_state_S3_out:
assumes 0 == S2 || !(r >= 0);
ensures 0 == S3;
-
+
behavior buch_state_S4_out:
ensures 0 == S4;
-
+
behavior buch_state_S5_out:
ensures 0 == S5;
-
+
behavior buch_state_S6_out:
ensures 0 == S6;
-
+
behavior buch_state_S7_out:
ensures 0 == S7;
*/
@@ -674,7 +668,7 @@ void opa_pre_func(int r);
\caption{Specification of \texttt{opa\_pre\_func}}\label{fig:pre-func}
\end{figure}
\begin{figure}[htbp]
-\begin{lstlisting}[language=C,alsolanguage=ACSL]
+\begin{lstlisting}[style=c]
int S1_tmp;
int S2_tmp;
int S3_tmp;
@@ -735,17 +729,17 @@ augmented with behaviors describing how the automaton's status changes during
a call to \texttt{f}. The specification of the \texttt{opa} function in our
running example is shown in figure~\ref{fig:generated-spec}.
\begin{figure}[ht]
-\begin{lstlisting}[language=C,alsolanguage=ACSL]
+\begin{lstlisting}[style=c]
/*@ requires
1 == S2 &&
0 == S1 && 0 == S3 && 0 == S4 &&
0 == S5 && 0 == S6 && 0 == S7;
requires 1 == S2 ==> r >= 0;
requires r < 5000;
-
+
behavior j:
ensures \result == \old(r)+1;
-
+
behavior Buchi_property_behavior:
ensures 1 == S4 ==> \result <= 5000;
ensures 0 == S1 && 0 == S2 && 0 == S3 &&
@@ -758,7 +752,7 @@ int opa(int r);
\label{fig:generated-spec}
\end{figure}
-\lstset{language=C,alsolanguage=ACSL}
+\lstset{style=c}
The first \lstinline|requires| clause indicates which state(s) can be active
before entering the function. Then, for each of these states, we have a
requirement that at least one of the guard of a transition exiting from this
@@ -778,7 +772,7 @@ interpretation and may thus be over-approximated.
For each loop, \aorai defines an invariant stating in which states the
automaton can be during the loop. Since the states of the automaton when
entering the loop the first time and the states found during the executions
-of the loop can be quite different, \aorai introduces in addition a
+of the loop can be quite different, \aorai introduces in addition a
new variable, that is initially set to 1 and reset to 0 when the loop is
entered. This allows to make a distinction between the first run and the other
ones and to refine the invariant according to value of the variable.
@@ -803,7 +797,7 @@ Sf: -> Sf;
\end{figure}
\begin{figure}[ht]
-\begin{lstlisting}[language=C,alsolanguage=ACSL]
+\begin{lstlisting}[style=c]
int f() {}
int g() {}
@@ -871,14 +865,14 @@ common issues that may arise during verification.
In addition to annotations, \aorai generates an implementation for the transition
functions, so that it is possible to use the Eva plug-in of Frama-C on the
instrumented code. However, there's no guarantee that Eva will be able to
-perform an analysis that stays precise enough to verify that the automaton
+perform an analyzis that stays precise enough to verify that the automaton
always ends in an accepting state. Aoraï will set up automatically a certain number
-of parameters in Eva to help make the analysis more precise, but,
+of parameters in Eva to help make the analyzis more precise, but,
in the case of deterministic automata it is also possible
to use option \texttt{-aorai-instrumentation-history n} to have the instrumentation
retain the \texttt{n} previous states of the automaton (in addition to the
current state), that will be used for splitting Eva's abstract states. Furthermore,
-each time Eva encounters a call to the
+each time Eva encounters a call to the
built-in function \texttt{Frama\_C\_show\_aorai\_state}, it will display the current
state (together with the previous ones up to \texttt{-aorai\-instrumentation-history}).
If the function is called with some arguments, their abstract value will also be
@@ -887,7 +881,7 @@ displayed.
Another possibility is to use the deductive verification plug-in WP.
Note however that the generated annotations are not guaranteed to be complete,
{\it i.e.} to it might be necessary to add further annotations in order to
-discharge all proof obligations. In particular, in presence of loops, \aorai
+discharge all proof obligations. In particular, in presence of loops, \aorai
generates loop invariants for its own auxiliary variables, but it is likely that
these variables (especially the counters) will need to be related to the
variables of the original programs. For instance, we must add to the loop
@@ -929,8 +923,8 @@ is correct with respect to an automaton, we need to verify two aspects:
\item[Liveness] for each program trace $t$, there is an infinite number of
states synchronized with a \buchi\ acceptance state. We propose to restrict
- this constraints to the weaker one : there is no dead-lock (always a
- crossable transition from a non acceptance state) and no live-lock (always a
+ these constraints to the weaker one : there is no deadlock (always a
+ crossable transition from a non-acceptance state) and no live-lock (always a
finite number of states between 2 acceptance states).\\
Note: At this time the liveness aspect is not included in the tool.
@@ -1170,8 +1164,8 @@ plug-ins. Remove corresponding ad'hoc options.
is usually either a dead code, or a code violating the
specification.
\item In the YA and Promela formats, it is now possible to speak about
- call parameters and returned value. f().a denotes the call parameter
- a of \lstinline|f| and
+ call parameters and returned value. \lstinline|f().a| denotes the call
+ parameter \lstinline|a| of \lstinline|f| and
\lstinline|f().return| denotes the returned value of f.
\item In the annotated C file generated, array of states are indexed
by the name of the state (defined as an enum structure)
@@ -1184,17 +1178,17 @@ plug-ins. Remove corresponding ad'hoc options.
\chapter{Conclusion}
-This manual is not always up-to-date and only gives some hints on the \aorai
+This manual is not always up-to-date and only gives some hints on the \aorai
plug-in. If you want more information, please send me a mail at:
\begin{center}
nicolas.stouls@insa-lyon.fr
\end{center}
-or visit the web site:
+or visit the website:
\begin{center}
- \url{http://amazones.gforge.inria.fr/aorai/index.html}
+ \url{https://www.frama-c.com/fc-plugins/aorai.html}
\end{center}
\end{document}