Skip to content

Commit ea0f54a

Browse files
jsalzbergeduJacob Salzbergjaisnan
authored
Test that boxed fn parameters are implemented. (rust-lang#3361)
This regression test ensures that issue rust-lang#2874 does not reoccur, which was last encountered in commit 9190831. Resolves rust-lang#2874 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: Jacob Salzberg <[email protected]> Co-authored-by: Jaisurya Nanduri <[email protected]>
1 parent 7ad4d1c commit ea0f54a

File tree

1 file changed

+22
-0
lines changed

1 file changed

+22
-0
lines changed

tests/kani/Closure/boxed_closure.rs

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
// compile-flags: -Zmir-opt-level=2
4+
5+
// The main function of this test moves an integer into a closure,
6+
// boxes the value, then passes the closure to a function that calls it.
7+
// This test covers the issue
8+
// https://github.com/model-checking/kani/issues/2874 .
9+
10+
fn call_boxed_closure(f: Box<dyn Fn() -> ()>) -> () {
11+
f()
12+
}
13+
14+
// #[kani::proof]
15+
fn main() {
16+
let x = 1;
17+
let closure = move || {
18+
let _ = x;
19+
()
20+
};
21+
call_boxed_closure(Box::new(closure));
22+
}

0 commit comments

Comments
 (0)