diff --git a/tests/kani/Overflow/pointer_overflow_fail.rs b/tests/kani/Overflow/pointer_overflow_fail.rs new file mode 100644 index 0000000000000..f40e4ea65ee2b --- /dev/null +++ b/tests/kani/Overflow/pointer_overflow_fail.rs @@ -0,0 +1,10 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-verify-fail + +pub fn main() { + let a = [0; 5]; + let i: i32 = 0; + let ptr1: *const i32 = &a[0]; + let ptr_overflow1 = unsafe { ptr1.offset(isize::MAX) }; +} diff --git a/tests/kani/Overflow/pointer_overflow_fixme.rs b/tests/kani/Overflow/pointer_overflow_fixme.rs new file mode 100644 index 0000000000000..56bae4eef48d8 --- /dev/null +++ b/tests/kani/Overflow/pointer_overflow_fixme.rs @@ -0,0 +1,14 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-verify-fail +// This should fail, but doesn't due to https://github.com/diffblue/cbmc/issues/6631 + +pub fn main() { + let a = [0; 5]; + let i: i32 = 0; + let ptr1: *const i32 = &a[1]; + let ptr2: *const i32 = &i; + let ptr2 = unsafe { ptr2.offset(1) }; + let ptr_overflow1 = unsafe { ptr1.offset(isize::MAX) }; + let ptr_overflow2 = unsafe { ptr2.offset(isize::MAX) }; +}