From 27df3fc31f7b333662ff8e51342de4cea8d8ce69 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 28 Apr 2022 17:25:33 +0200
Subject: [PATCH] [devguide] update index
---
doc/developer/advance.tex | 12 +++++++++---
1 file changed, 9 insertions(+), 3 deletions(-)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 541582d40ec..2de2c656364 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -2450,7 +2450,10 @@ following.
value analysis would not be consistent anymore with the current entry point,
leading to incorrect results.
\begin{example}
-\sscodeidx{Db}{Value}{is\_computed}
+\scodeidx{Analysis}{is\_computed}
+\sscodeidx{Eva}{Analysis}{is\_computed}
+\scodeidx{Analysis}{compute}
+\sscodeidx{Eva}{Analysis}{compute}
~
\begin{ocamlcode}
@@ -4019,8 +4022,9 @@ Similarly, in a loop annotation, \verb|loop kw e1, ..., en;| will be treated as
\verb|kw| extension. In case the loop annotation has a \verb|loop variant|, the extension must
occur before. Otherwise, there is no ordering constraint with other loop annotations clauses.
-Global extensions can appear either alone in a global annotation, or as part of an axiomatic with
-a set of other global annotations.
+Global extensions can either be a standalone global annotation, or a whole block
+of global extensions, the latter case following the syntax of
+\texttt{axiomatic} blocks.
Finally, a code annotation extension must appear as a single code annotation, like any code annotation.
@@ -4058,6 +4062,8 @@ registered by one of the following functions, depending on its category.
\scodeidx{Acsl\_extension}{register\_behavior}
\item \texttt{Acsl\_extension.register\_global}%
\scodeidx{Acsl\_extension}{register\_global}
+\item \texttt{Acsl\_extension.register\_global\_block}%
+\scodeidx{Acsl\_extension}{register\_global\_block}
\item \texttt{Acsl\_extension.register\_code\_annot}%
\scodeidx{Acsl\_extension}{register\_code\_annot}
\item \texttt{Acsl\_extension.register\_code\_annot\_next\_stmt}%
--
GitLab