Add regular & fixme tests for function contracts #8749
Workflow file for this run
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 | |
| name: Kani CI | |
| on: | |
| pull_request: | |
| merge_group: | |
| push: | |
| # Not just any push, as that includes tags. | |
| # We don't want to re-trigger this workflow when tagging an existing commit. | |
| branches: | |
| - '**' | |
| env: | |
| RUST_BACKTRACE: 1 | |
| jobs: | |
| regression: | |
| runs-on: ${{ matrix.os }} | |
| strategy: | |
| matrix: | |
| os: [macos-13, ubuntu-20.04, ubuntu-22.04, macos-14] | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v4 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ${{ matrix.os }} | |
| - name: Execute Kani regression | |
| run: ./scripts/kani-regression.sh | |
| write-json-symtab-regression: | |
| runs-on: ubuntu-20.04 | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v4 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ubuntu-20.04 | |
| - name: Build Kani | |
| run: cargo build-dev -- --features write_json_symtab | |
| - name: Run tests | |
| run: | | |
| cargo run -p compiletest --quiet -- --suite kani --mode kani --quiet --no-fail-fast | |
| cargo run -p compiletest --quiet -- --suite expected --mode expected --quiet --no-fail-fast | |
| cargo run -p compiletest --quiet -- --suite cargo-kani --mode cargo-kani --quiet --no-fail-fast | |
| benchcomp-tests: | |
| runs-on: ubuntu-20.04 | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v4 | |
| - name: Install benchcomp dependencies | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y python3-pip | |
| pushd tools/benchcomp && pip3 install -r requirements.txt | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ubuntu-20.04 | |
| - name: Build Kani using release mode | |
| run: cargo build-dev -- --release | |
| - name: Run benchcomp unit and regression tests | |
| run: pushd tools/benchcomp && PATH=$(realpath ../../scripts):$PATH test/run | |
| perf: | |
| runs-on: ubuntu-20.04 | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v4 | |
| - name: Setup Kani Dependencies | |
| uses: ./.github/actions/setup | |
| with: | |
| os: ubuntu-20.04 | |
| - name: Execute Kani performance tests | |
| run: ./scripts/kani-perf.sh | |
| env: | |
| RUST_TEST_THREADS: 1 | |
| documentation: | |
| runs-on: ubuntu-20.04 | |
| permissions: | |
| contents: write | |
| steps: | |
| - name: Checkout Kani | |
| uses: actions/checkout@v4 | |
| with: | |
| submodules: recursive | |
| - name: Install book dependencies | |
| run: ./scripts/setup/ubuntu/install_doc_deps.sh | |
| # On one OS only, build the documentation, too. | |
| - name: Build Documentation | |
| run: ./scripts/build-docs.sh | |
| # When we're pushed to main branch, only then actually publish the docs. | |
| - name: Publish Documentation | |
| if: ${{ github.event_name == 'push' && startsWith('refs/heads/main', github.ref) }} | |
| uses: JamesIves/github-pages-deploy-action@v4 | |
| with: | |
| branch: gh-pages | |
| folder: docs/book/ | |
| single-commit: true |