Federico Poli
Federico Poli
The following program makes Prusti raise an internal error, because currently `old(..)` expressions are only allowed in postconditions. ```rust use prusti_contracts::*; #[ensures(a % result == 0)] #[ensures(b % result ==...
While preparing a Prusti demo last week, I found that the order of the reported errors is a bit counter-intuitive. In the second function below, I'd expect the verification error...
The program ```rust use prusti_contracts::*; #[pure] // i32 { 123 } ``` fails with ```text custom attribute panicked message: internal error: entered unreachable code ``` However, the correct behaviour is...
The program ```rust fn main() { let mut a = 123; let x = &mut a; let gen = || { x }; let y = gen(); // &'?11 mut...
The program ```rust fn foo(mut x: &'a mut i32, y: &'a mut i32) { let mut x = x; x = y; } ``` The fold-unfold is not at fault;...
We should upgrade the test suite, replacing `compiletest-rs` with the new and less error-prone [`ui_test`](https://crates.io/crates/ui_test) crate. A good example to start from is [here](https://github.com/duchess-rs/duchess/blob/main/tests/ui.rs). While doing so, I believe that...
The `x.py` script interprets its subcommands and arguments using some custom parsing rules, but discovering them is difficult because the script does not print any help message. * `x.py` and...
The [domain definition of `read$` seems to be strictly better](https://github.com/viperproject/silicon/issues/765) than the current function definition that is used by Prusti. On a Rust function of 150 lines full of shared...
The following program generates a meaningless verification error, but as a workaround it is possible to wrap the mutable reference modification in a helper method. This is a bug. The...
@vakaras pointed out that the current encoding of mutually recursive functions might be unsound when the (optional) termination checks are enabled. Until that's fixes, it's up to the users to...