[wp/doc] wp_nullable / wp_nullable_args

src/plugins/wp/doc/manual/nullable.c

+void foo(int* p /*@ wp_nullable */, int* q /*@ wp_nullable */){
+
+}
+
+// or equivalently:
+//@ wp_nullable_args p, q ;
+void foo(int* p, int* q){
+
+}

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.