From b92bb6595b7ea5ff7b6954b0417b18d12d0934d2 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 16 Jan 2025 11:09:17 +0100
Subject: [PATCH] [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 | 17 ++++++++++-------
src/plugins/eva/engine/recursion.ml | 8 ++++----
.../eva/engine/transfer_specification.ml | 15 ++++++++-------
3 files changed, 22 insertions(+), 18 deletions(-)
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 30b6bc6e5f9..49efc48b0ba 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/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
diff --git a/src/plugins/eva/engine/recursion.ml b/src/plugins/eva/engine/recursion.ml
index 4852aa7590e..c984b0bc8b6 100644
--- a/src/plugins/eva/engine/recursion.ml
+++ b/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
*)
diff --git a/src/plugins/eva/engine/transfer_specification.ml b/src/plugins/eva/engine/transfer_specification.ml
index 27c8c62b98e..1539cc63406 100644
--- a/src/plugins/eva/engine/transfer_specification.ml
+++ b/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 =
--
GitLab