Ignore generator function parameters (rust-lang#1130)

Author: zhassan-aws

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,
         }
     }

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"

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