Open vfukala opened 1 year ago
On
use prusti_contracts::*; #[pure] #[requires(g())] fn f() -> bool { unreachable!() } #[pure] #[requires(f())] fn g() -> bool { unreachable!() } fn main() {}
, Prusti overflows the stack:
__ __ __ ___ |__) _\/_ |__) | | /__` | ____\/_ | | /\ | \ \__/ .__/ | /\ | Prusti version: 0.2.2, commit d3dc99990e2 2023-06-26 14:59:58 UTC, built on 2023-07-01 23:37:13 UTC Verification of 3 items... thread 'rustc' has overflowed its stack fatal runtime error: stack overflow
Note that Prusti also produces an unexpected internal error on
an unexpected internal error
use prusti_contracts::*; #[pure] #[requires(f())] fn f() -> bool { unreachable!() } fn main() {}
, but I think this is the same kind of error as the one expected in prusti-tests/tests/verify_partial/fail/issues/issues-769.rs.
prusti-tests/tests/verify_partial/fail/issues/issues-769.rs
On
, Prusti overflows the stack:
Note that Prusti also produces
an unexpected internal error
on, but I think this is the same kind of error as the one expected in
prusti-tests/tests/verify_partial/fail/issues/issues-769.rs
.