Skip to content

Commit ab64f85

Browse files
authored
Make forall compile
1 parent 98e10c4 commit ab64f85

File tree

1 file changed

+4
-2
lines changed

1 file changed

+4
-2
lines changed

library/core/src/slice/memchr.rs

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@
33

44
use crate::intrinsics::const_eval_select;
55
#[cfg(kani)]
6+
use crate::forall;
7+
#[cfg(kani)]
68
use crate::kani;
79

810
const LO_USIZE: usize = usize::repeat_u8(0x01);
@@ -38,7 +40,7 @@ const fn memchr_naive(x: u8, text: &[u8]) -> Option<usize> {
3840
let mut i = 0;
3941

4042
// FIXME(const-hack): Replace with `text.iter().pos(|c| *c == x)`.
41-
#[kani::loop_invariant(i <= text.len() && kani::forall!(|j in (0,i)| unsafe {*text.as_ptr().wrapping_add(j)} != x))]
43+
#[kani::loop_invariant(i <= text.len() && forall!(|j in (0,i)| unsafe {*text.as_ptr().wrapping_add(j)} != x))]
4244
while i < text.len() {
4345
if text[i] == x {
4446
return Some(i);
@@ -82,7 +84,7 @@ const fn memchr_aligned(x: u8, text: &[u8]) -> Option<usize> {
8284
// search the body of the text
8385
let repeated_x = usize::repeat_u8(x);
8486
#[kani::loop_invariant(len >= 2 * USIZE_BYTES && offset <= len &&
85-
kani::forall!(|j in (0,offset)| unsafe {*text.as_ptr().wrapping_add(j)} != x))]
87+
forall!(|j in (0,offset)| unsafe {*text.as_ptr().wrapping_add(j)} != x))]
8688
while offset <= len - 2 * USIZE_BYTES {
8789
// SAFETY: the while's predicate guarantees a distance of at least 2 * usize_bytes
8890
// between the offset and the end of the slice.

0 commit comments

Comments
 (0)