Merge remote-tracking branch 'origin/master' into grebingWeigl/ExploreGradle

# By Alexander Weigl (167) and others
# Via Alexander Weigl (46) and others
* origin/master: (231 commits)
  reenabled pruning in closed branches
  fix for #1480: set pruned/reopened goal back to interactive mode
  fix for #1551: escaping in filenames
  made the code more readable (SonarQube suggestion)
  Fix smells reported by Sonarcube
  Fix checkstyle
  repaired file information if a directory is opened in KeY
  repaired file information a directory is opened in KeY
  Fix proof loading in the CLI
  make ExceptionDialog able to show files in Jar files
  catch headless to make key --auto runnable again
  made tooltip, click detection, and area to change mouse cursor more precise
  checkstyle
  tooltip and hand cursor only appear if the mouse pointer is over the highlight (probably needs optimization performance-wise)
  add option to toggle SourceView tooltip, change mouse pointer over highlightings to hand, shorter tooltip
  swap lines in gitlab ci, such that sonarqube is always reported
  Fix \singleton(3)
  JML-Extension: Assert/Assume and *_free for block contracts
  Better exception message in JML parser
  Renovating the Jml Parser
  ...

# Conflicts:
#	.gitlab-ci.yml
#	key/key.core/src/main/java/de/uka/ilkd/key/logic/Term.java
#	key/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java
#	key/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLTranslator.java
#	key/key.ui/build.gradle
#	key/settings.gradle

.gitlab-ci.yml

@@ -64,7 +64,7 @@ compile:testClasses8:
   script:
     - javac -version
     - cd key
-    - gradle --parallel classes testClasses
+    - gradle --parallel clean classes testClasses
 
 sonarqube:
   dependencies:  ["compile:testClasses"]
@@ -73,6 +73,7 @@ sonarqube:
   allow_failure: true
   script:
     - cd key
+    - ./scripts/tools/sonarqube_hint.py
     - gradle --build-cache --continue -Dsonar.qualitygate.wait=true -DjacocoEnabled=true testFast sonarqube
   only:
     - merge_requests
@@ -93,12 +94,13 @@ checkstyle:
   image: wadoon/key-test-docker:jdk11
   allow_failure: true
   script:
-    - echo "**** Check the commit's gitlab page for a readable checkstyle report ****"
     - (key/scripts/tools/checkstyle/runIncrementalCheckstyle.sh | tee report.txt) || true
-    - key/scripts/tools/checkstyle/publishAudit.py report.txt
+    - key/scripts/tools/checkstyle/translateAudit.py report.txt > report.json
   artifacts:
     name: "checkstyle-report-$CI_JOB_ID"
-    expire_in: 1 year
-    when: always
     paths:
-    - report.txt
\ No newline at end of file
+      - report.txt
+    when: always
+    reports:
+      codequality: report.json
+    expire_in: 1 year

.gitlab/issue_templates/Bug.md

-<!-- KEY BUG REPORT  /label ~Bug 
+<!-- 
      Thank you for taking your time to make KeY a better tool!
-     Please replace the blockquotes below with your answered.
+     Please replace the quoted lines (`> ...`) below with your text.
 --> 
 
 ## Description
@@ -28,17 +28,14 @@
 
 ---
 
-* Commit: <!-- SHA checksum of the git commit -->
+* Commit: <!-- SHA checksum of the git commit where you observed the problem-->
 
-<!-- KeY Component
- Information Flow Engine, Calculus, Soundness, JML Parser,
- JML (Semantics), GUI, Counter Example Generator, KeY Parser, Deployment
- Prover Core, SMT, Symb. Debugger, Test Case Generator, Proof Loading/Saving,
- Command Line Interface, Strategy, Test cases, RIFL, Documentation, Webpage
+<!--
+  From the "labels" selection component below this textfield, please select appropriate labels:
+  * If you think this is a "bug" that should be fixed, please select Bug.
+  * Please select exactly one of the priority labels:  P:LOW, P:NORMAL, P:HIGH or P:URGENT.
+  * Please select those components (0, 1 or more) to which this issue refers 
+    (the labels with lilac background)
 -->
-* Component: /label ~Calculus 
-
-<!-- Please select one severity level -->
-/label ~LOW ~NORMAL ~HIGH ~URGENT 
 
 <!-- END OF BUG TEMPLATE -->

key/README.md

 # KeY -- Deductive Java Program Verifier
 
+[![Bugs](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=bugs)](https://sonarcloud.io/dashboard?id=key-main) [![Code Smells](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=code_smells)](https://sonarcloud.io/dashboard?id=key-main) [![Coverage](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=coverage)](https://sonarcloud.io/dashboard?id=key-main) [![Duplicated Lines (%)](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=duplicated_lines_density)](https://sonarcloud.io/dashboard?id=key-main) [![Lines of Code](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=ncloc)](https://sonarcloud.io/dashboard?id=key-main) [![Maintainability Rating](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=sqale_rating)](https://sonarcloud.io/dashboard?id=key-main) [![Quality Gate Status](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=alert_status)](https://sonarcloud.io/dashboard?id=key-main) [![Reliability Rating](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=reliability_rating)](https://sonarcloud.io/dashboard?id=key-main) [![Security Rating](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=security_rating)](https://sonarcloud.io/dashboard?id=key-main) [![Technical Debt](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=sqale_index)](https://sonarcloud.io/dashboard?id=key-main) [![Vulnerabilities](https://sonarcloud.io/api/project_badges/measure?project=key-main&metric=vulnerabilities)](https://sonarcloud.io/dashboard?id=key-main)
+
 This folder contains the interactive theorem prover KeY for the verification of Java programs.
 
-You can find more information on KeY on our [website](https://key-project.org) or in use the 
+You can find more information on KeY on our [website](https://key-project.org) or in use the
 documentation in the companion repository [key-docs](https://git.key-project.org/key/key-docs).
 
-The current version is 2.8.0, licensed under GPL v2. 
+The current version is 2.8.0, licensed under GPL v2.
 
 
-## Requirements: 
+## Requirements:
 
 * Hardware: >=2 GB RAM
 * Operating System: Linux/Unix, MacOSX, Windows
 * Java SE 8 or newer
 * Optionally, KeY can make use of the following binaries:
-  * SMT Solvers: 
-    * [Z3](https://github.com/Z3Prover/z3) 
-    * [CVC4](http://cvc4.cs.stanford.edu/web/) 
+  * SMT Solvers:
+	* [Z3](https://github.com/Z3Prover/z3)
+	* [CVC4](http://cvc4.cs.stanford.edu/web/)
 
 ## Content of the KeY folder
 
-This folder provides a [gradle](https://gradle.org)-managed project following 
+This folder provides a [gradle](https://gradle.org)-managed project following
 [Maven's standard folder layout](https://maven.apache.org/guides/introduction/introduction-to-the-standard-directory-layout.html).
-There are several modules in this folder. In general every `key.*/` contains a core component of KeY. Additional 
-and optional components are in `keyext.*/` folders. The file `build.gradle` is the root build script describing 
+There are several modules in this folder. In general every `key.*/` contains a core component of KeY. Additional
+and optional components are in `keyext.*/` folders. The file `build.gradle` is the root build script describing
 the dependencies and build tasks for all sub-modules.
 
-`key.util`, `key.core` and `key.ui` are the base for the product "KeY Prover". Special care are needed 
-if you plan to make changes here. 
+`key.util`, `key.core` and `key.ui` are the base for the product "KeY Prover". Special care are needed
+if you plan to make changes here.
 
 
 ## Compile and Run KeY
 
-Assuming you are in directory `key/`, the directory of this README file, 
+Assuming you are in directory `key/`, the directory of this README file,
 then you can create a runnable and deployable version with one of these commands:
 
 1. With `./gradlew :key.ui:run` you can run the user interface of KeY directly from the repository.
 
-2. Use `./gradlew classes` to compile KeY, includes running JavaCC and Antlr, additional use `./gradlew testClasses` if 
-   you also want to compile the JUnit test classes. 
+2. Use `./gradlew classes` to compile KeY, includes running JavaCC and Antlr, additional use `./gradlew testClasses` if
+   you also want to compile the JUnit test classes.
 
-3. Test your installation with `./gradlew test` or `./gradlew testFast`. 
+3. Test your installation with `./gradlew test` or `./gradlew testFast`.
    The later command disables the slow running test cases.
-   
-   You can select a specific test case with `--tests` argument. Wildcards are allowed. 
+
+   You can select a specific test case with `--tests` argument. Wildcards are allowed.
    ```
    ./gradlew :key.<subproject>:test --tests "<class>.<method>"
    ```
 
    You can debug KeY by adding the `--debug-jvm` option, then attaching a debugger at `localhost:5005`.
 
-4. You can create a single jar-version, aka *fat jar*, of KeY with 
+4. You can create a single jar-version, aka *fat jar*, of KeY with
    ```
-   ./gradlew :key.ui:shadowJar 
+   ./gradlew :key.ui:shadowJar
    ```
    The file is generated in `key.ui/build/libs/key-*-exe.jar`.
 
-5. A distributiion is build with 
+5. A distributiion is build with
    ```
    ./gradlew :key.ui:installDist :key.ui:distZip
    ```
-   The distribution can tested by calling `key.ui/install/key/bin/key.ui` 
+   The distribution can tested by calling `key.ui/install/key/bin/key.ui`
    and is zipped in `key.ui/build/distributions`.
 
    The distribution gives you potential of using single jar files.
-   
+
+# Developing KeY
+
+* Quality is automatically assessed using [SonarQube](https://sonarqube.org) on each merge requests.
+  The results of the assessments can be found on
+  [SonarCloud.io](https://sonarcloud.io/dashboard?id=key-main)
+  ([Branches](https://sonarcloud.io/project/branches?id=key-main))
+
+  The rules and quality gate are maintained by Alexander Weigl
+  <weigl@kit.edu> currently.
+
+* More guideline and documentation for the KeY development can be found under
+[key-docs](https://key-project.org/docs/).
+
+
+
 # Issues and Bug Reports
 
 If you encounter problems, please send a message to
@@ -72,17 +89,18 @@ If you encounter problems, please send a message to
 		<support@key-project.org>
 
 
+
 # License Remark
 
 ```
 This is the KeY project - Integrated Deductive Software Design
 Copyright (C) 2001-2011 Universität Karlsruhe, Germany
-                        Universität Koblenz-Landau, Germany
-                        and Chalmers University of Technology, Sweden
-Copyright (C) 2011-2020 Karlsruhe Institute of Technology, Germany
-                        Technical University Darmstadt, Germany
-                        Chalmers University of Technology, Sweden
+						Universität Koblenz-Landau, Germany
+						and Chalmers University of Technology, Sweden
+Copyright (C) 2011-2021 Karlsruhe Institute of Technology, Germany
+						Technical University Darmstadt, Germany
+						Chalmers University of Technology, Sweden
 
-The KeY system is protected by the GNU General Public License. 
+The KeY system is protected by the GNU General Public License.
 See LICENSE.TXT for details.
 ```

key/build.gradle

@@ -46,7 +46,15 @@ static def getDate() {
 def build = System.env.BUILD_NUMBER == null ? "" : "-${System.env.BUILD_NUMBER}"
 
 group = "org.key_project"
-version = "2.8.0$build"
+version = "2.9$build"
+
+sonarqube {
+    properties {
+        property "sonar.projectKey", "key-main"
+        property "sonar.organization", "keyproject"
+        property "sonar.host.url", "https://sonarcloud.io"
+    }
+}
 
 sonarqube {
     properties {
@@ -68,13 +76,13 @@ subprojects {
 
     repositories {
         mavenCentral()
-        flatDir { dirs "lib", "$rootDir/key.core/lib" }
+        flatDir { dirs "lib", "$rootDir/key.core/lib", "$rootDir/key.ui/lib" }
     }
 
     dependencies {
-        compile     'org.jetbrains:annotations:20.1.0'
-        testCompile 'junit:junit:4.13.1'
-        testCompile project(':key.util')
+        implementation 'com.google.code.findbugs:jsr305:3.0.2'
+        testImplementation 'junit:junit:4.12'
+        testImplementation project(':key.util')
     }
 
     // Setting UTF-8 as the java source encoding.
@@ -231,12 +239,15 @@ subprojects {
         }
         repositories {
             maven {
-                name = "GitHubPackages"
-                url = uri("https://maven.pkg.github.com/KeYProject/key")
-                credentials {
-                    username = project.findProperty("gpr.user") ?: System.getenv("USERNAME")
-                    password = project.findProperty("gpr.key") ?: System.getenv("TOKEN")
-                }
+                name = "GitlabPackages"
+		        url "https://git.key-project.org/api/v4/projects/35/packages/maven"
+		        credentials(HttpHeaderCredentials) {
+			        name = 'Private-Token'
+			        value = System.getenv("TOKEN")
+		        }
+		        authentication {
+			        header(HttpHeaderAuthentication)
+		        }           
             }
         }
     }

key/gradle/wrapper/gradle-wrapper.properties

 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-5.4.1-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-6.6-bin.zip
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

key/key.core.example/build.gradle

 dependencies {
-    compile project(":key.core")
+    implementation project(":key.core")
 }
\ No newline at end of file

key/key.core.proof_references/build.gradle

 dependencies {
-    compile project(":key.core")
+    implementation project(":key.core")
 }
-
-/*test {
-    systemProperty "testcases", "src/test/resources/testcase"
-    maxHeapSize = "4g"
-    systemProperty "testcases", "src/test/resources/testcase"
-    filter { includeTestsMatching "AllProofReferencesTests" }
-}*/
\ No newline at end of file

key/key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/TestProofReferenceUtil.java

@@ -46,7 +46,7 @@ public class TestProofReferenceUtil extends AbstractProofReferenceTestCase {
                 true,
                 ImmutableSLList.<IProofReferencesAnalyst>nil().append(new MethodBodyExpandProofReferencesAnalyst(), new ContractProofReferencesAnalyst()),
                 new ExpectedProofReferences(IProofReference.INLINE_METHOD, "UseOperationContractTest::main"),
-                new ExpectedProofReferences(IProofReference.USE_CONTRACT, "pre: {heap=java.lang.Object::<inv>(heap,self)<<impl>>}; mby: null; post: {heap=and(and(equals(result<<origin(ensures @ file UseOperationContractTest.java @ line 12) ([])>>,Z(2(4(#))))<<origin(ensures @ file UseOperationContractTest.java @ line 12) ([])>>,java.lang.Object::<inv>(heap,self)<<impl>>)<<SC>>,equals(exc<<origin(ensures (implicit)) ([])>>,null)<<impl, origin(ensures (implicit)) ([])>>)}; mods: {heap=allLocs, savedHeap=null}; hasMod: {heap=true, savedHeap=true}; termination: diamond; transaction: false"));
+                new ExpectedProofReferences(IProofReference.USE_CONTRACT, "pre: {heap=java.lang.Object::<inv>(heap,self)<<impl>>}; mby: null; post: {heap=and(and(equals(result,Z(2(4(#))))<<origin(ensures @ file UseOperationContractTest.java @ line 12) ([])>>,java.lang.Object::<inv>(heap,self)<<impl>>)<<SC>>,equals(exc<<origin(ensures (implicit)) ([])>>,null)<<impl, origin(ensures (implicit)) ([])>>)}; mods: {heap=allLocs, savedHeap=null}; hasMod: {heap=true, savedHeap=true}; termination: diamond; transaction: false"));
    }
 
    /**

key/key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/analyst/TestClassAxiomAndInvariantProofReferencesAnalyst.java

@@ -120,7 +120,6 @@ public class TestClassAxiomAndInvariantProofReferencesAnalyst extends AbstractPr
                               false,
                               new ClassAxiomAndInvariantProofReferencesAnalyst(),
                               new ExpectedProofReferences(IProofReference.USE_AXIOM, "equiv(java.lang.Object::<inv>(heap,self),java.lang.Object::<inv>(heap,test.AccessibleTest::select(heap,self,test.B::$c)))"),
-                              new ExpectedProofReferences(IProofReference.USE_AXIOM, "equiv(java.lang.Object::<inv>(heap,self),and(leq(Z(0(#)),int::select(heap,self,java.util.ListIterator::$index)),leq(int::select(heap,self,java.util.ListIterator::$index),seqLen(Seq::select(heap,self,java.util.ListIterator::$seq))))<<SC>>)"),
                               new ExpectedProofReferences(IProofReference.USE_AXIOM, "equiv(java.lang.Object::<inv>(heap,self),true)"));
    }
 }

key/key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/analyst/TestContractProofReferencesAnalyst.java

@@ -32,6 +32,6 @@ public class TestContractProofReferencesAnalyst extends AbstractProofReferenceTe
                             "main",
                             true,
                             new ContractProofReferencesAnalyst(),
-                            new ExpectedProofReferences(IProofReference.USE_CONTRACT, "pre: {heap=java.lang.Object::<inv>(heap,self)<<impl>>}; mby: null; post: {heap=and(and(equals(result<<origin(ensures @ file UseOperationContractTest.java @ line 12) ([])>>,Z(2(4(#))))<<origin(ensures @ file UseOperationContractTest.java @ line 12) ([])>>,java.lang.Object::<inv>(heap,self)<<impl>>)<<SC>>,equals(exc<<origin(ensures (implicit)) ([])>>,null)<<impl, origin(ensures (implicit)) ([])>>)}; mods: {heap=allLocs, savedHeap=null}; hasMod: {heap=true, savedHeap=true}; termination: diamond; transaction: false"));
+                            new ExpectedProofReferences(IProofReference.USE_CONTRACT, "pre: {heap=java.lang.Object::<inv>(heap,self)<<impl>>}; mby: null; post: {heap=and(and(equals(result,Z(2(4(#))))<<origin(ensures @ file UseOperationContractTest.java @ line 12) ([])>>,java.lang.Object::<inv>(heap,self)<<impl>>)<<SC>>,equals(exc<<origin(ensures (implicit)) ([])>>,null)<<impl, origin(ensures (implicit)) ([])>>)}; mods: {heap=allLocs, savedHeap=null}; hasMod: {heap=true, savedHeap=true}; termination: diamond; transaction: false"));
    }
 }

key/key.core.symbolic_execution.example/build.gradle

 dependencies {
-    compile project(":key.core")
-    compile project(":key.core.symbolic_execution")
+    implementation project(":key.core")
+    implementation project(":key.core.symbolic_execution")
 }
\ No newline at end of file

key/key.core.symbolic_execution.example/src/main/java/org/key_project/example/Main.java

@@ -131,7 +131,7 @@ public class Main {
     */
    protected static void printSymbolicExecutionTree(String title, SymbolicExecutionTreeBuilder builder) {
       System.out.println(title);
-      System.out.println(StringUtil.createLine("=", title.length()));
+      System.out.println(StringUtil.repeat("=", title.length()));
       ExecutionNodePreorderIterator iterator = new ExecutionNodePreorderIterator(builder.getStartNode());
       while (iterator.hasNext()) {
          IExecutionNode<?> next = iterator.next();

key/key.core.symbolic_execution/build.gradle

 dependencies {
-    compile project(":key.core")
-    testCompile project(":key.core").sourceSets.test.output
+    implementation project(":key.core")
+    testImplementation project(":key.core").sourceSets.test.output
 }
 
 test {

key/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/AbstractExecutionValue.java

@@ -8,6 +8,7 @@ import java.util.Set;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.Term;
+import de.uka.ilkd.key.logic.label.OriginTermLabel;
 import de.uka.ilkd.key.logic.op.ProgramVariable;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.init.ProofInputException;
@@ -125,7 +126,7 @@ public abstract class AbstractExecutionValue extends AbstractExecutionElement im
       if (term != null) {
          if (term.op() instanceof ProgramVariable ||
              SymbolicExecutionUtil.isSelect(services, term)) {
-            toFill.add(term);
+            toFill.add(OriginTermLabel.removeOriginLabels(term, services));
          }
          else {
             for (int i = 0; i < term.arity(); i++) {
@@ -142,7 +143,7 @@ public abstract class AbstractExecutionValue extends AbstractExecutionElement im
     * @return {@code true} at least one {@link Term} is contained, {@code false} none of the {@link Term}s is contained.
     */
    protected boolean containsTerm(Term term, Set<Term> toSearch) {
-      if (toSearch.contains(term)) {
+      if (toSearch.contains(OriginTermLabel.removeOriginLabels(term, getServices()))) {
          return true;
       }
       else {

key/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java

@@ -19,6 +19,7 @@ import java.util.List;
 import java.util.Map;
 import java.util.Properties;
 
+import de.uka.ilkd.key.speclang.njml.JmlIO;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
@@ -41,8 +42,6 @@ import de.uka.ilkd.key.logic.op.ProgramVariable;
 import de.uka.ilkd.key.proof.init.AbstractOperationPO;
 import de.uka.ilkd.key.proof.init.InitConfig;
 import de.uka.ilkd.key.speclang.PositionedString;
-import de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser;
-import de.uka.ilkd.key.speclang.translation.SLTranslationException;
 
 /**
  * <p>
@@ -174,25 +173,18 @@ public class ProgramMethodPO extends AbstractOperationPO {
                          ImmutableList<ProgramVariable> paramVars,
                          Map<LocationVariable, LocationVariable> atPreVars,
                          Services services) {
-      try {
-         if (precondition != null && !precondition.isEmpty()) {
-            PositionedString ps = new PositionedString(precondition);
-            KeYJMLParser parser = new KeYJMLParser(ps,
-                                                   services,
-                                                   getCalleeKeYJavaType(),
-                                                   selfVar,
-                                                   paramVars,
-                                                   null,
-                                                   null,
-                                                   null);
-            return parser.parseExpression();
-         }
-         else {
-            return tb.tt();
-         }
+      if (precondition != null && !precondition.isEmpty()) {
+         JmlIO io = new JmlIO()
+                 .services(services)
+                 .classType(getCalleeKeYJavaType())
+                 .selfVar(selfVar)
+                 .parameters(paramVars);
+
+         PositionedString ps = new PositionedString(precondition);
+         return io.parseExpression(ps);
       }
-      catch (SLTranslationException e) {
-         throw new RuntimeException("Can't parse precondition \"" + precondition + "\".", e);
+      else {
+         return tb.tt();
       }
    }
 

key/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java

@@ -13,21 +13,7 @@
 
 package de.uka.ilkd.key.symbolic_execution.strategy.breakpoint;
 
-import java.util.HashMap;
-import java.util.HashSet;
-import java.util.Iterator;
-import java.util.Map;
-import java.util.Map.Entry;
-import java.util.Set;
-
-import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.collection.ImmutableSLList;
-
-import de.uka.ilkd.key.java.JavaInfo;
-import de.uka.ilkd.key.java.JavaTools;
-import de.uka.ilkd.key.java.SourceElement;
-import de.uka.ilkd.key.java.StatementBlock;
-import de.uka.ilkd.key.java.StatementContainer;
+import de.uka.ilkd.key.java.*;
 import de.uka.ilkd.key.java.abstraction.Field;
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
 import de.uka.ilkd.key.java.declaration.ParameterDeclaration;
@@ -35,18 +21,9 @@ import de.uka.ilkd.key.java.declaration.TypeDeclaration;
 import de.uka.ilkd.key.java.declaration.VariableSpecification;
 import de.uka.ilkd.key.java.reference.IExecutionContext;
 import de.uka.ilkd.key.java.visitor.ProgramVariableCollector;
-import de.uka.ilkd.key.logic.PosInOccurrence;
-import de.uka.ilkd.key.logic.ProgramElementName;
-import de.uka.ilkd.key.logic.RenamingTable;
-import de.uka.ilkd.key.logic.Sequent;
-import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.logic.TermBuilder;
-import de.uka.ilkd.key.logic.VariableNamer;
-import de.uka.ilkd.key.logic.op.IProgramMethod;
-import de.uka.ilkd.key.logic.op.IProgramVariable;
-import de.uka.ilkd.key.logic.op.LocationVariable;
-import de.uka.ilkd.key.logic.op.ProgramVariable;
-import de.uka.ilkd.key.logic.op.SVSubstitute;
+import de.uka.ilkd.key.logic.*;
+import de.uka.ilkd.key.logic.op.*;
+import de.uka.ilkd.key.speclang.njml.JmlIO;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.OpReplacer;
@@ -56,11 +33,15 @@ import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
 import de.uka.ilkd.key.prover.impl.ApplyStrategyInfo;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.speclang.PositionedString;
-import de.uka.ilkd.key.speclang.jml.translation.KeYJMLParser;
 import de.uka.ilkd.key.speclang.translation.SLTranslationException;
 import de.uka.ilkd.key.strategy.StrategyProperties;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
+import org.key_project.util.collection.ImmutableList;
+import org.key_project.util.collection.ImmutableSLList;
+
+import java.util.*;
+import java.util.Map.Entry;
 
 /**
  * Adds the funtionality to breakpoints to evaluate conditions.
@@ -285,9 +266,8 @@ public abstract class AbstractConditionalBreakpoint extends AbstractHitCountBrea
     * Computes the Term that can be evaluated, from the user given condition
     * @param condition the condition given by the user
     * @return the {@link Term} that represents the condition
-    * @throws SLTranslationException if the Term could not be parsed
     */
-   private Term computeTermForCondition(String condition) throws SLTranslationException {
+   private Term computeTermForCondition(String condition) {
       if(condition==null){
          return getProof().getServices().getTermBuilder().tt();
       }
@@ -327,17 +307,14 @@ public abstract class AbstractConditionalBreakpoint extends AbstractHitCountBrea
       this.setVarsForCondition(varsForCondition);
       //parse string
       PositionedString ps = new PositionedString(condition);
-      KeYJMLParser parser = new KeYJMLParser(ps, 
-                                             getProof().getServices(), 
-                                             containerType, 
-                                             getSelfVar(), 
-                                             varsForCondition, 
-                                             null, 
-                                             null, 
-                                             null);
-      
-         return parser.parseExpression();
-      
+
+      JmlIO io = new JmlIO()
+              .services(getProof().getServices())
+              .classType(containerType)
+              .selfVar(getSelfVar())
+              .parameters(varsForCondition);
+
+      return io.parseExpression(ps);
    }
    
    /**

key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java

@@ -86,12 +86,14 @@ import de.uka.ilkd.key.util.HelperClassForTests;
 import de.uka.ilkd.key.util.KeYConstants;
 import junit.framework.TestCase;
 
+import static org.junit.Assert.*;
+
 /**
  * Provides the basic functionality of {@link TestCase}s which tests
  * the symbolic execution features.
  * @author Martin Hentschel
  */
-public abstract class AbstractSymbolicExecutionTestCase extends TestCase {
+public abstract class AbstractSymbolicExecutionTestCase {
    /**
     * <p>
     * If this constant is {@code true} a temporary directory is created with
@@ -207,10 +209,10 @@ public abstract class AbstractSymbolicExecutionTestCase extends TestCase {
          final String SUFFIX = " ###";
          String path = tempNewOracleDirectory.toString();
          int length = Math.max(path.length(), HEADER_LINE.length());
-         String borderLines = StringUtil.createLine("#", PREFIX.length() + length + SUFFIX.length());
+         String borderLines = StringUtil.repeat("#", PREFIX.length() + length + SUFFIX.length());
          System.out.println(borderLines);
-         System.out.println(PREFIX + HEADER_LINE + StringUtil.createLine(" ", length - HEADER_LINE.length()) + SUFFIX);
-         System.out.println(PREFIX + path + StringUtil.createLine(" ", length - path.length()) + SUFFIX);
+         System.out.println(PREFIX + HEADER_LINE + StringUtil.repeat(" ", length - HEADER_LINE.length()) + SUFFIX);
+         System.out.println(PREFIX + path + StringUtil.repeat(" ", length - path.length()) + SUFFIX);
          System.out.println(borderLines);
       }
    }
@@ -2049,15 +2051,15 @@ public abstract class AbstractSymbolicExecutionTestCase extends TestCase {
     * @return The original settings which are overwritten.
     */
    public static HashMap<String, String> setDefaultTacletOptions() {
-	   HashMap<String,String> original = HelperClassForTests.setDefaultTacletOptions();
-	   // set non modular reasoning
-	   System.out.println(ProofSettings.DEFAULT_SETTINGS);
-	   ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings();
-	   System.out.println(choiceSettings);
-	   ImmutableSet<Choice> cs = DefaultImmutableSet.nil();
-	   cs = cs.add(new Choice("noRestriction", "methodExpansion"));
-	   choiceSettings.updateWith(cs);
-	   return original;
+      HashMap<String, String> original = HelperClassForTests.setDefaultTacletOptions();
+      // set non modular reasoning
+      //System.out.println(ProofSettings.DEFAULT_SETTINGS);
+      ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings();
+      //System.out.println(choiceSettings);
+      ImmutableSet<Choice> cs = DefaultImmutableSet.nil();
+      cs = cs.add(new Choice("noRestriction", "methodExpansion"));
+      choiceSettings.updateWith(cs);
+      return original;
    }
 
    /**

key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestConditionalVariables.java

@@ -9,6 +9,8 @@ import de.uka.ilkd.key.symbolic_execution.model.IExecutionNode;
 import de.uka.ilkd.key.symbolic_execution.model.IExecutionStart;
 import de.uka.ilkd.key.symbolic_execution.model.IExecutionVariable;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionEnvironment;
+import static org.junit.Assert.*;
+import org.junit.Test;
 
 /**