Skip to content

Commit 0eb453b

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 ca5cce2 commit 0eb453b

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
@@ -1057,15 +1057,6 @@ mod verification {
10571057
}
10581058
}
10591059

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

0 commit comments

Comments
 (0)