Nightly: CBMC Latest #431
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # Copyright Kani Contributors | |
| # SPDX-License-Identifier: Apache-2.0 OR MIT | |
| # We use block scalar notation to allow us to add ":" to the workflow name. | |
| name: >- | |
| Nightly: CBMC Latest | |
| on: | |
| schedule: | |
| - cron: "0 9 * * *" # Run this every day at 9 AM UTC (4 AM ET/1 AM PT) | |
| workflow_dispatch: # Allow manual dispatching for a custom branch / tag. | |
| env: | |
| RUST_BACKTRACE: 1 | |
| jobs: | |
| regression: | |
| runs-on: ${{ matrix.os }} | |
| strategy: | |
| matrix: | |
| os: [macos-12, ubuntu-20.04, ubuntu-22.04] | |
| steps: | |
| - name: Checkout Kani under "kani" | |
| uses: actions/checkout@v3 | |
| with: | |
| path: kani | |
| - name: Setup Kani Dependencies | |
| uses: ./kani/.github/actions/setup | |
| with: | |
| os: ${{ matrix.os }} | |
| kani_dir: 'kani' | |
| - name: Build Kani | |
| working-directory: ./kani | |
| run: cargo build-dev | |
| - name: Checkout CBMC under "cbmc" | |
| uses: actions/checkout@v3 | |
| with: | |
| repository: diffblue/cbmc | |
| path: cbmc | |
| - name: Build CBMC | |
| working-directory: ./cbmc | |
| run: | | |
| make -C src minisat2-download cadical-download | |
| make -C src -j4 MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical | |
| # Prepend the bin directory to $PATH | |
| echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH | |
| - name: Execute Kani regressions | |
| working-directory: ./kani | |
| run: ./scripts/kani-regression.sh | |
| perf: | |
| runs-on: ubuntu-20.04 | |
| steps: | |
| - name: Checkout Kani under "kani" | |
| uses: actions/checkout@v3 | |
| with: | |
| path: kani | |
| - name: Setup Kani Dependencies | |
| uses: ./kani/.github/actions/setup | |
| with: | |
| os: ubuntu-20.04 | |
| kani_dir: 'kani' | |
| - name: Build Kani using release mode | |
| working-directory: ./kani | |
| run: cargo build-dev -- --release | |
| - name: Checkout CBMC under "cbmc" | |
| uses: actions/checkout@v3 | |
| with: | |
| repository: diffblue/cbmc | |
| path: cbmc | |
| - name: Build CBMC | |
| working-directory: ./cbmc | |
| run: | | |
| cmake -S . -Bbuild -DWITH_JBMC=OFF | |
| cmake --build build -- -j 4 | |
| # Prepend the bin directory to $PATH | |
| echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH | |
| - name: Execute Kani performance tests | |
| working-directory: ./kani | |
| run: ./scripts/kani-perf.sh | |
| - name: Execute Kani performance ignored tests | |
| working-directory: ./kani | |
| continue-on-error: true | |
| run: cargo run -p compiletest -- --suite perf --mode cargo-kani-test ignore --ignored --no-fail-fast |