fix: Allow multiple stub_verifieds on a single harness

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.parse_stub_verifieds();
                 }
                 KaniAttributeKind::FnMarker
                 | KaniAttributeKind::CheckedWith
@@ -519,7 +519,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                 }
                 KaniAttributeKind::Proof => { /* no-op */ }
                 KaniAttributeKind::ProofForContract => self.handle_proof_for_contract(&mut harness),
-                KaniAttributeKind::StubVerified => self.handle_stub_verified(&mut harness),
+                KaniAttributeKind::StubVerified => harness.verified_stubs.extend_from_slice(&self.parse_stub_verifieds()),
                 KaniAttributeKind::Unstable => {
                     // Internal attribute which shouldn't exist here.
                     unreachable!()
@@ -566,8 +566,9 @@ impl<'tcx> KaniAttributes<'tcx> {
         }
     }
 
-    fn handle_stub_verified(&self, harness: &mut HarnessAttributes) {
+    fn parse_stub_verifieds(&self) -> Vec<String> {
         let dcx = self.tcx.dcx();
+        let mut verified_stubs = Vec::new();
         for (name, def_id, span) in self.interpret_stub_verified_attribute() {
             if KaniAttributes::for_item(self.tcx, def_id).contract_attributes().is_none() {
                 dcx.struct_span_err(
@@ -585,10 +586,11 @@ impl<'tcx> KaniAttributes<'tcx> {
                         ),
                     )
                     .emit();
-                return;
+                return verified_stubs;
             }
-            harness.verified_stubs.push(name.to_string())
+            verified_stubs.push(name.to_string());
         }
+        verified_stubs
     }
 
     fn item_name(&self) -> Symbol {

tests/expected/function-contract/simple_replace_multiple_pass.expected

@@ -0,0 +1,13 @@
+.assertion\
+- Status: SUCCESS\
+- Description: "divisor != 0"
+
+.assertion\
+- Status: SUCCESS\
+- Description: "a >= b"
+
+main.assertion\
+- Status: SUCCESS\
+- Description: ""contract guarantees smallness""
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/simple_replace_multiple_pass.rs

@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+#[kani::requires(divisor != 0)]
+#[kani::ensures(|result : &u32| *result <= dividend)]
+fn div(dividend: u32, divisor: u32) -> u32 {
+    dividend / divisor
+}
+
+#[kani::requires(a >= b)]
+#[kani::ensures(|result : &u32| *result <= a)]
+fn sub(a: u32, b: u32) -> u32 {
+    a - b
+}
+
+#[kani::proof]
+#[kani::stub_verified(div)]
+#[kani::stub_verified(sub)]
+fn main() {
+    assert!(div(sub(9, 1), 1) != 10, "contract guarantees smallness");
+}