From b77a1c4036c3d96082620009e41a49fb9ca1d745 Mon Sep 17 00:00:00 2001 From: Basile Desloges <basile.desloges@cea.fr> Date: Tue, 21 Jan 2025 16:30:39 +0100 Subject: [PATCH] [Eva] Add wkey for missing assigns \result --- src/plugins/eva/self.ml | 3 ++- src/plugins/eva/self.mli | 1 + 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/plugins/eva/self.ml b/src/plugins/eva/self.ml index c9ada9d1231..5fb3cb9223b 100644 --- a/src/plugins/eva/self.ml +++ b/src/plugins/eva/self.ml @@ -138,10 +138,11 @@ let () = set_warn_status wkey_missing_loop_unroll Log.Winactive let wkey_missing_loop_unroll_for = register_warn_category "loop-unroll:missing:for" let () = set_warn_status wkey_missing_loop_unroll_for Log.Winactive let wkey_signed_overflow = register_warn_category "signed-overflow" -let wkey_invalid_assigns = register_warn_category "assigns:invalid" +let wkey_invalid_assigns = register_warn_category "assigns:invalid-location" let () = set_warn_status wkey_invalid_assigns Log.Wfeedback let wkey_missing_assigns = register_warn_category "assigns:missing" let () = set_warn_status wkey_missing_assigns Log.Werror +let wkey_missing_assigns_result = register_warn_category "assigns:missing-result" let wkey_experimental = register_warn_category "experimental" let wkey_unknown_size = register_warn_category "unknown-size" let wkey_ensures_false = register_warn_category "ensures-false" diff --git a/src/plugins/eva/self.mli b/src/plugins/eva/self.mli index 96b5d8e4365..0e05e69bb71 100644 --- a/src/plugins/eva/self.mli +++ b/src/plugins/eva/self.mli @@ -70,6 +70,7 @@ val wkey_missing_loop_unroll_for : warn_category val wkey_signed_overflow : warn_category val wkey_invalid_assigns : warn_category val wkey_missing_assigns : warn_category +val wkey_missing_assigns_result : warn_category val wkey_experimental : warn_category val wkey_unknown_size : warn_category val wkey_ensures_false : warn_category -- GitLab