Pointerbender

Consistency error: Labelled-old expressions are not allowed in postconditions.

1

The following Rust program: ```rust use prusti_contracts::*; #[derive(Clone, Copy)] pub struct A; #[derive(Clone, Copy, PartialEq, Eq)] pub struct B(usize); impl A { #[pure] #[trusted] #[ensures(b == old(b))] pub fn foo(a:...

Prusti performance deteriorates for larger structs that derive `PartialEq`

2

For the following Rust program: ```rust use prusti_contracts::*; #[derive(Copy, Clone, PartialEq, Eq)] pub struct A { pub field0: usize, pub field1: isize, pub field2: u64, pub field3: i64, pub field4:...

Performance issues when combining predicates and reborrows

2

The following Rust program: ```rust use prusti_contracts::*; #[derive(Copy, Clone)] pub struct A { pub field0: usize, pub field1: isize, pub field2: u64, pub field3: i64, pub field4: [i32; 64], pub...

The following Rust program: ```rust use prusti_contracts::*; #[derive(Clone, Copy)] pub struct A; impl PartialEq for A { #[pure] fn eq(&self, other: &Self) -> bool { true } } impl Eq...

value might not fit into the target type (due to check_overflows)

9

```rust use prusti_contracts::*; #[derive(Clone, Copy)] pub struct A { count: isize, } impl A { #[pure] #[ensures(result usize { if self.count < 0 { ((1_isize + self.count) + isize::MAX) as...

The following Rust program: ```rust use prusti_contracts::*; use core::ops::Deref; fn main() {} struct A; struct B { a: A, } impl Deref for B { type Target = A; fn...

Snap encoding of array assignments

20

This issue is a spin-off from #819, which revealed that currently Prusti is unable to verify programs like: ```rust #[ensures(result usize { let mut a = [1, 2, 3]; let...

`verify/pass/arrays/{merge,selection_sort}.rs` timeout issue

10

On commit 7e259b8 from PR #817 the test case `prusti-tests/tests/verify/pass/arrays/selection_sort.rs` is reliably failing due to a timeout error during the CI run on Ubuntu. This timeout issue is not reproducible...

Memory crash during Prusti encoding step

9

Somewhere between commits bb3cb3fe25 and f8e70f9 a regression was introduced that significantly increased memory usage, leading to a crash during the Prusti encoding step in both debug and release mode....

Specification refinement on `Cell<T>` with trait bounds

5

When feeding the following Rust program to Prusti: ```rust use prusti_contracts::*; use core::cell::Cell; fn main() { let foo = Cell::new(1); assert!(foo.get() == 1); } #[extern_spec] impl Cell { #[pure] pub...