diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 4413187be9efce693afa69a5795f59bdbcb68288..16930c7940eaea2fa7e2bbad111848b706a84caf 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 988103efebfd6817de6320945e69f06d9194cc12..5d90fa9220f5053c6cbf3da290875d2d92587cef 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