From d892bdaa71d0ddbd5f48c9d60c6ad2fa00b2e6ea Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 24 Feb 2021 17:06:58 +0100
Subject: [PATCH] [wp] wp_nullable(_pointers) -> (_args)
---
src/plugins/wp/RefUsage.ml | 4 ++--
src/plugins/wp/tests/wp_plugin/nullable_ext.i | 4 ++--
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 0bf6762b319..7e485e323be 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 dbb1ba79414..7225aa000f2 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;
--
GitLab