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
msullivan opened this issue
Aug 16, 2012
· 1 comment
Labels
A-runtimeArea: std's runtime and "pre-main" init for handling backtraces, unwinds, stack overflowsI-crashIssue: The compiler crashes (SIGSEGV, SIGABRT, etc). Use I-ICE instead when the compiler panics.
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]>
A-runtimeArea: std's runtime and "pre-main" init for handling backtraces, unwinds, stack overflowsI-crashIssue: The compiler crashes (SIGSEGV, SIGABRT, etc). Use I-ICE instead when the compiler panics.
will dump core.
The text was updated successfully, but these errors were encountered: