Aurea
Aurea
Pushing this off to `syn`: https://github.com/dtolnay/syn/issues/1153
Let's not actually touch this until after CAV.
It's not great because higher-ranked lifetimes are implicitly introduced (by way of the `Fn*` type), but at least it's a proper error and at the correct position.
Can you `assert!(...)` the `.contains_key` precondition before the `get_and_unwrap` call, and does it succeed? A minimal, reproducible example program would help us identify the problem. Finally, (especially if the internal...
There are several problems and the Prusti errors are not all internal (so you should read them): - `pure function parameters must be Copy` - you are trying to pass...
We have faced similar issues with @vl0w for deeply nested generics + iterators.
Does this extra replacement we added in #980 to `encoder_poly` fix this? https://github.com/viperproject/prusti-dev/blob/7d25c73cb63cc0f985b48e5d3d91a7e50264c152/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs#L56-L63
Requiring an extra attribute for this would not be very user friendly. There is actually a way to do a mutable visit over the AST; @LDY1998 was trying something similar...
At the very least this depends on having a solid library of stdlib specifications. Otherwise this kind of thing would quickly make any code unusable without a huge chunk of...
How do you invoke Prusti? What is the small project – have you tried with e.g. an empty `main` and nothing else?