Add tests for pointer overflow checking (rust-lang#792)

celinval · Feb 2, 2022 · 6720d44 · 6720d44
1 parent 6ce9a04
commit 6720d44
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 0 deletions.
diff --git a/tests/kani/Overflow/pointer_overflow_fail.rs 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
@@ -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) };
+}