-
Notifications
You must be signed in to change notification settings - Fork 109
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Incorrect verification results for function/closure dyn traits #240
Comments
This is blocking #220 |
A similar example (without an explicit fn takes_dyn_fun(fun: &dyn Fn() -> u32) {
let x = fun();
}
pub fn unit_to_u32() -> u32 {
assert!(false);
0
}
fn main() {
takes_dyn_fun(&unit_to_u32)
} Should fail from this explicit assert false, but:
|
FnOnce
dyn trait closure
This does fail as expected with
But, this means we are generating some bad function dereference, so still a bug. |
Weird thing to maybe investigate separately: The following hangs // Create a nested boxed once-callable closure
let f: Box<Box<dyn FnOnce(i32)>> = Box::new(Box::new(|x| assert!(x == 1)));
f(1);
// Create a pointer to a closure
let g = |y| assert!(y == 2);
let p: &dyn Fn(i32) = &g;
p(2);
// Additional level of pointer nesting
let q: &dyn Fn(i32) = &p;
q(2); Even though the first chunk of code should be independent from the 2nd, commenting it out gets rid of the hang. |
The following fails to verify:
In the generated CBMC-C code, in some places we pass the closure argument as a tuple, but in others we expect the flattened int.
The text was updated successfully, but these errors were encountered: