[doc] experimental feature

src/plugins/e-acsl/doc/userman/macros.tex

@@ -39,6 +39,8 @@
 \newcommand{\difficults}[1]{\emph{#1 are usually difficult to implement. Thus
     you would not wonder if most tools do not support them (or support
     them partially).}}
+\newcommand{\experimental}[1]{\emph{#1 is still an experimental feature. It may
+evolve in the future and/or not work as expected.}}
 
 \newcommand{\changeinsection}[2]{\textbf{Section \ref{sec:#1}:} #2.}
 
@@ -139,7 +141,7 @@
     \ifthenelse{\isundefined{\myrq}}{}{\footnote{\myrq}}\end{changebar}}{}}
 
 %%% Environnements et commandes non conditionnelles
-\newcommand{\experimental}{\textsc{Experimental}}
+\newcommand{\experimentalword}{\textsc{Experimental}}
 
 \newsavebox{\fmbox}
 \newenvironment{cadre}

src/plugins/e-acsl/doc/userman/provides.tex

@@ -865,10 +865,12 @@ particular part of the code, while reducing the global runtime overhead.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\subsection{Partial Instrumentation}
+\subsection{Partial Instrumentation (\experimentalword)}
 \label{sec:partial-instrumentation}
 \index{Function!Not Instrumented}
 
+\experimental{Partial instrumentation}
+
 By default, the E-ACSL plug-in generates all the necessary pieces of code for
 checking at runtime the provided annotations. This amount of instrumentation
 may be quite large. It is possible to reduce it by manually specifying the set