Allow multiple annotations, but check for duplicate targets.

kani-compiler/src/kani_middle/attributes.rs

@@ -371,7 +371,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                     attrs.iter().for_each(|attr| self.check_proof_attribute(kind, attr))
                 }
                 KaniAttributeKind::StubVerified => {
-                    expect_single(self.tcx, kind, &attrs);
+                    self.check_stub_verified();
                 }
                 KaniAttributeKind::FnMarker
                 | KaniAttributeKind::CheckedWith
@@ -566,15 +566,29 @@ impl<'tcx> KaniAttributes<'tcx> {
         }
     }
 
-    fn handle_stub_verified(&self, harness: &mut HarnessAttributes) {
+    fn check_stub_verified(&self) {
         let dcx = self.tcx.dcx();
+        let mut seen = HashSet::new();
         for (name, def_id, span) in self.interpret_stub_verified_attribute() {
+            if seen.contains(&name) {
+                dcx.struct_span_warn(
+                    span,
+                    format!("Multiple occurrences of `stub_verified({})`.", name),
+                )
+                .with_span_note(
+                    self.tcx.def_span(def_id),
+                    format!("Use a single `stub_verified({})` annotation.", name),
+                )
+                .emit();
+            } else {
+                seen.insert(name);
+            }
             if KaniAttributes::for_item(self.tcx, def_id).contract_attributes().is_none() {
                 dcx.struct_span_err(
                     span,
                     format!(
-                        "Failed to generate verified stub: Function `{}` has no contract.",
-                        self.item_name(),
+                        "Target function in `stub_verified({})` has no contract.",
+                        name,
                     ),
                 )
                     .with_span_note(
@@ -587,10 +601,21 @@ impl<'tcx> KaniAttributes<'tcx> {
                     .emit();
                 return;
             }
+        }
+    }
+
+    /// Adds the verified stub names to the `harness.verfied_stubs`.
+    ///
+    /// This method must be called after `check_stub_verified`, to ensure that
+    /// the target names are known and have contracts, and there are no
+    /// duplicate target names.
+    fn handle_stub_verified(&self, harness: &mut HarnessAttributes) {
+        for (name, _, _) in self.interpret_stub_verified_attribute() {
             harness.verified_stubs.push(name.to_string())
         }
     }
 
+
     fn item_name(&self) -> Symbol {
         self.tcx.item_name(self.item)
     }

tests/expected/function-contract/missing_contract_for_replace.expected

@@ -1,4 +1,4 @@
-error: Failed to generate verified stub: Function `harness` has no contract.
+error: Target function in `stub_verified(no_contract)` has no contract.
   |
 8 | #[kani::stub_verified(no_contract)]
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

tests/expected/function-contract/multiple_replace_fail.expected

@@ -0,0 +1 @@
+warning: Multiple occurrences of `stub_verified(one)`.

tests/expected/function-contract/multiple_replace_fail.rs

@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+#[kani::ensures(|result : &u32| *result == 1)]
+fn one() -> u32 {
+    1
+}
+
+#[kani::proof_for_contract(one)]
+fn check_one() {
+    let _ = one();
+}
+
+#[kani::ensures(|result : &u32| *result == 1)]
+fn one_too() -> u32 {
+    1
+}
+
+#[kani::proof_for_contract(one_too)]
+fn check_one_too() {
+    let _ = one_too();
+}
+
+#[kani::proof]
+#[kani::stub_verified(one)]
+#[kani::stub_verified(one)]
+#[kani::stub_verified(one_too)]
+fn main() {
+    assert_eq!(one(), one_too());
+}

tests/expected/function-contract/multiple_replace_pass.expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/multiple_replace_pass.rs

@@ -0,0 +1,30 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+#[kani::ensures(|result : &u32| *result == 1)]
+fn one() -> u32 {
+    1
+}
+
+#[kani::proof_for_contract(one)]
+fn check_one() {
+    let _ = one();
+}
+
+#[kani::ensures(|result : &u32| *result == 1)]
+fn one_too() -> u32 {
+    1
+}
+
+#[kani::proof_for_contract(one_too)]
+fn check_one_too() {
+    let _ = one_too();
+}
+
+#[kani::proof]
+#[kani::stub_verified(one)]
+#[kani::stub_verified(one_too)]
+fn main() {
+    assert_eq!(one(), one_too());
+}