From b1a7e11f550c115aa3d450612acb839aa0743857 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 8 Jun 2025 17:48:32 +0000 Subject: [PATCH 1/2] Kani: use -Z unstable-options instead of --enable-unstable `--enable-unstable` has been removed from Kani's latest version and will, thus, break upgrading to a newer Kani version. --- scripts/run-kani.sh | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 6fb4b926ffda5..2c8c17cc69b2a 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -218,7 +218,7 @@ run_verification_subset() { -j \ --output-format=terse \ "${command_args[@]}" \ - --enable-unstable \ + -Z unstable-options \ --cbmc-args --object-bits 12 } @@ -300,7 +300,7 @@ main() { $unstable_args \ --no-assert-contracts \ "${command_args[@]}" \ - --enable-unstable \ + -Z unstable-options \ --cbmc-args --object-bits 12 fi elif [[ "$run_command" == "autoharness" ]]; then @@ -311,7 +311,7 @@ main() { $unstable_args \ --no-assert-contracts \ "${command_args[@]}" \ - --enable-unstable \ + -Z unstable-options \ --cbmc-args --object-bits 12 elif [[ "$run_command" == "list" ]]; then echo "Running Kani list command..." @@ -347,7 +347,7 @@ main() { $unstable_args \ --no-assert-contracts \ "${command_args[@]}" \ - --enable-unstable \ + -Z unstable-options \ --cbmc-args --object-bits 12 # remove metadata file for Kani-generated "dummy" crate that we won't # get scanner data for From bd466bf3d48238331b8d2f9e2e6dd8c471b6cbb2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 9 Jun 2025 18:39:23 +0000 Subject: [PATCH 2/2] Remove redundant option --- scripts/run-kani.sh | 4 ---- 1 file changed, 4 deletions(-) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 2c8c17cc69b2a..a2b11eb627154 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -218,7 +218,6 @@ run_verification_subset() { -j \ --output-format=terse \ "${command_args[@]}" \ - -Z unstable-options \ --cbmc-args --object-bits 12 } @@ -300,7 +299,6 @@ main() { $unstable_args \ --no-assert-contracts \ "${command_args[@]}" \ - -Z unstable-options \ --cbmc-args --object-bits 12 fi elif [[ "$run_command" == "autoharness" ]]; then @@ -311,7 +309,6 @@ main() { $unstable_args \ --no-assert-contracts \ "${command_args[@]}" \ - -Z unstable-options \ --cbmc-args --object-bits 12 elif [[ "$run_command" == "list" ]]; then echo "Running Kani list command..." @@ -347,7 +344,6 @@ main() { $unstable_args \ --no-assert-contracts \ "${command_args[@]}" \ - -Z unstable-options \ --cbmc-args --object-bits 12 # remove metadata file for Kani-generated "dummy" crate that we won't # get scanner data for