Validate usage of inline attributes #2809
Comments
|
I don't believe this is backwards incompatible, renominating. |
|
Also I don't know what this means. |
|
I can't tell where the comment originally came from, but I'm assuming it means checking that |
|
just a bug, removing milestone/nomination. |
|
Consensus is that this means a lint pass detecting #[inline] being applied |
|
Visiting for triage, nontrivial amount of work so leaving as properly classified for now. |
|
Amusingly, today this says No more always, but it's still there. |
|
#22490 validates well-formedness of the inline attribute, but it is still unknown whether there’s any ways to misuse #[inline] attribute in a way which would be invalid (e.g. not on a function). If the comment in original report happens to have referred to validation of attribute well-formedness, this issue can then be closed. Do not forget to remove the FIXME comment too. |
Implement round_ties_even For tests, I just copied over the standard library's tests for this feature. It looks like the library uses an approximate equality check for most/all float tests, and I've replaced that check with our float equality check pattern.
…ust-lang#2809) This adds support for verifying the contracts of recursive functions inductively. The idea is quite simple. We use a global variable to track whether we're reentering a function and depending on that value we either continue with checking the contract or assume the hypothesis by using its replacement. The precise mechanism that I implemented is explained in the documentation [here](https://github.com/JustusAdam/kani/blob/a31176c79098205ca0b2c2b199cdf06653754551/library/kani_macros/src/sysroot/contracts.rs#L126) Resolves rust-lang#2724 **Open Question:** to facilitate induction the return type of the function must implement `kani::Arbitrary`. Since we can't discriminate between recursive and non-recursive functions in the proc-macro this means that this applies to all functions with contracts, not just recursive ones. This may be an unacceptable restriction. We could consider making inductive verification explicit with an annotation like `#[kani::inductive]` or conversely make inductive the default and let users opt-out with `#[kani::no_inductive]`. This is now tracked in rust-lang#2823 I had to remove the names of the functions in which the messages occur in the test cases, since they are now generated, hard to read names By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Zyad Hassan <[email protected]>
syntax::attr::find_inline_attrhas a FIXME saying "validate the usage of#[inline]and#[inline(always)]".The text was updated successfully, but these errors were encountered: