From d232d01094e5c6c59c36d5a47589bf512bee1539 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 27 Sep 2024 09:19:50 +0200
Subject: [PATCH] [doc] minor fixes to devman
---
doc/developer/advance.tex | 6 +++---
doc/frama-c-book.cls | 2 +-
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 6474f804b2d..fdcff5ee232 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -1382,7 +1382,7 @@ be changed by using the
\paragraph{Source Options.} By default, a message is not localized. You may
specify a source location, either specifically or by using the current
location of an \texttt{AST} visitor.
-\lstset{style=frama-c-style}
+\lstset{style=frama-c-style,language=}
\begin{itemize}
\item[] \lstinline{~source:$s$} use the source position $s$ (see \texttt{Log.mli})
\item[] \lstinline{~current:true} use the source location
@@ -4131,8 +4131,8 @@ definitions from other languages, e.g. \textsf{Coq} or \textsf{Why3}, as regular
\acsl module definitions. From the user point the view, this takes the form
of an extended \verb+import+ clause:
-\begin{lstlisting}
-//@ import <loader>: <module-name> [ \as <alias-name> ];
+\begin{lstlisting}[style=c]
+//@ import <loader>: <module_name> [ \as <alias-name> ];
\end{lstlisting}
The syntax is similar to the general ACSL \verb+import+ annotation, except that the
diff --git a/doc/frama-c-book.cls b/doc/frama-c-book.cls
index 8b421293990..91a947dc0db 100644
--- a/doc/frama-c-book.cls
+++ b/doc/frama-c-book.cls
@@ -489,7 +489,7 @@
\\tainted,
Here,LoopCurrent,LoopEntry,Pre,Post,Old,
\\Cons,\\Down,\\NearestAway,\\NearestEven,\\Nil,\\ToZero,\\Up,
- \\at,\\allocable,\\allocation,\\automatic,\\base_addr,\\block_length,\\dangling,
+ \\as,\\at,\\allocable,\\allocation,\\automatic,\\base_addr,\\block_length,\\dangling,
\\dynamic,\\exists,\\exit_status,\\false,\\forall,\\freeable,\\fresh,\\from,
\\in,\\initialized,\\lambda,\\let,\\list,\\match,\\nothing,\\null,\\numof,
\\object_pointer,\\offset,\\old,\\register,\\result,\\separated,\\static,
--
GitLab