Further Refactorings for Java 17+

key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java

@@ -204,81 +204,49 @@ private void checkFlows() {
 
     @Override
     public void startElement(String uri, String localName, String qName, Attributes attributes) {
-
         switch (localName) {
-        case "sourcedompair":
-        case "source":
-            startSources();
-            break;
-        case "sinkdompair":
-        case "sink":
-            startSinks();
-            break;
-        case "category": // TODO: different semantics in "domains" and "sinkdompair"
+        case "sourcedompair", "source" -> startSources();
+        case "sinkdompair", "sink" -> startSinks();
+        case "category" -> // TODO: different semantics in "domains" and "sinkdompair"
             setCategory(attributes);
-            break;
-        case "assign":
-            assignHandle(attributes);
-            break;
+        case "assign" -> assignHandle(attributes);
+
         // case "domainassignment":
-        case "domains":
-            startDomains();
-            break;
-        case "domain":
-            putDomain(attributes);
-            break;
-        case "assignable":
-            setAssignable(attributes);
-            break;
-        case "field":
-            putField(attributes);
-            break;
-        case "parameter":
-            putParam(attributes);
-            break;
-        case "returnvalue":
-            putReturn(attributes);
-            break;
-        case "flowrelation":
-            startFlow();
-            break;
-        case "flow":
-            putFlow(attributes);
-            break;
+        case "domains" -> startDomains();
+        case "domain" -> putDomain(attributes);
+        case "assignable" -> setAssignable(attributes);
+        case "field" -> putField(attributes);
+        case "parameter" -> putParam(attributes);
+        case "returnvalue" -> putReturn(attributes);
+        case "flowrelation" -> startFlow();
+        case "flow" -> putFlow(attributes);
+
         // a lot of elements without their own semantics
         // case "riflspec":
         // case "attackerio":
         // case "top":
         // case "bottom":
         // case "source":
         // case "sink":
-        case "dompair": // TODO
-            // case "domainhierarchy":
-        case "flowpair": // TODO
-            // case "flowpolicy":
-        default:
+        // TODO
+        // case "domainhierarchy":
+        // TODO
+        // case "flowpolicy":
+        default -> {
+        }
         }
     }
 
     @Override
     public void endElement(String uri, String localName, String qName) {
         switch (localName) {
-        case "assignable":
-            unsetAssignable();
-            break;
-        case "category":
-            unsetCategory();
-            break;
-        case "domains":
-            checkDomains();
-            break;
-        case "domainassignment":
-            checkDomainAssignmentsWithFlows();
-            break;
-        case "flowrelation":
-            checkFlows();
-            break;
-        default:
+        case "assignable" -> unsetAssignable();
+        case "category" -> unsetCategory();
+        case "domains" -> checkDomains();
+        case "domainassignment" -> checkDomainAssignmentsWithFlows();
+        case "flowrelation" -> checkFlows();
+        default -> {
+        }
         }
     }
 

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeReader.java

@@ -408,7 +408,7 @@ public void startElement(String uri, String localName, String qName, Attributes
          * {@inheritDoc}
          */
         @Override
-        public void endElement(String uri, String localName, String qName) throws SAXException {
+        public void endElement(String uri, String localName, String qName) {
             if (isConstraint(uri, localName, qName)) {
                 // Nothing to do.
             } else if (isCallStateVariable(uri, localName, qName)) {
@@ -1823,7 +1823,7 @@ public static class KeYlessTermination extends AbstractKeYlessExecutionNode<Sour
          * @param name The name of this node.
          * @param formatedPathCondition The formated path condition.
          * @param pathConditionChanged Is the path condition changed compared to parent?
-         * @param exceptionalTermination Exceptional termination?
+         * @param terminationKind kind of termination
          * @param branchVerified The branch verified flag.
          */
         public KeYlessTermination(IExecutionNode<?> parent, String name,
@@ -2887,7 +2887,7 @@ public static class KeYlessVariable extends AbstractKeYlessExecutionElement
         /**
          * Constructor.
          *
-         * @param parentVariable The parent {@link IExecutionValue} if available.
+         * @param parentValue The parent {@link IExecutionValue} if available.
          * @param isArrayIndex The is array flag.
          * @param arrayIndexString The array index.
          * @param name The name.
@@ -3026,7 +3026,7 @@ public IExecutionNode<?> getTarget() {
         /**
          * Sets the source.
          *
-         * @param target The source to set.
+         * @param source The source to set.
          */
         public void setSource(IExecutionNode<?> source) {
             this.source = source;
@@ -3159,7 +3159,7 @@ public IExecutionVariable getVariable() {
          * {@inheritDoc}
          */
         @Override
-        public IExecutionVariable[] getChildVariables() throws ProofInputException {
+        public IExecutionVariable[] getChildVariables() {
             return childVariables.toArray(new IExecutionVariable[0]);
         }
 
@@ -3216,7 +3216,7 @@ public void addConstraint(IExecutionConstraint constraint) {
          * {@inheritDoc}
          */
         @Override
-        public IExecutionConstraint[] getConstraints() throws ProofInputException {
+        public IExecutionConstraint[] getConstraints() {
             return constraints.toArray(new IExecutionConstraint[0]);
         }
 

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractBackwardSlicer.java

@@ -119,8 +119,7 @@ protected void updateRelevantLocations(final ProgramElement read,
         if (relevantElement != null) {
             Location normalizedElement = normalizeAlias(services, relevantElement, info);
             relevantLocations.add(normalizedElement);
-        } else if (read instanceof NonTerminalProgramElement) {
-            NonTerminalProgramElement ntpe = (NonTerminalProgramElement) read;
+        } else if (read instanceof NonTerminalProgramElement ntpe) {
             for (int i = 0; i < ntpe.getChildCount(); i++) {
                 updateRelevantLocations(ntpe.getChildAt(i), relevantLocations, info, services);
             }

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ReflectionClassCreator.java

@@ -430,24 +430,12 @@ private boolean checkBraces(final StringBuilder buf) {
         int edged = 0;
         for (int i = 0; i < buf.length(); i++) {
             switch (buf.charAt(i)) {
-            case '{':
-                curly++;
-                break;
-            case '}':
-                curly--;
-                break;
-            case '(':
-                round++;
-                break;
-            case ')':
-                round--;
-                break;
-            case '[':
-                edged++;
-                break;
-            case ']':
-                edged--;
-                break;
+            case '{' -> curly++;
+            case '}' -> curly--;
+            case '(' -> round++;
+            case ')' -> round--;
+            case '[' -> edged++;
+            case ']' -> edged--;
             }
         }
         if (curly == 0 && round == 0 && edged == 0) {

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleGenerator.java

@@ -234,18 +234,16 @@ public OracleTerm generateOracle(Term term, boolean initialSelect) {
             OracleTerm left = generateOracle(term.sub(0), initialSelect);
             OracleTerm right = generateOracle(term.sub(1), initialSelect);
             String javaOp = ops.get(op);
+            return switch (javaOp) {
+            case EQUALS -> eq(left, right);
+            case AND -> and(left, right);
+            case OR -> or(left, right);
+            default ->
+                // Todo wiesler: What is this for? No field nor method of OracleBinTerm has any
+                // usages
+                new OracleBinTerm(javaOp, left, right);
+            };
 
-            switch (javaOp) {
-            case EQUALS:
-                return eq(left, right);
-            case AND:
-                return and(left, right);
-            case OR:
-                return or(left, right);
-            }
-
-            // Todo wiesler: What is this for? No field nor method of OracleBinTerm has any usages
-            return new OracleBinTerm(javaOp, left, right);
         } // negation
         else if (op == Junctor.NOT) {
             OracleTerm sub = generateOracle(term.sub(0), initialSelect);

key.core/src/main/java/de/uka/ilkd/key/api/ProofScriptCommandApi.java

@@ -17,12 +17,13 @@
  * @version 1 (21.04.17)
  */
 public class ProofScriptCommandApi {
-    private final Map<String, ProofScriptCommand> commandMap = new HashMap<>();
+    private final Map<String, ProofScriptCommand<?>> commandMap = new HashMap<>();
 
     public ProofScriptCommandApi() {
         initialize();
     }
 
+    @SuppressWarnings("rawtypes")
     private void initialize() {
         ServiceLoader<ProofScriptCommand> loader = ServiceLoader.load(ProofScriptCommand.class);
         loader.forEach(psc -> commandMap.put(psc.getName(), psc));
@@ -35,7 +36,7 @@ private void initialize() {
      *
      * @return a collection of proof script commands
      */
-    public Collection<ProofScriptCommand> getScriptCommands() {
+    public Collection<ProofScriptCommand<?>> getScriptCommands() {
         return commandMap.values();
     }
 

key.core/src/main/java/de/uka/ilkd/key/java/CompilationUnit.java

@@ -7,7 +7,6 @@
 import de.uka.ilkd.key.java.declaration.TypeDeclaration;
 import de.uka.ilkd.key.java.declaration.TypeDeclarationContainer;
 import de.uka.ilkd.key.java.visitor.Visitor;
-import de.uka.ilkd.key.pp.PrettyPrinter;
 
 import org.key_project.util.ExtList;
 import org.key_project.util.collection.ImmutableArray;
@@ -242,10 +241,4 @@ public void visit(Visitor v) {
     }
 
 
-    /** toString */
-    public String toString() {
-        PrettyPrinter pp = PrettyPrinter.purePrinter();
-        pp.print(this);
-        return pp.result();
-    }
 }

key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java

@@ -83,10 +83,6 @@ public static MethodFrame getInnermostMethodFrame(ProgramElement pe, Services se
         final MethodFrame result = new JavaASTVisitor(pe, services) {
             private MethodFrame res;
 
-            protected void doAction(ProgramElement node) {
-                node.visit(this);
-            }
-
             protected void doDefaultAction(SourceElement node) {
                 if (node instanceof MethodFrame && res == null) {
                     res = (MethodFrame) node;