Move checks earlier in the process.

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 => {
-                    // Actual validation happens when the annotation are handled
+                    self.check_stub_verified();
                 }
                 KaniAttributeKind::FnMarker
                 | KaniAttributeKind::CheckedWith
@@ -566,12 +566,12 @@ 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_err(
+                dcx.struct_span_warn(
                     span,
                     format!("Multiple occurrences of `stub_verified({})`.", name),
                 )
@@ -587,8 +587,8 @@ impl<'tcx> KaniAttributes<'tcx> {
                 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(
@@ -601,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

@@ -1 +1 @@
-error: Multiple occurrences of the same `stub_verified` target: 'one'
+warning: Multiple occurrences of `stub_verified(one)`.

tests/expected/function-contract/multiple_replace_pass.rs

@@ -26,5 +26,5 @@ fn check_one_too() {
 #[kani::stub_verified(one)]
 #[kani::stub_verified(one_too)]
 fn main() {
-    assert_eq!(one() == one_too());
+    assert_eq!(one(), one_too());
 }