docs

model-checking · Oct 30, 2024 · 7770e3f · 7770e3f
1 parent 1301123
commit 7770e3f
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs
@@ -410,15 +410,17 @@
 //!                            kani::internal::apply_closure(|result|
 //!                              (remember_kani_internal_2e780b148d45b5c8) == * ptr,
 //!                              &result_kani_internal
-//!                         ),
+//!                             ),
+//!                         "The contract's postcondition is reachable.");
 //!                         kani::assert(kani::internal::apply_closure(|result|
 //!                                     (remember_kani_internal_92cc419d8aca576c) == *ptr,
 //!                                 &result_kani_internal), "|result| old(*ptr + 1) == *ptr");
 //!                         kani::internal::contract_cover(
 //!                            kani::internal::apply_closure(|result|
 //!                              (remember_kani_internal_2e780b148d45b5c8) == * ptr,
 //!                              &result_kani_internal
-//!                         ),
+//!                             ),
+//!                         "The contract's postcondition is reachable.");
 //!                         kani::assert(kani::internal::apply_closure(|result|
 //!                                     (remember_kani_internal_92cc419d8aca576c) == *ptr,
 //!                                 &result_kani_internal), "|result| old(*ptr + 1) == *ptr");