Add a test without loop contracts enabled

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -567,7 +567,7 @@ impl GotocHook for LoopInvariantRegister {
         gcx: &mut GotocCtx,
         instance: Instance,
         fargs: Vec<Expr>,
-        _assign_to: &Place,
+        assign_to: &Place,
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
@@ -583,6 +583,12 @@ impl GotocHook for LoopInvariantRegister {
                 BuiltinFn::Free
                     .call(vec![Expr::pointer_constant(0, Type::void_pointer())], loc)
                     .as_stmt(loc),
+                unwrap_or_return_codegen_unimplemented_stmt!(
+                    gcx,
+                    gcx.codegen_place_stable(assign_to, loc)
+                )
+                .goto_expr
+                .assign(Expr::c_true(), loc),
                 Stmt::goto(bb_label(target.unwrap()), loc).with_loop_contracts(
                     func_exp.call(fargs).cast_to(Type::CInteger(CIntType::Bool)),
                 ),

kani-driver/src/call_goto_instrument.rs

@@ -37,7 +37,13 @@ impl KaniSession {
             self.goto_sanity_check(output)?;
         }
 
-        self.instrument_contracts(harness, output)?;
+        let is_loop_contracts_enabled = self
+            .args
+            .common_args
+            .unstable_features
+            .contains(kani_metadata::UnstableFeature::LoopContracts)
+            && harness.has_loop_contracts;
+        self.instrument_contracts(harness, is_loop_contracts_enabled, output)?;
 
         if self.args.checks.undefined_function_on() {
             self.add_library(output)?;
@@ -164,16 +170,21 @@ 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,
+        is_loop_contracts_enabled: bool,
+        file: &Path,
+    ) -> Result<()> {
         // Do nothing if neither loop contracts nor function contracts is enabled.
-        if !harness.has_loop_contracts && harness.contract.is_none() {
+        if !is_loop_contracts_enabled && harness.contract.is_none() {
             return Ok(());
         }
 
         let mut args: Vec<OsString> =
             vec!["--dfcc".into(), (&harness.mangled_name).into(), "--no-malloc-may-fail".into()];
 
-        if harness.has_loop_contracts {
+        if is_loop_contracts_enabled {
             args.append(&mut vec![
                 "--apply-loop-contracts".into(),
                 "--loop-contracts-no-unwind".into(),

kani-driver/src/metadata.rs

@@ -223,6 +223,7 @@ pub mod tests {
             attributes,
             goto_file: model_file,
             contract: Default::default(),
+            has_loop_contracts: false,
         }
     }
 

tests/expected/loop-contract/multiple_loops.expected

@@ -1 +1,2 @@
 VERIFICATION:- SUCCESSFUL
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.

tests/expected/loop-contract/simple_while_loop_not_enabled.expected

@@ -0,0 +1,2 @@
+Unwinding loop
+VERIFICATION:- SUCCESSFUL

tests/expected/loop-contract/simple_while_loop_not_enabled.rs

@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags:
+
+//! Check if the harness can be proved when loop contracts is not enabled.
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+#[kani::proof]
+fn simple_while_loop_harness() {
+    let mut x: u8 = 10;
+
+    #[kani::loop_invariant(x >= 2)]
+    while x > 2 {
+        x = x - 1;
+    }
+
+    assert!(x == 2);
+}