[wp] wp_nullable(_pointers) -> (_args)

src/plugins/wp/RefUsage.ml

@@ -848,7 +848,7 @@ struct
       | Logic_ptree.PLvar s ->
           let lv = typing_context.Logic_typing.find_var s in
           begin match lv.lv_origin with
-            | Some vi when Cil.isPointerType vi.vtype ->
+            | Some vi when Cil.isPointerType vi.vtype && vi.vformal ->
                 make_nullable vi ;
                 Logic_const.tvar ~loc lv
             | _ ->
@@ -864,7 +864,7 @@ struct
 
   let () =
     Acsl_extension.register_behavior
-      "wp_nullable_pointers" Nullable_extension.typer false
+      "wp_nullable_args" Nullable_extension.typer false
 
   module HasNullable =
     State_builder.Option_ref(Datatype.Bool)

src/plugins/wp/tests/wp_plugin/nullable_ext.i

@@ -9,7 +9,7 @@ int x ;
 int *g ;
 
 /*@ assigns *g, *p, x ;
-    wp_nullable_pointers p ;
+    wp_nullable_args p ;
 */
 void nullable_coherence(int* p){
   if(p == (void*)0){
@@ -23,7 +23,7 @@ void nullable_coherence(int* p){
 }
 
 /*@ assigns *p, *q, *r, *s, *t ;
-    wp_nullable_pointers p, q, r ;
+    wp_nullable_args p, q, r ;
 */
 void nullable_in_context(int* p, int* q, int* r, int* s, int* t){
   *p = 42;