Skip to content

Commit ca044db

Browse files
roypatManciukic
authored andcommitted
fix: remove useless kani harness
verify_size only had assertions about our mocks, which is not very useful (in fact, the second assertion was trivially true, no matter what we did). So let's just remove it. Signed-off-by: Patrick Roy <[email protected]>
1 parent fe0b5a2 commit ca044db

File tree

1 file changed

+0
-9
lines changed

1 file changed

+0
-9
lines changed

src/vmm/src/devices/virtio/queue.rs

Lines changed: 0 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1054,15 +1054,6 @@ mod verification {
10541054
}
10551055
}
10561056

1057-
#[kani::proof]
1058-
#[kani::unwind(0)]
1059-
fn verify_size() {
1060-
let ProofContext(queue, _) = kani::any();
1061-
1062-
assert!(queue.size <= queue.max_size);
1063-
assert!(queue.size <= queue.size);
1064-
}
1065-
10661057
#[kani::proof]
10671058
#[kani::unwind(0)]
10681059
fn verify_avail_ring_idx_get() {

0 commit comments

Comments
 (0)