From ea0f54a6ddf9e1d449c6c96662e02bc339c6bb0c Mon Sep 17 00:00:00 2001
From: Jacob Salzberg <jsalzbergedu@yahoo.com>
Date: Tue, 23 Jul 2024 14:25:24 -0400
Subject: [PATCH] Test that boxed fn parameters are implemented. (#3361)

This regression test ensures that issue #2874 does not reoccur, which
was last encountered in commit 9190831.

Resolves #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 <salzber@amazon.com>
Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com>
---
 tests/kani/Closure/boxed_closure.rs | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 tests/kani/Closure/boxed_closure.rs

diff --git a/tests/kani/Closure/boxed_closure.rs b/tests/kani/Closure/boxed_closure.rs
new file mode 100644
index 000000000000..4071978d28b1
--- /dev/null
+++ b/tests/kani/Closure/boxed_closure.rs
@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// compile-flags: -Zmir-opt-level=2
+
+// The main function of this test moves an integer into a closure,
+// boxes the value, then passes the closure to a function that calls it.
+// This test covers the issue
+// https://github.com/model-checking/kani/issues/2874 .
+
+fn call_boxed_closure(f: Box<dyn Fn() -> ()>) -> () {
+    f()
+}
+
+// #[kani::proof]
+fn main() {
+    let x = 1;
+    let closure = move || {
+        let _ = x;
+        ()
+    };
+    call_boxed_closure(Box::new(closure));
+}