Allow multiple annotations, but check for duplicate targets. #3808
Conversation
|
Is this a duplicate of #3805? |
| if seen.contains(&name) { | ||
| dcx.struct_span_err( | ||
| 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 { |
There was a problem hiding this comment.
Can this be a warning instead? They will be redundant, but they can be safely ignored.
There was a problem hiding this comment.
Changed it to a warning, and moved the checks earlier in the process.
| @@ -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); | |||
| // Actual validation happens when the annotation are handled | |||
There was a problem hiding this comment.
Ideally, this should be similar to parse_stubs so we can emit as many errors as possible, and sooner rather than later. Can you please add a test to see if that is the case today. Something like:
#[kani::proof]
#[kani::stub_verified(dummy)]
fn stub_does_not_exist() { }
#[kani::proof]
#[kani::stub_verified(dummy, dummy2)]
fn stub_invalid_args() { }That said, for this PR, I think a TODO comment should suffice, since you are not introducing this limitation. Thanks!
There was a problem hiding this comment.
We already have tests for these cases in missing_contracts_for_check.rs and missing_contracts_for_replace.rs
Resolves #3804.
Enables multiple
stub_verified(TARGET)annotations on a harness, but still detect and report duplicate targets.Adds positive and negative tests.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.