51
51
with :
52
52
path : head
53
53
submodules : true
54
- - name : Apply stdarch patch
55
- run : cd head/library/stdarch && patch -p1 < ../../stdarch.patch
56
-
54
+
57
55
# Step 2: Install jq
58
56
- name : Install jq
59
57
if : matrix.os == 'ubuntu-latest'
90
88
uses : actions/checkout@v4
91
89
with :
92
90
submodules : true
93
- - name : Apply stdarch patch
94
- run : cd library/stdarch && patch -p1 < ../../stdarch.patch
95
91
96
92
# Step 2: Run Kani autoharness on the std library for selected functions.
97
93
# Uses "--include-pattern" to make sure we do not try to run across all
102
98
# - We use >::disjoint_bitor (and >::unchecked_disjoint_bitor) as pattern
103
99
# as whitespace is not supported, cf.
104
100
# https://github.com/model-checking/kani/issues/4046
105
- # - core_arch::x86::__m128d::as_f64x2 is just one example of hundreds of
106
- # core_arch::x86:: functions that are known to verify successfully.
107
101
- name : Run Kani Verification
108
102
run : |
109
103
scripts/run-kani.sh --run autoharness --kani-args \
@@ -113,7 +107,6 @@ jobs:
113
107
--include-pattern alloc::layout::Layout::from_size_align \
114
108
--include-pattern ascii::ascii_char::AsciiChar::from_u8 \
115
109
--include-pattern char::convert::from_u32_unchecked \
116
- --include-pattern core_arch::x86::__m128d::as_f64x2 \
117
110
--include-pattern "num::nonzero::NonZero::<i8>::count_ones" \
118
111
--include-pattern "num::nonzero::NonZero::<i16>::count_ones" \
119
112
--include-pattern "num::nonzero::NonZero::<i32>::count_ones" \
@@ -295,8 +288,6 @@ jobs:
295
288
with :
296
289
path : head
297
290
submodules : true
298
- - name : Apply stdarch patch
299
- run : cd head/library/stdarch && patch -p1 < ../../stdarch.patch
300
291
301
292
# Step 2: Run list on the std library
302
293
- name : Run Kani List
@@ -329,8 +320,6 @@ jobs:
329
320
uses : actions/checkout@v4
330
321
with :
331
322
submodules : true
332
- - name : Apply stdarch patch
333
- run : cd library/stdarch && patch -p1 < ../../stdarch.patch
334
323
335
324
# Step 2: Run autoharness analyzer on the std library
336
325
- name : Run Autoharness Analyzer
0 commit comments