diff --git a/doc/userman/user-analysis.tex b/doc/userman/user-analysis.tex
index 89fdc0a9b599051aec566618ee018f0022e0ece5..926fc9eecd7aba7b21d073d120f60b8fa075ed65 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 3da22e9e8283d86f4ad57a93d32f8eacdf162be1..045d671af556cb814c6e345c026116b3599559ca 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 706d54135e1785b604e998aaccc3522b72559ceb..0fa77b175c62a1cc67debb77d2c4654444e360fd 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 ce56197c3e948b460514eedb2979d4a8b162ebe7..235124894053d3e0cceaa86f8793860a090af0d0 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