From cd47c9f8c109ff208bc54cfaccdb3687c789d206 Mon Sep 17 00:00:00 2001
From: jaisnan <jaisnan@amazon.com>
Date: Fri, 28 Jul 2023 12:31:29 -0400
Subject: [PATCH] Run formatting

---
 kani-driver/src/cbmc_output_parser.rs                    | 4 ++--
 kani-driver/src/cbmc_property_renderer.rs                | 2 +-
 tests/coverage/reachable/bounds/reachable_fail/test.rs   | 6 +++---
 tests/coverage/reachable/div-zero/reachable_fail/test.rs | 2 +-
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs
index 58ffc8b15b95..8f3e1d933ee7 100644
--- a/kani-driver/src/cbmc_output_parser.rs
+++ b/kani-driver/src/cbmc_output_parser.rs
@@ -328,8 +328,8 @@ impl std::fmt::Display for TraceData {
 #[serde(rename_all = "UPPERCASE")]
 pub enum CheckStatus {
     Failure,
-    Covered,       // for `code_coverage` properties only
-    Satisfied,     // for `cover` properties only
+    Covered,   // for `code_coverage` properties only
+    Satisfied, // for `cover` properties only
     Success,
     Undetermined,
     Unreachable,
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
index dd84efa019a8..b8ce44942443 100644
--- a/kani-driver/src/cbmc_property_renderer.rs
+++ b/kani-driver/src/cbmc_property_renderer.rs
@@ -456,7 +456,7 @@ pub fn format_coverage(
 ///  - A status `FULL` if all checks pertaining to a line number are `COVERED`
 ///  - A status `NONE` if all checks related to a line are `UNCOVERED`
 ///  - Otherwise (i.e., if the line contains both) it reports `PARTIAL`.
-/// 
+///
 /// Used when the user requests coverage information with `--coverage`.
 /// Output is tested through the `coverage-based` testing suite, not the regular
 /// `expected` suite.
diff --git a/tests/coverage/reachable/bounds/reachable_fail/test.rs b/tests/coverage/reachable/bounds/reachable_fail/test.rs
index 1044ecd03fcb..0353768ae122 100644
--- a/tests/coverage/reachable/bounds/reachable_fail/test.rs
+++ b/tests/coverage/reachable/bounds/reachable_fail/test.rs
@@ -2,10 +2,10 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 fn get(s: &[i16], index: usize) -> i16 {
-    s[index]                // PARTIAL: `index = 15` causes failure, but `s[index]` is `COVERED`
-}                           // NONE: `index = 15` caused failure earlier
+    s[index] // PARTIAL: `index = 15` causes failure, but `s[index]` is `COVERED`
+} // NONE: `index = 15` caused failure earlier
 
 #[kani::proof]
 fn main() {
     get(&[7, -83, 19], 15);
-}                           // NONE: `index = 15` caused failure earlier
+} // NONE: `index = 15` caused failure earlier
diff --git a/tests/coverage/reachable/div-zero/reachable_fail/test.rs b/tests/coverage/reachable/div-zero/reachable_fail/test.rs
index a7f1cd63f5f9..5f69005ee712 100644
--- a/tests/coverage/reachable/div-zero/reachable_fail/test.rs
+++ b/tests/coverage/reachable/div-zero/reachable_fail/test.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 fn div(x: u16, y: u16) -> u16 {
-    x / y         // PARTIAL: `y = 0` causes failure, but `x / y` is `COVERED`
+    x / y // PARTIAL: `y = 0` causes failure, but `x / y` is `COVERED`
 }
 
 #[kani::proof]