Do not create a ProjectedPlace for unsupported fields

[zhassan-aws]

Description of changes:

With the mechanism for handling unsupported scenarios in projection code introduced in #1057, it is now possible to avoid creating a projected place for unsupported fields. This PR introduces a similar mechanism for handling unsupported fields in codegen_field that propagates an error upstream.

Resolved issues:

Call-outs:

Testing:

• How is this change tested? Existing tests

• Is this a refactor change? Partially

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[celinval]

Is there any test case for this?

[zhassan-aws]

This test: https://github.com/model-checking/kani/blob/3c008db98f2559b131f2b10ba355ee73d6dd4943/tests/kani/Generator/main.rs
has a generator. I'm not sure it's hitting this case though. I'll check.

[zhassan-aws]

I found out that the assert(false) that is generated in https://github.com/model-checking/kani/blob/3c008db98f2559b131f2b10ba355ee73d6dd4943/tests/kani/Generator/main.rs is due to this block:

kani/src/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

Line 611 in 3c008db

ty::Generator(..) => {

and not the one in place.rs. However, my attempts at creating a test that covers the line of code in place.rs, which I think requires having a struct with a generator field, e.g.:

#![feature(generators, generator_trait)]

use std::ops::{Generator};

struct HasGeneratorField<T> 
where T: Generator {
    _g: T,
}

impl<T> HasGeneratorField<T> 
where T: Generator {
    pub fn new(g: T) -> Self {
        HasGeneratorField { _g: g }
    }
}

//#[kani::proof]
fn main() {
    let _s = HasGeneratorField::new(|| { yield 1; return 2; });
}

all resulted in a crash that I filed as #1075.

So I think this may have to stay untested till the other issue is fixed.

[celinval]

Thanks for trying to add a test. I think this is still beneficial as is.