Commit 26776c00 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[aorai] update manual to introduce YA variables + small improvements

parent 4d4b7b03
......@@ -98,8 +98,10 @@ autom4te.cache
......@@ -8,7 +8,7 @@ EXAMPLES=example.c example.ltl example.ya \
example_loop2.c example_loop2.ya \
BNF=basic_ya.bnf extended_ya.bnf
BNF=ya_file.bnf basic_ya.bnf extended_ya.bnf ya_variables.bnf
all: main.pdf $(ARCHIVENAME).tgz
......@@ -14,7 +14,7 @@
......@@ -36,12 +36,16 @@
\title{\aorai\ Plugin Tutorial\\\textit{\normalsize (A.k.a. LTL to ACSL)}}
\author{Nicolas Stouls and Virgile Prevosto\\
......@@ -332,35 +336,27 @@ For compatibility reasons, other syntaxes, like LTL or PROMELA, are supported.
\subsection{YA file}\label{sec:ya-file}
The description of the automaton can be done in more than one way, but we
recommend to follow the guidelines explained below:
\item Initial states of automaton are specified using the
\emph{\%init} keyword followed by a comma-separated list
containing the states' name:
%init: S1, S2, ..., Sn;
\item Acceptance states are specified using the \emph{\%accept} keyword
followed by a comma separated list containing the states' name
%accept: S1, S2, ..., Sn;
\item Reject states are specified using the \emph{\%reject} keyword,
followed by a comma separated list containing the states' name
%reject: S1, S2, ..., Sn;
\item If the automaton is supposed to be deterministic, this can be
specified using the following directive:
A YA file follows the grammar described in Fig.~\ref{ya-file}.
\caption{Structure of a YA file}\label{ya-file}
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
states afterwards.
A state is simply described by its name and the list of transitions
starting from this state with their guard. The specific \lstinline|other|
guard indicates that this transition is taken if none of the other ones
can be taken. If it appears, it must be last in the list of transitions.
Conditions that can occur in guards are described in the next section.
\item By default, \aorai considers that all functions calls and returns trigger
By default, \aorai considers that all functions calls and returns trigger
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:
......@@ -368,26 +364,6 @@ following directive must be used:
%explicit transitions;
\item States and transitions are described by sets of the following form
state: { condition_1 } -> new_state_1
| { condition_2 } -> new_state_2
| { condition_n } -> new_state_n
A condition which is always true can be omitted along with its surrounding
state: -> new_state;
In addition, the last transition can have the following form:
state: ...
other -> new_state
indicating that this transition is crossed if and only if none of the
preceding transitions is activated.
\subsection{Basic YA guards}\label{sec:basic-ya-guards}
The syntax for basic YA conditions is described in
......@@ -491,7 +467,7 @@ most common patterns:
\item \lstinline|{,e}| is equivalent to \lstinline|{0,e}|
Note that a repetition modifier that allows to have a non-fixed number of
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,
......@@ -531,36 +507,72 @@ S0: { main::bhv() } -> Sf
Sf: -> Sf;
\subsubsection{Sharing values}
\subsubsection{YA variables}
Extended guards do not allow to specify relations between the parameters of
distinct, non-nested calls. For instance, we cannot specify that a call to
\texttt{fopen(f)} must be followed by a call to \texttt{fclose(f)} with the same
\texttt{f} in both cases. In order to do that, it is possible to parameterize
the description of the automaton by directives of the following form:
%parameter: decl;
where \texttt{decl} is an ACSL declaration. The parameter declared that way will
be treated as an existentially-quantified variable across the automaton.
For instance, in order to check whether a call to \texttt{fopen} is always
matched by a call to \texttt{fclose}, we can use the following automaton:
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}.
\caption{Syntax for declaring and using YA variables}
Only \lstinline|char|, \lstinline|int|, \lstinline|long| variables are currently
supported. Furthermore, variables can only be introduced in deterministic automata,
which do not use extended guards.
A variable \lstinline|$x| %$
must have been declared in the directives of the file to be used in a guard. Furthermore
if it is used in a transition starting from state \lstinline|S|, then all possible paths
from the initial state to \lstinline|S| must contain at least one assignment to \lstinline|$x|.
Note that assignments are performed sequentially, so that if
\lstinline|$x| has already been assigned in a given sequence of actions, it can automatically
be used in subsequent assignments (on the other hand, since conditions are evaluated
before actions, it must have been initialized elsewhere if it were to be used in the
condition part of the guard.
in the right hand side of an action, it is possible to refer to the value of a formal
parameter of \lstinline|f| when the transition is triggered over a \lstinline|CALL|
to \lstinline|f| and to its return value when hangling a \lstinline|RETURN| event,
as described in section~\ref{sec:basic-ya-guards} for conditions.
An example of YA automaton with variables is given below. It uses variables \lstinline|$x| and
\lstinline|$y| that are updated when calling \lstinline|f| and returning from \lstinline|i|,
while \lstinline|$x| is used when calling \lstinline|h|.%$
%init: S0;
%accept: Sf;
%reject: S1;
%parameter: FILE* f;
%explicit transitions;
%init: a;
%accept: i;
S0: { fopen(){\result==f}; } -> S1;
| -> S0;
$x : int;
$y : int;
S1: { fclose{stream==f}(); } -> Sf
a : { CALL(main) } -> b;
Sf: -> Sf
b :
{ CALL(f) } $x:=f().x; $y := $x; -> c
| { CALL(g) } -> d
c : { RETURN(f) } -> e;
d : { RETURN(g) } -> g;
e :
{ CALL(h) && $x > 0 } -> f
| { RETURN(main) } -> i
f : { RETURN(h) } -> g;
g : { CALL(i) } -> h;
h : { RETURN(i) } $y := 0; $x := 1; -> e;
i : -> i;
......@@ -1225,6 +1237,11 @@ The plug-in is composed of three parts:
\section{Recent updates}
\subsection{Frama-C Titanium}
\item Various bug fixes
\item Introduction of YA variables
\subsection{Frama-C Aluminium}
\item Generated functions now have a body in addition to a specification
......@@ -17,9 +17,10 @@
let make_keyword () =
let keyword = Buffer.contents full_kw in
let sep = if String.contains keyword '$' then '|' else '$' in
print_string "\\addspace";
"\\lstinline$%s$" keyword;
"\\lstinline%c%s%c" sep keyword sep;
print_string "\\spacetrue";
Buffer.clear full_kw
file ::= directive* state+;
directive ::= '%init' ':' id+ ';'; name of initial state(s)
| '%accept' ':' id+ ';'; name of accepting state(s)
| '%deterministic' ';' ; deterministic automaton
state ::= id ':' transition;
('|' transition)* ';'; state name and transitions from state
transition ::= guard '->' id; guard and end state of the transition
| '->' id; transition that is always taken
| 'other' '->' id; default transition. must appear last
guard ::= '{' condition '}'
directive ::= ... | '$' id ':' type
type::= 'char' | 'int' | 'long'
guard ::= '{' condition '}' action*
action ::= '$' id ':=' lval ';'
lval ::= ... | '$'id
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment