prusti-dev
prusti-dev copied to clipboard
viperproject
A static verifier for Rust, based on the Viper verification infrastructure.
I am trying to use the function [get_and_unwrap](https://github.com/viperproject/prusti-dev/issues/1029) which has the precondition `requires(map.contains_key(key))`. My HashMap spec looks like this: ``` #[extern_spec] impl HashMap where K: Eq + Hash, S: BuildHasher,...
Summary: Automatically import specifications from dependency crates and inline them when respective functions or types are referenced in the current crate. This eliminates the need for `#[extern_spec]` blocks for declarations...
counterexample support for Prusti's snapshot encoding For this branch to work correctly it needs my version of Fabio's branch of Silicon: [https://github.com/mlimbeck/silicon/tree/fabio-counterexample-improvements](https://github.com/viperproject/prusti-dev/pull/url)
While running `prusti-rustc` on the following code: ```rust struct Params { letter: char, password: String } fn check(params: Params) -> usize { return params.password.chars().filter(|c| c == ¶ms.letter).count(); } fn main()...
I copied the Option code that was given in the user guide, and tried to convert it to use generics: ``` pub enum TrustedOption { Some(T), None, } impl TrustedOption...
The following code: ```rust #[requires(i == Int::new(2))] fn test(i: Int) {} #[requires(s.lookup(3) == 5)] fn test2(s: Seq) {} #[requires(m.lookup(7) == 11)] fn test3(m: Map) {} ``` gives the following errors:...
The following code verifies successfully even though it calls an impure function from a predicate: ```rust use prusti_contracts::*; fn impure() -> u32 { 5 } predicate! { fn pred(x: u32)...
Metadata
Owner
Metadata
A static verifier for Rust, based on the Viper verification infrastructure.