diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml index d906da5f79b27e2e694c38f41f5bee3d969020f9..17a4c1015ae22dc472cf02194e7fabe80a104410 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 3eb58bc719b5c817306bdf9f861732a90ea68f05..ff08ead486c94dfc77c8b34d2a9a7553b6cec248 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 5ce753cddf769def9bead79590d10b27423dacc9..56ad3f4718767e2045b4f79d57537d2d694dd9a7 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 b3655559e316c7a6f74fef40f3995dee587e0a92..61dd62765ab4591e18b667710261985f0c5348a7 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);