diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml index 0bf6762b319c3fd3d343326a91354fa8e00cbec6..7e485e323bef5d461e2985706f00e47022059611 100644 --- a/src/plugins/wp/RefUsage.ml +++ b/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) diff --git a/src/plugins/wp/tests/wp_plugin/nullable_ext.i b/src/plugins/wp/tests/wp_plugin/nullable_ext.i index dbb1ba794148d03aab849f55c2ce55c0ebe073c5..7225aa000f21516ce9c2596b9ff62f4e7245e7ca 100644 --- a/src/plugins/wp/tests/wp_plugin/nullable_ext.i +++ b/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;