@@ -179,3 +179,145 @@ jobs:
179
179
files : build/html/coverage.info
180
180
fail_ci_if_error : true
181
181
verbose : true
182
+
183
+ # This job takes approximately 36 to 85 minutes
184
+ macOS-cache-build :
185
+ runs-on : macos-13
186
+ steps :
187
+ - uses : actions/checkout@v4
188
+ with :
189
+ submodules : recursive
190
+ - name : Fetch dependencies
191
+ run : |
192
+ # maven is already installed and upgrading to a newer version yields
193
+ # symlink conflicts as previously reported in https://github.com/actions/runner-images/issues/4020
194
+ brew install cmake flex bison llvm lcov ccache z3
195
+ - name : Prepare ccache
196
+ uses : actions/cache@v4
197
+ with :
198
+ save-always : true
199
+ path : .ccache
200
+ key : ${{ runner.os }}-Coverage-${{ github.ref }}-${{ github.sha }}-PR
201
+ restore-keys : |
202
+ ${{ runner.os }}-Coverage-${{ github.ref }}
203
+ ${{ runner.os }}-Coverage
204
+ - name : ccache environment
205
+ run : |
206
+ echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
207
+ echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
208
+ - name : Configure CMake CBMC build with coverage instrumentation parameters
209
+ run : cmake -S . -Bbuild -Denable_coverage=1 -Dparallel_tests=4 -DCMAKE_C_COMPILER=$(brew --prefix llvm)/bin/clang -DCMAKE_CXX_COMPILER=$(brew --prefix llvm)/bin/clang++
210
+ - name : Zero ccache stats and limit in size
211
+ run : ccache -z --max-size=7G
212
+ - name : Execute CMake CBMC build
213
+ run : cmake --build build -- -j4
214
+ - name : Print ccache stats
215
+ run : ccache -s
216
+
217
+ # This job takes approximately 36 to 85 minutes
218
+ macOS-non-JBMC :
219
+ needs : macOS-cache-build
220
+ runs-on : macos-13
221
+ steps :
222
+ - uses : actions/checkout@v4
223
+ with :
224
+ submodules : recursive
225
+ - name : Fetch dependencies
226
+ run : |
227
+ # maven is already installed and upgrading to a newer version yields
228
+ # symlink conflicts as previously reported in https://github.com/actions/runner-images/issues/4020
229
+ brew install cmake flex bison llvm lcov ccache z3
230
+ - name : Confirm z3 solver is available and log the version installed
231
+ run : z3 --version
232
+ - name : Download cvc5 binary and make sure it can be deployed
233
+ run : |
234
+ curl -L https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-macOS --output cvc5
235
+ chmod u+x cvc5
236
+ mv cvc5 /usr/local/bin
237
+ cvc5 --version
238
+ - name : Prepare ccache
239
+ uses : actions/cache/restore@v4
240
+ with :
241
+ path : .ccache
242
+ key : ${{ runner.os }}-Coverage-${{ github.ref }}-${{ github.sha }}-PR
243
+ restore-keys : |
244
+ ${{ runner.os }}-Coverage-${{ github.ref }}
245
+ ${{ runner.os }}-Coverage
246
+ - name : ccache environment
247
+ run : |
248
+ echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
249
+ echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
250
+ - name : Configure CMake CBMC build with coverage instrumentation parameters
251
+ run : cmake -S . -Bbuild -Denable_coverage=1 -Dparallel_tests=4 -DCMAKE_C_COMPILER=$(brew --prefix llvm)/bin/clang -DCMAKE_CXX_COMPILER=$(brew --prefix llvm)/bin/clang++ -DCOVERAGE_CTEST_EXTRA_FLAGS="-E;^jbmc" -DLCOV_FLAGS="--keep-going"
252
+ - name : Zero ccache stats and limit in size
253
+ run : ccache -z --max-size=7G
254
+ - name : Execute CMake CBMC build
255
+ run : cmake --build build -- -j4
256
+ - name : Print ccache stats
257
+ run : ccache -s
258
+ - name : Run CTest and collect coverage statistics
259
+ run : |
260
+ echo "lcov_excl_line = UNREACHABLE" > ~/.lcovrc
261
+ echo "geninfo_external = 0" >> ~/.lcovrc
262
+ cmake --build build --target coverage -- -j4
263
+ - name : Upload coverage statistics to Codecov
264
+ uses : codecov/codecov-action@v4
265
+ with :
266
+ token : ${{ secrets.CODECOV_TOKEN }}
267
+ files : build/html/coverage.info
268
+ fail_ci_if_error : true
269
+ verbose : true
270
+
271
+ # This job takes approximately 36 to 85 minutes
272
+ macOS-JBMC :
273
+ needs : macOS-cache-build
274
+ runs-on : macos-13
275
+ steps :
276
+ - uses : actions/checkout@v4
277
+ with :
278
+ submodules : recursive
279
+ - name : Fetch dependencies
280
+ run : |
281
+ # maven is already installed and upgrading to a newer version yields
282
+ # symlink conflicts as previously reported in https://github.com/actions/runner-images/issues/4020
283
+ brew install cmake flex bison llvm lcov ccache z3
284
+ - name : Confirm z3 solver is available and log the version installed
285
+ run : z3 --version
286
+ - name : Download cvc5 binary and make sure it can be deployed
287
+ run : |
288
+ curl -L https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-macOS --output cvc5
289
+ chmod u+x cvc5
290
+ mv cvc5 /usr/local/bin
291
+ cvc5 --version
292
+ - name : Prepare ccache
293
+ uses : actions/cache/restore@v4
294
+ with :
295
+ path : .ccache
296
+ key : ${{ runner.os }}-Coverage-${{ github.ref }}-${{ github.sha }}-PR
297
+ restore-keys : |
298
+ ${{ runner.os }}-Coverage-${{ github.ref }}
299
+ ${{ runner.os }}-Coverage
300
+ - name : ccache environment
301
+ run : |
302
+ echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
303
+ echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
304
+ - name : Configure CMake CBMC build with coverage instrumentation parameters
305
+ run : cmake -S . -Bbuild -Denable_coverage=1 -Dparallel_tests=4 -DCMAKE_C_COMPILER=$(brew --prefix llvm)/bin/clang -DCMAKE_CXX_COMPILER=$(brew --prefix llvm)/bin/clang++ -DCOVERAGE_CTEST_EXTRA_FLAGS="-R;^jbmc" -DLCOV_FLAGS="--keep-going"
306
+ - name : Zero ccache stats and limit in size
307
+ run : ccache -z --max-size=7G
308
+ - name : Execute CMake CBMC build
309
+ run : cmake --build build -- -j4
310
+ - name : Print ccache stats
311
+ run : ccache -s
312
+ - name : Run CTest and collect coverage statistics
313
+ run : |
314
+ echo "lcov_excl_line = UNREACHABLE" > ~/.lcovrc
315
+ echo "geninfo_external = 0" >> ~/.lcovrc
316
+ cmake --build build --target coverage -- -j4
317
+ - name : Upload coverage statistics to Codecov
318
+ uses : codecov/codecov-action@v4
319
+ with :
320
+ token : ${{ secrets.CODECOV_TOKEN }}
321
+ files : build/html/coverage.info
322
+ fail_ci_if_error : true
323
+ verbose : true
0 commit comments