Merge branch 'issue-3022-test' into tests-for-issues

model-checking · Sep 3, 2024 · 29a009c · 29a009c
2 parents 2db3d3b + 8f4c07d
commit 29a009c
Show file tree

Hide file tree

Showing 2 changed files with 29 additions and 0 deletions.
diff --git a/tests/expected/issue-3022/issue_3022.expected b/tests/expected/issue-3022/issue_3022.expected
@@ -0,0 +1,5 @@
+main.assertion\
+- Status: SUCCESS\
+- Description: "assertion failed: inner == func2.inner"
+
+VERIFICATION:- SUCCESSFUL
diff --git a/tests/expected/issue-3022/issue_3022.rs b/tests/expected/issue-3022/issue_3022.rs
@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+type BuiltIn = for<'a> fn(&str);
+
+struct Function {
+ inner: BuiltIn,
+}
+
+impl Function {
+ fn new(subr: BuiltIn) -> Self {
+ Self { inner: subr }
+ }
+}
+
+fn dummy(_: &str) {}
+
+#[kani::proof]
+fn main() {
+ let func1 = Function::new(dummy);
+ let func2 = Function::new(dummy);
+ let inner: fn(&'static _) -> _ = func1.inner;
+ assert!(inner == func2.inner);
+}