List workflow #55
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
| name: Kani | |
| on: | |
| workflow_dispatch: | |
| pull_request: | |
| branches: [ main ] | |
| push: | |
| paths: | |
| - 'library/**' | |
| - '.github/workflows/kani.yml' | |
| - 'scripts/run-kani.sh' | |
| defaults: | |
| run: | |
| shell: bash | |
| jobs: | |
| check-kani-on-std: | |
| name: Verify std library | |
| runs-on: ${{ matrix.os }} | |
| strategy: | |
| matrix: | |
| os: [ubuntu-latest, macos-latest] | |
| include: | |
| - os: ubuntu-latest | |
| base: ubuntu | |
| - os: macos-latest | |
| base: macos | |
| steps: | |
| # Step 1: Check out the repository | |
| - name: Checkout Repository | |
| uses: actions/checkout@v4 | |
| with: | |
| path: head | |
| submodules: true | |
| # Step 2: Run Kani on the std library (default configuration) | |
| - name: Run Kani Verification | |
| run: head/scripts/run-kani.sh --path ${{github.workspace}}/head | |
| test-kani-script: | |
| name: Test Kani script | |
| runs-on: ${{ matrix.os }} | |
| strategy: | |
| matrix: | |
| os: [ubuntu-latest, macos-latest] | |
| include: | |
| - os: ubuntu-latest | |
| base: ubuntu | |
| - os: macos-latest | |
| base: macos | |
| steps: | |
| # Step 1: Check out the repository | |
| - name: Checkout Repository | |
| uses: actions/checkout@v4 | |
| with: | |
| path: head | |
| submodules: true | |
| # Step 2: Test Kani verification script with specific arguments | |
| - name: Test Kani script (Custom Args) | |
| run: head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr --output-format=terse | |
| # Step 3: Test Kani verification script in the repository directory | |
| - name: Test Kani script (In Repo Directory) | |
| working-directory: ${{github.workspace}}/head | |
| run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr --output-format=terse | |
| # Step 3: Run list on the std library (assumes it creates kani_list.txt) | |
| - name: Run Kani List | |
| uses: actions/github-script@v6 | |
| with: | |
| script: | | |
| head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head; | |
| const fs = require('fs'); | |
| const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani_list.txt', 'utf8'); | |
| kaniOutput >> "$GITHUB_STEP_SUMMARY"; |