Handle hook for loop contracts register function when loop contracts …

…didsabled
model-checking · Nov 8, 2024 · deef703 · deef703
1 parent 94862d4
commit deef703
Showing 1 changed file with 37 additions and 19 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
@@ -576,25 +576,43 @@ impl GotocHook for LoopInvariantRegister {
 
         gcx.has_loop_contracts = true;
 
-        // Add `free(0)` to make sure the body of `free` won't be dropped to
-        // satisfy the requirement of DFCC.
-        Stmt::block(
-            vec![
-                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)),
-                ),
-            ],
-            loc,
-        )
+        if gcx.queries.args().unstable_features.contains(&"loop-contracts".to_string()) {
+            // When loop-contracts is enabled, codegen
+            // free(0)
+            // goto target --- with loop contracts annotated.
+
+            // Add `free(0)` to make sure the body of `free` won't be dropped to
+            // satisfy the requirement of DFCC.
+            Stmt::block(
+                vec![
+                    BuiltinFn::Free
+                        .call(vec![Expr::pointer_constant(0, Type::void_pointer())], loc)
+                        .as_stmt(loc),
+                    Stmt::goto(bb_label(target.unwrap()), loc).with_loop_contracts(
+                        func_exp.call(fargs).cast_to(Type::CInteger(CIntType::Bool)),
+                    ),
+                ],
+                loc,
+            )
+        } else {
+            // When loop-contracts is not enabled, codegen
+            // assign_to = true
+            // goto target
+            Stmt::block(
+                vec![
+                    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)),
+                    ),
+                ],
+                loc,
+            )
+        }
     }
 }