Fix format

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,
         }
     }
 }

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(());

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.

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);
 }