Repository navigation
verify: Report each conversion error at its source, with its line and caret - #47
Merged
Merged
Conversation
…e being converted.
…r expression it is about.
…s JSON record the range.
This was referenced Oct 20, 2026
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 join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
An error about a construct the verifier does not represent named only the function:
In a file with several functions, or a function with several
switches, the user had to find the construct themselves. The converter recorded its 189 error sites as plain strings (std::vector<std::string> Errors), so no location was available to print.The change gives every conversion error a source range and prints it as a compiler error is:
ASTConverterkeepsCurrentRange, the range of the innermost declaration, statement, or expression being converted.convertFunction,convertStmt, andconvertExprset it withllvm::SaveAndRestore, anderror(Message)records it. Each site therefore points at what it is about without being edited one by one. Sites outside the conversion of a function name their place: a member function's or template's declaration, and for the checks made after every function is converted (recursion without a measure, mutual recursion, an inductive predicate reached through another spec), the function's declaration.expandInductivePredicatesreports through a callback with a location, the predicate'scppverify::inductivemarker, instead of appending strings to the converter's list.Transform/takes no dependency on the converter.TextDiagnostic, into its own stream rather than through theDiagnosticsEngine. Verification at compile time runs on another thread, and the engine is not thread-safe. It uses presumed locations, as Clang's driver does, so#lineis honored. The JSON record carries the start and end of the range.The message text is unchanged; saying in C++ terms what is unsupported is the second half of E2.
Docs: the tooling page shows the error with its line and caret, as a checked
rejectsexample, and says where whole-function errors point. ARCHITECTURE describes the mechanism, and the release notes get an entry under "Running cpp-verify".Testing:
Verify/located_errors.cppchecks, with--strict-whitespace, the location, line, and caret of five errors: a statement (switch), a member function, a misplaced[[cppverify::trusted]], a non-bool inductive predicate, and a recursion without a measure, which is reported after conversion. It also checks the JSON record of the first. Both RUN lines fail on main. Three mutations fail it: no range for statements, no location for the checks made after conversion, and the old one-line printing.Over all 396 Verify sources, converted with
--lower-only, no converter error prints without a location now. Four other errors still do. Three arevalidmarker errors fromUBChecks(valid marker must be a positive top-level conjunction clause, and two like it), and one is the reads check's error for a callee without a reads clause. Locating them changesUBChecks, which #40 changes too, so they follow once it merges.Checked: the Verify suite passes in a release build and in a build with assertions (424 with the new test, 1 unsupported), as do the documentation examples and the site build with
-W. A verdict differential against main over 431 Verify sources (the ULEB128 exhaustive decoder left out, as it has no error path) changes no verdict and no time; the new test's errors are errors on main too, without their locations.