From b86586c1c00366f4537ff0745e37d44d221e2e37 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 23 Feb 2021 14:05:07 +0100
Subject: [PATCH] [wp] nullable annot now prefixed with "wp_"

---
 src/plugins/wp/RefUsage.ml                                | 2 +-
 src/plugins/wp/tests/wp_plugin/nullable.i                 | 8 ++++----
 src/plugins/wp/tests/wp_plugin/oracle/nullable.res.oracle | 7 ++++---
 .../wp/tests/wp_plugin/oracle_qualif/nullable.res.oracle  | 7 ++++---
 4 files changed, 13 insertions(+), 11 deletions(-)

diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index d906da5f79b..17a4c1015ae 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -838,7 +838,7 @@ module HasNullable =
       let dependencies = [Ast.self]
     end)
 
-let is_nullable vi = vi.vformal && Cil.hasAttribute "nullable" vi.vattr
+let is_nullable vi = vi.vformal && Cil.hasAttribute "wp_nullable" vi.vattr
 
 let compute_nullable () =
   let module F = Globals.Functions in
diff --git a/src/plugins/wp/tests/wp_plugin/nullable.i b/src/plugins/wp/tests/wp_plugin/nullable.i
index 3eb58bc719b..ff08ead486c 100644
--- a/src/plugins/wp/tests/wp_plugin/nullable.i
+++ b/src/plugins/wp/tests/wp_plugin/nullable.i
@@ -9,7 +9,7 @@ int x ;
 int *g ;
 
 /*@ assigns *g, *p, x ; */
-void nullable_coherence(int* p /*@ nullable */){
+void nullable_coherence(int* p /*@ wp_nullable */){
   if(p == (void*)0){
     //@ check must_fail: \false ;
     return;
@@ -22,9 +22,9 @@ void nullable_coherence(int* p /*@ nullable */){
 
 //@ assigns *p, *q, *r, *s, *t ;
 void nullable_in_context
-(int* p /*@ nullable */,
- int* q /*@ nullable */,
- int* r /*@ nullable */,
+(int* p /*@ wp_nullable */,
+ int* q /*@ wp_nullable */,
+ int* r /*@ wp_nullable */,
  int* s, int* t)
 {
   *p = 42;
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nullable.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nullable.res.oracle
index 5ce753cddf7..56ad3f47187 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/nullable.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nullable.res.oracle
@@ -46,7 +46,7 @@ Prove: true.
        requires p ≢ \null ⇒ \separated(g, p, &x);
        requires \valid(p) ∨ p ≡ \null;
      */
-  void nullable_coherence(int *p /*@ nullable */);
+  void nullable_coherence(int *p /*@ wp_nullable */);
 [wp] tests/wp_plugin/nullable.i:24: Warning: 
   Memory model hypotheses for function 'nullable_in_context':
   /*@
@@ -63,5 +63,6 @@ Prove: true.
        requires \valid(q) ∨ q ≡ \null;
        requires \valid(r) ∨ r ≡ \null;
      */
-  void nullable_in_context(int *p /*@ nullable */, int *q /*@ nullable */,
-                           int *r /*@ nullable */, int *s, int *t);
+  void nullable_in_context(int *p /*@ wp_nullable */,
+                           int *q /*@ wp_nullable */,
+                           int *r /*@ wp_nullable */, int *s, int *t);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable.res.oracle
index b3655559e31..61dd62765ab 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable.res.oracle
@@ -27,7 +27,7 @@
        requires p ≢ \null ⇒ \separated(g, p, &x);
        requires \valid(p) ∨ p ≡ \null;
      */
-  void nullable_coherence(int *p /*@ nullable */);
+  void nullable_coherence(int *p /*@ wp_nullable */);
 [wp] tests/wp_plugin/nullable.i:24: Warning: 
   Memory model hypotheses for function 'nullable_in_context':
   /*@
@@ -44,5 +44,6 @@
        requires \valid(q) ∨ q ≡ \null;
        requires \valid(r) ∨ r ≡ \null;
      */
-  void nullable_in_context(int *p /*@ nullable */, int *q /*@ nullable */,
-                           int *r /*@ nullable */, int *s, int *t);
+  void nullable_in_context(int *p /*@ wp_nullable */,
+                           int *q /*@ wp_nullable */,
+                           int *r /*@ wp_nullable */, int *s, int *t);
-- 
GitLab