Federico Poli
Federico Poli
Prusti by default uses the sysroot of the nightly rustc version specified in Prusti's repository. The `RUST_SYSROOT` environment variable can be used to force Prusti to use a different sysroot....
`cargo prusti` and the IDE extension should ideally always work out of the box (i.e. in any situation where `cargo clippy` works), so what you reported is a bug in...
`ui_test` might also be used to test the crates in `prusti-tests/tests/cargo_verify/`, replacing `cargotest.rs`. We should check.
This is blocked by https://github.com/oli-obk/ui_test/issues/147, because we need to test on Windows.
Thanks for the suggestions! In almost all of our cases the bottleneck is the Viper tool that we have to use internally, not Rust code. So, I don't think that...
Sure, we plan to update Prusti to the latest nightly version.
Thanks for the report. Could you provide a full example with the specification of `SliceIndex`?
Nice catch! It seems that overflow conditions of old expressions are encoded without an `old(..)` around them. That is, the postcondition `old(0 - self.sz) == 0` is being encoded as...
See also https://cbea.ms/git-commit/
As discussed, in that program Prusti does *not* generate the axiom that encodes that the discriminants are different. This seems the result of a too aggressive optimization because the following...