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(g: T) +where + T: Generator, +{ + let _ = g; +} + +#[kani::proof] +fn main() { + foo(|| { + yield 1; + return 2; + }); +}