Federico Poli
Federico Poli
Hi! The verification unit of Prusti are functions, but not everything that Prusti does can be split per function. For example, rustc's execution (type checker, borrow checker...) and the translation...
That would be great. We could also check if `./x.py metadata` provides all the data that we need. That would be more robust than collecting `Cargo.toml` files.
#1187 is done. When `PRUSTI_OPT_IN_VERIFICATION` is enabled, we can now use `false` as the default precondition.
From the discussion at rust-lang/rust#63929 it seems that `rustc` is not going to depend on a `compiletest` out of tree. So, what is the future of `compiletest-rs`? To me, it...
Minus one :tada:
`verify_overflow/pass/rosetta /Knights_tour_generic.rs` is disabled too because it was flaky due to random verification timeouts.
Could the label invariant be encoded as an `assert ` in case the label is not a loop head? Anyway, in Prusti we currently encode loops as loop-free Viper CFGs,...
PR #25 might fix this, but it seems the changes were lost in the migration to GitHub.
@marcoeilers I vaguely remember that you might know the cause. If so, could you drop a hint?
Can you fix the linter errors?