Artiweb > Pull Request #3152

Test parsing exceptions in JML and Java parsing #3152

Github

Description

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