From ee9eacf3b7b9aa14076d34b19ca133b61a549917 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 29 Nov 2021 10:20:15 +0100
Subject: [PATCH] [useman] proof-read new Standard Library section and add
Changelog
---
doc/userman/user-changes.tex | 5 +++++
doc/userman/user-sources.tex | 16 +++++++++-------
2 files changed, 14 insertions(+), 7 deletions(-)
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index bef69332908..9a37650c699 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -3,6 +3,11 @@
This chapter summarizes the changes in this documentation between each \FramaC
release. First we list changes of the last release.
+\section*{24.0 (Chromium)}
+\begin{itemize}
+\item \textbf{Standard library (libc):} Section added
+\end{itemize}
+
\section*{23.0 (Vanadium)}
\begin{itemize}
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index 16722ff85a6..a93678e60ec 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -418,7 +418,10 @@ indicate the option needed to allow the file to be parsed:
\FramaC bundles a C standard library in order to help parse and analyze code
that relies on the functions specified in the ISO C standard.
-Such library is provided on a best-effort basis, and it is part of the
+Furthermore, In order to simplify parsing of code using common open-source libraries,
+\FramaC's standard library also includes some POSIX and non-POSIX headers which
+are not part of ISO C.
+Such libraries are provided on a best-effort basis, and they are part of the
{\em trusted computing base}: to ensure its correctness, the specifications
must be ultimately proofread by the user.
@@ -431,8 +434,11 @@ By default, \FramaC's preprocessing will include the headers of its own standard
library, instead of those installed in the user's machine. This avoids issues
with non-portable, compiler-specific features.
Option \optiondef{-}{frama-c-stdlib} (set by default)
-adds \texttt{-I\$FRAMAC\_SHARE/libc} to the preprocessor command, and also
-\texttt{-nostdinc} if \optionuse{-}{cpp-frama-c-compliant} is set.
+adds \texttt{-I\$FRAMAC\_SHARE/libc} to the preprocessor command, as well as
+GCC-specific option \texttt{-nostdinc}. If the latter is not recognized by
+your preprocessor,
+\optionuse{-}{no-cpp-frama-c-compliant} can be given to \FramaC
+(see section~\ref{sec:preprocessing}).
The use of \FramaC's standard library contains a few caveats:
\begin{itemize}
@@ -452,10 +458,6 @@ The use of \FramaC's standard library contains a few caveats:
inclusion of such headers and/or definitions in \FramaC's standard library.
\end{itemize}
-In order to simplify parsing of code using common open-source libraries,
-\FramaC's standard library also includes some POSIX and non-POSIX headers which
-are not part of ISO C.
-
Note that, while \FramaC's library intends to offer maximum portability, some
definitions such as numeric constants require actual values to be defined.
For pragmatic reasons, such definitions are most often based on the values
--
GitLab