Federico Poli

Relevant cargo issue: https://github.com/rust-lang/cargo/issues/4316

Pending on https://github.com/rust-lang/cargo/issues/9096

Thank you for the report! I think the reason of the error is that `push_all` uses an iterator (`for i in 0..slice_len(slice)`), which is currently unsupported. Prusti should have reported...

> The actual source of the error is the `.clone()` call. Thanks for identifying the reason. That's strange, we need to debug this.

I investigated a bit more. The issue is caused by `index_slice`, whose result reborrows an argument of type shared reference. Reborrowing a shared reference is still unsupported. A slightly simpler...

The first example now reports the correct error ``` error: [Prusti: unsupported feature] iterators are not fully supported yet --> program.rs:39:14 | 39 | for i in 0..slice_len(slice) { |...

Another case of this: ```rust fn foo() {} fn bar(mut i: i32) { while { i += 1; i > 0 } { foo(); } } fn main() {} ```

The general issue is that loop invariant permissions are computed incorrectly if during a loop execution a structure is initialized (in the loop guard or body) and then one of...

A generic example: ```rust use prusti_contracts::*; struct NonCopy(u32); #[trusted] fn non_copy_tuple() -> (NonCopy, NonCopy) { unimplemented!() } #[trusted] fn consume(x: NonCopy) { unimplemented!() } fn main() { while { let...

Slightly better error message for the latest example, after https://github.com/viperproject/prusti-dev/pull/788: ``` error: [Prusti internal error] cannot generate fold-unfold Viper statements. The required permission Pred(_3.tuple_0, write) cannot be obtained. ```