Skip to content

Add first proof

Add first proof #6

Workflow file for this run

# This workflow is responsible for verifying the standard library with Kani.
name: Kani
on:
workflow_dispatch:
pull_request:
branches: [ main ]
push:
paths:
- 'library/**'
- '.github/workflows/kani.yml'
defaults:
run:
shell: bash
jobs:
build:
runs-on: ${{ matrix.os }}
strategy:
matrix:
# Kani does not support windows.
os: [ubuntu-latest, macos-latest]
include:
- os: ubuntu-latest
base: ubuntu
- os: macos-latest
base: macos
steps:
- name: Checkout Library
uses: actions/checkout@v4
with:
path: verify-rust-std
submodules: true
# We currently build Kani from a branch that tracks a rustc version compatible with this library version.
- name: Checkout `Kani`
uses: actions/checkout@v4
with:
repository: model-checking/kani
path: kani
ref: features/verify-rust-std
- name: Setup Dependencies
working-directory: kani
run: |
./scripts/setup/${{ matrix.base }}/install_deps.sh
- name: Build `Kani`
working-directory: kani
run: |
cargo build-dev --release
echo "$(pwd)/scripts" >> $GITHUB_PATH
- name: Run tests
working-directory: verify-rust-std
env:
RUST_BACKTRACE: 1
run: |
kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
-Z mem-predicates -Z ptr-to-ref-cast-checks