From 7f24a14abf205904462cc8328f7a9e750950d472 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Date: Tue, 1 Mar 2022 11:34:39 -0500
Subject: [PATCH] Negative test case for `variant_count` (#854)

* Negative test case for `variant_count`

* Add "fixme" test and update negative test

Co-authored-by: Celina G. Val <celinval@amazon.com>
---
 .../kani/Intrinsics/Compiler/variant_count.rs | 16 ++++++++++++++
 .../Compiler/variant_count_fixme.rs           | 21 +++++++++++++++++++
 2 files changed, 37 insertions(+)
 create mode 100644 tests/kani/Intrinsics/Compiler/variant_count.rs
 create mode 100644 tests/kani/Intrinsics/Compiler/variant_count_fixme.rs

diff --git a/tests/kani/Intrinsics/Compiler/variant_count.rs b/tests/kani/Intrinsics/Compiler/variant_count.rs
new file mode 100644
index 000000000000..3a7c330aefe7
--- /dev/null
+++ b/tests/kani/Intrinsics/Compiler/variant_count.rs
@@ -0,0 +1,16 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-verify-fail
+
+// Check that `variant_count` is not supported.
+// This test can be replaced with `variant_count_fixme.rs` once the intrinsic is
+// supported and works as expected.
+
+#![feature(variant_count)]
+use std::mem;
+
+enum Void {}
+
+fn main() {
+    let _ = mem::variant_count::<Void>();
+}
diff --git a/tests/kani/Intrinsics/Compiler/variant_count_fixme.rs b/tests/kani/Intrinsics/Compiler/variant_count_fixme.rs
new file mode 100644
index 000000000000..37a14dc967b1
--- /dev/null
+++ b/tests/kani/Intrinsics/Compiler/variant_count_fixme.rs
@@ -0,0 +1,21 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `variant_count` is supported and returns the expected result.
+
+#![feature(variant_count)]
+use std::mem;
+
+enum Void {}
+enum MyError {
+    Error1,
+    Error2,
+    Error3,
+}
+
+fn main() {
+    assert!(mem::variant_count::<Void>() == 0);
+    assert!(mem::variant_count::<MyError>() == 3);
+    assert!(mem::variant_count::<Option<u32>>() == 2);
+    assert!(mem::variant_count::<Result<u32, MyError>>() == 2);
+}