From 5db4d91b90390c90ae1fbee5e78d0285fae517c8 Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Thu, 16 Jul 2026 23:34:01 +0100 Subject: [PATCH 1/3] refactor: replace success/negate_success with success + failure verdict gates MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- CLAUDE.md | 6 +-- formal_lib/issue_parser.py | 45 ++++++++++++------ formal_lib/specs/base.py | 23 ++++++--- formal_lib/specs/clang.py | 6 ++- formal_lib/specs/kani.py | 27 +++++------ formal_lib/specs/pytest.py | 5 +- tests/test_specs/test_verdict.py | 81 ++++++++++++++++++++++++++++++++ 7 files changed, 152 insertions(+), 41 deletions(-) create mode 100644 tests/test_specs/test_verdict.py diff --git a/CLAUDE.md b/CLAUDE.md index d3396c0..dd92cf1 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -32,9 +32,9 @@ hatch build The library uses a **specification-driven regex parsing** pattern with three layers: -1. **Specs** (`formal_lib/specs/`) — Each verifier backend defines an `IssueRegexSpec` containing regex patterns for extracting issue blocks, error types, messages, severity, and nested `StackTraceRegexSpec`/`CounterexampleRegexSpec` for traces. Specs also define a `success` pattern to determine verification outcome from the output text (with `negate_success` for backends where absence of failure indicates success). Specs are plain dataclass instances (e.g., `esbmc_spec`, `cbmc_spec`, `clang_spec`, `pytest_spec`). Any `block` pattern can be wrapped with `missing_hint("Needs --flag")(pattern)` to annotate it — when the block fails to match and verification failed, the hint is collected into `VerifierOutput.hints` and displayed by the CLI. +1. **Specs** (`formal_lib/specs/`) — Each verifier backend defines an `IssueRegexSpec` containing regex patterns for extracting issue blocks, error types, messages, severity, and nested `StackTraceRegexSpec`/`CounterexampleRegexSpec` for traces. The verification outcome is a data-driven baseline — a run passes when it has no error-severity issue — that a spec can gate with an optional positive `success` pattern (fail-closed: it must match to pass, e.g. ESBMC/CBMC's `VERIFICATION SUCCESSFUL`) and/or a `failure` pattern (a match forces failure — the gate for backends whose failures don't surface as issues by default, e.g. Kani without `--trace`). Specs are plain dataclass instances (e.g., `esbmc_spec`, `cbmc_spec`, `clang_spec`, `pytest_spec`). Any `block` pattern can be wrapped with `missing_hint("Needs --flag")(pattern)` to annotate it — when the block fails to match and verification failed, the hint is collected into `VerifierOutput.hints` and displayed by the CLI. -2. **Parser** (`formal_lib/issue_parser.py`) — `IssueSpecOutputParser` applies a spec's regex hierarchy to raw output: the `success` pattern determines the `successful` flag, the block pattern finds issue boundaries, then field patterns extract structured data from each block. Traces are parsed via a nested block→entry→fields hierarchy. +2. **Parser** (`formal_lib/issue_parser.py`) — `IssueSpecOutputParser` applies a spec's regex hierarchy to raw output: the block pattern finds issue boundaries and field patterns extract structured data from each block, then `_is_successful` computes the `successful` flag from the parsed issues' severities gated by the spec's `success`/`failure` patterns. Traces are parsed via a nested block→entry→fields hierarchy. 3. **Runner** (`formal_lib/verifier_runner.py`) — `VerifierRunner` executes a verifier command, feeds output to the parser, and optionally caches results using content-based hashing (zlib.adler32 + pickle). @@ -52,4 +52,4 @@ The library uses a **specification-driven regex parsing** pattern with three lay ## Adding a New Verifier Backend -Create a new `IssueRegexSpec` instance in `formal_lib/specs/`, including a `success` pattern for determining verification outcome. Wrap any `block` pattern with `missing_hint("Needs --flag")(pattern)` when the verifier requires a specific flag for that data. Export it from `formal_lib/specs/__init__.py`, add it to the `SPECS` dict, and add a CLI flag in `__main__.py`. +Create a new `IssueRegexSpec` instance in `formal_lib/specs/`. The verdict defaults to "no error-severity issue"; add a `success` pattern (positive verdict line) and/or a `failure` pattern (forces failure) only if the backend needs one. Wrap any `block` pattern with `missing_hint("Needs --flag")(pattern)` when the verifier requires a specific flag for that data. Export it from `formal_lib/specs/__init__.py` and add it to the `SPECS` dict (which also registers the `--backend` choice in `__main__.py`). diff --git a/formal_lib/issue_parser.py b/formal_lib/issue_parser.py index 0313bac..0738d19 100644 --- a/formal_lib/issue_parser.py +++ b/formal_lib/issue_parser.py @@ -33,23 +33,18 @@ def parse_output( ) -> VerifierOutput: # Strip ANSI escape codes in case the tool emits colored output. output = ANSI_ESCAPE_PATTERN.sub("", output) - - # Determine success from the spec's success pattern. spec = self.regex_spec - if spec.success: - matched = bool(re.search(spec.success, output, re.MULTILINE)) - successful = not matched if spec.negate_success else matched - else: - successful = True - - # Extract all issue blocks from the output - issue_blocks: list[str] = [] - for match in re.finditer(spec.block, output, re.DOTALL | re.MULTILINE): - issue_blocks.append(match.group(0)) - - # Parse each issue block to extract individual issues + + # Extract issue blocks, then parse each into an issue. The verdict's + # data-driven baseline reads issue severities, so issues are parsed first. + issue_blocks: list[str] = [ + match.group(0) + for match in re.finditer(spec.block, output, re.DOTALL | re.MULTILINE) + ] issues: list[Issue] = [self._parse_issue(block) for block in issue_blocks] + successful = self._is_successful(output, issues) + # Collect hints from annotated blocks that failed to match. hints: list[str] = [] if not successful and not issues: @@ -65,6 +60,28 @@ def parse_output( hints=hints, ) + def _is_successful(self, output: str, issues: list[Issue]) -> bool: + """Determine the verdict from a data-driven baseline gated by the spec's + optional ``success`` / ``failure`` patterns. + + The run passed iff there is no error-severity issue AND — when the spec + provides them — the positive ``success`` pattern matched and the ``failure`` + pattern did not. Warning/info issues never flip the verdict. The three + checks are independent gates, so a miss in one (a failure whose pattern + didn't match, or one the issue extractor dropped) is still caught by + another; only a simultaneous miss reports a false success. + """ + spec = self.regex_spec + if any(issue.severity == "error" for issue in issues): + return False + if spec.success is not None and not re.search( + spec.success, output, re.MULTILINE + ): + return False + if spec.failure is not None and re.search(spec.failure, output, re.MULTILINE): + return False + return True + @staticmethod def _get_hint(pattern: str) -> str: return pattern.hint if isinstance(pattern, AnnotatedPattern) else "" diff --git a/formal_lib/specs/base.py b/formal_lib/specs/base.py index d389dd8..7e28c65 100644 --- a/formal_lib/specs/base.py +++ b/formal_lib/specs/base.py @@ -243,12 +243,23 @@ class IssueRegexSpec: header (e.g. ESBMC's ``Violated property:`` block, clang's diagnostic header). When set, ``Issue`` properties prefer this location over the stack trace's last frame.""" - success: str = "" - """Regex pattern for determining verification success from output text. - Matched with re.MULTILINE against the full output.""" - negate_success: bool = False - """When False, a match means success. When True, a match means failure - (i.e. success is the absence of the pattern).""" + success: str | None = None + """Regex whose match confirms the run PASSED — a positive verdict line such as + ESBMC/CBMC's ``VERIFICATION SUCCESSFUL``. ``None`` means the verifier has no + positive success signal, so this gate is skipped. Matched with re.MULTILINE. + + The verdict is fail-closed on this gate: when set and it does *not* match, the + run is reported as failed.""" + failure: str | None = None + """Regex whose match forces the verdict to FAILED. Use it for verifiers with no + positive success signal, or whose failures don't always surface as issues (e.g. + Kani run without ``--trace``) so the pattern gates those cases. ``None`` skips it. + Matched with re.MULTILINE. + + ``success`` and ``failure`` are independent gates layered on the data-driven + baseline (see :meth:`IssueSpecOutputParser._is_successful`): a run passes iff it + has no error-severity issue, ``success`` (if set) matched, and ``failure`` (if + set) did not.""" cache_properties: CachePropertiesFn | None = field(default=None) """Optional function to compute cache properties from verify_source args. When None, default properties are used.""" diff --git a/formal_lib/specs/clang.py b/formal_lib/specs/clang.py index b8360ed..83f7093 100644 --- a/formal_lib/specs/clang.py +++ b/formal_lib/specs/clang.py @@ -5,8 +5,10 @@ clang_spec: IssueRegexSpec = IssueRegexSpec( # Detect clang/gcc diagnostics by the "file:line:col: error/warning:" pattern. detect=r"^[^\s:]+:\d+:\d+:\s+(?:error|warning):", - success=r":\d+:\s+error:", - negate_success=True, + # No positive success signal (a clean compile is silent), so the verdict is the + # failure pattern — an `error:` diagnostic — plus the parser's error-issue + # baseline. Warnings are issues but never fail the build. + failure=r":\d+:\s+error:", # Each diagnostic is a block: "file:line:col: type: message\n\n" # Match the diagnostic line plus optional following source/indicator lines. block=r"^[^\s:]+:\d+:\d+:\s+(?:error|warning):[^\n]*\n(?:[^\n]*\n[^\s:]*[~^ ]*\n?)?", diff --git a/formal_lib/specs/kani.py b/formal_lib/specs/kani.py index 1f8fa87..18dd7f8 100644 --- a/formal_lib/specs/kani.py +++ b/formal_lib/specs/kani.py @@ -32,23 +32,22 @@ def _kani_message(value: str) -> str: cbmc_spec, # Kani prints its own banner above CBMC's; detect on that. detect=r"^Kani Rust Verifier", - # Derive the verdict from the per-check statuses in CBMC's `** Results:` section, - # NOT the top-line `VERIFICATION` verdict. In old format Kani does not post-process - # its assertion-reachability probes, so a *passing* run still prints `VERIFICATION - # FAILED`: each `reachability_check` property "fails" precisely because the assertion - # is reachable (normal). Keying off the real per-check statuses lets Kani keep - # reachability checks enabled — they catch unreachable, vacuously-passing assertions, - # so disabling them would weaken verification — while still reporting correctly. - # - # negate_success: a match means FAILURE. A real failure is either a `** Results:` - # line for a non-`reachability_check` check with status FAILURE, or the native-format - # `VERIFICATION:- FAILED` line (native format has no such Results lines and is already - # correctly post-processed by Kani, so its verdict line is trustworthy). - success=( + # Kani has no positive success line in old format — a *passing* run still prints + # `VERIFICATION FAILED`, because Kani does not post-process its assertion-reachability + # probes there (each `reachability_check` "fails" precisely because the assertion is + # reachable, which is normal). So clear the `success` pattern inherited from cbmc_spec + # and derive the verdict from a `failure` pattern over the per-check statuses instead. + # This lets Kani keep reachability checks enabled — they catch unreachable, + # vacuously-passing assertions, so disabling them would weaken verification. + success=None, + # A match means FAILED: either a `** Results:` line for a non-`reachability_check` + # check with status FAILURE, or the native-format `VERIFICATION:- FAILED` line (native + # format has no such Results lines and is already correctly post-processed by Kani). + # The pattern also gates the no-`--trace` case, where a failure produces no issues. + failure=( r"^\[[^\]]*\.(?!reachability_check\.)[A-Za-z][\w-]*\.\d+\][^\n]*: FAILURE$" r"|^VERIFICATION:- FAILED$" ), - negate_success=True, # Same trace-block boundaries as CBMC, with two Kani adjustments: # * skip the `reachability_check` properties Kani injects (its native format # hides them; they are not real bugs), and diff --git a/formal_lib/specs/pytest.py b/formal_lib/specs/pytest.py index 3a801d2..a48ae19 100644 --- a/formal_lib/specs/pytest.py +++ b/formal_lib/specs/pytest.py @@ -24,8 +24,9 @@ def _pytest_cache_properties( pytest_spec: IssueRegexSpec = IssueRegexSpec( # Detect pytest by its distinctive session header. detect=r"^={5,} test session starts ={5,}$", - success=r"(?:FAILED|ERROR)", - negate_success=True, + # pytest has no reliable positive success line (a summary can mix passed with + # failed/error), so the verdict is the failure pattern plus the error-issue baseline. + failure=r"(?:FAILED|ERROR)", # Match both collection ERROR blocks and test FAILURE blocks # Test failure: "_____ test_name _____" (underscores, space, identifier, space, underscores) # Collection error: "_____ ERROR collecting path _____" diff --git a/tests/test_specs/test_verdict.py b/tests/test_specs/test_verdict.py new file mode 100644 index 0000000..da90da4 --- /dev/null +++ b/tests/test_specs/test_verdict.py @@ -0,0 +1,81 @@ +# Author: Yiannis Charalambous + +"""Tests for the verdict logic in IssueSpecOutputParser._is_successful. + +The verdict is a data-driven baseline (no error-severity issue) gated by the spec's +optional `success` (positive, fail-closed) and `failure` (gate) patterns. These use a +tiny synthetic spec: a line `ISSUE ` becomes one issue of that severity, and +`PASS` / `FAIL` markers drive the patterns. +""" + +from formal_lib import IssueSpecOutputParser +from formal_lib.specs.base import IssueRegexSpec, StackTraceRegexSpec + +# A stack-trace spec whose block never matches, so issues have an empty stack trace. +_NO_TRACE = StackTraceRegexSpec( + block=r"ZZZ_NOMATCH", trace_entry=r"ZZZ", trace_index=r"ZZZ", + path=r"ZZZ", name=r"ZZZ", line_index=r"ZZZ", +) + + +def _verdict(output: str, *, success: str | None = None, failure: str | None = None) -> bool: + spec = IssueRegexSpec( + block=r"^ISSUE \w+$", + error_type=r"^(ISSUE)", + message=r"^ISSUE (\w+)", + severity=r"^ISSUE (\w+)", + stack_trace_spec=_NO_TRACE, + success=success, + failure=failure, + ) + return IssueSpecOutputParser(spec).parse_output(output).successful + + +# --- data-driven baseline (no patterns) --- + +def test_no_patterns_error_issue_fails() -> None: + assert _verdict("ISSUE error") is False + + +def test_no_patterns_warning_issue_passes() -> None: + """A warning-severity issue must not flip the verdict.""" + assert _verdict("ISSUE warning") is True + + +def test_no_patterns_no_issue_passes() -> None: + assert _verdict("nothing to see") is True + + +# --- success pattern: positive confirmation, fail-closed --- + +def test_success_pattern_must_match_to_pass() -> None: + assert _verdict("PASS", success=r"PASS") is True + # No match -> failed, even with no issues (fail-closed on garbage/crash output). + assert _verdict("truncated output", success=r"PASS") is False + + +def test_success_pattern_overridden_by_error_issue() -> None: + """Even if the success line matched, an error issue means not successful.""" + assert _verdict("PASS\nISSUE error", success=r"PASS") is False + + +# --- failure pattern: the gate for no-issue failures --- + +def test_failure_pattern_gates_a_failure_with_no_issues() -> None: + """The key case the data-driven baseline can't see: a failure that produced no + issues (e.g. Kani without --trace) is still caught by the failure pattern.""" + assert _verdict("FAIL", failure=r"FAIL") is False + assert _verdict("all clear", failure=r"FAIL") is True + + +def test_error_issue_catches_a_missed_failure_pattern() -> None: + """The independent gates close the fail-open: if the failure pattern misses but + the failure surfaced as an error issue, the run is still reported as failed.""" + assert _verdict("ISSUE error", failure=r"FAIL") is False + + +# --- both patterns --- + +def test_both_patterns_failure_wins() -> None: + assert _verdict("PASS", success=r"PASS", failure=r"FAIL") is True + assert _verdict("PASS\nFAIL", success=r"PASS", failure=r"FAIL") is False From 4f06931d0e7244cdabd6641b07ff42825afde617 Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Thu, 16 Jul 2026 23:43:58 +0100 Subject: [PATCH 2/3] test: add clang verdict fixtures and severity verdict cases 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). --- .../samples/clang/undeclared_error.json | 20 +++++++++++++++++++ .../samples/clang/undeclared_error.log | 5 +++++ .../clang/unused_variable_warning.json | 20 +++++++++++++++++++ .../samples/clang/unused_variable_warning.log | 4 ++++ tests/test_specs/test_verdict.py | 11 ++++++++++ 5 files changed, 60 insertions(+) create mode 100644 tests/regressions/samples/clang/undeclared_error.json create mode 100644 tests/regressions/samples/clang/undeclared_error.log create mode 100644 tests/regressions/samples/clang/unused_variable_warning.json create mode 100644 tests/regressions/samples/clang/unused_variable_warning.log diff --git a/tests/regressions/samples/clang/undeclared_error.json b/tests/regressions/samples/clang/undeclared_error.json new file mode 100644 index 0000000..da397d8 --- /dev/null +++ b/tests/regressions/samples/clang/undeclared_error.json @@ -0,0 +1,20 @@ +{ + "successful": false, + "issues": [ + { + "error_type": "error", + "message": "\u2018zzz\u2019 undeclared (first use in this function)", + "stack_trace": [ + { + "trace_index": 0, + "path": "err.c", + "name": null, + "line_idx": 0 + } + ], + "severity": "error", + "error_location": null + } + ], + "duration": 0.0 +} diff --git a/tests/regressions/samples/clang/undeclared_error.log b/tests/regressions/samples/clang/undeclared_error.log new file mode 100644 index 0000000..cd58211 --- /dev/null +++ b/tests/regressions/samples/clang/undeclared_error.log @@ -0,0 +1,5 @@ +err.c: In function ‘main’: +err.c:1:23: error: ‘zzz’ undeclared (first use in this function) + 1 | int main(void){return zzz;} + | ^~~ +err.c:1:23: note: each undeclared identifier is reported only once for each function it appears in diff --git a/tests/regressions/samples/clang/unused_variable_warning.json b/tests/regressions/samples/clang/unused_variable_warning.json new file mode 100644 index 0000000..cd66756 --- /dev/null +++ b/tests/regressions/samples/clang/unused_variable_warning.json @@ -0,0 +1,20 @@ +{ + "successful": true, + "issues": [ + { + "error_type": "warning", + "message": "unused variable \u2018x\u2019 [-Wunused-variable]", + "stack_trace": [ + { + "trace_index": 0, + "path": "warn.c", + "name": null, + "line_idx": 0 + } + ], + "severity": "warning", + "error_location": null + } + ], + "duration": 0.0 +} diff --git a/tests/regressions/samples/clang/unused_variable_warning.log b/tests/regressions/samples/clang/unused_variable_warning.log new file mode 100644 index 0000000..3b76193 --- /dev/null +++ b/tests/regressions/samples/clang/unused_variable_warning.log @@ -0,0 +1,4 @@ +warn.c: In function ‘main’: +warn.c:1:20: warning: unused variable ‘x’ [-Wunused-variable] + 1 | int main(void){int x; return 0;} + | ^ diff --git a/tests/test_specs/test_verdict.py b/tests/test_specs/test_verdict.py index da90da4..b3327eb 100644 --- a/tests/test_specs/test_verdict.py +++ b/tests/test_specs/test_verdict.py @@ -42,10 +42,19 @@ def test_no_patterns_warning_issue_passes() -> None: assert _verdict("ISSUE warning") is True +def test_no_patterns_info_issue_passes() -> None: + assert _verdict("ISSUE info") is True + + def test_no_patterns_no_issue_passes() -> None: assert _verdict("nothing to see") is True +def test_mixed_warning_and_error_fails() -> None: + """A single error-severity issue fails the run even alongside non-error issues.""" + assert _verdict("ISSUE warning\nISSUE error") is False + + # --- success pattern: positive confirmation, fail-closed --- def test_success_pattern_must_match_to_pass() -> None: @@ -77,5 +86,7 @@ def test_error_issue_catches_a_missed_failure_pattern() -> None: # --- both patterns --- def test_both_patterns_failure_wins() -> None: + """When a spec sets BOTH patterns (no shipping spec does today, but the API + allows it), the failure gate wins over a matching success line.""" assert _verdict("PASS", success=r"PASS", failure=r"FAIL") is True assert _verdict("PASS\nFAIL", success=r"PASS", failure=r"FAIL") is False From 52afa202dc81bc9d2a5ed901fca73b7434feb290 Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Thu, 16 Jul 2026 23:51:42 +0100 Subject: [PATCH 3/3] refactor: drop redundant clang failure pattern, trim duplicated docstrings MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit /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. --- formal_lib/issue_parser.py | 16 +++++++--------- formal_lib/specs/base.py | 15 +++++---------- formal_lib/specs/clang.py | 7 +++---- tests/test_specs/test_verdict.py | 8 ++------ 4 files changed, 17 insertions(+), 29 deletions(-) diff --git a/formal_lib/issue_parser.py b/formal_lib/issue_parser.py index 0738d19..b1c48ce 100644 --- a/formal_lib/issue_parser.py +++ b/formal_lib/issue_parser.py @@ -61,15 +61,13 @@ def parse_output( ) def _is_successful(self, output: str, issues: list[Issue]) -> bool: - """Determine the verdict from a data-driven baseline gated by the spec's - optional ``success`` / ``failure`` patterns. - - The run passed iff there is no error-severity issue AND — when the spec - provides them — the positive ``success`` pattern matched and the ``failure`` - pattern did not. Warning/info issues never flip the verdict. The three - checks are independent gates, so a miss in one (a failure whose pattern - didn't match, or one the issue extractor dropped) is still caught by - another; only a simultaneous miss reports a false success. + """Return whether the run passed: no error-severity issue, and — when the + spec sets them — the ``success`` pattern matched and the ``failure`` pattern + did not. Warning/info issues never flip the verdict. + + The error-issue baseline and the ``failure`` pattern are independent failure + signals, so a failure missed by one is still caught by the other; ``success`` + is a fail-closed positive requirement (its absence fails the run). """ spec = self.regex_spec if any(issue.severity == "error" for issue in issues): diff --git a/formal_lib/specs/base.py b/formal_lib/specs/base.py index 7e28c65..739c010 100644 --- a/formal_lib/specs/base.py +++ b/formal_lib/specs/base.py @@ -245,21 +245,16 @@ class IssueRegexSpec: stack trace's last frame.""" success: str | None = None """Regex whose match confirms the run PASSED — a positive verdict line such as - ESBMC/CBMC's ``VERIFICATION SUCCESSFUL``. ``None`` means the verifier has no - positive success signal, so this gate is skipped. Matched with re.MULTILINE. - - The verdict is fail-closed on this gate: when set and it does *not* match, the - run is reported as failed.""" + ESBMC/CBMC's ``VERIFICATION SUCCESSFUL``. Fail-closed: when set and it does not + match, the run is reported as failed. ``None`` skips this gate. re.MULTILINE.""" failure: str | None = None """Regex whose match forces the verdict to FAILED. Use it for verifiers with no positive success signal, or whose failures don't always surface as issues (e.g. Kani run without ``--trace``) so the pattern gates those cases. ``None`` skips it. - Matched with re.MULTILINE. + re.MULTILINE. - ``success`` and ``failure`` are independent gates layered on the data-driven - baseline (see :meth:`IssueSpecOutputParser._is_successful`): a run passes iff it - has no error-severity issue, ``success`` (if set) matched, and ``failure`` (if - set) did not.""" + ``success`` and ``failure`` layer on the data-driven baseline; see + :meth:`IssueSpecOutputParser._is_successful` for how the three combine.""" cache_properties: CachePropertiesFn | None = field(default=None) """Optional function to compute cache properties from verify_source args. When None, default properties are used.""" diff --git a/formal_lib/specs/clang.py b/formal_lib/specs/clang.py index 83f7093..4d8dcf1 100644 --- a/formal_lib/specs/clang.py +++ b/formal_lib/specs/clang.py @@ -5,10 +5,9 @@ clang_spec: IssueRegexSpec = IssueRegexSpec( # Detect clang/gcc diagnostics by the "file:line:col: error/warning:" pattern. detect=r"^[^\s:]+:\d+:\d+:\s+(?:error|warning):", - # No positive success signal (a clean compile is silent), so the verdict is the - # failure pattern — an `error:` diagnostic — plus the parser's error-issue - # baseline. Warnings are issues but never fail the build. - failure=r":\d+:\s+error:", + # No verdict pattern: a clang `error:` diagnostic is extracted as an error-severity + # issue, so the parser's data-driven baseline already fails the run. Warnings are + # issues too, but severity "warning", so they never fail the build. # Each diagnostic is a block: "file:line:col: type: message\n\n" # Match the diagnostic line plus optional following source/indicator lines. block=r"^[^\s:]+:\d+:\d+:\s+(?:error|warning):[^\n]*\n(?:[^\n]*\n[^\s:]*[~^ ]*\n?)?", diff --git a/tests/test_specs/test_verdict.py b/tests/test_specs/test_verdict.py index b3327eb..0e90d31 100644 --- a/tests/test_specs/test_verdict.py +++ b/tests/test_specs/test_verdict.py @@ -2,10 +2,8 @@ """Tests for the verdict logic in IssueSpecOutputParser._is_successful. -The verdict is a data-driven baseline (no error-severity issue) gated by the spec's -optional `success` (positive, fail-closed) and `failure` (gate) patterns. These use a -tiny synthetic spec: a line `ISSUE ` becomes one issue of that severity, and -`PASS` / `FAIL` markers drive the patterns. +Uses a tiny synthetic spec: a line ``ISSUE `` becomes one issue of that +severity, and ``PASS`` / ``FAIL`` markers drive the ``success`` / ``failure`` patterns. """ from formal_lib import IssueSpecOutputParser @@ -38,7 +36,6 @@ def test_no_patterns_error_issue_fails() -> None: def test_no_patterns_warning_issue_passes() -> None: - """A warning-severity issue must not flip the verdict.""" assert _verdict("ISSUE warning") is True @@ -51,7 +48,6 @@ def test_no_patterns_no_issue_passes() -> None: def test_mixed_warning_and_error_fails() -> None: - """A single error-severity issue fails the run even alongside non-error issues.""" assert _verdict("ISSUE warning\nISSUE error") is False