Fabian Zaiser

The relevant function `fn_sig_for_fn_abi` is [here](https://github.com/rust-lang/rust/blob/848090dcd18553b790461132ca9d2a020aeea9a2/compiler/rustc_middle/src/ty/layout.rs#L2754). It has a comment saying: ```rust // NOTE(eddyb) this is private to avoid using it from outside of // `fn_abi_of_instance` - any other uses...

@celinval The adjustments to the signature could be related to #1350. These adjustments don't currently happen in the Kani code, but they probably should.

As of #1378, there is now a generator variant: `TypeOrVariant::GeneratorVariant` that needs to be handled too.

Reduced to ```rust use std::iter::FromIterator; #[kani::proof] pub fn main() { let coll: Vec = FromIterator::from_iter(std::iter::empty()); assert_eq!(Vec::::new(), coll); } ```

Reduced further: ```rust #[kani::proof] pub fn main() { assert_eq!(Vec::::new(), Vec::::new()); } ``` The reason seems to be that `Vec::new` sets its pointer to dangling: https://github.com/rust-lang/rust/blob/aeb5067967ef58e4a324b19dd0dba2f385d5959f/library/alloc/src/raw_vec.rs#L123 Furthermore, in the `PartialEq` implementation,...

I've [asked on Zulip](https://rust-lang.zulipchat.com/#narrow/stream/131828-t-compiler/topic/.E2.9C.94.20Vec.3A.3Anew.3A.20invalid.20pointers.20in.20memcmp) again, and apparently it is fine to call `memcmp` on the dangling pointer.

While we argue about the true semantics, here's a plan for mitigation discussed with @danielsn: add a hook for `memcmp` and check if the size is 0. If so, return...

A workaround that worked for me: run `kani` first without `--debug` and then again with `--debug`.

Looks good to me. Two things: * Is there a way this could be tested? Specifically test that it does zero initialization? (Not sure it's worth the hassle.) * Did...

One more thing: shouldn't we zero-initialize `StatementKind::DeInit` as well? As far as I can tell, that part of the code still uses `nondet`. In particular, `DeInit` is used to "initialize"...