KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
41 stars 24 forks source link

Nicer error message for parse errors #3417

Closed FliegendeWurst closed 4 months ago

FliegendeWurst commented 5 months ago

Intended Change

3406 leads to user-facing ParseCancellationExceptions, which are not debuggable. This PR enhances the user experience by actually showing the error in the context of the input file, and listing the found token and the expected token types. Previously, only the class name of the exception was displayed.

Type of pull request

Ensuring quality

missing_semicolon.key

\rules {
   missingSemicolon {
      \find(0=0)
      \replacewith(1=1)
  }
}

\problem { 0=0 }

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

codecov[bot] commented 5 months ago

Codecov Report

Attention: 11 lines in your changes are missing coverage. Please review.

Comparison is base (1fb0c10) 37.77% compared to head (4d3b3ad) 37.78%.

Files Patch % Lines
...main/java/de/uka/ilkd/key/util/ExceptionTools.java 72.50% 9 Missing and 2 partials :warning:
Additional details and impacted files ```diff @@ Coverage Diff @@ ## main #3417 +/- ## ============================================ + Coverage 37.77% 37.78% +0.01% - Complexity 17031 17037 +6 ============================================ Files 2076 2076 Lines 126950 126992 +42 Branches 21381 21387 +6 ============================================ + Hits 47952 47981 +29 - Misses 73092 73102 +10 - Partials 5906 5909 +3 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

MarcoScaletta commented 5 months ago

\rules { wrongTypeSchemaVar { \schemaVar update x, x2; \find(0=0) \replacewith(1=1) }; }

\problem { true }

FliegendeWurst commented 5 months ago

I added another case that handles your problematic input.