From 3b7f4f7ad7eb2da805ea64c7b2b3bd5a4d6034c4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 3 Oct 2023 14:01:36 +0200
Subject: [PATCH] [Eva] User manual: adds paragraph about the alternative
 syntax of Eva directives.

---
 doc/eva/main.tex | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/doc/eva/main.tex b/doc/eva/main.tex
index ed0067e6151..e02854e67d8 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}
-- 
GitLab