Migrate to JMLtk

[wadoon]

Intended Change

With this PR, wadoon/key-javaparser becomes obsolete in favour of the JMLtk fork!

This PR does not

• use JMLtk to parse JML.
• use JML-AST classes.

Regressions:

• Positioning on invalid ExpressionStmt (int x = ;)

Changes to key-javaparser

• JML modifiers are printed escaped => (/*@ ghost */ int x;)
• KeyRangeExpression gone
• KeyMarkerStatement gone
• Consistent names are in favour of JavaParser (e.g., XStatement vs. XStmt)

Plan

Things to do after review:

• decide when to make JMLtk first release

  • update K counter on JMLtk

• discuss sacrifices in JMLtk for KeY compat:
  /*@ghost*/ int #x; vs. ghost int #x;

• How to proceed further with exchanging JML parsing

Type of pull request

• Refactoring (behaviour should not change or only minimally change)

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I have tested the feature as follows: unit-tests

[wadoon]

Squash before merge

[unp1]

Thanks! I think all the mentioned issues are just one comment. Otherwise the changes to error reporting seem to be a regression in the reported position, so we should fix that position reporting not the tests. I'll look into that myself.

[unp1]

Improved the position recording slightly. But the parser now reports "int" as last successfull token and no longer "=", so the position is no longer as precise as before where the dialog underlined the empty space after '='

[unp1]

Sorry my fault, restored to open.

First pushed to the wrong branch due to a typo jmtk and then deleted the correct one....
Nothing got lost everything restored

[wadoon]

The question is rather: Can we get rid of the stupid ghost and model modifier on Java-level?
See here: https://github.com/jmltoolkit/jmltk/blob/168dfa039c2d26582e57450c7029da434242daa8/javaparser-key-testing/src/test/java/com/github/javaparser/ast/key/GhostTest.java

Correctly, it should be /@ghost int x;*/ as the whole thing has JML semantics.
To be clearly, /*@ ghost #t #a = #se;*/ should be translated into /*@ ghost #t #a;*/ /*ghost #a = #se; */.

[unp1]

The question is rather: Can we get rid of the stupid ghost and model modifier on Java-level? See here: https://github.com/jmltoolkit/jmltk/blob/168dfa039c2d26582e57450c7029da434242daa8/javaparser-key-testing/src/test/java/com/github/javaparser/ast/key/GhostTest.java

Correctly, it should be /@ghost int x;*/ as the whole thing has JML semantics. To be clearly, /*@ ghost #t #a = #se;*/ should be translated into /*@ ghost #t #a;*/ /*ghost #a = #se; */.

I assume you mean /*@ ghost #t #a;*/ /*@ set #a = #se; */? But yes, it would be better if JML is not on the Java level.

[unp1]

Thanks a lot. Fine from my side. Only question if you want to have a second review from someone else in addition.

[wadoon]

Thanks a lot. Fine from my side. Only question if you want to have a second review from someone else in addition.

We need to have a discussion on the needed ghost modifier at the Java level.

In JMLtk, I have the syntax /*@ ghost <stmt>; */ on the statement level. The following is valid:

public void foo() {
  //@ ghost int x = e;
  //@ ghost if(x>2) x = -2;
  //@       else    x =  1/0;
}

Allowing JML in Taclets would now allow writing Taclets specific to ghost code, i.e., appropriate handling of exceptions (WD problem).

All in all, ghost should not be considered as a Java modifier for long in JMLtk.