diff --git a/tests/kani/SaturatingIntrinsics/main.rs b/tests/kani/Intrinsics/Saturating/main.rs similarity index 91% rename from tests/kani/SaturatingIntrinsics/main.rs rename to tests/kani/Intrinsics/Saturating/main.rs index 08326922a990..413db77bac22 100644 --- a/tests/kani/SaturatingIntrinsics/main.rs +++ b/tests/kani/Intrinsics/Saturating/main.rs @@ -1,5 +1,9 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that `saturating_add` and `saturating_sub` are supported and return the +// expected results. + #![feature(core_intrinsics)] use std::intrinsics; @@ -54,10 +58,12 @@ fn main() { test_saturating_intrinsics!(u16); test_saturating_intrinsics!(u32); test_saturating_intrinsics!(u64); + test_saturating_intrinsics!(u128); test_saturating_intrinsics!(usize); test_saturating_intrinsics!(i8); test_saturating_intrinsics!(i16); test_saturating_intrinsics!(i32); test_saturating_intrinsics!(i64); + test_saturating_intrinsics!(i128); test_saturating_intrinsics!(isize); } diff --git a/tests/kani/SaturatingIntrinsics/add_128.rs b/tests/kani/SaturatingIntrinsics/add_128.rs deleted file mode 100644 index f65c12c0c60d..000000000000 --- a/tests/kani/SaturatingIntrinsics/add_128.rs +++ /dev/null @@ -1,12 +0,0 @@ -// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 OR MIT -// Currently fails with thread 'rustc' panicked at 'assertion failed: w < 128', compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/typ.rs:508:9 - -#![feature(core_intrinsics)] -use std::intrinsics; - -fn main() { - let v: u128 = kani::any(); - let w: u128 = kani::any(); - intrinsics::saturating_add(v, w); -}