From c755ae58b061b4adf1cd4d895758704899ab6b7a Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Wed, 16 Mar 2022 15:00:08 -0700
Subject: [PATCH 1/3] Enabled test for #786

---
 .../{pointer_overflow_fixme.rs => pointer_overflow2_fail.rs}     | 1 -
 1 file changed, 1 deletion(-)
 rename tests/kani/Overflow/{pointer_overflow_fixme.rs => pointer_overflow2_fail.rs} (83%)

diff --git a/tests/kani/Overflow/pointer_overflow_fixme.rs b/tests/kani/Overflow/pointer_overflow2_fail.rs
similarity index 83%
rename from tests/kani/Overflow/pointer_overflow_fixme.rs
rename to tests/kani/Overflow/pointer_overflow2_fail.rs
index 27ec5bd43bda..935b94bbe217 100644
--- a/tests/kani/Overflow/pointer_overflow_fixme.rs
+++ b/tests/kani/Overflow/pointer_overflow2_fail.rs
@@ -1,7 +1,6 @@
 // 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
 
 #[kani::proof]
 fn main() {

From 90ecd7448ddbb3dd3c0ef559442d91dd43ed822d Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Tue, 12 Apr 2022 12:25:19 -0700
Subject: [PATCH 2/3] Use an expected test instead to check for the expected
 failure

---
 tests/expected/pointer-overflow/expected      |  2 ++
 tests/expected/pointer-overflow/main.rs       | 11 +++++++++++
 tests/kani/Overflow/pointer_overflow2_fail.rs | 14 --------------
 3 files changed, 13 insertions(+), 14 deletions(-)
 create mode 100644 tests/expected/pointer-overflow/expected
 create mode 100644 tests/expected/pointer-overflow/main.rs
 delete mode 100644 tests/kani/Overflow/pointer_overflow2_fail.rs

diff --git a/tests/expected/pointer-overflow/expected b/tests/expected/pointer-overflow/expected
new file mode 100644
index 000000000000..58914ccdbc86
--- /dev/null
+++ b/tests/expected/pointer-overflow/expected
@@ -0,0 +1,2 @@
+Status: FAILURE\
+arithmetic overflow on signed multiplication
diff --git a/tests/expected/pointer-overflow/main.rs b/tests/expected/pointer-overflow/main.rs
new file mode 100644
index 000000000000..eac6bd306d06
--- /dev/null
+++ b/tests/expected/pointer-overflow/main.rs
@@ -0,0 +1,11 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that overflow for pointers operations is reported
+
+#[kani::proof]
+fn main() {
+    let a = [0; 5];
+    let ptr: *const i32 = &a[1];
+    let _ = unsafe { ptr.offset(isize::MAX) };
+}
diff --git a/tests/kani/Overflow/pointer_overflow2_fail.rs b/tests/kani/Overflow/pointer_overflow2_fail.rs
deleted file mode 100644
index 935b94bbe217..000000000000
--- a/tests/kani/Overflow/pointer_overflow2_fail.rs
+++ /dev/null
@@ -1,14 +0,0 @@
-// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
-
-#[kani::proof]
-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) };
-}

From a4e620d9dfc391447aef04c6f68a26458d7df056 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Date: Tue, 12 Apr 2022 12:32:51 -0700
Subject: [PATCH 3/3] Update tests/expected/pointer-overflow/main.rs

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
---
 tests/expected/pointer-overflow/main.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/expected/pointer-overflow/main.rs b/tests/expected/pointer-overflow/main.rs
index eac6bd306d06..a2b35a56c296 100644
--- a/tests/expected/pointer-overflow/main.rs
+++ b/tests/expected/pointer-overflow/main.rs
@@ -1,7 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// This test checks that overflow for pointers operations is reported
+// Checks that overflows for pointer arithmetic are reported
 
 #[kani::proof]
 fn main() {