Run kani as part of the CI pipeline

MatiasVara · priyasiddharth · commit 76bc969eb8a2 · 2025-06-11T10:10:55.000-04:00
Run kani as a part of the CI pipeline. In particular, run the proofs for
virtio-queue. In some cases, kani may not finish so set a twenty minutes
timeout.

Signed-off-by: Matias Ezequiel Vara Larsen &lt;mvaralar@redhat.com&gt;
diff --git a/.buildkite/custom-tests.json b/.buildkite/custom-tests.json
@@ -48,6 +48,12 @@
       "command": "cd fuzz && cargo test --package common --lib blk && cargo +nightly fuzz run blk -- -max_total_time=900 -timeout=60s",
       "platform": ["x86_64", "aarch64"],
       "timeout_in_minutes": 20
+    },
+    {
+      "test_name": "prove-virtio-queue",
+      "command": "cargo kani --package virtio-queue",
+      "platform": ["x86_64", "aarch64"],
+      "timeout_in_minutes": 20
     }
   ]
 }

Original file line number	Diff line number	Diff line change
`@@ -48,6 +48,12 @@`
`48`	`48`	`"command": "cd fuzz && cargo test --package common --lib blk && cargo +nightly fuzz run blk -- -max_total_time=900 -timeout=60s",`
`49`	`49`	`"platform": ["x86_64", "aarch64"],`
`50`	`50`	`"timeout_in_minutes": 20`
	`51`	`+ },`
	`52`	`+ {`
	`53`	`+ "test_name": "prove-virtio-queue",`
	`54`	`+ "command": "cargo kani --package virtio-queue",`
	`55`	`+ "platform": ["x86_64", "aarch64"],`
	`56`	`+ "timeout_in_minutes": 20`
`51`	`57`	`}`
`52`	`58`	`]`
`53`	`59`	`}`