Remove a quadrillion IOExceptions

KeYProject · Feb 10, 2023 · f6a843a · f6a843a
1 parent b7f828a
commit f6a843a
Show file tree

Hide file tree

Showing 194 changed files with 1,147 additions and 2,273 deletions.
diff --git a/...src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionBranchStatement.java b/...src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionBranchStatement.java
@@ -1,8 +1,5 @@
 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.BranchStatement;
 import de.uka.ilkd.key.java.statement.If;
@@ -38,21 +35,17 @@ 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) {
+            StringBuilder sw = new StringBuilder();
+            PrettyPrinter sb = new PrettyPrinter(sw, true);
+            sb.printIf((If) bs, false);
+            return sw.toString();
+        } else if (bs instanceof Switch) {
+            StringBuilder sw = new StringBuilder();
+            PrettyPrinter sb = new PrettyPrinter(sw, true);
+            sb.printSwitch((Switch) bs, false);
+            return sw.toString();
+        } else {
             return bs.toString();
         }
     }

diff --git a/...n/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionLoopStatement.java b/...n/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.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,31 @@ 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) {
+                StringBuilder sw = new StringBuilder();
+                PrettyPrinter sb = new PrettyPrinter(sw, true);
+                sb.printWhile((While) ls, false);
+                return sw.toString();
+            } else if (ls instanceof For) {
+                StringBuilder sw = new StringBuilder();
+                PrettyPrinter sb = new PrettyPrinter(sw, true);
+                sb.printFor((For) ls, false);
+                return sw.toString();
+            } else if (ls instanceof EnhancedFor) {
+                StringBuilder sw = new StringBuilder();
+                PrettyPrinter sb = new PrettyPrinter(sw, true);
+                sb.printEnhancedFor((EnhancedFor) ls, false);
+                return sw.toString();
+            } else if (ls instanceof Do) {
+                StringBuilder sw = new StringBuilder();
+                PrettyPrinter sb = new PrettyPrinter(sw, true);
+                sb.printDo((Do) ls, false);
+                return sw.toString();
             } else {
                 return ls.toString();
             }
-        } catch (IOException e) {
+        } else {
             return ls.toString();
         }
     }

diff --git a/...mbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java b/...mbolic_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;
@@ -30,6 +13,17 @@
 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 +252,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()) {
@@ -272,23 +266,17 @@ public void fillSaveProperties(Properties properties) throws IOException {
      * @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.
      */
-    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) {
+        StringBuilder sw = new StringBuilder();
+        PrettyPrinter x = new PrettyPrinter(sw);
+        if (includeType) {
+            KeYJavaType type = pm.getContainerType();
+            sw.append(type.getFullName());
+            sw.append("#");
         }
+        x.printFullMethodSignature(pm);
+        return sw.toString();
     }
 
     /**

diff --git a/..._execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java b/..._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() + "");