nokunish

Unsound verification when cloning vector elements

1

Verifying the properties of a vector after cloning its elements cause unsoundness. For instance, given an element, ``` struct Elem where T: Copy { val: T, next: usize } ```...

Issues with verifying the result is None

4

Hi, calling a function that always returns None from the pre/post-condition/ prusti assertions, i.e., ``` #[pure] fn test(u: u32) -> Option { return None } #[requires(test(10).is_none())] fn main() { }...

Insufficient access permission

1

Hi! I was wondering why this causes an error? ``` #[ensures(x == old(x) + 10)] // or old(x+ 10) fn inc(mut x: usize) { while x < 10 { x...

There seems to be some issues with verifying properties of wrapper structs for HashMap, specifically when a predicate is used as a restriction. For instance, when we impose `wrapper_predicate(..)` ```...

Imposing pre-condition when implementing traits?

1

When implementing traits for different structs, is there a way to impose pre/post-conditions? For instance, if I want to have a peek function, ``` pub trait OptionExt { fn peek(&self)...

Prusti has some issues detecting the types of parameters, and this seems to only occur when accessing fields of elements in a Vector / HashMap from inside a while loop....

```rust use prusti_contracts::*; use std::{alloc::Allocator, ops::Deref, slice::SliceIndex, option::Option}; #[extern_spec] impl Deref for Vec where A: Allocator { #[pure] fn deref(&self) -> &Self::Target; } #[extern_spec] impl SliceIndex for usize { #[pure]...