[wp] nullable annot now prefixed with "wp_"

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

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;

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);

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);