Minor improvements in test descriptions

model-checking · Jan 10, 2024 · 12ecc4b · 12ecc4b
1 parent fc08166
commit 12ecc4b
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 6 deletions.
diff --git a/tests/ui/fail-uncoverable/all-covered/test.rs b/tests/ui/fail-uncoverable/all-covered/test.rs
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: --enable-unstable --fail-uncoverable
 
-//! Checks that all cover statements are satisfied and `--fail-uncoverable`
-//! doesn't cause failures.
+//! Checks that all cover statements are satisfied and enabling
+//! `--fail-uncoverable` doesn't cause unexpected failures.
 
 #[kani::proof]
 fn harness1() {

diff --git a/tests/ui/fail-uncoverable/uncoverable/test.rs b/tests/ui/fail-uncoverable/uncoverable/test.rs
@@ -2,8 +2,10 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: --enable-unstable --fail-uncoverable
 
-//! Checks that the `--fail-uncoverable` option causes a failure due to a cover
-//! statement not being covered.
+//! Checks that enabling the `--fail-uncoverable` option triggers a
+//! condition-based failure due to a `cover` statement not being satisfied.
+//!
+//! Note: The `cover` statement isn't satisfied because it's unreachable.
 
 #[kani::proof]
 fn harness_uncoverable() {

diff --git a/tests/ui/fail-uncoverable/unsatisfied/test.rs b/tests/ui/fail-uncoverable/unsatisfied/test.rs
@@ -2,8 +2,11 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: --enable-unstable --fail-uncoverable
 
-//! Checks that the `--fail-uncoverable` option causes a failure due to a cover
-//! statement not being satisfied.
+//! Checks that enabling the `--fail-uncoverable` option triggers a
+//! condition-based failure due to a `cover` statement not being satisfied.
+//!
+//! Note: The `cover` statement isn't satisfied because the condition `x == -1`
+//! cannot be satisfied.
 
 #[kani::proof]
 fn harness_unsatisfied() {