diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index 634021c6eccb088daea3311546445e8d09afb663..74a8d6d679985101272a63334dc9c6a1bb24a24e 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 84e12b63e791fbc0c4193ff32bc6ca8113e8fdfe..430ed2dfde6c190fe6d58c1fca3c4af01cadfcf1 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 f975ab4db65c66f3a491aedc74f8b647f0c675b5..97b25ff341643a3f700ffffb5f2fe9a0ab4a8ddb 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