From 1bf184078145ed1f932bb695edbf3267439b4c39 Mon Sep 17 00:00:00 2001 From: Julien Signoles <julien.signoles@cea.fr> Date: Tue, 26 Feb 2019 14:32:50 +0100 Subject: [PATCH] [doc] experimental feature --- src/plugins/e-acsl/doc/userman/macros.tex | 4 +++- src/plugins/e-acsl/doc/userman/provides.tex | 4 +++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/plugins/e-acsl/doc/userman/macros.tex b/src/plugins/e-acsl/doc/userman/macros.tex index f0e91c4d3da..fd7bfa93e03 100644 --- a/src/plugins/e-acsl/doc/userman/macros.tex +++ b/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} diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex index f02025a18c1..18df5fe9d39 100644 --- a/src/plugins/e-acsl/doc/userman/provides.tex +++ b/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 -- GitLab