Replace negate_success with success + failure verdict gates#2
Merged
Conversation
…ct gates The `negate_success` boolean silently reinterpreted the `success` field as a failure pattern and defaulted fail-open — a missed failure pattern reported the run as successful (how the NaN verdict bug hid). Replace it with two explicit nullable patterns over a data-driven baseline: - `success` (positive, fail-closed): must match to pass. - `failure` (gate): a match forces failure; covers verifiers whose failures do not surface as issues by default (e.g. Kani without --trace). - baseline: a run passes iff it has no error-severity issue; warnings/info never flip the verdict. The three checks are independent gates, so a miss in one is still caught by another. Migrate specs: esbmc/cbmc keep `success`; clang/kani/pytest move to `failure` (kani also clears the `success` it inherits from cbmc_spec via replace). Behaviour preserved across all regression fixtures; adds parser-level verdict unit tests.
Close the coverage gaps the code review flagged: the clang negate_success -> failure migration had no test. Add real gcc-produced regression fixtures (unused_variable_warning -> successful, undeclared_error -> failed) that pin the "warnings never fail the build" behaviour on real diagnostics, plus verdict unit cases for info-severity (passes) and mixed warning+error (fails).
…rings /simplify cleanup. clang's `error:` diagnostic is already extracted as an error-severity issue, so the data-driven baseline fails the run — the `failure` pattern was pure redundancy (clang, unlike kani/pytest, has no failure-without-an- issue mode). Drop it so clang is cleanly data-driven. Also de-duplicate the verdict invariant that was spelled out in three docstrings down to one authoritative place, and correct the "gates catch each other" note (only the error-issue baseline and `failure` are mutually-catching failure signals; `success` is a fail-closed positive requirement). Behaviour unchanged; all fixtures pass.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Removes the
negate_successboolean, which silently reinterpreted thesuccessfield as a failure pattern and defaulted fail-open — a failure whose pattern
didn't match was reported as a successful run. That's how the
NaNverdict bug hid.Replaces it with two explicit, nullable patterns layered on a data-driven baseline:
never flip the verdict).
success(optional, positive, fail-closed) — must match to pass; a crash ortruncated output with no success line reports failed. Used by esbmc/cbmc.
failure(optional, gate) — a match forces failure; covers verifiers whosefailures don't surface as issues by default (Kani without
--trace). Used byclang/kani/pytest.
The three are independent gates, so a miss in one is caught by another (a failure
whose pattern was missed is still caught if it produced an error issue, and vice
versa) — closing the fail-open that a single signal left open.
Behaviour is preserved across every regression fixture. Adds parser-level unit tests
for the verdict matrix (data-driven, success fail-closed, failure gate, error-issue
backstop, both patterns).