Run formatting

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,

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.

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

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]