Pointerbender

Use snapshot encoding for Rust assertions

7

The following Rust program: ```rust use prusti_contracts::*; #[requires(forall(|i: usize| (0 (array[i] > 100) ))] pub fn assert_example(array: &[usize; 16]) { assert!(array[0] > 100); } fn main() {} ``` fails verification...

ASSERT_TIMEOUT=0 not properly passed to Viper?

33

I have an example which I believe should verify: ```rust extern crate prusti_contracts; use prusti_contracts::*; pub const MAX_DEPTH: usize = usize::BITS as usize; pub struct Path { current: usize, depth:...

Documentation for Type-Conditional Spec Refinements

2

I'm playing around with the recently stabilized Type-Conditional Spec Refinements feature. I have a question about how to use it. For example, reading the [docs](https://viperproject.github.io/prusti-dev/user-guide/verify/type_cond_spec.html) I would expect that I...

Limitations on structs with reference-typed fields

2

Hi! I have the following program and I have a question on what is and what is not supported atm: ```rust use prusti_contracts::*; pub struct Foo { foo: T, }...

Fix drop order of tls and statics and avoid double panics on deadlock

3

Hello! I ran into some of the same issues as mentioned in #152, #179 and #291 and developed a fix for all of those issues. In a nutshell, the changes...

(AdtPlugin) fixes and regression tests for #581

2

The new ADT plugin did not handle `result` expressions in post-conditions yet properly. This PR is a patch to fix a couple of corner cases with additional regression tests.

AdtPlugin java.lang.ClassCastException

5

Hello! I found my way here through doing some research for Prusti and I noticed the ADT plugin got merged very recently :) This looks like a really great feature,...