diff --git a/src/plugins/wp/doc/manual/nullable.c b/src/plugins/wp/doc/manual/nullable.c
new file mode 100644
index 0000000000000000000000000000000000000000..9b403ffe91cb9148bcff3b461de90cec89c09cb1
--- /dev/null
+++ b/src/plugins/wp/doc/manual/nullable.c
@@ -0,0 +1,9 @@
+void foo(int* p /*@ wp_nullable */, int* q /*@ wp_nullable */){
+
+}
+
+// or equivalently:
+//@ wp_nullable_args p, q ;
+void foo(int* p, int* q){
+
+}
diff --git a/src/plugins/wp/doc/manual/wp_caveat.tex b/src/plugins/wp/doc/manual/wp_caveat.tex
index 6e7afa77c066bb52273da98252d093d08b6980f3..4a49fd03c2be8622dc6700db76484395853348bf 100644
--- a/src/plugins/wp/doc/manual/wp_caveat.tex
+++ b/src/plugins/wp/doc/manual/wp_caveat.tex
@@ -21,7 +21,14 @@ global ones).
 
 Additionally, the \texttt{Caveat} memory model of \textsf{Frama-C}
 performs a local allocation of formal parameters with pointer
-types that cannot be treated as \textit{reference parameters}. 
+types that cannot be treated as \textit{reference parameters}.
+Note that it means that the pointer is considered valid. If one needs
+to accept \texttt{NULL} for this pointer, a \texttt{wp\_nullable} ghost
+annotation or the clause \texttt{wp\_nullage\_args} can be used to bring
+this information to WP:
+
+\listingname{nullable.c}
+\cinput{nullable.c}
 
 This makes explicit the separation hypothesis of memory regions
 pointed by formals in the \textsf{Caveat} tool. The major benefit of
@@ -29,7 +36,7 @@ the \textsf{WP} version is that aliases are taken into account by the
 \texttt{Typed} memory model, hence, there are no more suspicious
 \textit{aliasing} warnings.
 
-\paragraph{Warning:} using the \texttt{Caveat} memory model, 
+\paragraph{Warning:} using the \texttt{Caveat} memory model,
 the user \emph{must} check by manual code review that no aliases are
 introduced \emph{via} pointers passed to formal parameters at call sites.