Skip to content

Fix exit code swallowed by --quiet on verification failure - #4787

Open
rbeauchamp wants to merge 1 commit into
model-checking:mainfrom
rbeauchamp:fix-4745-quiet-exit-code
Open

Fix exit code swallowed by --quiet on verification failure#4787
rbeauchamp wants to merge 1 commit into
model-checking:mainfrom
rbeauchamp:fix-4745-quiet-exit-code

Conversation

@rbeauchamp

Copy link
Copy Markdown

Description

kani --quiet (and cargo kani --quiet) always exits 0, even when verification fails. print_final_summary in kani-driver/src/harness_runner.rs returned Ok(()) early under --quiet, skipping the process::exit(1) path used in non-quiet mode. This silently breaks CI pipelines that rely on the exit code while suppressing output.

The fix hoists the failure/success partitions (and the autoharness failing count) above the quiet gate so the exit status is computed the same way in both modes. The quiet-mode contract — no verification output on stdout — is preserved; only the exit code changes (0 → 1 on failure).

Context

Reported by @ivmat in #4745: running kani --quiet on a failing harness prints nothing (correct) but returns exit status 0 (incorrect), so failures are invisible to scripts and CI.

Manual testing

New script-based regression test tests/script-based-pre/quiet-exit-code/: runs kani --quiet on a failing and a passing harness and asserts (a) exit code 1 / 0 respectively, and (b) empty stdout/stderr in both cases. Verified RED without the fix (exit 0 on failure) and GREEN with it, on this branch. cargo test -p kani-driver passes (101/101).

Resolves #4745

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

not sure if issue, more a question, is this expected or not: --quiet makes a failing verification run exit 0

1 participant