Formatter

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelMerger.java

@@ -1,5 +1,7 @@
 package de.uka.ilkd.key.rule.label;
 
+import java.util.ArrayList;
+import java.util.Arrays;
 import java.util.LinkedList;
 import java.util.List;
 
@@ -27,10 +29,9 @@ public boolean mergeLabels(SequentFormula existingSF, Term existingTerm,
             FormulaTermLabel fExisting = (FormulaTermLabel) existingLabel;
             FormulaTermLabel fRejected = (FormulaTermLabel) rejectedLabel;
             // Compute new label
-            List<String> newBeforeIds = new LinkedList<String>();
-            CollectionUtil.addAll(newBeforeIds, fExisting.getBeforeIds());
-            CollectionUtil.addAll(newBeforeIds, fRejected.getId());
-            CollectionUtil.addAll(newBeforeIds, fRejected.getBeforeIds());
+            List<String> newBeforeIds = new ArrayList<>(Arrays.asList(fExisting.getBeforeIds()));
+            newBeforeIds.add(fRejected.getId());
+            newBeforeIds.addAll(Arrays.asList(fRejected.getBeforeIds()));
             FormulaTermLabel newLabel =
                 new FormulaTermLabel(fExisting.getMajorId(), fExisting.getMinorId(), newBeforeIds);
             // Remove existing label

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java

@@ -1,11 +1,6 @@
 package de.uka.ilkd.key.rule.label;
 
-import java.util.Collections;
-import java.util.LinkedHashSet;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.Map;
-import java.util.Set;
+import java.util.*;
 
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.java.CollectionUtil;
@@ -233,8 +228,8 @@ protected void refactorBewlowUpdates(PosInOccurrence applicationPosInOccurrence,
                 labels.add(applicationLabel);
             } else {
                 labels.remove(termLabel);
-                Set<String> beforeIds = new LinkedHashSet<String>();
-                CollectionUtil.addAll(beforeIds, termLabel.getBeforeIds());
+                Set<String> beforeIds =
+                    new LinkedHashSet<>(Arrays.asList(termLabel.getBeforeIds()));
                 beforeIds.add(applicationLabel.getId());
                 labels.add(new FormulaTermLabel(termLabel.getMajorId(), termLabel.getMinorId(),
                     beforeIds));
@@ -288,8 +283,8 @@ protected void refactorSubstitution(Term term, Term tacletTerm, List<TermLabel>
             if (existingLabel == null) {
                 labels.add(tacletLabel);
             } else {
-                List<String> beforeIds = new LinkedList<String>();
-                CollectionUtil.addAll(beforeIds, existingLabel.getBeforeIds());
+                List<String> beforeIds =
+                    new ArrayList<>(Arrays.asList(existingLabel.getBeforeIds()));
                 boolean changed = true;
                 if (!beforeIds.contains(tacletLabel.getId())) {
                     changed = true;

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

@@ -1,9 +1,6 @@
 package de.uka.ilkd.key.symbolic_execution.model.impl;
 
-import java.io.IOException;
-import java.io.StringWriter;
-
-import de.uka.ilkd.key.java.PrettyPrinter;
+import de.uka.ilkd.key.pp.PrettyPrinter;
 import de.uka.ilkd.key.java.statement.BranchStatement;
 import de.uka.ilkd.key.java.statement.If;
 import de.uka.ilkd.key.java.statement.Switch;
@@ -38,21 +35,15 @@ public ExecutionBranchStatement(ITreeSettings settings, Node proofNode) {
     @Override
     protected String lazyComputeName() {
         BranchStatement bs = getActiveStatement();
-        try {
-            if (bs instanceof If) {
-                StringWriter sw = new StringWriter();
-                PrettyPrinter sb = new PrettyPrinter(sw, true);
-                sb.printIf((If) bs, false);
-                return sw.toString();
-            } else if (bs instanceof Switch) {
-                StringWriter sw = new StringWriter();
-                PrettyPrinter sb = new PrettyPrinter(sw, true);
-                sb.printSwitch((Switch) bs, false);
-                return sw.toString();
-            } else {
-                return bs.toString();
-            }
-        } catch (IOException e) {
+        if (bs instanceof If) {
+            PrettyPrinter p = PrettyPrinter.purePrinter();
+            p.performActionOnIf((If) bs, false);
+            return p.result();
+        } else if (bs instanceof Switch) {
+            PrettyPrinter p = PrettyPrinter.purePrinter();
+            p.performActionOnSwitch((Switch) bs, false);
+            return p.result();
+        } else {
             return bs.toString();
         }
     }

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

@@ -1,14 +1,7 @@
 package de.uka.ilkd.key.symbolic_execution.model.impl;
 
-import java.io.IOException;
-import java.io.StringWriter;
-
-import de.uka.ilkd.key.java.PrettyPrinter;
-import de.uka.ilkd.key.java.statement.Do;
-import de.uka.ilkd.key.java.statement.EnhancedFor;
-import de.uka.ilkd.key.java.statement.For;
-import de.uka.ilkd.key.java.statement.LoopStatement;
-import de.uka.ilkd.key.java.statement.While;
+import de.uka.ilkd.key.pp.PrettyPrinter;
+import de.uka.ilkd.key.java.statement.*;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.symbolic_execution.model.IExecutionConstraint;
 import de.uka.ilkd.key.symbolic_execution.model.IExecutionLoopStatement;
@@ -40,35 +33,27 @@ public ExecutionLoopStatement(ITreeSettings settings, Node proofNode) {
     @Override
     protected String lazyComputeName() {
         LoopStatement ls = getActiveStatement();
-        try {
-            if (ls.getGuardExpression() != null) {
-                if (ls instanceof While) {
-                    StringWriter sw = new StringWriter();
-                    PrettyPrinter sb = new PrettyPrinter(sw, true);
-                    sb.printWhile((While) ls, false);
-                    return sw.toString();
-                } else if (ls instanceof For) {
-                    StringWriter sw = new StringWriter();
-                    PrettyPrinter sb = new PrettyPrinter(sw, true);
-                    sb.printFor((For) ls, false);
-                    return sw.toString();
-                } else if (ls instanceof EnhancedFor) {
-                    StringWriter sw = new StringWriter();
-                    PrettyPrinter sb = new PrettyPrinter(sw, true);
-                    sb.printEnhancedFor((EnhancedFor) ls, false);
-                    return sw.toString();
-                } else if (ls instanceof Do) {
-                    StringWriter sw = new StringWriter();
-                    PrettyPrinter sb = new PrettyPrinter(sw, true);
-                    sb.printDo((Do) ls, false);
-                    return sw.toString();
-                } else {
-                    return ls.toString();
-                }
+        if (ls.getGuardExpression() != null) {
+            if (ls instanceof While) {
+                PrettyPrinter p = PrettyPrinter.purePrinter();
+                p.performActionOnWhile((While) ls, false);
+                return p.result();
+            } else if (ls instanceof For) {
+                PrettyPrinter p = PrettyPrinter.purePrinter();
+                p.performActionOnFor((For) ls, false);
+                return p.result();
+            } else if (ls instanceof EnhancedFor) {
+                PrettyPrinter p = PrettyPrinter.purePrinter();
+                p.performActionOnEnhancedFor((EnhancedFor) ls, false);
+                return p.result();
+            } else if (ls instanceof Do) {
+                PrettyPrinter p = PrettyPrinter.purePrinter();
+                p.performActionOnDo((Do) ls, false);
+                return p.result();
             } else {
                 return ls.toString();
             }
-        } catch (IOException e) {
+        } else {
             return ls.toString();
         }
     }

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

@@ -1,23 +1,6 @@
 package de.uka.ilkd.key.symbolic_execution.po;
 
-import java.io.IOException;
-import java.io.StringWriter;
-import java.util.List;
-import java.util.Map;
-import java.util.Properties;
-
-import de.uka.ilkd.key.speclang.jml.translation.Context;
-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;
-import org.key_project.util.java.ObjectUtil;
-
-import de.uka.ilkd.key.java.Expression;
-import de.uka.ilkd.key.java.JavaInfo;
-import de.uka.ilkd.key.java.PrettyPrinter;
-import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.java.StatementBlock;
+import de.uka.ilkd.key.java.*;
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
 import de.uka.ilkd.key.java.statement.MethodBodyStatement;
 import de.uka.ilkd.key.logic.Sequent;
@@ -27,9 +10,22 @@
 import de.uka.ilkd.key.logic.op.LocationVariable;
 import de.uka.ilkd.key.logic.op.Modality;
 import de.uka.ilkd.key.logic.op.ProgramVariable;
+import de.uka.ilkd.key.pp.PosTableLayouter;
+import de.uka.ilkd.key.pp.PrettyPrinter;
 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.Context;
+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;
+import org.key_project.util.java.ObjectUtil;
+
+import java.io.IOException;
+import java.util.List;
+import java.util.Map;
+import java.util.Properties;
 
 /**
  * <p>
@@ -258,7 +254,7 @@ public String getPrecondition() {
      * {@inheritDoc}
      */
     @Override
-    public void fillSaveProperties(Properties properties) throws IOException {
+    public void fillSaveProperties(Properties properties) {
         super.fillSaveProperties(properties);
         properties.setProperty("method", getProgramMethodSignature(getProgramMethod(), true));
         if (getPrecondition() != null && !getPrecondition().isEmpty()) {
@@ -267,28 +263,24 @@ public void fillSaveProperties(Properties properties) throws IOException {
     }
 
     /**
-     * Returns a human readable full qualified method signature.
+     * Returns a human-readable full qualified method signature.
      *
      * @param pm The {@link IProgramMethod} which provides the signature.
      * @param includeType Include the container type?
-     * @return The human readable method signature.
-     * @throws IOException Occurred Exception.
+     * @return The human-readable method signature.
      */
-    public static String getProgramMethodSignature(IProgramMethod pm, boolean includeType)
-            throws IOException {
-        StringWriter sw = new StringWriter();
-        try {
-            PrettyPrinter x = new PrettyPrinter(sw);
-            if (includeType) {
-                KeYJavaType type = pm.getContainerType();
-                sw.append(type.getFullName());
-                sw.append("#");
-            }
-            x.printFullMethodSignature(pm);
-            return sw.toString();
-        } finally {
-            sw.close();
+    public static String getProgramMethodSignature(IProgramMethod pm, boolean includeType) {
+        PosTableLayouter l = PosTableLayouter.pure();
+        l.beginC(0);
+        if (includeType) {
+            KeYJavaType type = pm.getContainerType();
+            l.print(type.getFullName());
+            l.print("#");
         }
+        PrettyPrinter x = new PrettyPrinter(l);
+        x.writeFullMethodSignature(pm);
+        l.end();
+        return x.result();
     }
 
     /**

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

@@ -1,22 +1,6 @@
 package de.uka.ilkd.key.symbolic_execution.po;
 
-import java.io.IOException;
-import java.util.Collection;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.Map;
-import java.util.Properties;
-import java.util.Set;
-
-import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.collection.ImmutableSLList;
-import org.key_project.util.java.ObjectUtil;
-
-import de.uka.ilkd.key.java.Position;
-import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.java.Statement;
-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.KeYJavaType;
 import de.uka.ilkd.key.java.reference.ExecutionContext;
 import de.uka.ilkd.key.java.reference.TypeRef;
@@ -32,6 +16,12 @@
 import de.uka.ilkd.key.logic.op.LocationVariable;
 import de.uka.ilkd.key.logic.op.ProgramVariable;
 import de.uka.ilkd.key.proof.init.InitConfig;
+import org.key_project.util.collection.ImmutableList;
+import org.key_project.util.collection.ImmutableSLList;
+import org.key_project.util.java.ObjectUtil;
+
+import java.io.IOException;
+import java.util.*;
 
 /**
  * <p>
@@ -305,7 +295,7 @@ public Position getEndPosition() {
      * {@inheritDoc}
      */
     @Override
-    public void fillSaveProperties(Properties properties) throws IOException {
+    public void fillSaveProperties(Properties properties) {
         super.fillSaveProperties(properties);
         if (getStartPosition() != null) {
             properties.setProperty("startLine", getStartPosition().getLine() + "");