Skip to content

Commit 9d50e3f

Browse files
authored
Add fixme tests for issue rust-lang#2121 (rust-lang#2122)
Add fixme tests for rust-lang#2121 to the expected suite since the test should fail, but not crash.
1 parent ce697e6 commit 9d50e3f

File tree

5 files changed

+29
-0
lines changed

5 files changed

+29
-0
lines changed
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Kani unexpectedly panicked during compilation.
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
//! Check that we correctly handle type mistmatch when the argument is a ZST type.
4+
//! The compiler crashes today: https://github.com/model-checking/kani/issues/2121
5+
6+
#![feature(core_intrinsics)]
7+
use std::intrinsics::ctpop;
8+
9+
// These shouldn't compile.
10+
#[kani::proof]
11+
pub fn check_zst_ctpop() {
12+
let n = ctpop(());
13+
assert!(n == ());
14+
}
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
//! Check that arithmetic operations with overflow compilation fails.
4+
//! The compiler crashes today: https://github.com/model-checking/kani/issues/2121
5+
6+
#![feature(core_intrinsics)]
7+
use std::intrinsics::sub_with_overflow;
8+
9+
#[kani::proof]
10+
pub fn check_zst_sub_with_overflow() {
11+
let n = sub_with_overflow((), ());
12+
assert!(!n.1);
13+
}
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Kani unexpectedly panicked during compilation.

0 commit comments

Comments
 (0)