diff --git a/tests/expected/arith_checks/fixme_check_arith_failures.rs b/tests/expected/arith_checks/check_arith_failures.rs similarity index 100% rename from tests/expected/arith_checks/fixme_check_arith_failures.rs rename to tests/expected/arith_checks/check_arith_failures.rs diff --git a/tests/expected/intrinsics/ctpop_ice_fixme/expected b/tests/expected/intrinsics/ctpop_ice_fixme/expected new file mode 100644 index 000000000000..dca276fb90c0 --- /dev/null +++ b/tests/expected/intrinsics/ctpop_ice_fixme/expected @@ -0,0 +1 @@ +Kani unexpectedly panicked during compilation. diff --git a/tests/expected/intrinsics/ctpop_ice_fixme/fixme_ctpop_ice.rs b/tests/expected/intrinsics/ctpop_ice_fixme/fixme_ctpop_ice.rs new file mode 100644 index 000000000000..ea11400e8161 --- /dev/null +++ b/tests/expected/intrinsics/ctpop_ice_fixme/fixme_ctpop_ice.rs @@ -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 == ()); +} diff --git a/tests/expected/intrinsics/sub_with_workflow_ice_fixme/arithmetic_zst_fixme.rs b/tests/expected/intrinsics/sub_with_workflow_ice_fixme/arithmetic_zst_fixme.rs new file mode 100644 index 000000000000..a8f8575e8e38 --- /dev/null +++ b/tests/expected/intrinsics/sub_with_workflow_ice_fixme/arithmetic_zst_fixme.rs @@ -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); +} diff --git a/tests/expected/intrinsics/sub_with_workflow_ice_fixme/expected b/tests/expected/intrinsics/sub_with_workflow_ice_fixme/expected new file mode 100644 index 000000000000..dca276fb90c0 --- /dev/null +++ b/tests/expected/intrinsics/sub_with_workflow_ice_fixme/expected @@ -0,0 +1 @@ +Kani unexpectedly panicked during compilation.