Minor improvements in documentation

model-checking · Jan 3, 2024 · 1dda0ed · 1dda0ed
1 parent b5b8447
commit 1dda0ed
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 4 deletions.
diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
@@ -472,7 +472,9 @@ fn outcome_from_global_conditions(
         .filter(|cond| cond.enabled())
         .collect::<Vec<&GlobalCondition>>()
         .is_empty();
+
     if !enabled_global_conditions {
+        // If no global conditions are enabled, the outcome only depends on failed properties
         let failed_properties = determine_failed_properties(properties);
         if failed_properties == FailedProperties::None {
             VerificationStatus::Success

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 covered/satisfied and
-//! `--fail-uncoverable` doesn't cause failures.
+//! Checks that all cover statements are satisfied and `--fail-uncoverable`
+//! doesn't cause failures.
 
 #[kani::proof]
 fn harness1() {

diff --git a/tests/ui/fail-uncoverable/uncoverable/test.rs b/tests/ui/fail-uncoverable/uncoverable/test.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: --enable-unstable --fail-uncoverable
 
-//! Checks that the `--fail-uncoverable` option cause a failure due to a cover
+//! Checks that the `--fail-uncoverable` option causes a failure due to a cover
 //! statement not being covered.
 
 #[kani::proof]

diff --git a/tests/ui/fail-uncoverable/unsatisfied/test.rs b/tests/ui/fail-uncoverable/unsatisfied/test.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: --enable-unstable --fail-uncoverable
 
-//! Checks that the `--fail-uncoverable` option cause a failure due to a cover
+//! Checks that the `--fail-uncoverable` option causes a failure due to a cover
 //! statement not being satisfied.
 
 #[kani::proof]