Patrick-6

The `extern_spec` attribute seems to panic on this code example: ```rust use prusti_contracts::*; #[extern_spec] // Self; } ``` Error message: ``` custom attribute panicked extern_spec_panic.rs(7, 1): message: not implemented: Unimplemented...

Asking Prusti to print counterexamples with `counterexample = true` works for `assert` and pre-/postcondition violations, but not for `prusti_assert` and its variants: ```rust use prusti_contracts::*; #[requires(_x >= 10)] fn more_than_ten(_x:...

The following code fails with a error about `snapshot equality` not being a pure function, but only when using `extern crate prusti_contracts;` at the beginning of the file. Without the...

Prusti can verify the following code with `check_overflows = false` and `counterexample = false`. By using `check_overflows = false` and `counterexample = true`, an error will be shown on the...

Attempting to verify the following code with the `counterexample = true` flag set, Prusti will panic: ```rust use prusti_contracts::*; pub struct List { head: Link, } enum Link { Empty,...

Having multiple pledges (`assert_on_expiry` or `after_expiry`) on a single function causes an internal error, but it should be a proper error: ```rust use prusti_contracts::*; #[after_expiry(true)] #[assert_on_expiry(true, true)] fn _test(x: &mut...

`snap` function can be used in normal code

2

Using the `snap` function in normal code does not always cause a compiler error like in the first function. The second function causes Prusti to crash: ```rust use prusti_contracts::*; //...

The command `Prusti: update verifier` in VSCode fails if you have multiple instances of VSCode running with Prusti. Prusti seems to have `prusti-server.exe` and `prusti-server-driver.exe` running once per VSCode instance,...

I noticed that my cmake project was getting completely rebuilt on every tiny change. The issue was that I used `path/to/cmake/project/CMakeLists.txt` instead of `path/to/cmake/project/` when calling `cmake::Config::new(path)` in my build...