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..e663b0178c09 --- /dev/null +++ b/tests/expected/issue-2239/issue_2239.rs @@ -0,0 +1,12 @@ +#![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-2732/issue_2732.expected b/tests/expected/issue-2732/issue_2732.expected new file mode 100644 index 000000000000..ad4c07cd69ff --- /dev/null +++ b/tests/expected/issue-2732/issue_2732.expected @@ -0,0 +1,5 @@ +test.assertion\ +- Status: FAILURE\ +- Description: "index out of bounds: the length is less than or equal to the given index" + +VERIFICATION:- FAILED \ No newline at end of file diff --git a/tests/expected/issue-2732/issue_2732.rs b/tests/expected/issue-2732/issue_2732.rs new file mode 100644 index 000000000000..b2ea4c25795e --- /dev/null +++ b/tests/expected/issue-2732/issue_2732.rs @@ -0,0 +1,11 @@ +const C: [u32; 5] = [0; 5]; + +#[allow(unconditional_panic)] +fn test() -> u32 { + C[10] +} + +#[kani::proof] +fn main() { + test(); +}