Skip to content

Commit

Permalink
Add fixme tests for issue rust-lang#2121 (rust-lang#2122)
Browse files Browse the repository at this point in the history
Add fixme tests for rust-lang#2121 to the expected suite since the test should fail, but not crash.
  • Loading branch information
celinval authored Jan 14, 2023
1 parent ce697e6 commit 9d50e3f
Show file tree
Hide file tree
Showing 5 changed files with 29 additions and 0 deletions.
1 change: 1 addition & 0 deletions tests/expected/intrinsics/ctpop_ice_fixme/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Kani unexpectedly panicked during compilation.
14 changes: 14 additions & 0 deletions tests/expected/intrinsics/ctpop_ice_fixme/fixme_ctpop_ice.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//! Check that we correctly handle type mistmatch when the argument is a ZST type.
//! The compiler crashes today: https://github.com/model-checking/kani/issues/2121
#![feature(core_intrinsics)]
use std::intrinsics::ctpop;

// These shouldn't compile.
#[kani::proof]
pub fn check_zst_ctpop() {
let n = ctpop(());
assert!(n == ());
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//! Check that arithmetic operations with overflow compilation fails.
//! The compiler crashes today: https://github.com/model-checking/kani/issues/2121
#![feature(core_intrinsics)]
use std::intrinsics::sub_with_overflow;

#[kani::proof]
pub fn check_zst_sub_with_overflow() {
let n = sub_with_overflow((), ());
assert!(!n.1);
}
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Kani unexpectedly panicked during compilation.

0 comments on commit 9d50e3f

Please sign in to comment.