[Kernel] do not emit warnings-as-feedback when verbosity is 0

src/kernel_services/plugin_entry_points/log.ml

@@ -1133,7 +1133,13 @@ struct
       ?current ?source
       ?echo ?append text =
     let status = get_warn_status wkey in
-    if status <> Winactive then
+    let kind =
+      match status with
+      | Wfeedback | Wfeedback_once -> Feedback
+      | (Wactive | Werror | Wabort | Wonce | Werror_once | Winactive) ->
+        Warning
+    in
+    if status <> Winactive && (kind <> Feedback || verbose_atleast 1)  then
       begin
         let action, once_suffix =
           match status with
@@ -1157,12 +1163,6 @@ struct
           | Some e, None | None, Some e -> Some e
           | Some e1, Some e2 -> Some (fun evt -> e1 evt; e2 evt)
         in
-        let kind =
-          match status with
-          | Wfeedback | Wfeedback_once -> Feedback
-          | (Wactive | Werror | Wabort | Wonce | Werror_once | Winactive) ->
-            Warning
-        in
         let category = if wkey = "" then None else Some wkey in
         let append_once_suffix = (fun fmt ->
             Format.fprintf fmt

src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle

@@ -2,6 +2,3 @@
 [e-acsl] translation done in project "e-acsl".
 [kernel:annot:missing-spec] hidden_malloc.c:11: Warning: 
   Neither code nor specification for function realpath, generating default assigns from the prototype
-[eva:invalid-assigns] hidden_malloc.c:11: 
-  Completely invalid destination for assigns clause *(resolved_name + (0 ..)).
-  Ignoring.