diff --git a/tests/expected/issue-2239/issue_2239.expected b/tests/expected/issue-2239/issue_2239.expected new file mode 100644 index 000000000000..8bdab0df1862 --- /dev/null +++ b/tests/expected/issue-2239/issue_2239.expected @@ -0,0 +1,5 @@ +test_trivial_bounds.unreachable.1\ +- Status: FAILURE\ +- Description: "unreachable code" + +VERIFICATION:- FAILED \ No newline at end of file diff --git a/tests/expected/issue-2239/issue_2239.rs b/tests/expected/issue-2239/issue_2239.rs new file mode 100644 index 000000000000..36c41dec604d --- /dev/null +++ b/tests/expected/issue-2239/issue_2239.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#![feature(trivial_bounds)] +#![allow(unused, trivial_bounds)] + +#[kani::proof] +fn test_trivial_bounds() +where + i32: Iterator, +{ + for _ in 2i32 {} +} + +fn main() {} diff --git a/tests/expected/issue-3022/issue_3022.expected b/tests/expected/issue-3022/issue_3022.expected new file mode 100644 index 000000000000..9600182a5209 --- /dev/null +++ b/tests/expected/issue-3022/issue_3022.expected @@ -0,0 +1,5 @@ +main.assertion\ +- Status: SUCCESS\ +- Description: "assertion failed: inner == func2.inner" + +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/issue-3022/issue_3022.rs b/tests/expected/issue-3022/issue_3022.rs new file mode 100644 index 000000000000..6ef6f944395f --- /dev/null +++ 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); +}