From 949ae2cbd6c4ef4f8a8a073c5cb6035a44bcb401 Mon Sep 17 00:00:00 2001 From: Matias Ezequiel Vara Larsen Date: Fri, 6 Jun 2025 10:50:53 +0200 Subject: [PATCH] Run kani as part of the CI pipeline 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 --- .buildkite/custom-tests.json | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.buildkite/custom-tests.json b/.buildkite/custom-tests.json index defc9d47..442b9059 100644 --- 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 } ] }