Skip to content

Commit d4c6ec5

Browse files
committed
Make autoharness in run-kani.sh --run list optional
1 parent 267fa99 commit d4c6ec5

File tree

3 files changed

+17
-4
lines changed

3 files changed

+17
-4
lines changed

.github/workflows/kani-metrics.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ jobs:
2626
python-version: '3.x'
2727

2828
- name: Compute Kani Metrics
29-
run: ./scripts/run-kani.sh --run metrics --path ${{github.workspace}}
29+
run: ./scripts/run-kani.sh --run metrics --with-autoharness --path ${{github.workspace}}
3030

3131
- name: Create Pull Request
3232
uses: peter-evans/create-pull-request@v7

.github/workflows/kani.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -110,7 +110,7 @@ jobs:
110110
# Step 2: Run list on the std library
111111
- name: Run Kani List
112112
run: |
113-
head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head
113+
head/scripts/run-kani.sh --run list --with-autoharness --path ${{github.workspace}}/head
114114
# remove duplicate white space to reduce file size (GitHub permits at
115115
# most one 1MB)
116116
ls -l ${{github.workspace}}/head/kani-list.md

scripts/run-kani.sh

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ usage() {
1616
command_args=""
1717
path=""
1818
run_command="verify-std"
19+
with_autoharness="false"
1920

2021
# Parse command line arguments
2122
# TODO: Improve parsing with getopts
@@ -42,6 +43,10 @@ while [[ $# -gt 0 ]]; do
4243
usage
4344
fi
4445
;;
46+
--with-autoharness)
47+
with_autoharness="true"
48+
shift
49+
;;
4550
--kani-args)
4651
shift
4752
command_args="$@"
@@ -309,11 +314,19 @@ main() {
309314
--cbmc-args --object-bits 12
310315
elif [[ "$run_command" == "list" ]]; then
311316
echo "Running Kani list command..."
312-
"$kani_path" autoharness -Z autoharness --list -Z list $unstable_args --std ./library --format markdown
317+
if [[ "$with_autoharness" == "true" ]]; then
318+
"$kani_path" autoharness -Z autoharness --list -Z list $unstable_args --std ./library --format markdown
319+
else
320+
"$kani_path" list -Z list $unstable_args ./library --std --format markdown
321+
fi
313322
elif [[ "$run_command" == "metrics" ]]; then
314323
local current_dir=$(pwd)
315324
echo "Running Kani list command..."
316-
"$kani_path" autoharness -Z autoharness --list -Z list $unstable_args --std ./library --format json
325+
if [[ "$with_autoharness" == "true" ]]; then
326+
"$kani_path" autoharness -Z autoharness --list -Z list $unstable_args --std ./library --format json
327+
else
328+
"$kani_path" list -Z list $unstable_args ./library --std --format json
329+
fi
317330
pushd scripts/kani-std-analysis
318331
echo "Running Kani's std-analysis command..."
319332
./std-analysis.sh $build_dir

0 commit comments

Comments
 (0)