From cbac10c9d3dd3b664648eacb7664a1c891316ef5 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Date: Fri, 29 Apr 2022 15:16:45 -0700
Subject: [PATCH] Ignore generator function parameters (#1130)

---
 .../src/codegen_cprover_gotoc/codegen/typ.rs  |  4 ++++
 .../expected/generators/as_parameter/expected |  2 ++
 .../expected/generators/as_parameter/main.rs  | 24 +++++++++++++++++++
 3 files changed, 30 insertions(+)
 create mode 100644 tests/expected/generators/as_parameter/expected
 create mode 100644 tests/expected/generators/as_parameter/main.rs

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 4525946f9ce81..811aafc5bdc2a 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -1315,6 +1315,10 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn ignore_var_ty(&self, ty: Ty<'tcx>) -> bool {
         match ty.kind() {
             ty::FnDef(_, _) => true,
+            // Ignore variables of the generator type until we add support for
+            // them:
+            // https://github.com/model-checking/kani/issues/416
+            ty::Generator(..) => true,
             _ => false,
         }
     }
diff --git a/tests/expected/generators/as_parameter/expected b/tests/expected/generators/as_parameter/expected
new file mode 100644
index 0000000000000..9207afd95b24c
--- /dev/null
+++ b/tests/expected/generators/as_parameter/expected
@@ -0,0 +1,2 @@
+Status: FAILURE\
+Description: "ty::Generator is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/416"
diff --git a/tests/expected/generators/as_parameter/main.rs b/tests/expected/generators/as_parameter/main.rs
new file mode 100644
index 0000000000000..c9c1ce4254045
--- /dev/null
+++ b/tests/expected/generators/as_parameter/main.rs
@@ -0,0 +1,24 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Test that includes a generator as a parameter to a function
+// Codegen should succeed, but verification should fail (codegen_unimplemented)
+
+#![feature(generators, generator_trait)]
+
+use std::ops::Generator;
+
+fn foo<T>(g: T)
+where
+    T: Generator,
+{
+    let _ = g;
+}
+
+#[kani::proof]
+fn main() {
+    foo(|| {
+        yield 1;
+        return 2;
+    });
+}