From f758c84b18a939d365ca3b0e0db46ad1775ec8c8 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 2 Apr 2020 18:43:53 +0200
Subject: [PATCH] [doc] Minor fixes after review
---
doc/userman/user-analysis.tex | 8 ++++----
doc/value/main.tex | 4 ++--
man/frama-c.1 | 15 ++++++++++++++-
man/frama-c.1.header | 2 +-
4 files changed, 21 insertions(+), 8 deletions(-)
diff --git a/doc/userman/user-analysis.tex b/doc/userman/user-analysis.tex
index 89fdc0a9b59..926fc9eecd7 100644
--- a/doc/userman/user-analysis.tex
+++ b/doc/userman/user-analysis.tex
@@ -156,12 +156,12 @@ regardless of the value of the option.)
does not perform illegal pointer arithmetics, creating pointers that do not
point inside an object or one past an object.
This option is disabled by default, allowing the creation of such invalid
- pointers without alarm — but the dereference of an invalid pointer
- \emph{always} generate an alarm.
+ pointers without alarm — but the dereferencing of an invalid pointer
+ \emph{always} generates an alarm.
For instance, no error is detected by default in the following example, as
- the dereference is correct. However, if option \texttt{-warn-invalid-pointer}
- is enabled, an error is detected at line 4.
+ the dereferencing is correct. However, if option
+ \texttt{-warn-invalid-pointer} is enabled, an error is detected at line 4.
\begin{ccode}
int x;
int *p = &x;
diff --git a/doc/value/main.tex b/doc/value/main.tex
index 3da22e9e828..045d671af55 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -1490,7 +1490,7 @@ This may happen on:
resulting pointer points inside or one past the object \lstinline|o|.
\end{itemize}
In all other cases, an alarm is emitted, which reports the possible
- implementation-defined behavior mentionned above.
+ implementation-defined behavior mentioned above.
\end{itemize}
In the example below, the first increment of the pointer \lstinline|p| is valid,
@@ -1594,7 +1594,7 @@ option \verb+-warn-unsigned-overflow+ can be used.
By default, Eva emits alarms for downcasts of pointer values to (signed
or unsigned) integer types. Such downcasts are indeed undefined behavior
-according to section 6.3.2.3, §6 of the ISO/IE 9899:1999 standard.
+according to section 6.3.2.3, §6 of the ISO/IEC 9899:1999 standard.
However, option \lstinline|-no-warn-pointer-downcast| can be used to disable
these alarms.
diff --git a/man/frama-c.1 b/man/frama-c.1
index 706d54135e1..0fa77b175c6 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -25,7 +25,7 @@
.\" using pandoc 2.0 or newer. To modify this file, edit the Markdown file
.\" and run `make man/frama-c.1`.
-.TH FRAMA-C 1 2020-03-05
+.TH FRAMA-C 1 2020-04-02
.SH NAME
.PP
frama\-c[.byte] \- a static analyzer for C programs
@@ -737,6 +737,12 @@ parser:decimal\-float=once\f[] (and variants) instead.
.RS
.RE
.TP
+.B [\-no]\-warn\-invalid\-pointer
+generate alarms for invalid pointer arithmetic.
+Defaults to no.
+.RS
+.RE
+.TP
.B [\-no]\-warn\-left\-shift\-negative
generate alarms for signed left shifts on negative values.
Defaults to yes.
@@ -749,6 +755,13 @@ Defaults to no.
.RS
.RE
.TP
+.B [\-no]\-warn\-pointer\-downcast
+generates alarms when the downcast of a pointer may exceed the
+destination range.
+Defaults to yes.
+.RS
+.RE
+.TP
.B [\-no]\-warn\-signed\-downcast
generates alarms when signed downcasts may exceed the destination range.
Defaults to no.
diff --git a/man/frama-c.1.header b/man/frama-c.1.header
index ce56197c3e9..23512489405 100644
--- a/man/frama-c.1.header
+++ b/man/frama-c.1.header
@@ -25,4 +25,4 @@
.\" using pandoc 2.0 or newer. To modify this file, edit the Markdown file
.\" and run `make man/frama-c.1`.
-.TH FRAMA-C 1 2020-03-05
+.TH FRAMA-C 1 2020-04-02
--
GitLab