From abda0180afceacd868ec455851ab55cacdb81c55 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Date: Wed, 6 Apr 2022 14:50:06 -0400
Subject: [PATCH] Tests for `assume` (#1015)

---
 tests/kani/Intrinsics/Assume/assume_fail.rs | 11 +++++++++++
 tests/kani/Intrinsics/Assume/assume_ok.rs   | 10 ++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 tests/kani/Intrinsics/Assume/assume_fail.rs
 create mode 100644 tests/kani/Intrinsics/Assume/assume_ok.rs

diff --git a/tests/kani/Intrinsics/Assume/assume_fail.rs b/tests/kani/Intrinsics/Assume/assume_fail.rs
new file mode 100644
index 000000000000..2079994cae7f
--- /dev/null
+++ b/tests/kani/Intrinsics/Assume/assume_fail.rs
@@ -0,0 +1,11 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `assume` fails if the condition is false (undefined behavior)
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    unsafe { core::intrinsics::assume(false) };
+}
diff --git a/tests/kani/Intrinsics/Assume/assume_ok.rs b/tests/kani/Intrinsics/Assume/assume_ok.rs
new file mode 100644
index 000000000000..7208419966e9
--- /dev/null
+++ b/tests/kani/Intrinsics/Assume/assume_ok.rs
@@ -0,0 +1,10 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `assume` does not fail if the condition is true
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    unsafe { core::intrinsics::assume(true) };
+}