Skip to content

Commit 0ce06de

Browse files
author
Siddharth Priya
committed
virtio-queue: disable verify_add_used proof
Re-enable this proof once #373 is fixed. Signed-off-by: Siddharth Priya <[email protected]>
1 parent d9e9f23 commit 0ce06de

File tree

1 file changed

+4
-2
lines changed

1 file changed

+4
-2
lines changed

virtio-queue/src/queue/verification.rs

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -571,8 +571,10 @@ fn get_used_idx(
571571
/// if the descriptor index is out of bounds, the operation must fail and the
572572
/// used index must not be incremented. Note that this proof does not verify
573573
/// Section 2.7.8.2: "Device Requirements: The Virtqueue Used Ring"
574-
#[kani::proof]
575-
#[kani::unwind(0)]
574+
// Re-enable this proof once https://github.com/rust-vmm/vm-virtio/issues/373
575+
// is fixed.
576+
// #[kani::proof]
577+
// #[kani::unwind(0)]
576578
fn verify_add_used() {
577579
let ProofContext { mut queue, memory } = kani::any();
578580
let used_idx = queue.next_used;

0 commit comments

Comments
 (0)