Pointerbender

Definition collector too strict

7

I discovered another instance where the definition collector is too strict, here: https://github.com/viperproject/prusti-dev/blob/d2a9c802df1f3c1f31efab9071df1de58f001f77/prusti-viper/src/encoder/definition_collector.rs#L423-L427 `is_unfoldable` is defined as: https://github.com/viperproject/prusti-dev/blob/d2a9c802df1f3c1f31efab9071df1de58f001f77/prusti-viper/src/encoder/definition_collector.rs#L408-L409 Unfortunately, I don't have a minimal reproduction, but I will do my...

New filenames break Viper IDE

3

In commit [882fb31c](https://github.com/viperproject/prusti-dev/commit/882fb31c74bb9bb0dbbff01ec81c23b1c0df8bc7#diff-c97b049428f4a5d2ffe363af30726fc42590cd1d50421d8ab32c4775bc6982c6) there was an update to how filenames are generated. When using `dump_viper_program=true` this now results in filenames with `$$` in them, which breaks Viper IDE on Ubuntu...

False negative on multiplication

5

The following Rust program: ```rust use prusti_contracts::*; fn main() {} pub struct A { foo: usize, bar: usize, } predicate! { fn invariant(a: &A) -> bool { a.foo * a.bar...

Consistency error in postcondition when calling pure function that returns a slice

7

The following Rust program: ```rust use prusti_contracts::*; #[derive(Copy, Clone)] pub struct A { inner: usize, } impl A { #[pure] pub const fn get(&self) -> usize { self.inner } }...

Specifications on implementation of the `Drop` trait are not checked

2

Consider the following Rust program: ```rust use prusti_contracts::*; fn main() { let a = A; } pub struct A; #[refine_trait_spec] impl Drop for A { #[requires(false)] fn drop(&mut self) {}...

The following Rust Program: ```rust use prusti_contracts::*; fn main() {} pub struct A { entries: [usize; 64], } predicate! { pub fn entry_equal(a: &A, b: &A, i: usize) -> bool...

unregistered verification error: [application.precondition:insufficient.permission; 0]

22

The below program outputs a rather mysterious error: ```rust pub struct A { inner: [usize; 4], } impl A { #[pure] #[requires(index < self.inner.len())] pub fn is_valid(&self, index: usize) ->...

Failing (trivial) assertion in presence of a quantifier over a slice

1

The following Rust program: ```rust use prusti_contracts::*; pub fn main() {} #[requires(forall(|i: usize| (0 (slice[i] == i), triggers=[(slice[i],)] ))] pub fn test(slice: &mut [usize]) { if slice.len() == 3 {...

The following Rust program: ```rust use prusti_contracts::*; fn main() {} pub fn test() { let a = &mut [1,2,3]; // let a: &mut [_] = a; swap(a); assert!(a[0] == 3);...

Currently Prusti supports `Expr::{Local, Const, FuncApp, DomainFuncApp}` in quantifier triggers: https://github.com/viperproject/prusti-dev/blob/0f079017d1fb75f0264b1e652746f16266a25773/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs#L303-L311 Should these also be supported when wrapped in `old(..)`, i.e. `Expr::LabelledOld`? Down at the Prusti level, there are some...