Skip to content

Commit

Permalink
Add tests for fixed issues. (#3484)
Browse files Browse the repository at this point in the history
#2239 and #3022 are resolved in Kani v0.5.4. Add tests for them.

Resolves #2239

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
carolynzech authored Sep 3, 2024
1 parent eb4d5a6 commit 6cf4ea4
Show file tree
Hide file tree
Showing 4 changed files with 49 additions and 0 deletions.
5 changes: 5 additions & 0 deletions tests/expected/issue-2239/issue_2239.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
test_trivial_bounds.unreachable.1\
- Status: FAILURE\
- Description: "unreachable code"

VERIFICATION:- FAILED
15 changes: 15 additions & 0 deletions tests/expected/issue-2239/issue_2239.rs
Original file line number Diff line number Diff line change
@@ -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() {}
5 changes: 5 additions & 0 deletions tests/expected/issue-3022/issue_3022.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
main.assertion\
- Status: SUCCESS\
- Description: "assertion failed: inner == func2.inner"

VERIFICATION:- SUCCESSFUL
24 changes: 24 additions & 0 deletions tests/expected/issue-3022/issue_3022.rs
Original file line number Diff line number Diff line change
@@ -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);
}

0 comments on commit 6cf4ea4

Please sign in to comment.