diff --git a/doc/eva/main.tex b/doc/eva/main.tex index ed0067e61511e43e7067b300eaae38017acd48ea..e02854e67d8a84f90dd2b9bffc92a6ca35777ffe 100644 --- a/doc/eva/main.tex +++ b/doc/eva/main.tex @@ -5440,6 +5440,14 @@ This section lists such directives supported by \Eva{}, with a short description of their behavior and a reference to the relevant section of this manual that explains in more details their effect on the analysis. +Each of these directives also has an alternative syntax where the keyword is +prefixed by \texttt{\textbackslash eva::}. Thus, one can write +\texttt{//@ \textbackslash eva::split x; //@ loop \textbackslash eva::unroll 100;} +instead of \texttt{//@ split x; //@ loop unroll 100;}. +This syntax makes explicit that the directive is specific to the \Eva{} plug-in, +and avoids parsing failure if \Eva{} is not loaded (for instance when using +the \verb|-no-autoload-plugins| parameter). + \subsection{Directives guiding trace partitioning} \begin{center}