From 1dfee4bad2282e34707da0e187475f4f4307bfb4 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Mon, 13 Mar 2023 15:56:13 -0400 Subject: [PATCH] Add existing roundtrip test to Kani CI and avoid recursive submoduling (#828) * Add existing roundtrip test to Kani CI * Bump up Kani version * Remove `v` from GA version --- .github/workflows/continuous-integration-workflow.yaml | 7 +++---- KANI.md | 4 ++-- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/.github/workflows/continuous-integration-workflow.yaml b/.github/workflows/continuous-integration-workflow.yaml index 19745eebb..9bad4a45d 100644 --- a/.github/workflows/continuous-integration-workflow.yaml +++ b/.github/workflows/continuous-integration-workflow.yaml @@ -103,15 +103,14 @@ jobs: steps: - name: checkout uses: actions/checkout@v3 - with: - submodules: recursive - name: Verify with Kani - uses: model-checking/kani-github-action@v0.19 + uses: model-checking/kani-github-action@0.23 with: enable-propproof: true args: | --tests -p prost-types --default-unwind 3 \ - --harness "tests::check_timestamp_roundtrip_via_system_time" + --harness "tests::check_timestamp_roundtrip_via_system_time" \ + --harness "tests::check_duration_roundtrip_nanos" # --default-unwind N roughly corresponds to how much effort # Kani will spend trying to prove correctness of the # program. Higher the number, more programs can be proven diff --git a/KANI.md b/KANI.md index c3c4031f0..cafb0131d 100644 --- a/KANI.md +++ b/KANI.md @@ -19,7 +19,7 @@ capabilities and limitations. from the Kani repository. ```bash git clone https://github.com/model-checking/kani.git --branch features/proptest propproof - cd propproof; git submodule update --init --recursive + cd propproof; git submodule update --init ``` Then, use `.cargo/config.toml` enable it in the local directory you @@ -34,7 +34,7 @@ capabilities and limitations. **Please Note**: - `features/proptest` branch under Kani is likely not the final - location for this code. If this instruction stops working, please + location for this code. If these instructions stop working, please consult the Kani documentation and file an issue on [the Kani repo](https://github.com/model-checking/kani.git). - The cargo config file will force cargo to always use PropProof. To