Skip to content

Commit

Permalink
Added comment describing the unwind value.
Browse files Browse the repository at this point in the history
  • Loading branch information
Yoshiki Takashima committed Jan 13, 2023
1 parent ada5828 commit 341df0b
Showing 1 changed file with 7 additions and 1 deletion.
8 changes: 7 additions & 1 deletion .github/workflows/continuous-integration-workflow.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -106,10 +106,16 @@ jobs:
- name: Verify with Kani
uses: model-checking/[email protected]
with:
enable-propproof: true
args: |
--tests -p prost-types --default-unwind 3 \
--harness "tests::check_timestamp_roundtrip_via_system_time"
enable-propproof: true
# --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
# correct. However, Kani will require more time and memory. If
# Kani fails with "Failed Checks: unwinding assertion," this
# number may need to be raised for Kani to succeed.
no-std:
runs-on: ubuntu-latest
Expand Down

0 comments on commit 341df0b

Please sign in to comment.