Merge branch 'weigl/key-javaparser3' of https://github.com/KeYProject/key into weigl/key-javaparser3

Author: Drodt

key.core/src/test/resources/testcase/classpath/classpath.key

@@ -3,12 +3,17 @@
 \classpath "classpath";
 \javaSource "javaSource";
 
+\programVariables {
+  cp.E x;
+}
 
 // referencing both classpath and javaSource classes
 \problem {
 
-   \[{ cp.C1.m_C(); cp.C1.m_C1(); }\]true
- & \[{ js.C2.m_C2(); js.C2.m_C1(); js.C2.m_C();}\]true
- & \[{ cp.E x = cp.E.e2; }\]true
+wellFormed(heap)
+==>
+   \<{ cp.C1.field = 42; }\>cp.C1.field = 42
+ & \<{ js.C2.m_C2(); cp.C1.m_C1(); cp.C.m_C(); }\>true
+ & \<{  x = cp.E.e4; }\> x = cp.E.e4
 
 }

key.core/src/test/resources/testcase/classpath/classpath/C.jml

@@ -3,6 +3,9 @@ package cp;
 
 class C {
 
+  /*@ public normal_behaviour
+    @  ensures true;
+    @*/
   public static void m_C();
 
 }

key.core/src/test/resources/testcase/classpath/classpath/C1.java

@@ -3,8 +3,13 @@
 
 public class C1 extends C {
 
+  public static int field; // should not be removed
+    
+  /*@ public normal_behaviour
+    @   ensures true;
+    @*/
   public static void m_C1() {
-    that.is.going.to.be.discarded();
+//    that.is.going.to.be.discarded();
   }
 
 }

key.core/src/test/resources/testcase/classpath/classpath/E.java

@@ -5,7 +5,7 @@
 
 enum E {
   e1(1), e2(20), e3(300);
-  public static final E e4 = e2;
+  public static E e4 = e2;
   E(int i) { }
 }