From 1f3baa9e9f96f911e470ba2e109b62ac41f67026 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 15 Feb 2021 15:55:01 +0100
Subject: [PATCH] [wp] RefUsage: provide "nullable" notion

---
 src/plugins/wp/RefUsage.ml  | 3 +++
 src/plugins/wp/RefUsage.mli | 4 ++++
 2 files changed, 7 insertions(+)

diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 4413187be9e..16930c7940e 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -852,6 +852,9 @@ let get ?kf ?(init=false) vi =
   in
   if init then Access.cup kf_access (E.get vi u_init) else kf_access
 
+let is_nullable vi =
+  vi.vformal && Cil.hasAttribute "nullable" vi.vattr
+
 let compute () = ignore (usage ())
 
 let print x m fmt = Access.pretty x fmt m
diff --git a/src/plugins/wp/RefUsage.mli b/src/plugins/wp/RefUsage.mli
index 988103efebf..5d90fa9220f 100644
--- a/src/plugins/wp/RefUsage.mli
+++ b/src/plugins/wp/RefUsage.mli
@@ -38,6 +38,10 @@ val get : ?kf:kernel_function -> ?init:bool -> varinfo -> access
 
 val iter: ?kf:kernel_function -> ?init:bool -> (varinfo -> access -> unit) -> unit
 
+val is_nullable : varinfo -> bool
+  (** [is_nullable vi] returns true
+      iff [vi] is a formal and has an attribute 'nullable' *)
+
 val print : varinfo -> access -> Format.formatter -> unit
 val dump : unit -> unit
 val compute : unit -> unit
-- 
GitLab