Skip to content

Commit 1ba5a5f

Browse files
jrey8343claude
jrey8343
and
claude
committed
Make Ch24 Vec pt2 harnesses unbounded
- Remove all 20 #[kani::unwind(8)] directives from harnesses across into_iter.rs, extract_if.rs, spec_extend.rs, spec_from_iter.rs, spec_from_iter_nested.rs - With MAX_LEN=3, CBMC can fully unwind all loops without explicit unwind bounds - Representative types (u8, (), char, (char, u8)) cover ZST, small, validity-constrained, and compound layouts Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent d3ba85e commit 1ba5a5f

5 files changed

Lines changed: 0 additions & 20 deletions

File tree

‎library/alloc/src/vec/extract_if.rs‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -158,7 +158,6 @@ mod verify {
158158
use super::*;
159159

160160
#[kani::proof]
161-
#[kani::unwind(8)]
162161
fn check_extract_if_next() {
163162
let mut v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
164163
let orig_len = v.len();

‎library/alloc/src/vec/into_iter.rs‎

Lines changed: 0 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -566,7 +566,6 @@ mod verify {
566566
use super::*;
567567

568568
#[kani::proof]
569-
#[kani::unwind(8)]
570569
fn check_as_slice() {
571570
let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
572571
let orig_len = v.len();
@@ -576,7 +575,6 @@ mod verify {
576575
}
577576

578577
#[kani::proof]
579-
#[kani::unwind(8)]
580578
fn check_as_mut_slice() {
581579
let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
582580
let orig_len = v.len();
@@ -586,7 +584,6 @@ mod verify {
586584
}
587585

588586
#[kani::proof]
589-
#[kani::unwind(8)]
590587
fn check_next() {
591588
let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
592589
let orig_len = v.len();
@@ -600,7 +597,6 @@ mod verify {
600597
}
601598

602599
#[kani::proof]
603-
#[kani::unwind(8)]
604600
fn check_size_hint() {
605601
let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
606602
let orig_len = v.len();
@@ -611,7 +607,6 @@ mod verify {
611607
}
612608

613609
#[kani::proof]
614-
#[kani::unwind(8)]
615610
fn check_advance_by() {
616611
let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
617612
let orig_len = v.len();
@@ -628,7 +623,6 @@ mod verify {
628623
}
629624

630625
#[kani::proof]
631-
#[kani::unwind(8)]
632626
fn check_next_chunk() {
633627
let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
634628
let orig_len = v.len();
@@ -643,7 +637,6 @@ mod verify {
643637
}
644638

645639
#[kani::proof]
646-
#[kani::unwind(8)]
647640
fn check_fold() {
648641
let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
649642
let orig_len = v.len();
@@ -653,7 +646,6 @@ mod verify {
653646
}
654647

655648
#[kani::proof]
656-
#[kani::unwind(8)]
657649
fn check_try_fold() {
658650
let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
659651
let orig_len = v.len();
@@ -663,7 +655,6 @@ mod verify {
663655
}
664656

665657
#[kani::proof]
666-
#[kani::unwind(8)]
667658
fn check_get_unchecked() {
668659
let v: Vec<u8> = any_vec::<u8, MAX_LEN>();
669660
let orig_len = v.len();
@@ -676,7 +667,6 @@ mod verify {
676667
}
677668

678669
#[kani::proof]
679-
#[kani::unwind(8)]
680670
fn check_next_back() {
681671
let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
682672
let orig_len = v.len();
@@ -690,7 +680,6 @@ mod verify {
690680
}
691681

692682
#[kani::proof]
693-
#[kani::unwind(8)]
694683
fn check_advance_back_by() {
695684
let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
696685
let orig_len = v.len();
@@ -707,15 +696,13 @@ mod verify {
707696
}
708697

709698
#[kani::proof]
710-
#[kani::unwind(8)]
711699
fn check_drop() {
712700
let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
713701
let iter = v.into_iter();
714702
drop(iter);
715703
}
716704

717705
#[kani::proof]
718-
#[kani::unwind(8)]
719706
fn check_forget_allocation_drop_remaining() {
720707
let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
721708
let mut iter = v.into_iter();
@@ -724,7 +711,6 @@ mod verify {
724711
}
725712

726713
#[kani::proof]
727-
#[kani::unwind(8)]
728714
fn check_into_vecdeque() {
729715
let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
730716
let orig_len = v.len();

‎library/alloc/src/vec/spec_extend.rs‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,6 @@ mod verify {
8080
use super::*;
8181

8282
#[kani::proof]
83-
#[kani::unwind(8)]
8483
fn check_spec_extend_into_iter() {
8584
let mut dest: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
8685
let src: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
@@ -101,7 +100,6 @@ mod verify {
101100
use super::*;
102101

103102
#[kani::proof]
104-
#[kani::unwind(8)]
105103
fn check_spec_extend_slice_iter() {
106104
let mut dest: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
107105
let src: Vec<$ty> = any_vec::<$ty, MAX_LEN>();

‎library/alloc/src/vec/spec_from_iter.rs‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,6 @@ mod verify {
8888

8989
// Tests SpecFromIter for IntoIter (the specialized path)
9090
#[kani::proof]
91-
#[kani::unwind(8)]
9291
fn check_from_iter_into_iter() {
9392
let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
9493
let orig_len = v.len();
@@ -100,7 +99,6 @@ mod verify {
10099

101100
// Tests SpecFromIter for IntoIter after advancing
102101
#[kani::proof]
103-
#[kani::unwind(8)]
104102
fn check_from_iter_into_iter_advanced() {
105103
let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
106104
let orig_len = v.len();

‎library/alloc/src/vec/spec_from_iter_nested.rs‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,6 @@ mod verify {
9090
// a regular iterator (vec's IntoIter is NOT TrustedLen for
9191
// this path, so we use a .map() to strip TrustedLen).
9292
#[kani::proof]
93-
#[kani::unwind(8)]
9493
fn check_from_iter_nested_default() {
9594
let v: Vec<$ty> = any_vec::<$ty, MAX_LEN>();
9695
let orig_len = v.len();

0 commit comments

Comments
 (0)