Skip to content

Commit 6fbb59c

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 <roypat@amazon.co.uk>
1 parent ae63573 commit 6fbb59c

1 file changed

Lines changed: 0 additions & 9 deletions

File tree

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)