Federico Poli

I found that `cargo outdated` panics when running on our project. Project: https://github.com/viperproject/prusti-dev, commit `5705580`. Command: ``` RUST_BACKTRACE=1 cargo outdated --root-deps-only --workspace ``` Output: ``` thread 'main' panicked at 'index...

Implement normalization of position ids in the server

1

@JonasAlaif This PR implements the second normalization described in https://github.com/viperproject/prusti-dev/pull/971#issuecomment-1146060967. A lot of the new code is boilerplate to visit all positions of a program. Unfortunately, the `Program` that is...

Failing magic wand generation

5

Prusti fails to generate the magic wand at the end of the `next` method: ```rust use prusti_contracts::*; struct Node { next: Option, } impl Node { fn next(&mut self) ->...

len() bounds encoded only if there is a call in pure code

2

The proper range bounds of `.len()` seem to be encoded only if the `len()` call happens in pure code. ```rust use prusti_contracts::*; #[ensures(a.len() * 4

Cache collisions

5

It's possible to trigger collisions in the caching of verification results. Step 1: open the Prusti IDE and verify this program ```rust use prusti_contracts::*; fn a() {} #[ensures(false)] fn test()...

Clarify failing postcondition of trait method

2

In the following program Prusti identifies a verification error as expected: the method implementation `A::bar` does not specify a postcondition, so it gets by default the `result > 10` from...

Spans of quantified variables

1

The `Spanned::get_spans` method needs a MIR body to obtain the spans of variables stored in the `ForAllVars

When running Prusti with panic and overflow check disabled on the following program, no error message should be raised. However, Prusti reports "[Prusti: invalid specification] the loop invariant cannot be...

The following program crashes while encoding `test` with an "internal error: entered unreachable code: 1" in `vir_gen.rs`. Backtrace ``` [2022-03-24T10:14:30Z INFO prusti_viper::encoder::encoder] Encoding: 20220324_110509::test (20220324_110509::test) thread 'rustc' panicked at 'internal...

Check prusti-contracts version

1

When verifying a crate that depends on `prusti-contracts`, Prusti should check that the version of `prusti-contracts` is compatible with the version of Prusti, reporting a readable error message if they...