Skip to content

Commit f3ba917

Browse files
Edit quantifiers' documentation. (#4142)
This PR fixed the examples in the documentation of quantifier feature. Resolves #4133 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 37fb634 commit f3ba917

File tree

1 file changed

+5
-5
lines changed

1 file changed

+5
-5
lines changed

docs/src/reference/experimental/quantifiers.md

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -14,8 +14,8 @@ Kani currently supports the following quantifiers:
1414
```rust
1515
#[kani::proof]
1616
fn test_forall() {
17-
let v = vec![10; 10];
18-
kani::assert(kani::forall!(|i in 0..10| v[i] == 10));
17+
let v : [u8;10] = [10; 10];
18+
assert!(kani::forall!(|i in (0,10)| v[i] == 10) );
1919
}
2020
```
2121

@@ -27,19 +27,19 @@ fn test_forall() {
2727
```rust
2828
#[kani::proof]
2929
fn test_exists() {
30-
let v = vec![1, 2, 3, 4, 5];
31-
kani::assert(kani::exists!(|i in 0..v.len()| v[i] == 3));
30+
let v : [u8;5] = [1, 2, 3, 4, 5];
31+
assert!(kani::exists!(|i in (0,v.len())| v[i] == 3));
3232
}
3333
```
3434

35+
3536
### Limitations
3637

3738
#### Array Indexing
3839

3940
The performance of quantifiers can be affected by the depth of call stacks in the quantified expressions. If the call stack is too deep, Kani may not be able to evaluate the quantifier effectively, leading to potential timeouts or running out of memory. Actually, array indexing in Rust leads to a deep call stack, which can cause issues with quantifiers. To mitigate this, consider using *unsafe* pointer dereferencing instead of array indexing when working with quantifiers. For example:
4041

4142
```rust
42-
4343
#[kani::proof]
4444
fn vec_assert_forall_harness() {
4545
let v = vec![10 as u8; 128];

0 commit comments

Comments
 (0)