[wp] Warn RTE using Caveat or Ref with nullable

src/plugins/wp/Generator.ml

@@ -50,7 +50,20 @@ let user_setup () : Factory.setup =
           cint = Cint.Natural ;
           cfloat = Cfloat.Real ;
         }
-    | spec -> Factory.parse spec
+    | spec ->
+        let setup = Factory.parse spec in
+        let mvar_special = match setup.mvar with
+          | Caveat -> "Caveat" | Ref -> "Ref" | _ -> ""
+        in
+        if mvar_special <> ""
+        && RefUsage.has_nullable ()
+        && not (Wp_parameters.RTE.is_set ())
+        then
+          Wp_parameters.warning ~current:false ~once:true
+            "In %s mode, with nullable variables,\
+             -wp-rte should be explicitly positioned"
+            mvar_special;
+        setup
   end
 
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/RefUsage.ml

@@ -831,14 +831,6 @@ let is_computed () = S.is_computed ()
 (* --- Nullable variables                                             --- *)
 (* ---------------------------------------------------------------------- *)
 
-module NullableStatuses =
-  State_builder.Hashtbl(Varinfo.Hashtbl)(Datatype.Bool)
-    (struct
-      let size = 17
-      let name = "Wp.RefUsage.NullableStatuses"
-      let dependencies = [Ast.self]
-    end)
-
 module HasNullable =
   State_builder.Option_ref(Datatype.Bool)
     (struct
@@ -846,17 +838,13 @@ module HasNullable =
       let dependencies = [Ast.self]
     end)
 
-let is_nullable =
-  NullableStatuses.memo
-    (fun vi -> vi.vformal && Cil.hasAttribute "nullable" vi.vattr)
+let is_nullable vi = vi.vformal && Cil.hasAttribute "nullable" vi.vattr
 
 let compute_nullable () =
   let module F = Globals.Functions in
-  (* Avoid short-circuit optimization so that all variables are visited *)
-  let force_or a b = a || b in
-  F.fold
-    (fun f -> List.fold_right (fun v -> force_or @@ is_nullable v)
-        (F.get_params f)) false
+  F.fold (fun f b ->
+      b || List.fold_left (fun b v -> b || is_nullable v) b (F.get_params f)
+    ) false
 
 let has_nullable () = HasNullable.memo compute_nullable
 
@@ -887,6 +875,8 @@ let get ?kf ?(init=false) vi =
 
 let compute () = ignore (usage ())
 
+
+
 let print x m fmt = Access.pretty x fmt m
 
 let dump () =

src/plugins/wp/RefUsage.mli

@@ -39,8 +39,12 @@ 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' *)
+(** [is_nullable vi] returns true
+    iff [vi] is a formal and has an attribute 'nullable' *)
+
+val has_nullable : unit -> bool
+(** [has_nullable ()] return true
+    iff there exists a variable that satisfies [is_nullable] *)
 
 val print : varinfo -> access -> Format.formatter -> unit
 val dump : unit -> unit