You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
catamorphism opened this issue
Jun 14, 2012
· 1 comment
Labels
I-slowIssue: Problems and improvements with respect to performance of generated code.T-rustdocRelevant to the rustdoc team, which will review and decide on the PR/issue.
This change now separates the front facing "result" name and the
internal facing "result_kani_internal" ident where the user can specify
with the keyword "result" but then the system replaces this with the
internal representation.
If the user chooses to use a different variable name than result, this
now supports the syntax of
`#[kani::ensures(|result_var| expr)]`
where result_var can be any arbitrary name.
For example, the following test now works:
```
#[kani::ensures(|banana : &u32| *banana == a.wrapping_add(b))]
fn simple_addition(a: u32, b: u32) -> u32 {
return a.wrapping_add(b);
}
```
In addition, the string "result_kani_internal" is now a global constant
and can be updated in a single place if needed.
Resolvesrust-lang#2597 since the user can specify the variable name they want
within the ensures binding
An important change is that the result is now a pass by reference
instead, so as in the example an `&u32` instead of `u32`
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: Matias Scharager <[email protected]>
flip1995
pushed a commit
to flip1995/rust
that referenced
this issue
Apr 3, 2025
…4438)
rust-lang#2597 appears to be already resolved, so the applicability of `op_ref`
can be set to `MachineApplicable`.
closerust-lang#2597
changelog: [`op_ref`]: set the applicability to `MachineApplicable`
I-slowIssue: Problems and improvements with respect to performance of generated code.T-rustdocRelevant to the rustdoc team, which will review and decide on the PR/issue.
as per a FIXME. (I tried making this change, but it didn't combine because hash maps aren't sendable.)
The text was updated successfully, but these errors were encountered: