From 2ccb1c9f37e6839bcf421ac561360232c1d491d5 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 21 Jun 2023 14:45:24 +0200
Subject: [PATCH] [Kernel] do not emit warnings-as-feedback when verbosity is 0
---
src/kernel_services/plugin_entry_points/log.ml | 14 +++++++-------
.../tests/memory/oracle/hidden_malloc.res.oracle | 3 ---
2 files changed, 7 insertions(+), 10 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/log.ml b/src/kernel_services/plugin_entry_points/log.ml
index d6923055b24..7ebcab452aa 100644
--- a/src/kernel_services/plugin_entry_points/log.ml
+++ b/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
diff --git a/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
index ef3478f02e7..b795e7d036e 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
+++ b/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.
--
GitLab