Federico Poli

This error arises from the *impure* encoding of pure functions; the *pure* encoding works fine with types containing shared references. This implementation of `PartialEq` doesn't contain any panic, function call...

Adding `#[trusted]` should avoid this issue. Since there is no user-written function on which to add the attribute, [`#[extern_spec]`](https://github.com/viperproject/prusti-dev/search?q=%23%5Bextern_spec%5D) should help. I haven't tried.

For the record, I tried the following but it's still not enough. ```rust #[extern_spec] impl PartialEq { #[pure] #[trusted] fn eq(&self, other: &Binop) -> bool; #[pure] #[trusted] fn ne(&self, other:...

It could be, but I don't see anything obviously wrong in that snippet and I suspect that the `#[extern_spec]` doesn't work because of the generic type parameter on the trait,...

This is the same issue of https://github.com/viperproject/prusti-dev/issues/749. `(l, r)` is a type containing shared references, and that generates bad transfer-permission statements when expiring borrows. The pure encoding would work fine,...

Regarding how to detect the case and report an error, before https://github.com/viperproject/prusti-dev/pull/117 and https://github.com/viperproject/prusti-dev/pull/121 we had a validation pass to report unsupported types. We could do something similar. The code...

I think this is one more instance of https://github.com/viperproject/prusti-dev/issues/389. The permissions computed for the loop body invariant are wrong.

Issue 1000! :tada: :tada: :tada:

The following verifies. Mentioning `a.len()` in pure code seems enough to generate a more complete encoding: ```rust use prusti_contracts::*; #[ensures(a.len() * 4

I believe this is an instance of #364: the postcondition requires `_old$pre$0` to be folded to call `is_valid` but also unfolded to access `inner`. The issue was fixed by encoding...