From 9260e22e4ff49932743651ca3d0fd85c2a2f244f Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 24 Mar 2022 07:46:03 +0100
Subject: [PATCH] [Eva] add wkey for 'ensures \false' check
---
src/plugins/value/engine/transfer_logic.ml | 2 +-
src/plugins/value/self.ml | 1 +
src/plugins/value/self.mli | 1 +
3 files changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index 634021c6ecc..74a8d6d6799 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -359,7 +359,7 @@ module Make
| Postcondition (PostLeaf | PostUseSpec) -> true
| _ -> false)
&& pr.pred_content <> Pfalse then
- Self.warning ~once:true ~source
+ Self.warning ~once:true ~source ~wkey:Self.wkey_ensures_false
"@[%a:@ this postcondition@ evaluates to@ false@ in this@ context.\
@ If it is valid,@ either@ a precondition@ was not@ verified@ \
for this@ call%t,@ or some assigns/from@ clauses@ are \
diff --git a/src/plugins/value/self.ml b/src/plugins/value/self.ml
index 84e12b63e79..430ed2dfde6 100644
--- a/src/plugins/value/self.ml
+++ b/src/plugins/value/self.ml
@@ -132,3 +132,4 @@ let wkey_invalid_assigns = register_warn_category "invalid-assigns"
let () = set_warn_status wkey_invalid_assigns Log.Wfeedback
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/value/self.mli b/src/plugins/value/self.mli
index f975ab4db65..97b25ff3416 100644
--- a/src/plugins/value/self.mli
+++ b/src/plugins/value/self.mli
@@ -77,3 +77,4 @@ val wkey_signed_overflow : warn_category
val wkey_invalid_assigns : warn_category
val wkey_experimental : warn_category
val wkey_unknown_size : warn_category
+val wkey_ensures_false : warn_category
--
GitLab