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>

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>();
+}

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);
+}