Test parsing exceptions in JML and Java parsing #3152
JML parsing and error reporting is not yet ideal, we should fix these case. They can also serve as valuable test cases for future replacement frameworks.
This also fixes a bug in the position treatement of Recoder2KeY.
From the javadoc:
This test case is used to ensure that errors in JML (and perhaps also in Java) are reported with a reasonable error message and the right position pointing into the file. To add a test case, locate the "exceptional" directory in the resources (below the directory for this package here) and add your single Java file that contains an error that should be presented to the user (like syntax error, unresolved names, ...) The first lines of the Java file may contain meta data on what to expect from the exception.
- introducing exceptional JML tests
- more test cases for exceptional jml cases
- fixing an NPE bug in the error reporting of Recoder2KeY
- spotless and documentation
Artifacts
- 31. May 2023 13:33 (29984.86 kB large)
- 31. May 2023 12:53 (29986.77 kB large)
- 31. May 2023 12:09 (29986.32 kB large)
- 31. May 2023 11:08 (8012.80 kB large)
- 31. May 2023 09:14 (8008.36 kB large)
- 31. May 2023 09:06 (8008.71 kB large)
- 31. May 2023 09:03 (7964.90 kB large)