Skip to content

Commit 1f40c65

Browse files
authored
Remove obsolete note on missing output when unwinding forever (rust-lang#1883)
1 parent 4b7f6c3 commit 1f40c65

File tree

1 file changed

+0
-5
lines changed

1 file changed

+0
-5
lines changed

docs/src/tutorial-loop-unwinding.md

-5
Original file line numberDiff line numberDiff line change
@@ -27,11 +27,6 @@ VERIFICATION:- FAILED
2727
If we try removing this "unwind" annotation and re-running Kani, the result is worse: non-termination.
2828
Kani simply doesn't produce a result.
2929

30-
> **NOTE**: Presently, [due to a bug](https://github.com/model-checking/kani/issues/493), this is especially bad: we don't see any output at all.
31-
> Kani is supposed to emit some log lines that might give some clue that an infinite loop is occurring.
32-
> If Kani doesn't terminate, it's most frequently the problem that this section covers.
33-
> The workaround is to use the technique we're demoing here: use `#[kani::unwind(1)]` to force termination of the loops, and work upwards from there.
34-
3530
The problem we're struggling with is the technique Kani uses to verify code.
3631
We're not able to handle code with "unbounded" loops, and what "bounded" means can be quite subtle.
3732
It has to have a constant number of iterations that's _"obviously constant"_ enough for the verifier to actually figure this out.

0 commit comments

Comments
 (0)