[Eva] Update missing assigns messages

The warning messages for missing assigns and missing from now have a
category that is set to `error` by default. Moreover, the message is
expanded to note that `assigns \nothing` and `assigns \from \nothing` is
assumed instead and that the analysis is probably incorrect.

src/plugins/eva/engine/compute_functions.ml

@@ -59,12 +59,14 @@ let options_ok () =
   check Parameters.EqualityCallFunction.get;
   let check_assigns kf =
     if need_assigns kf then
-      Self.error "@[no assigns@ specified@ for function '%a',@ for \
-                  which@ a builtin@ or the specification@ will be used.@ \
-                  Potential unsoundness.@]" Kernel_function.pretty kf
+      Self.warning ~wkey:Self.wkey_missing_assigns
+        "@[No assigns specified for function '%a', for which a builtin will be \
+         used. Potential unsoundness.@]"
+        Kernel_function.pretty kf
   in
-  Parameters.BuiltinsOverrides.iter (fun (kf, _) -> check_assigns kf);
-  Parameters.UsePrototype.iter (fun kf -> check_assigns kf)
+  Parameters.BuiltinsOverrides.iter (fun (kf, _) -> check_assigns kf)
+
+(* Parameters.UsePrototype.iter (fun kf -> check_assigns kf) *)
 
 let plugins_ok () =
   if not (Plugin.is_present "inout") then
@@ -77,8 +79,9 @@ let plugins_ok () =
 let generate_specs () =
   let aux kf =
     if need_assigns kf then begin
-      Self.warning "Generating potentially incorrect assigns \
-                    for function '%a' for which option %s is set"
+      Self.warning ~wkey:Self.wkey_missing_assigns
+        "@[No assigns specified for function '%a' for which option %s is set. \
+         Generating potentially incorrect assigns.@]"
         Kernel_function.pretty kf Parameters.UsePrototype.option_name;
       Populate_spec.populate_funspec ~do_body:true kf [`Assigns];
     end

src/plugins/eva/engine/recursion.ml

@@ -48,11 +48,11 @@ let check_spec kinstr kf =
   let funspec = Annotations.funspec kf in
   if List.for_all (fun b -> b.b_assigns = WritesAny) funspec.spec_behavior
   then
-    Self.error ~current:true
-      "@[Recursive call to %a@ without assigns clause.@ \
+    Self.warning ~current:true ~wkey:Self.wkey_missing_assigns
+      "@[Recursive call to %a without assigns clause.@ \
        Generating probably incomplete assigns to interpret the call.@ \
-       Try to increase@ the %s parameter@ \
-       or write a correct specification@ for function %a.@\n%t@]"
+       Try to increase the %s parameter \
+       or write a correct specification for function %a.@\n%t@]"
       (* note: the "\n" before the pretty print of the stack is required by:
          FRAMAC_LIB/analysis-scripts/make_wrapper.py
       *)

src/plugins/eva/engine/transfer_specification.ml

@@ -40,9 +40,9 @@ let find_default_behavior spec =
   List.find (fun b' -> b'.b_name = Cil.default_behavior_name) spec.spec_behavior
 
 let warn_empty_assigns () =
-  Self.warning ~current:true ~once:true
-    "Cannot handle empty assigns clause. Assuming assigns \\nothing: \
-     be aware this is probably incorrect."
+  Self.warning ~current:true ~once:true ~wkey:Self.wkey_missing_assigns
+    "Cannot handle empty assigns clause. Assuming assigns \\nothing so that \
+     the analysis can continue, but be aware this is probably incorrect."
 
 (* Warn for assigns clauses without \from. *)
 let warn_empty_from list =
@@ -51,8 +51,9 @@ let warn_empty_from list =
   | [] -> ()
   | (out, _) :: _ ->
     let source = fst out.it_content.term_loc in
-    Self.warning ~source ~once:true
-      "@[no \\from part@ for clause '%a'@]"
+    Self.warning ~source ~once:true ~wkey:Self.wkey_missing_assigns
+      "@[no \\from part for clause@ '%a'.@ Assuming \\from \\nothing so that \
+       the analysis can continue, but be aware this is probably incorrect.@]"
       Printer.pp_assigns (Writes no_from)
 
 let get_assigns = function
@@ -124,8 +125,8 @@ let warn_on_missing_result_assigns kinstr kf spec =
   if return_used && not (List.for_all assigns_result spec.spec_behavior)
   then
     let source = fst (Kernel_function.get_location kf) in
-    Self.warning ~once:true ~source
-      "@[no 'assigns \\result@ \\from ...'@ clause@ specified for@ function %a@]"
+    Self.warning ~wkey:Self.wkey_missing_assigns_result  ~once:true ~source
+      "@[no 'assigns \\result \\from ...' clause specified for function %a@]"
       Kernel_function.pretty kf
 
 let reduce_to_valid_location kind term loc =