Skip to content

Add harnesses for safety of primitive conversions #1175

Add harnesses for safety of primitive conversions

Add harnesses for safety of primitive conversions #1175

Workflow file for this run

name: Kani
on:
workflow_dispatch:
merge_group:
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 (partition ${{ matrix.partition }})
runs-on: ${{ matrix.os }}
strategy:
matrix:
os: [ubuntu-latest, macos-latest]
partition: [1, 2, 3, 4]
include:
- os: ubuntu-latest
base: ubuntu
- os: macos-latest
base: macos
fail-fast: false
env:
# Define the index of this particular worker [1-WORKER_TOTAL]
WORKER_INDEX: ${{ matrix.partition }}
# Total number of workers running this step
WORKER_TOTAL: 4
steps:
# Step 1: Check out the repository
- name: Checkout Repository
uses: actions/checkout@v4
with:
path: head
submodules: true
# Step 2: Install jq
- name: Install jq
if: matrix.os == 'ubuntu-latest'
run: sudo apt-get install -y jq
# Step 3: Run Kani on the std library (default configuration)
- name: Run Kani Verification
run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
run-kani-list:
name: Kani List
runs-on: ubuntu-latest
steps:
# Step 1: Check out the repository
- name: Checkout Repository
uses: actions/checkout@v4
with:
path: head
submodules: true
# Step 2: Run list on the std library
- name: Run Kani List
run: head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head
# Step 3: Add output to job summary
- 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.md', 'utf8');
await core.summary
.addHeading('Kani List Output', 2)
.addRaw(kaniOutput, false)
.write();