Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

use markdown format; move to separate job #15

Closed
wants to merge 4 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
37 changes: 11 additions & 26 deletions .github/workflows/kani.yml
Original file line number Diff line number Diff line change
Expand Up @@ -38,18 +38,10 @@ jobs:
# 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

run-kani-list:
name: Kani List
runs-on: ubuntu-latest
steps:
# Step 1: Check out the repository
- name: Checkout Repository
Expand All @@ -58,25 +50,18 @@ jobs:
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
# 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.txt', 'utf8');
const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani-list.md', 'utf8');
await core.summary
.addRaw(kaniOutput)
.write();
.addHeading('Kani List Output', 2)
.addRaw(kaniOutput, false)
.write();
2 changes: 1 addition & 1 deletion scripts/run-kani.sh
Original file line number Diff line number Diff line change
Expand Up @@ -221,7 +221,7 @@ main() {
--cbmc-args --object-bits 12
elif [[ "$run_command" == "list" ]]; then
echo "Running Kani list command..."
"$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib ./library --std > $path/kani_list.txt
"$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib ./library --std --format markdown
fi
}

Expand Down
Loading