From 4e4831c8b6fe174728edf065bfb55cdb2fde0a26 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Tue, 12 Aug 2025 18:07:26 -0400
Subject: [PATCH 1/4] error for invalid stub_verified path

---
 kani-compiler/src/kani_middle/attributes.rs            |  1 +
 .../invalid-path/stub_verified_invalid_path.expected   |  9 +++++++++
 .../invalid-path/stub_verified_invalid_path.rs         | 10 ++++++++++
 3 files changed, 20 insertions(+)
 create mode 100644 tests/ui/stubbing/invalid-path/stub_verified_invalid_path.expected
 create mode 100644 tests/ui/stubbing/invalid-path/stub_verified_invalid_path.rs

diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 678c24a20aca..3c0e19d8cebb 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -369,6 +369,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                 KaniAttributeKind::StubVerified => {
                     attrs.iter().for_each(|attr| {
                         self.check_stub_verified(attr);
+                        let res = self.parse_single_path_attr(attr);
                     });
                 }
                 KaniAttributeKind::FnMarker
diff --git a/tests/ui/stubbing/invalid-path/stub_verified_invalid_path.expected b/tests/ui/stubbing/invalid-path/stub_verified_invalid_path.expected
new file mode 100644
index 000000000000..e0f6e88f9aba
--- /dev/null
+++ b/tests/ui/stubbing/invalid-path/stub_verified_invalid_path.expected
@@ -0,0 +1,9 @@
+error: failed to resolve `nonexistent_function`: unable to find `nonexistent_function` inside module `stub_verified_invalid_path`\
+stub_verified_invalid_path.rs:8:1\
+|\
+| #[kani::stub_verified(nonexistent_function)]\
+| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
+|
+
+error: aborting due to 1 previous error
+
diff --git a/tests/ui/stubbing/invalid-path/stub_verified_invalid_path.rs b/tests/ui/stubbing/invalid-path/stub_verified_invalid_path.rs
new file mode 100644
index 000000000000..4184a72beda4
--- /dev/null
+++ b/tests/ui/stubbing/invalid-path/stub_verified_invalid_path.rs
@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z function-contracts
+
+// Test that Kani catches invalid paths in stub_verified attributes
+
+#[kani::stub_verified(nonexistent_function)]
+#[kani::proof]
+fn test_invalid_path() {}

From 0d36c5d5f8e0349f30de61dd3c8ea35de4c5d8e4 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Tue, 12 Aug 2025 18:30:48 -0400
Subject: [PATCH 2/4] error if stub verified doesn't have a proof_for_contract
 harness

---
 kani-compiler/src/kani_middle/attributes.rs   | 17 ++++++++--
 kani-compiler/src/kani_middle/mod.rs          | 24 +++++++++++++-
 .../as-assertions/precedence.expected         |  2 +-
 .../as-assertions/precedence.rs               |  9 ++++++
 .../gcd_rec_replacement_pass.rs               | 12 +++++--
 .../function-contract/gcd_replacement_fail.rs |  8 +++++
 .../function-contract/gcd_replacement_pass.rs |  8 +++++
 .../modifies/check_invalid_modifies.rs        |  6 ++++
 .../modifies/check_only_verification.rs       |  6 ++++
 .../modifies/expr_replace_fail.rs             |  7 ++++
 .../modifies/expr_replace_pass.rs             |  7 ++++
 .../modifies/field_replace_fail.rs            |  7 ++++
 .../modifies/field_replace_pass.rs            |  9 ++++++
 .../modifies/global_replace_fail.rs           |  7 ++++
 .../modifies/global_replace_pass.rs           |  8 +++++
 .../modifies/mistake_condition_return.rs      |  6 ++++
 .../function-contract/simple_replace_fail.rs  |  7 ++++
 .../function-contract/simple_replace_pass.rs  |  7 ++++
 .../stub_verified_no_harness.expected         | 27 ++++++++++++++++
 .../stub_verified_no_harness.rs               | 32 +++++++++++++++++++
 20 files changed, 210 insertions(+), 6 deletions(-)
 create mode 100644 tests/ui/stub-verified-without-contract/stub_verified_no_harness.expected
 create mode 100644 tests/ui/stub-verified-without-contract/stub_verified_no_harness.rs

diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 3c0e19d8cebb..98de8c516fae 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -4,6 +4,7 @@
 
 use std::collections::{BTreeMap, HashSet};
 
+use fxhash::FxHashMap;
 use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub};
 use quote::ToTokens;
 use rustc_ast::{LitKind, MetaItem, MetaItemKind};
@@ -300,11 +301,16 @@ impl<'tcx> KaniAttributes<'tcx> {
     }
 
     /// Check that all attributes assigned to an item is valid.
+    /// Returns a tuple of (stub_verified_targets_with_spans, proof_for_contract_targets).
     /// Errors will be added to the session. Invoke self.tcx.sess.abort_if_errors() to terminate
     /// the session and emit all errors found.
-    pub(super) fn check_attributes(&self) {
+    pub(super) fn check_attributes(&self) -> (FxHashMap<FnDefStable, Span>, HashSet<FnDefStable>) {
         // Check that all attributes are correctly used and well formed.
         let is_harness = self.is_proof_harness();
+
+        let mut contract_targets = HashSet::default();
+        let mut stub_verified_targets = FxHashMap::default();
+
         for (&kind, attrs) in self.map.iter() {
             let local_error = |msg| self.tcx.dcx().span_err(attrs[0].span(), msg);
 
@@ -363,13 +369,19 @@ impl<'tcx> KaniAttributes<'tcx> {
                     expect_single(self.tcx, kind, attrs);
                     attrs.iter().for_each(|attr| {
                         self.check_proof_attribute(kind, attr);
-                        let _ = self.parse_single_path_attr(attr);
+                        let res = self.parse_single_path_attr(attr);
+                        if let Ok(target) = res {
+                            contract_targets.insert(target.def().to_owned());
+                        }
                     })
                 }
                 KaniAttributeKind::StubVerified => {
                     attrs.iter().for_each(|attr| {
                         self.check_stub_verified(attr);
                         let res = self.parse_single_path_attr(attr);
+                        if let Ok(target) = res {
+                            stub_verified_targets.insert(target.def().to_owned(), attr.span());
+                        }
                     });
                 }
                 KaniAttributeKind::FnMarker
@@ -394,6 +406,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                 }
             }
         }
+        (stub_verified_targets, contract_targets)
     }
 
     /// Get the value of an attribute if one exists.
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
index 698fff6dc7d0..76a1985d2b9a 100644
--- a/kani-compiler/src/kani_middle/mod.rs
+++ b/kani-compiler/src/kani_middle/mod.rs
@@ -41,9 +41,16 @@ pub mod transform;
 /// error was found.
 pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) {
     let krate = tcx.crate_name(LOCAL_CRATE);
+    let mut all_stub_verified_targets = FxHashMap::default();
+    let mut all_contract_targets = HashSet::new();
+
     for item in tcx.hir_free_items() {
         let def_id = item.owner_id.def_id.to_def_id();
-        KaniAttributes::for_item(tcx, def_id).check_attributes();
+        let (stub_verified_targets, contract_targets) =
+            KaniAttributes::for_item(tcx, def_id).check_attributes();
+        all_stub_verified_targets.extend(stub_verified_targets);
+        all_contract_targets.extend(contract_targets);
+
         if tcx.def_kind(def_id) == DefKind::GlobalAsm {
             if !ignore_asm {
                 let error_msg = format!(
@@ -59,6 +66,21 @@ pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) {
             }
         }
     }
+
+    // Validate that all stub_verified targets have corresponding proof_for_contract harnesses
+    for (stub_verified_target, span) in all_stub_verified_targets {
+        if !all_contract_targets.contains(&stub_verified_target) {
+            tcx.dcx().struct_span_err(
+                span,
+                format!(
+                    "stub verified target `{}` does not have a corresponding `#[proof_for_contract]` harness",
+                    stub_verified_target.name()
+                ),
+            ).with_help("verified stubs are meant to be sound abstractions for a function's behavior, so Kani enforces that proofs exist for the stub's contract")
+            .emit();
+        }
+    }
+
     tcx.dcx().abort_if_errors();
 }
 
diff --git a/tests/expected/function-contract/as-assertions/precedence.expected b/tests/expected/function-contract/as-assertions/precedence.expected
index 0fa0efc5b0fc..f515ffce42da 100644
--- a/tests/expected/function-contract/as-assertions/precedence.expected
+++ b/tests/expected/function-contract/as-assertions/precedence.expected
@@ -31,4 +31,4 @@ assertion\
 	 - Status: SUCCESS\
 	 - Description: "|_| old(*add_one_ptr + 1) == *add_one_ptr"
 
-Complete - 3 successfully verified harnesses, 0 failures, 3 total.
+Complete - 4 successfully verified harnesses, 0 failures, 4 total.
diff --git a/tests/expected/function-contract/as-assertions/precedence.rs b/tests/expected/function-contract/as-assertions/precedence.rs
index 3d347eb74d5e..78dc03e42e26 100644
--- a/tests/expected/function-contract/as-assertions/precedence.rs
+++ b/tests/expected/function-contract/as-assertions/precedence.rs
@@ -12,6 +12,7 @@ fn add_three(add_three_ptr: &mut u32) {
 }
 
 #[kani::requires(*add_two_ptr < 101)]
+#[kani::modifies(add_two_ptr)]
 #[kani::ensures(|_| old(*add_two_ptr + 2) == *add_two_ptr)]
 fn add_two(add_two_ptr: &mut u32) {
     *add_two_ptr += 1;
@@ -59,3 +60,11 @@ fn stub_verified_takes_precedence() {
     let mut i = kani::any();
     add_three(&mut i);
 }
+
+// The stub_verified contract mandates that we have a proof for the target of the verified stub
+#[kani::proof_for_contract(add_two)]
+fn check_add_two() {
+    // 3 so that when add_one's contract is generated as an assertion, its precondition holds
+    let mut x = 3;
+    add_two(&mut x);
+}
diff --git a/tests/expected/function-contract/gcd_rec_replacement_pass.rs b/tests/expected/function-contract/gcd_rec_replacement_pass.rs
index 0fd04b0076ba..4cc724a9f75c 100644
--- a/tests/expected/function-contract/gcd_rec_replacement_pass.rs
+++ b/tests/expected/function-contract/gcd_rec_replacement_pass.rs
@@ -47,13 +47,21 @@ impl Frac {
     }
 }
 
+#[kani::proof_for_contract(gcd)]
+#[kani::unwind(64)]
+fn gcd_harness() {
+    let x: T = kani::any();
+    let y: T = kani::any();
+    gcd(x, y);
+}
+
 #[kani::proof]
 #[kani::stub_verified(gcd)]
 fn gcd_as_replace() {
-    gcd_harness()
+    gcd_test_harness()
 }
 
-fn gcd_harness() {
+fn gcd_test_harness() {
     // Needed to avoid having `free` be removed as unused function. This is
     // because DFCC contract enforcement assumes that a definition for `free`
     // exists.
diff --git a/tests/expected/function-contract/gcd_replacement_fail.rs b/tests/expected/function-contract/gcd_replacement_fail.rs
index 0186a369c3b2..54d9539e919a 100644
--- a/tests/expected/function-contract/gcd_replacement_fail.rs
+++ b/tests/expected/function-contract/gcd_replacement_fail.rs
@@ -54,6 +54,14 @@ impl Frac {
     }
 }
 
+#[kani::proof_for_contract(gcd)]
+#[kani::unwind(64)]
+fn gcd_harness() {
+    let x: T = kani::any();
+    let y: T = kani::any();
+    gcd(x, y);
+}
+
 #[kani::proof]
 #[kani::stub_verified(gcd)]
 fn main() {
diff --git a/tests/expected/function-contract/gcd_replacement_pass.rs b/tests/expected/function-contract/gcd_replacement_pass.rs
index b45241198737..abe1369811ff 100644
--- a/tests/expected/function-contract/gcd_replacement_pass.rs
+++ b/tests/expected/function-contract/gcd_replacement_pass.rs
@@ -54,6 +54,14 @@ impl Frac {
     }
 }
 
+#[kani::proof_for_contract(gcd)]
+#[kani::unwind(64)]
+fn gcd_harness() {
+    let x: T = kani::any();
+    let y: T = kani::any();
+    gcd(x, y);
+}
+
 #[kani::proof]
 #[kani::stub_verified(gcd)]
 fn main() {
diff --git a/tests/expected/function-contract/modifies/check_invalid_modifies.rs b/tests/expected/function-contract/modifies/check_invalid_modifies.rs
index 5cd832d0f456..6555cd03f697 100644
--- a/tests/expected/function-contract/modifies/check_invalid_modifies.rs
+++ b/tests/expected/function-contract/modifies/check_invalid_modifies.rs
@@ -25,3 +25,9 @@ fn harness() {
     let mut i = kani::any_where(|x| *x < 100);
     use_modify(&mut i);
 }
+
+#[kani::proof_for_contract(modify)]
+fn check_modify() {
+    let mut x: u32 = kani::any();
+    modify(&mut x);
+}
diff --git a/tests/expected/function-contract/modifies/check_only_verification.rs b/tests/expected/function-contract/modifies/check_only_verification.rs
index 9f3fb3614733..c68cdca6ecaf 100644
--- a/tests/expected/function-contract/modifies/check_only_verification.rs
+++ b/tests/expected/function-contract/modifies/check_only_verification.rs
@@ -26,6 +26,12 @@ fn use_modify(ptr: &mut u32) {
     assert!(modify(ptr) == 100);
 }
 
+#[kani::proof_for_contract(modify)]
+fn modify_harness() {
+    let ptr = &mut kani::any();
+    modify(ptr);
+}
+
 #[kani::proof]
 #[kani::stub_verified(modify)]
 fn harness() {
diff --git a/tests/expected/function-contract/modifies/expr_replace_fail.rs b/tests/expected/function-contract/modifies/expr_replace_fail.rs
index 09fa840d8696..5ac2c0fa87d2 100644
--- a/tests/expected/function-contract/modifies/expr_replace_fail.rs
+++ b/tests/expected/function-contract/modifies/expr_replace_fail.rs
@@ -20,3 +20,10 @@ fn main() {
     modify(&mut i);
     assert!(*i == val + 1, "Increment");
 }
+
+#[kani::proof_for_contract(modify)]
+fn check_modify() {
+    let val = kani::any();
+    let mut ptr = Box::new(val);
+    modify(&mut ptr);
+}
diff --git a/tests/expected/function-contract/modifies/expr_replace_pass.rs b/tests/expected/function-contract/modifies/expr_replace_pass.rs
index 779280dd46b4..bb871ba4b8f3 100644
--- a/tests/expected/function-contract/modifies/expr_replace_pass.rs
+++ b/tests/expected/function-contract/modifies/expr_replace_pass.rs
@@ -9,6 +9,13 @@ fn modify(ptr: &mut Box<u32>, prior: u32) {
     *ptr.as_mut() += 1;
 }
 
+#[kani::proof_for_contract(modify)]
+fn modify_harness() {
+    let ptr = &mut Box::new(kani::any());
+    let prior = kani::any();
+    modify(ptr, prior);
+}
+
 #[kani::proof]
 #[kani::stub_verified(modify)]
 fn main() {
diff --git a/tests/expected/function-contract/modifies/field_replace_fail.rs b/tests/expected/function-contract/modifies/field_replace_fail.rs
index 261e4ebd4974..4b8e6e4e6aa0 100644
--- a/tests/expected/function-contract/modifies/field_replace_fail.rs
+++ b/tests/expected/function-contract/modifies/field_replace_fail.rs
@@ -21,3 +21,10 @@ fn main() {
     modify(s);
     kani::assert(i == i_copy + 1, "Increment havocked");
 }
+
+#[kani::proof_for_contract(modify)]
+fn check_modify() {
+    let mut x: u32 = kani::any();
+    let s = S { distraction: 0, target: &mut x };
+    modify(s);
+}
diff --git a/tests/expected/function-contract/modifies/field_replace_pass.rs b/tests/expected/function-contract/modifies/field_replace_pass.rs
index b73af85d9597..0187a5e84e18 100644
--- a/tests/expected/function-contract/modifies/field_replace_pass.rs
+++ b/tests/expected/function-contract/modifies/field_replace_pass.rs
@@ -13,6 +13,15 @@ fn modify(s: &mut S, prior: u32) {
     *s.target += 1;
 }
 
+#[kani::proof_for_contract(modify)]
+fn modify_harness() {
+    let mut target = kani::any();
+    let mut distraction = kani::any();
+    let mut s = S { distraction: &mut distraction, target: &mut target };
+    let prior = kani::any();
+    modify(&mut s, prior);
+}
+
 #[kani::proof]
 #[kani::stub_verified(modify)]
 fn main() {
diff --git a/tests/expected/function-contract/modifies/global_replace_fail.rs b/tests/expected/function-contract/modifies/global_replace_fail.rs
index 25169918b120..51c34ba6731b 100644
--- a/tests/expected/function-contract/modifies/global_replace_fail.rs
+++ b/tests/expected/function-contract/modifies/global_replace_fail.rs
@@ -20,3 +20,10 @@ fn main() {
         kani::assert(compare + 1 == PTR, "not havocked");
     }
 }
+
+#[kani::proof_for_contract(modify)]
+fn check_modify() {
+    unsafe {
+        modify();
+    }
+}
diff --git a/tests/expected/function-contract/modifies/global_replace_pass.rs b/tests/expected/function-contract/modifies/global_replace_pass.rs
index 69d36bd96033..75a02c42718c 100644
--- a/tests/expected/function-contract/modifies/global_replace_pass.rs
+++ b/tests/expected/function-contract/modifies/global_replace_pass.rs
@@ -10,6 +10,14 @@ unsafe fn modify(src: u32) {
     PTR = src;
 }
 
+#[kani::proof_for_contract(modify)]
+fn modify_harness() {
+    let src = kani::any();
+    unsafe {
+        modify(src);
+    }
+}
+
 #[kani::proof]
 #[kani::stub_verified(modify)]
 fn main() {
diff --git a/tests/expected/function-contract/modifies/mistake_condition_return.rs b/tests/expected/function-contract/modifies/mistake_condition_return.rs
index b2d6ad6a8a55..aff9ab2edb16 100644
--- a/tests/expected/function-contract/modifies/mistake_condition_return.rs
+++ b/tests/expected/function-contract/modifies/mistake_condition_return.rs
@@ -37,3 +37,9 @@ fn harness() {
     let mut i = kani::any();
     use_modify(&mut i);
 }
+
+#[kani::proof_for_contract(modify)]
+fn check_modify() {
+    let mut x: u32 = kani::any();
+    modify(&mut x);
+}
diff --git a/tests/expected/function-contract/simple_replace_fail.rs b/tests/expected/function-contract/simple_replace_fail.rs
index dd448d2cdee6..da1a360c2eb8 100644
--- a/tests/expected/function-contract/simple_replace_fail.rs
+++ b/tests/expected/function-contract/simple_replace_fail.rs
@@ -13,3 +13,10 @@ fn div(dividend: u32, divisor: u32) -> u32 {
 fn main() {
     assert!(div(9, 4) == 2, "contract doesn't guarantee equality");
 }
+
+#[kani::proof_for_contract(div)]
+fn check_div() {
+    let dividend: u32 = kani::any();
+    let divisor: u32 = kani::any();
+    div(dividend, divisor);
+}
diff --git a/tests/expected/function-contract/simple_replace_pass.rs b/tests/expected/function-contract/simple_replace_pass.rs
index 7c57cc6a0b7f..71bdfbd2b6eb 100644
--- a/tests/expected/function-contract/simple_replace_pass.rs
+++ b/tests/expected/function-contract/simple_replace_pass.rs
@@ -8,6 +8,13 @@ fn div(dividend: u32, divisor: u32) -> u32 {
     dividend / divisor
 }
 
+#[kani::proof_for_contract(div)]
+fn div_harness() {
+    let dividend: u32 = kani::any();
+    let divisor: u32 = kani::any();
+    div(dividend, divisor);
+}
+
 #[kani::proof]
 #[kani::stub_verified(div)]
 fn main() {
diff --git a/tests/ui/stub-verified-without-contract/stub_verified_no_harness.expected b/tests/ui/stub-verified-without-contract/stub_verified_no_harness.expected
new file mode 100644
index 000000000000..ab14fcf78c5d
--- /dev/null
+++ b/tests/ui/stub-verified-without-contract/stub_verified_no_harness.expected
@@ -0,0 +1,27 @@
+error: Target function in stub_verified, `no_contract`, has no contract.\
+stub_verified_no_harness.rs\
+   |\
+   | #[kani::stub_verified(no_contract)]\
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
+   |
+note: Try adding a contract to this function or use the unsound `stub` attribute instead.\
+stub_verified_no_harness.rs\
+   |\
+   | fn no_contract() -> u32 {\
+   | ^^^^^^^^^^^^^^^^^^^^^^^
+
+error: stub verified target `target_function` does not have a corresponding `#[proof_for_contract]` harness\
+stub_verified_no_harness.rs\
+   |\
+   | #[kani::stub_verified(target_function)]\
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
+   |\
+   = help: verified stubs are meant to be sound abstractions for a function's behavior, so Kani enforces that proofs exist for the stub's contract
+
+error: stub verified target `no_contract` does not have a corresponding `#[proof_for_contract]` harness\
+stub_verified_no_harness.rs\
+   |\
+   | #[kani::stub_verified(no_contract)]\
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
+   |\
+   = help: verified stubs are meant to be sound abstractions for a function's behavior, so Kani enforces that proofs exist for the stub's contract
diff --git a/tests/ui/stub-verified-without-contract/stub_verified_no_harness.rs b/tests/ui/stub-verified-without-contract/stub_verified_no_harness.rs
new file mode 100644
index 000000000000..406944fe98b3
--- /dev/null
+++ b/tests/ui/stub-verified-without-contract/stub_verified_no_harness.rs
@@ -0,0 +1,32 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z function-contracts
+
+// Test that Kani catches stub_verified attributes without corresponding proof_for_contract harnesses
+
+#[kani::requires(x > 0)]
+#[kani::ensures(|result| *result > x)]
+fn target_function(x: u32) -> u32 {
+    x + 1
+}
+
+fn no_contract() -> u32 {
+    42
+}
+
+// This should fail because target_function has no `#[proof_for_contract]` harness
+#[kani::stub_verified(target_function)]
+#[kani::proof]
+fn test_stub_without_harness() {
+    let x = target_function(5);
+    assert!(x > 5);
+}
+
+// This should also fail because no_contract has no contract at all
+#[kani::stub_verified(no_contract)]
+#[kani::proof]
+fn test_stub_without_contract() {
+    let x = no_contract();
+    assert!(x == 42);
+}

From 779d1acf8f917f68f31a37a7f16e5d8d26aed144 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Tue, 12 Aug 2025 18:56:21 -0400
Subject: [PATCH 3/4] fail for stub verified if -Z stubbing isn't provided

---
 kani-compiler/src/kani_middle/attributes.rs   | 21 +++++++++++++++++++
 .../as-assertions/precedence.rs               |  2 +-
 .../gcd_rec_replacement_pass.rs               |  2 +-
 .../function-contract/gcd_replacement_fail.rs |  2 +-
 .../function-contract/gcd_replacement_pass.rs |  2 +-
 .../function-contract/history/stub.rs         |  2 +-
 .../interior-mutability/api/cell_stub.rs      |  2 +-
 .../missing_contract_for_replace.rs           |  2 +-
 .../modifies/check_invalid_modifies.rs        |  2 +-
 .../modifies/check_only_verification.rs       |  2 +-
 .../modifies/expr_replace_fail.rs             |  2 +-
 .../modifies/expr_replace_pass.rs             |  2 +-
 .../modifies/field_replace_fail.rs            |  2 +-
 .../modifies/field_replace_pass.rs            |  2 +-
 .../modifies/global_replace_fail.rs           |  2 +-
 .../modifies/global_replace_pass.rs           |  2 +-
 .../function-contract/modifies/havoc_pass.rs  |  2 +-
 .../modifies/havoc_pass_reordered.rs          |  2 +-
 .../modifies/mistake_condition_return.rs      |  2 +-
 .../modifies/unique_arguments.rs              |  2 +-
 .../modifies/unsafe_rc_fixme.rs               |  2 +-
 .../function-contract/modifies/vec_pass.rs    |  2 +-
 .../multiple_replace_fail.rs                  |  2 +-
 .../multiple_replace_pass.rs                  |  2 +-
 .../function-contract/simple_replace_fail.rs  |  2 +-
 .../function-contract/simple_replace_pass.rs  |  2 +-
 .../promoted_constants_enum.rs                |  2 +-
 .../stub_verified_no_harness.rs               |  2 +-
 .../stub_verified_invalid_path.rs             |  2 +-
 .../stub_verified_missing_flag.expected       |  7 +++++++
 .../stub_verified_missing_flag.rs             | 18 ++++++++++++++++
 31 files changed, 74 insertions(+), 28 deletions(-)
 create mode 100644 tests/ui/stubbing/missing-stubbing-flag/stub_verified_missing_flag.expected
 create mode 100644 tests/ui/stubbing/missing-stubbing-flag/stub_verified_missing_flag.rs

diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 98de8c516fae..96702be45e4d 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -119,6 +119,11 @@ impl KaniAttributeKind {
     pub fn demands_function_contract_use(self) -> bool {
         matches!(self, KaniAttributeKind::ProofForContract)
     }
+
+    /// Is this a stubbing attribute that requires the experimental stubbing feature?
+    pub fn demands_stubbing_use(self) -> bool {
+        matches!(self, KaniAttributeKind::Stub | KaniAttributeKind::StubVerified)
+    }
 }
 
 /// Bundles together common data used when evaluating the attributes of a given
@@ -447,6 +452,22 @@ impl<'tcx> KaniAttributes<'tcx> {
             }
         }
 
+        // If the `stubbing` unstable feature is not enabled then no
+        // function should use any of those APIs.
+        if !enabled_features.iter().any(|feature| feature == "stubbing") {
+            for kind in self.map.keys().copied().filter(|a| a.demands_stubbing_use()) {
+                let msg = format!(
+                    "Using the {} attribute requires activating the unstable `stubbing` feature",
+                    kind.as_ref()
+                );
+                if let Some(attr) = self.map.get(&kind).unwrap().first() {
+                    self.tcx.dcx().span_err(attr.span(), msg);
+                } else {
+                    self.tcx.dcx().err(msg);
+                }
+            }
+        }
+
         if let Some(unstable_attrs) = self.map.get(&KaniAttributeKind::Unstable) {
             for attr in unstable_attrs {
                 let unstable_attr = UnstableAttribute::try_from(*attr).unwrap();
diff --git a/tests/expected/function-contract/as-assertions/precedence.rs b/tests/expected/function-contract/as-assertions/precedence.rs
index 78dc03e42e26..5e8e2fe66145 100644
--- a/tests/expected/function-contract/as-assertions/precedence.rs
+++ b/tests/expected/function-contract/as-assertions/precedence.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 // If a function is the target of a proof_for_contract or stub_verified, we should defer to the contract handling for those modes.
 
diff --git a/tests/expected/function-contract/gcd_rec_replacement_pass.rs b/tests/expected/function-contract/gcd_rec_replacement_pass.rs
index 4cc724a9f75c..9c1bda86625e 100644
--- a/tests/expected/function-contract/gcd_rec_replacement_pass.rs
+++ b/tests/expected/function-contract/gcd_rec_replacement_pass.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 type T = u8;
 
 /// Euclid's algorithm for calculating the GCD of two numbers
diff --git a/tests/expected/function-contract/gcd_replacement_fail.rs b/tests/expected/function-contract/gcd_replacement_fail.rs
index 54d9539e919a..2608d32a2cf9 100644
--- a/tests/expected/function-contract/gcd_replacement_fail.rs
+++ b/tests/expected/function-contract/gcd_replacement_fail.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 type T = u8;
 
 /// Euclid's algorithm for calculating the GCD of two numbers
diff --git a/tests/expected/function-contract/gcd_replacement_pass.rs b/tests/expected/function-contract/gcd_replacement_pass.rs
index abe1369811ff..08bd0fae620c 100644
--- a/tests/expected/function-contract/gcd_replacement_pass.rs
+++ b/tests/expected/function-contract/gcd_replacement_pass.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 type T = u8;
 
 /// Euclid's algorithm for calculating the GCD of two numbers
diff --git a/tests/expected/function-contract/history/stub.rs b/tests/expected/function-contract/history/stub.rs
index 5ede5fed16ee..431766e1a8c9 100644
--- a/tests/expected/function-contract/history/stub.rs
+++ b/tests/expected/function-contract/history/stub.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // This test consumes > 9 GB of memory with 16 object bits. Reducing the number
 // of object bits to 8 to avoid running out of memory.
-// kani-flags: -Zfunction-contracts -Z unstable-options --cbmc-args --object-bits 8
+// kani-flags: -Zfunction-contracts -Zstubbing -Z unstable-options --cbmc-args --object-bits 8
 
 #[kani::ensures(|result| old(*ptr + *ptr) == *ptr)]
 #[kani::requires(*ptr < 100)]
diff --git a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
index 9752bec5d272..fcebc1a152b0 100644
--- a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
+++ b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts --solver minisat
+// kani-flags: -Zfunction-contracts -Zstubbing --solver minisat
 
 /// The objective of this test is to show that the contracts for double can be replaced as a stub within the contracts for quadruple.
 /// This shows that we can generate `kani::any()` for Cell.
diff --git a/tests/expected/function-contract/missing_contract_for_replace.rs b/tests/expected/function-contract/missing_contract_for_replace.rs
index 25abe89bb80e..73e557829b82 100644
--- a/tests/expected/function-contract/missing_contract_for_replace.rs
+++ b/tests/expected/function-contract/missing_contract_for_replace.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 fn no_contract() {}
 
diff --git a/tests/expected/function-contract/modifies/check_invalid_modifies.rs b/tests/expected/function-contract/modifies/check_invalid_modifies.rs
index 6555cd03f697..603d4243af36 100644
--- a/tests/expected/function-contract/modifies/check_invalid_modifies.rs
+++ b/tests/expected/function-contract/modifies/check_invalid_modifies.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 //! Check that Kani reports the correct error message when modifies clause
 //! includes objects of types that do not implement `kani::Arbitrary`.
diff --git a/tests/expected/function-contract/modifies/check_only_verification.rs b/tests/expected/function-contract/modifies/check_only_verification.rs
index c68cdca6ecaf..87129dad4c59 100644
--- a/tests/expected/function-contract/modifies/check_only_verification.rs
+++ b/tests/expected/function-contract/modifies/check_only_verification.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 //! Check that Kani does not report any error when unused modifies clauses
 //! includes objects of types that do not implement `kani::Arbitrary`.
diff --git a/tests/expected/function-contract/modifies/expr_replace_fail.rs b/tests/expected/function-contract/modifies/expr_replace_fail.rs
index 5ac2c0fa87d2..271c40620829 100644
--- a/tests/expected/function-contract/modifies/expr_replace_fail.rs
+++ b/tests/expected/function-contract/modifies/expr_replace_fail.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 // Tests that providing the "modifies" clause havocks the pointer such
 // that the increment can no longer be observed (in the absence of an
diff --git a/tests/expected/function-contract/modifies/expr_replace_pass.rs b/tests/expected/function-contract/modifies/expr_replace_pass.rs
index bb871ba4b8f3..95dd20e34b06 100644
--- a/tests/expected/function-contract/modifies/expr_replace_pass.rs
+++ b/tests/expected/function-contract/modifies/expr_replace_pass.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 #[kani::requires(**ptr < 100)]
 #[kani::modifies(ptr.as_ref())]
diff --git a/tests/expected/function-contract/modifies/field_replace_fail.rs b/tests/expected/function-contract/modifies/field_replace_fail.rs
index 4b8e6e4e6aa0..181fb316fc6a 100644
--- a/tests/expected/function-contract/modifies/field_replace_fail.rs
+++ b/tests/expected/function-contract/modifies/field_replace_fail.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 struct S<'a> {
     distraction: usize,
diff --git a/tests/expected/function-contract/modifies/field_replace_pass.rs b/tests/expected/function-contract/modifies/field_replace_pass.rs
index 0187a5e84e18..737a811db431 100644
--- a/tests/expected/function-contract/modifies/field_replace_pass.rs
+++ b/tests/expected/function-contract/modifies/field_replace_pass.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 struct S<'a> {
     distraction: &'a mut u32,
diff --git a/tests/expected/function-contract/modifies/global_replace_fail.rs b/tests/expected/function-contract/modifies/global_replace_fail.rs
index 51c34ba6731b..0eb165489d99 100644
--- a/tests/expected/function-contract/modifies/global_replace_fail.rs
+++ b/tests/expected/function-contract/modifies/global_replace_fail.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 static mut PTR: u32 = 0;
 
diff --git a/tests/expected/function-contract/modifies/global_replace_pass.rs b/tests/expected/function-contract/modifies/global_replace_pass.rs
index 75a02c42718c..49048ae677a6 100644
--- a/tests/expected/function-contract/modifies/global_replace_pass.rs
+++ b/tests/expected/function-contract/modifies/global_replace_pass.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 static mut PTR: u32 = 0;
 
diff --git a/tests/expected/function-contract/modifies/havoc_pass.rs b/tests/expected/function-contract/modifies/havoc_pass.rs
index ebdd139727d3..83eaf9bbf016 100644
--- a/tests/expected/function-contract/modifies/havoc_pass.rs
+++ b/tests/expected/function-contract/modifies/havoc_pass.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 #[kani::modifies(dst)]
 #[kani::ensures(|result| *dst == src)]
diff --git a/tests/expected/function-contract/modifies/havoc_pass_reordered.rs b/tests/expected/function-contract/modifies/havoc_pass_reordered.rs
index 43581ee677a6..bd99e8b590ae 100644
--- a/tests/expected/function-contract/modifies/havoc_pass_reordered.rs
+++ b/tests/expected/function-contract/modifies/havoc_pass_reordered.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 // These two are reordered in comparison to `havoc_pass` and we expect the test case to pass still
 #[kani::ensures(|result| *dst == src)]
diff --git a/tests/expected/function-contract/modifies/mistake_condition_return.rs b/tests/expected/function-contract/modifies/mistake_condition_return.rs
index aff9ab2edb16..ce9b6bb86460 100644
--- a/tests/expected/function-contract/modifies/mistake_condition_return.rs
+++ b/tests/expected/function-contract/modifies/mistake_condition_return.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 //! Provide an example where users might get confuse on how to constrain
 //! the return value of functions when writing function contracts.
diff --git a/tests/expected/function-contract/modifies/unique_arguments.rs b/tests/expected/function-contract/modifies/unique_arguments.rs
index ea4502bde2ad..e7dbaa526e9b 100644
--- a/tests/expected/function-contract/modifies/unique_arguments.rs
+++ b/tests/expected/function-contract/modifies/unique_arguments.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 #[kani::modifies(a)]
 #[kani::modifies(b)]
diff --git a/tests/expected/function-contract/modifies/unsafe_rc_fixme.rs b/tests/expected/function-contract/modifies/unsafe_rc_fixme.rs
index 81cc65ce9957..39ec9d4e4d3b 100644
--- a/tests/expected/function-contract/modifies/unsafe_rc_fixme.rs
+++ b/tests/expected/function-contract/modifies/unsafe_rc_fixme.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 use std::ops::Deref;
 /// Illustrates the problem from https://github.com/model-checking/kani/issues/2907
diff --git a/tests/expected/function-contract/modifies/vec_pass.rs b/tests/expected/function-contract/modifies/vec_pass.rs
index e3ac28ac3b3d..5472e50f5e61 100644
--- a/tests/expected/function-contract/modifies/vec_pass.rs
+++ b/tests/expected/function-contract/modifies/vec_pass.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 #[kani::requires(v.len() > 0)]
 #[kani::modifies(&v[0])]
diff --git a/tests/expected/function-contract/multiple_replace_fail.rs b/tests/expected/function-contract/multiple_replace_fail.rs
index ecd3c099b2ab..4d557eb1d541 100644
--- a/tests/expected/function-contract/multiple_replace_fail.rs
+++ b/tests/expected/function-contract/multiple_replace_fail.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 #[kani::ensures(|result : &u32| *result == 1)]
 fn one() -> u32 {
diff --git a/tests/expected/function-contract/multiple_replace_pass.rs b/tests/expected/function-contract/multiple_replace_pass.rs
index bd3cb81e136a..1b5dfcb40db1 100644
--- a/tests/expected/function-contract/multiple_replace_pass.rs
+++ b/tests/expected/function-contract/multiple_replace_pass.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 #[kani::ensures(|result : &u32| *result == 1)]
 fn one() -> u32 {
diff --git a/tests/expected/function-contract/simple_replace_fail.rs b/tests/expected/function-contract/simple_replace_fail.rs
index da1a360c2eb8..5882302f8b2c 100644
--- a/tests/expected/function-contract/simple_replace_fail.rs
+++ b/tests/expected/function-contract/simple_replace_fail.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 #[kani::requires(divisor != 0)]
 #[kani::ensures(|result : &u32| *result <= dividend)]
diff --git a/tests/expected/function-contract/simple_replace_pass.rs b/tests/expected/function-contract/simple_replace_pass.rs
index 71bdfbd2b6eb..c32d70ff032f 100644
--- a/tests/expected/function-contract/simple_replace_pass.rs
+++ b/tests/expected/function-contract/simple_replace_pass.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 
 #[kani::requires(divisor != 0)]
 #[kani::ensures(|result : &u32| *result <= dividend)]
diff --git a/tests/kani/FunctionContracts/promoted_constants_enum.rs b/tests/kani/FunctionContracts/promoted_constants_enum.rs
index 12878eee8044..597ec084ce76 100644
--- a/tests/kani/FunctionContracts/promoted_constants_enum.rs
+++ b/tests/kani/FunctionContracts/promoted_constants_enum.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zfunction-contracts
+// kani-flags: -Zfunction-contracts -Zstubbing
 //! This test checks that contracts does not havoc
 //! [promoted constants](https://github.com/rust-lang/const-eval/blob/master/promotion.md)
 //! that represents an enum variant.
diff --git a/tests/ui/stub-verified-without-contract/stub_verified_no_harness.rs b/tests/ui/stub-verified-without-contract/stub_verified_no_harness.rs
index 406944fe98b3..58934942c70d 100644
--- a/tests/ui/stub-verified-without-contract/stub_verified_no_harness.rs
+++ b/tests/ui/stub-verified-without-contract/stub_verified_no_harness.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: -Z function-contracts
+// kani-flags: -Z function-contracts -Z stubbing
 
 // Test that Kani catches stub_verified attributes without corresponding proof_for_contract harnesses
 
diff --git a/tests/ui/stubbing/invalid-path/stub_verified_invalid_path.rs b/tests/ui/stubbing/invalid-path/stub_verified_invalid_path.rs
index 4184a72beda4..153626ed05f0 100644
--- a/tests/ui/stubbing/invalid-path/stub_verified_invalid_path.rs
+++ b/tests/ui/stubbing/invalid-path/stub_verified_invalid_path.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: -Z function-contracts
+// kani-flags: -Z function-contracts -Z stubbing
 
 // Test that Kani catches invalid paths in stub_verified attributes
 
diff --git a/tests/ui/stubbing/missing-stubbing-flag/stub_verified_missing_flag.expected b/tests/ui/stubbing/missing-stubbing-flag/stub_verified_missing_flag.expected
new file mode 100644
index 000000000000..131f132b935d
--- /dev/null
+++ b/tests/ui/stubbing/missing-stubbing-flag/stub_verified_missing_flag.expected
@@ -0,0 +1,7 @@
+error: Using the stub_verified attribute requires activating the unstable `stubbing` feature\
+stub_verified_missing_flag\
+|\
+| #[kani::stub_verified(some_function)]\
+| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: aborting due to 1 previous error
\ No newline at end of file
diff --git a/tests/ui/stubbing/missing-stubbing-flag/stub_verified_missing_flag.rs b/tests/ui/stubbing/missing-stubbing-flag/stub_verified_missing_flag.rs
new file mode 100644
index 000000000000..1153b04df806
--- /dev/null
+++ b/tests/ui/stubbing/missing-stubbing-flag/stub_verified_missing_flag.rs
@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z function-contracts
+
+// Test that Kani complains when stub_verified is used without the stubbing feature enabled
+
+#[kani::requires(true)]
+fn some_function() {}
+
+#[kani::proof_for_contract(some_function)]
+fn harness() {
+    some_function();
+}
+
+#[kani::stub_verified(some_function)]
+#[kani::proof]
+fn test_missing_stubbing_flag() {}

From 0c0a604ecb2279c096bfc0f074b6ace60b6da6c0 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Tue, 12 Aug 2025 19:24:45 -0400
Subject: [PATCH 4/4] remove redundant stub checking

---
 kani-driver/src/harness_runner.rs             | 29 -------------------
 .../expected/function-stubbing-error/expected |  2 --
 .../expected/function-stubbing-error/main.rs  | 20 -------------
 .../stub_missing_flag.expected                |  7 +++++
 .../stub_missing_flag.rs                      | 13 +++++++++
 5 files changed, 20 insertions(+), 51 deletions(-)
 delete mode 100644 tests/expected/function-stubbing-error/expected
 delete mode 100644 tests/expected/function-stubbing-error/main.rs
 create mode 100644 tests/ui/stubbing/missing-stubbing-flag/stub_missing_flag.expected
 create mode 100644 tests/ui/stubbing/missing-stubbing-flag/stub_missing_flag.rs

diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index 4a7f22b477b9..708a4064cd72 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/kani-driver/src/harness_runner.rs
@@ -55,8 +55,6 @@ impl<'pr> HarnessRunner<'_, 'pr> {
         &self,
         harnesses: &'pr [&HarnessMetadata],
     ) -> Result<Vec<HarnessResult<'pr>>> {
-        self.check_stubbing(harnesses)?;
-
         let sorted_harnesses = crate::metadata::sort_harnesses_by_loc(harnesses);
         let pool = {
             let mut builder = rayon::ThreadPoolBuilder::new();
@@ -114,33 +112,6 @@ impl<'pr> HarnessRunner<'_, 'pr> {
             }
         }
     }
-
-    /// Return an error if the user is trying to verify a harness with stubs without enabling the
-    /// experimental feature.
-    fn check_stubbing(&self, harnesses: &[&HarnessMetadata]) -> Result<()> {
-        if !self.sess.args.is_stubbing_enabled() {
-            let with_stubs: Vec<_> = harnesses
-                .iter()
-                .filter_map(|harness| {
-                    (!harness.attributes.stubs.is_empty()).then_some(harness.pretty_name.as_str())
-                })
-                .collect();
-            match with_stubs.as_slice() {
-                [] => { /* do nothing */ }
-                [harness] => bail!(
-                    "Use of unstable feature 'stubbing' in harness `{}`.\n\
-                    To enable stubbing, pass option `-Z stubbing`",
-                    harness
-                ),
-                harnesses => bail!(
-                    "Use of unstable feature 'stubbing' in harnesses `{}`.\n\
-                    To enable stubbing, pass option `-Z stubbing`",
-                    harnesses.join("`, `")
-                ),
-            }
-        }
-        Ok(())
-    }
 }
 
 impl KaniSession {
diff --git a/tests/expected/function-stubbing-error/expected b/tests/expected/function-stubbing-error/expected
deleted file mode 100644
index 6adf1ad27631..000000000000
--- a/tests/expected/function-stubbing-error/expected
+++ /dev/null
@@ -1,2 +0,0 @@
-error: Use of unstable feature 'stubbing' in harness `main`.
-To enable stubbing, pass option `-Z stubbing`
diff --git a/tests/expected/function-stubbing-error/main.rs b/tests/expected/function-stubbing-error/main.rs
deleted file mode 100644
index 4b206bfaee44..000000000000
--- a/tests/expected/function-stubbing-error/main.rs
+++ /dev/null
@@ -1,20 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-//
-// kani-flags: --harness main
-//
-//! This tests whether we abort if a stub is specified for a harness but stubbing is not enabled.
-
-fn foo() -> u32 {
-    0
-}
-
-fn bar() -> u32 {
-    42
-}
-
-#[kani::proof]
-#[kani::stub(foo, bar)]
-fn main() {
-    assert_eq!(foo(), 42);
-}
diff --git a/tests/ui/stubbing/missing-stubbing-flag/stub_missing_flag.expected b/tests/ui/stubbing/missing-stubbing-flag/stub_missing_flag.expected
new file mode 100644
index 000000000000..29982be01637
--- /dev/null
+++ b/tests/ui/stubbing/missing-stubbing-flag/stub_missing_flag.expected
@@ -0,0 +1,7 @@
+error: Using the stub attribute requires activating the unstable `stubbing` feature\
+stub_missing_flag\
+|\
+| #[kani::stub(some_function, replacement_function)]\
+| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: aborting due to 1 previous error
\ No newline at end of file
diff --git a/tests/ui/stubbing/missing-stubbing-flag/stub_missing_flag.rs b/tests/ui/stubbing/missing-stubbing-flag/stub_missing_flag.rs
new file mode 100644
index 000000000000..5b12816c06a7
--- /dev/null
+++ b/tests/ui/stubbing/missing-stubbing-flag/stub_missing_flag.rs
@@ -0,0 +1,13 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z function-contracts
+
+// Test that Kani complains when stub is used without the stubbing feature enabled
+
+fn some_function() {}
+fn replacement_function() {}
+
+#[kani::stub(some_function, replacement_function)]
+#[kani::proof]
+fn test_missing_stubbing_flag() {}