From 46477e252d1b26d05e5c2c7fc282a6078b8e1b30 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 18 Apr 2024 19:18:26 +0200
Subject: [PATCH] [doc] fix changes
---
doc/userman/user-changes.tex | 5 ++++-
doc/userman/user-sources.tex | 12 ++++++++++--
2 files changed, 14 insertions(+), 3 deletions(-)
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index 6d9b6206bae..87f624c5635 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -5,8 +5,11 @@ release. First we list changes of the last release.
\section*{Frama-C+dev}
\begin{itemize}
-\item \textbf{Normalizing the Source Code:} document the possibility of
+ \item \textbf{Normalizing the Source Code:} document the possibility of
undefining builtin macros from the chosen \texttt{-machdep}.
+\item \textbf{Preparing the Sources:} loop pragmas are removed and replaced
+ by dedicated ACSL extension.
+ Use \verb+loop unfold+ in place of \verb+loop pragma UNROLL+.
\item \textbf{Preparing the Sources:} add subsection on standard library about
portability considerations.
\end{itemize}
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index ed70dadc191..271b6b6d318 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -304,10 +304,18 @@ underscores as prefix and suffix, \texttt{-UMACRO} will also undefine
\texttt{do ... while(0)}. This option is set by default.
\item \texttt{\optiondef{-}{ulevel} <n>} unrolls all loops n times. This is a
- purely syntactic operation. Loops can be unfolded individually, by
+ purely syntactic operation. Loops can be unfolded individually, by
inserting a \verb+loop unfold+ annotation just before the loop statement. Do
not confuse this option with plug-in-specific options that may also be called
- ``unrolling''~\cite{value}. Below is a typical example of use.
+ ``unrolling''~\cite{value}\footnote{
+ Historically, \textit{syntactic} loop unrolling was denoted by
+ \texttt{loop pragma UNROLL} annotations. Later on, \textsf{EVA} introduced
+ \textit{semantic} unrolling with \texttt{loop unroll} annotations.
+ Loop pragams was removed for Frama-C 29 (Copper) and it was
+ decided to introduce \texttt{loop unfold} annotations for \textit{syntactic}
+ unrolling and to reserve \texttt{loop unroll} annotations for \textit{semantic}
+ loop unrolling with \textsf{EVA}.
+ }. Below is a typical example of use:
\begin{ccode}
/*@ loop unfold 10; */
for(i = 0; i < 9; i++) ...
--
GitLab