Skip to content

Commit

Permalink
Update verify-std-check workflow to enable loop contracts (#3705)
Browse files Browse the repository at this point in the history
Update the verify-std-check workflow to be consistent with
https://github.com/model-checking/verify-rust-std/blob/main/scripts/run-kani.sh#L186

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
qinheping authored Nov 11, 2024
1 parent c776a54 commit 40246f5
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions .github/workflows/verify-std-check.yml
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ jobs:
continue-on-error: true
run: |
kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
-Z mem-predicates
-Z mem-predicates -Z loop-contracts --enable-unstable --cbmc-args --object-bits 12
# If the head failed, check if it's a new failure.
- name: Checkout base
Expand All @@ -77,7 +77,7 @@ jobs:
continue-on-error: true
run: |
kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
-Z mem-predicates
-Z mem-predicates -Z loop-contracts --enable-unstable --cbmc-args --object-bits 12
- name: Compare PR results
if: steps.check-head.outcome != 'success' && steps.check-head.outcome != steps.check-base.outcome
Expand Down

0 comments on commit 40246f5

Please sign in to comment.