vfukala
vfukala
In the user guide, in the section about closures, the (only) example ```rust use prusti_contracts::*; fn main() { let cl = closure!( requires(a > b), ensures(result > b), |a: i32,...
For ```rust use prusti_contracts::*; fn MY_FUNC() {} #[extern_spec(crate)] fn MY_FUNC(); fn main() {} ``` , Prusti output is ``` __ __ __ ___ |__) _\/_ |__) | | /__` |...
On ```rust use prusti_contracts::*; #[pure] #[requires(g())] fn f() -> bool { unreachable!() } #[pure] #[requires(f())] fn g() -> bool { unreachable!() } fn main() {} ``` , Prusti overflows the...
NOTE: Caching has been disabled in this PR (see `prusti-server/src/process_verification.rs`) because it led to errors in the Github CI. Consider re-enabling it before merging. Adding time reasoning (see #1275), resources,...
`prusti-tests/tests/verify_overflow/pass/extern-spec/linked-list.rs` still passes even when `prusti_assert!(false);` is added to line 115. The entire test case then looks like this: ```rust use prusti_contracts::*; use std::collections::LinkedList; use std::option::Option; #[extern_spec] impl std::option::Option {...
This program should verify: ```rust use prusti_contracts::*; enum MyEnum { A, B, } fn main() { prusti_assert!(MyEnum::A !== MyEnum::B); } ``` However, verification fails with ``` error: [Prusti: verification error]...
The verification of this program ```rust use prusti_contracts::*; fn main() { prusti_assert!(0 !== 1); } ``` fails with ``` error: [Prusti internal error] Prusti encountered an unexpected internal error -->...
Even when the overflow checks are disabled (`check_overflows = false` is set), ```Rust #[requires(b != 0)] fn do_div(a: i32, b: i32) -> i32 { a / b } ``` and...
If I have the `Proof:Delegation` setting set to `Delegate proofs` and I quickly edit the `H_edit_me` name (e.g. by holding down a key) in the following file... ```coq Require Import...
### Description of the problem Consider the code below. In 8.18.0, the `change` tactic succeeds, but in 8.19.0 and 8.19.1, it fails with ``` Error: This quotation is not supported...