From c3f6e4077fff781c66522f54fee85c1f87163584 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 25 Feb 2019 19:19:11 +0100
Subject: [PATCH] [devman] fixes version in Change section + doc `status` flag
in ACSL extensions
---
doc/developer/advance.tex | 11 ++++++++++-
doc/developer/changes.tex | 5 +++++
src/kernel_services/ast_queries/logic_typing.mli | 1 +
3 files changed, 16 insertions(+), 1 deletion(-)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index f6889b211e8..d6dceaa1bf7 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -3926,7 +3926,7 @@ the corresponding list is traversed normally by the visitor
(see section~\ref{adv:visitors}).
In order for the extension to be recognized by the parser, it must be
-registered by one of the following functions, depending on its category:
+registered by one of the following functions, depending on its category.
\begin{itemize}
\item \texttt{Logic\_typing.register\_behavior\_extension}%
\scodeidx{Logic\_typing}{register\_behavior\_extension}
@@ -3941,6 +3941,15 @@ registered by one of the following functions, depending on its category:
\item \texttt{Logic\_typing.register\_code\_annot\_next\_both\_extension}%
\scodeidx{Logic\_typing}{register\_code\_annot\_next\_loop\_extension}
\end{itemize}
+
+Each function takes three arguments:
+\begin{itemize}
+\item \texttt{kw} the name of the extension,
+\item \texttt{status}, a boolean flag indicating whether the extended annotation
+ may have a validity status, and
+\item \texttt{f} the type-checking function itself.
+\end{itemize}
+
After a call to the appropriate registration function,
a clause of the form \verb|kw e1,...,en;|, where each \verb|ei| can be
any syntactically valid ACSL term or predicate,
diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex
index 6e3243e90cf..41a4ee2c9fc 100644
--- a/doc/developer/changes.tex
+++ b/doc/developer/changes.tex
@@ -7,7 +7,12 @@ This chapter summarizes the major changes in this documentation between each
\section*{Frama-C+dev}
\begin{itemize}
+\item \textbf{ACSL Extension}: Document new \texttt{status} flag for registration functions
\item \textbf{Testing}: Document of usage \texttt{@@} in a directive
+\end{itemize}
+
+\section*{18.0 Argon}
+\begin{itemize}
\item \textbf{Logging Services}: Document \texttt{error} and \texttt{failure} behaviors.
\item \textbf{ACSL Extensions}: New extension categories, for global and plain code annotations
\end{itemize}
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index a05bd2a0ebb..c204d9df8e2 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -172,6 +172,7 @@ type typing_context = {
@since Carbon-20101201
@modify Silicon-20161101 change type of the function
+ @Frama-C+dev add [status] argument
*)
val register_behavior_extension:
string -> bool ->
--
GitLab