Merge branch 'add-script-to-automate-build' of https://github.com/jai… #40
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 Rust Verification | |
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 Rust Code (Default Configuration) | |
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 (Default) | |
run: head/scripts/run-kani.sh --path ${{github.workspace}}/head | |
test-kani-script: | |
name: Verify Rust Code (Custom Configuration) | |
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: Run Kani Verification (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: Run Kani Verification (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 |