Tests for assume (model-checking#1015)

tedinski · Apr 25, 2022 · abda018 · abda018
1 parent 4e1dead
commit abda018
Show file tree

Hide file tree

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