From fbf71aef72b1700c2ef4300b39c4e3ab0286469c Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Thu, 7 Nov 2024 16:59:29 -0600
Subject: [PATCH] Fix format

---
 kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs | 2 +-
 kani-driver/src/call_goto_instrument.rs                     | 6 +-----
 kani_metadata/src/harness.rs                                | 2 ++
 tests/expected/loop-contract/multiple_loops.rs              | 2 +-
 4 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
index ec95f7e908cd..6fd9da651002 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -105,7 +105,7 @@ impl<'tcx> GotocCtx<'tcx> {
             unsupported_constructs: FxHashMap::default(),
             concurrent_constructs: FxHashMap::default(),
             transformer,
-            has_loop_contracts: false
+            has_loop_contracts: false,
         }
     }
 }
diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs
index 6825392e3309..8f4eb150ff7b 100644
--- a/kani-driver/src/call_goto_instrument.rs
+++ b/kani-driver/src/call_goto_instrument.rs
@@ -164,11 +164,7 @@ impl KaniSession {
     }
 
     /// Apply annotated function contracts and loop contracts with goto-instrument.
-    pub fn instrument_contracts(
-        &self,
-        harness: &HarnessMetadata,
-        file: &Path,
-    ) -> Result<()> {
+    pub fn instrument_contracts(&self, harness: &HarnessMetadata, file: &Path) -> Result<()> {
         // Do nothing if neither loop contracts nor function contracts is enabled.
         if !harness.has_loop_contracts && harness.contract.is_none() {
             return Ok(());
diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs
index 426cf8d9e960..6932b15dc1a7 100644
--- a/kani_metadata/src/harness.rs
+++ b/kani_metadata/src/harness.rs
@@ -36,6 +36,8 @@ pub struct HarnessMetadata {
     pub attributes: HarnessAttributes,
     /// A CBMC-level assigns contract that should be enforced when running this harness.
     pub contract: Option<AssignsContract>,
+    /// If the harness contains some usage of loop contracts.
+    pub has_loop_contracts: bool,
 }
 
 /// The attributes added by the user to control how a harness is executed.
diff --git a/tests/expected/loop-contract/multiple_loops.rs b/tests/expected/loop-contract/multiple_loops.rs
index 8c844eee2f95..b99278d32b43 100644
--- a/tests/expected/loop-contract/multiple_loops.rs
+++ b/tests/expected/loop-contract/multiple_loops.rs
@@ -47,7 +47,7 @@ fn simple_while_loops() {
 /// Check that `loop-contracts` works correctly for harness
 /// without loop contracts.
 #[kani::proof]
-fn no_loop_harness(){
+fn no_loop_harness() {
     let x = 2;
     assert!(x == 2);
 }