From 9137703d1c417c1796f9f08570f9c675aae074dc Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 24 Feb 2021 17:27:16 +0100
Subject: [PATCH] [wp/doc] wp_nullable / wp_nullable_args
---
src/plugins/wp/doc/manual/nullable.c | 9 +++++++++
src/plugins/wp/doc/manual/wp_caveat.tex | 11 +++++++++--
2 files changed, 18 insertions(+), 2 deletions(-)
create mode 100644 src/plugins/wp/doc/manual/nullable.c
diff --git a/src/plugins/wp/doc/manual/nullable.c b/src/plugins/wp/doc/manual/nullable.c
new file mode 100644
index 00000000000..9b403ffe91c
--- /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 6e7afa77c06..4a49fd03c2b 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.
--
GitLab