Skip to content

Commit 6fda6ac

Browse files
committed
ci: add -Z stubbing to run kani
cc model-checking/kani#4295 cc model-checking/verify-rust-std@c090506#diff-8348895dea8741e872b7dd41b86e35d72e0f497c56ff6ed5c42bf5958ba2fe45 error: Using the stub_verified attribute requires activating the unstable `stubbing` feature --> /home/runner/work/distributed-verification/distributed-verification/verify-rust-std/library/core/src/intrinsics/mod.rs:3583:13 | 3583 | #[kani::stub_verified(transmute_unchecked_wrapper)] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ... 3605 | should_succeed_no_validity_reqs!(should_succeed_char_to_i32, char, i32); | ----------------------------------------------------------------------- in this macro invocation | = note: this error originates in the attribute macro `kani::stub_verified` which comes from the expansion of the macro `should_succeed_no_validity_reqs` (in Nightly builds, run with -Z macro-backtrace for more info)
1 parent 8f7eb52 commit 6fda6ac

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

.github/workflows/test.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ jobs:
5454
autoharness: ["", "-autoharness"]
5555
if: true
5656
env:
57-
UNSTABLE_ARGS: -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts
57+
UNSTABLE_ARGS: -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z stubbing
5858
AUTO: ${{ matrix.autoharness }}
5959
steps:
6060
- name: Remove unnecessary software to free up disk space

0 commit comments

Comments
 (0)