Skip to content

Commit 1b59b66

Browse files
author
Carolyn Zech
committed
disable is_ascii harness for x86 sse2; add FIXME
1 parent 6b250a2 commit 1b59b66

1 file changed

Lines changed: 4 additions & 0 deletions

File tree

library/core/src/slice/ascii.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -517,6 +517,10 @@ pub mod verify {
517517

518518
#[kani::proof]
519519
#[kani::unwind(8)]
520+
// FIXME: the loop invariant in the x_64 & sse2 version of is_ascii
521+
// fails because Kani does not yet support modifies clauses for loop invariants.
522+
// Once it does, remove this cfg.
523+
#[cfg(not(all(target_arch = "x86_64", target_feature = "sse2")))]
520524
pub fn check_is_ascii() {
521525
if kani::any() {
522526
// TODO: ARR_SIZE can be much larger with cbmc argument

0 commit comments

Comments
 (0)