More tests for exact_div

tests/kani/Intrinsics/ExactDiv/divisor_is_zero.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
+
+// Check that `exact_div` results in undefined behavior if `y == 0`
+// https://doc.rust-lang.org/std/intrinsics/fn.exact_div.html
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let x = kani::any();
+    let y = 0;
+    let _ = unsafe { std::intrinsics::exact_div(x, y) };
+}

tests/kani/Intrinsics/ExactDiv/main.rs

@@ -0,0 +1,15 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `exact_div` returns the expected result if none
+// of the conditions for undefined behavior are met
+// https://doc.rust-lang.org/std/intrinsics/fn.exact_div.html
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let x = 8;
+    let y = 4;
+    let res = unsafe { std::intrinsics::exact_div(x, y) };
+    assert!(res == 2);
+}

tests/kani/Intrinsics/ExactDiv/not_exact_division.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
+
+// Check that `exact_div` results in undefined behavior if `x % y != 0`
+// https://doc.rust-lang.org/std/intrinsics/fn.exact_div.html
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let x = 9;
+    let y = 4;
+    let _ = unsafe { std::intrinsics::exact_div(x, y) };
+}

tests/kani/Intrinsics/ExactDiv/overflow_division.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
+
+// Check that `exact_div` results in undefined behavior if `x == T::MIN && y == -1`
+// https://doc.rust-lang.org/std/intrinsics/fn.exact_div.html
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let x = i32::MIN;
+    let y = -1;
+    let _ = unsafe { std::intrinsics::exact_div(x, y) };
+}