Skip to content

Commit

Permalink
test: Simplify test_kani.py
Browse files Browse the repository at this point in the history
Prior to #4120, our unique way of running seccompiler inside of build.rs
made it impossible to run kani or miri on the workspace (requiring it to
be run on some crate which did not use the build script). With that all
gone, we can finally run kani properly.

Signed-off-by: Patrick Roy <[email protected]>
  • Loading branch information
roypat committed Sep 21, 2023
1 parent f19f684 commit 0c3c9fc
Showing 1 changed file with 3 additions and 5 deletions.
8 changes: 3 additions & 5 deletions tests/integration_tests/test_kani.py
Original file line number Diff line number Diff line change
Expand Up @@ -11,13 +11,11 @@
from framework import utils

PLATFORM = platform.machine()
CRATES_WITH_PROOFS = ["dumbo", "vmm"]


@pytest.mark.timeout(1800)
@pytest.mark.skipif(PLATFORM != "x86_64", reason="Kani proofs run only on x86_64.")
@pytest.mark.parametrize("crate", CRATES_WITH_PROOFS)
def test_kani(results_dir, crate):
def test_kani(results_dir):
"""
Test all Kani proof harnesses.
"""
Expand All @@ -27,9 +25,9 @@ def test_kani(results_dir, crate):
# --output-format terse is required by -j
# --enable-unstable is needed for each of the above
rc, stdout, stderr = utils.run_cmd(
f"cargo kani -p {crate} --enable-unstable --enable-stubbing --restrict-vtable -j --output-format terse"
"cargo kani --enable-unstable --enable-stubbing --restrict-vtable -j --output-format terse"
)

assert rc == 0, stderr

(results_dir / f"kani_log_{crate}").write_text(stdout, encoding="utf-8")
(results_dir / "kani_log").write_text(stdout, encoding="utf-8")

0 comments on commit 0c3c9fc

Please sign in to comment.