Merge branch 'main' into chores-170-target #62
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 4: Run list on the std library and add output to job summary | |
| - name: Run Kani List | |
| run: head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head | |
| - name: Add Kani List output to job summary | |
| uses: actions/github-script@v6 | |
| with: | |
| script: | | |
| const fs = require('fs'); | |
| const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani_list.txt', 'utf8'); | |
| await core.summary | |
| .addRaw(kaniOutput) | |
| .write(); |