Skip to content

Commit f8cff4e

Browse files
committed
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 31c4dbe commit f8cff4e

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
@@ -1055,15 +1055,6 @@ mod verification {
10551055
}
10561056
}
10571057

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

0 commit comments

Comments
 (0)