diff --git a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java index ea49e8bd3b3..94addf6468f 100644 --- a/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java +++ b/key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java @@ -204,47 +204,23 @@ 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": @@ -252,33 +228,25 @@ public void startElement(String uri, String localName, String qName, Attributes // 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 -> { + } } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeReader.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeReader.java index 4a0e30d57b9..b49e9b3751b 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeReader.java +++ b/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 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]); } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractBackwardSlicer.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractBackwardSlicer.java index deaa769c55d..bfb10ac3e91 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/slicing/AbstractBackwardSlicer.java +++ b/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); } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ReflectionClassCreator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ReflectionClassCreator.java index db6f015b607..de0aaf772bb 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ReflectionClassCreator.java +++ b/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) { diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleGenerator.java index 00effd2f09e..92b17312e1a 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleGenerator.java +++ b/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); diff --git a/key.core/src/main/java/de/uka/ilkd/key/api/ProofScriptCommandApi.java b/key.core/src/main/java/de/uka/ilkd/key/api/ProofScriptCommandApi.java index 543efa937d2..bd23b64bc18 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/api/ProofScriptCommandApi.java +++ b/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 commandMap = new HashMap<>(); + private final Map> commandMap = new HashMap<>(); public ProofScriptCommandApi() { initialize(); } + @SuppressWarnings("rawtypes") private void initialize() { ServiceLoader 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 getScriptCommands() { + public Collection> getScriptCommands() { return commandMap.values(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/CompilationUnit.java b/key.core/src/main/java/de/uka/ilkd/key/java/CompilationUnit.java index 6e9995109b1..1f4573e5f3f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/CompilationUnit.java +++ b/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(); - } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java b/key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java index f8d3d329ac0..0d3b0f3f3e0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java +++ b/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; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java index e82ce386636..8e21443c5ea 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java @@ -57,17 +57,17 @@ /** * Objects of this class can be used to transform an AST returned by the recoder library to the * corresponding yet immutable KeY data structures. - * + *

* Call the method process() to convert an arbitrary object. - * + *

* The method callConvert is used to perform a run-time dispatch upon the parameters. - * + *

* The actual conversion is done in convert-methods which must be declared public due to the used * reflection method lookup function. - * + *

* There is a general method {@link #callConvert(recoder.java.ProgramElement)} that does the job in * general. Several special cases must be treated separately. - * + *

* This code used to be part of {@link Recoder2KeY} and has been 'out-sourced'. * * @author mattias ulbrich @@ -216,10 +216,10 @@ private boolean isParsingLibs() { /** * convert a recoder ProgramElement to a corresponding KeY data structure entity. - * + *

* Almost always the returned type carries the same Classname but in a KeY rather than a recoder * package. - * + *

* Determines the right convert method using reflection * * @param pe the recoder.java.JavaProgramElement to be converted, not null. @@ -304,7 +304,7 @@ protected Object callConvert(recoder.java.ProgramElement pe) throws ConvertExcep /** * iterate over all children and call convert upon them. Gather the resulting KeY structures in * an ExtList. - * + *

* In addition to the child ast-branches, all comments are gathered also. * * @param pe the NonTerminalProgramElement that needs its children before being converted @@ -396,32 +396,24 @@ private PositionInfo positionInfo(recoder.java.SourceElement se) { * @return a literal constant representing the value of p_er */ private Literal getLiteralFor(recoder.service.ConstantEvaluator.EvaluationResult p_er) { - switch (p_er.getTypeCode()) { - case recoder.service.ConstantEvaluator.BOOLEAN_TYPE: - return BooleanLiteral.getBooleanLiteral(p_er.getBoolean()); - case recoder.service.ConstantEvaluator.CHAR_TYPE: - return new CharLiteral(p_er.getChar()); - case recoder.service.ConstantEvaluator.DOUBLE_TYPE: - return new DoubleLiteral(p_er.getDouble()); - case recoder.service.ConstantEvaluator.FLOAT_TYPE: - return new FloatLiteral(p_er.getFloat()); - case recoder.service.ConstantEvaluator.BYTE_TYPE: - return new IntLiteral(p_er.getByte()); - case recoder.service.ConstantEvaluator.SHORT_TYPE: - return new IntLiteral(p_er.getShort()); - case recoder.service.ConstantEvaluator.INT_TYPE: - return new IntLiteral(p_er.getInt()); - case recoder.service.ConstantEvaluator.LONG_TYPE: - return new LongLiteral(p_er.getLong()); - case recoder.service.ConstantEvaluator.STRING_TYPE: - if (p_er.getString() == null) { - return NullLiteral.NULL; + return switch (p_er.getTypeCode()) { + case recoder.service.ConstantEvaluator.BOOLEAN_TYPE -> BooleanLiteral.getBooleanLiteral(p_er.getBoolean()); + case recoder.service.ConstantEvaluator.CHAR_TYPE -> new CharLiteral(p_er.getChar()); + case recoder.service.ConstantEvaluator.DOUBLE_TYPE -> new DoubleLiteral(p_er.getDouble()); + case recoder.service.ConstantEvaluator.FLOAT_TYPE -> new FloatLiteral(p_er.getFloat()); + case recoder.service.ConstantEvaluator.BYTE_TYPE -> new IntLiteral(p_er.getByte()); + case recoder.service.ConstantEvaluator.SHORT_TYPE -> new IntLiteral(p_er.getShort()); + case recoder.service.ConstantEvaluator.INT_TYPE -> new IntLiteral(p_er.getInt()); + case recoder.service.ConstantEvaluator.LONG_TYPE -> new LongLiteral(p_er.getLong()); + case recoder.service.ConstantEvaluator.STRING_TYPE -> { + if (p_er.getString() == null) { + yield NullLiteral.NULL; + } + yield new StringLiteral("\"" + p_er.getString() + "\""); } - return new StringLiteral("\"" + p_er.getString() + "\""); - default: - throw new ConvertException( - "Don't know how to handle type " + p_er.getTypeCode() + " of " + p_er); - } + default -> throw new ConvertException( + "Don't know how to handle type " + p_er.getTypeCode() + " of " + p_er); + }; } @@ -464,9 +456,9 @@ private ProgramVariable find(String name, ImmutableList fields) { /** * The default procedure. - * + *

* It iterates over all children, calls convert upon them - * + *

* collect all children, convert them. Create a new instance of the corresponding KeY class and * call its constructor with the list of children. * @@ -567,7 +559,7 @@ private String getKeYName(Class recod /** * determines the right standard constructor of the KeYClass. - * + *

* Use a cache to only look up classes once. * * @param recoderClass the Class of the recoder AST object diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java index 8a0ff3c8dce..1b0a1f4c1bc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java @@ -185,12 +185,6 @@ public MethodFrame convert(de.uka.ilkd.key.java.recoderext.RMethodCallStatement (StatementBlock) callConvert(l.getBody())); } - public LoopScopeBlock convert(de.uka.ilkd.key.java.recoderext.LoopScopeBlock l) { - return new LoopScopeBlock( - (de.uka.ilkd.key.logic.op.IProgramVariable) callConvert(l.getIndexPV()), - (StatementBlock) callConvert(l.getBody())); - } - /** * translate method body statements. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/Operator.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/Operator.java index 7cdd80bb1ec..ff1a653287a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/Operator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/Operator.java @@ -23,18 +23,11 @@ public abstract class Operator extends JavaNonTerminalProgramElement implements Expression, ExpressionContainer { - - - /** - * Children. - */ protected final ImmutableArray children; - /** * Relative positioning of the operator. */ - public static final int PREFIX = 0; public static final int INFIX = 1; public static final int POSTFIX = 2; @@ -123,37 +116,25 @@ public boolean isLeftAssociative() { } public SourceElement getFirstElement() { - switch (getNotation()) { - case INFIX: - case POSTFIX: - return children.get(0).getFirstElement(); - case PREFIX: - default: - return this; - } + return switch (getNotation()) { + case INFIX, POSTFIX -> children.get(0).getFirstElement(); + default -> this; + }; } @Override public SourceElement getFirstElementIncludingBlocks() { - switch (getNotation()) { - case INFIX: - case POSTFIX: - return children.get(0).getFirstElementIncludingBlocks(); - case PREFIX: - default: - return this; - } + return switch (getNotation()) { + case INFIX, POSTFIX -> children.get(0).getFirstElementIncludingBlocks(); + default -> this; + }; } public SourceElement getLastElement() { - switch (getNotation()) { - case INFIX: - case PREFIX: - return children.get(getArity() - 1).getLastElement(); - case POSTFIX: - default: - return this; - } + return switch (getNotation()) { + case INFIX, PREFIX -> children.get(getArity() - 1).getLastElement(); + default -> this; + }; } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/ParenthesizedExpression.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/ParenthesizedExpression.java index 23d197a71fe..f2f60d7b999 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/ParenthesizedExpression.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/ParenthesizedExpression.java @@ -33,29 +33,6 @@ public ParenthesizedExpression(Expression child) { super(child); } - /** - * Returns the number of children of this node. - * - * @return an int giving the number of children of this node - */ - public int getChildCount() { - return (children != null) ? children.size() : 0; - } - - /** - * Returns the child at the specified index in this node's "virtual" child array - * - * @param index an index into this node's "virtual" child array - * @return the program element at the given position - * @exception ArrayIndexOutOfBoundsException if index is out of bounds - */ - public ProgramElement getChildAt(int index) { - if (children != null) { - return children.get(index); - } - throw new ArrayIndexOutOfBoundsException(); - } - /** * Get arity. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/CharLiteral.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/CharLiteral.java index a758c9d87c3..ebf7131ff37 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/CharLiteral.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/CharLiteral.java @@ -36,7 +36,7 @@ public CharLiteral(char charVal) { * the Java 8 Language Specification: chars written directly (like 'a', '0', 'Z'), Java escape * chars (like '\n', '\r'), and octal Unicode escapes (like '\040'). Note that unicode escapes * in hexadecimal form are processed earlier and don't have to be handled here. - * + *

* Note that the char must be enclosed in single-quotes. * * @param children an ExtList with all children(comments). May contain: Comments @@ -94,7 +94,7 @@ public String getValueString() { * 'a', '0', 'Z'), Java escape chars (like '\n', '\r'), and octal Unicode escapes (like '\040'). * Note that unicode escapes in hexadecimal form are processed earlier and don't have to be * handled by this method. - * + *

* This method does not check the length of the literal for validity. * * @param sourceStr the String containing the literal surrounded by single-quotes @@ -116,37 +116,20 @@ protected char parseFromString(final String sourceStr) { * 3. octal Unicode escape like '\040' */ if (valStr.charAt(0) == '\\') { - switch (valStr.charAt(1)) { - case 'b': - return '\b'; - case 't': - return '\t'; - case 'n': - return '\n'; - case 'f': - return '\f'; - case 'r': - return '\r'; - case '\"': - return '\"'; - case '\'': - return '\''; - case '\\': - return '\\'; - case '0': - case '1': - case '2': - case '3': - case '4': - case '5': - case '6': - case '7': - return (char) Integer.parseInt(valStr.substring(1), 8); - case 'u': - return (char) Integer.parseInt(valStr.substring(2), 16); - default: - throw new NumberFormatException("Invalid char: " + sourceStr); - } + return switch (valStr.charAt(1)) { + case 'b' -> '\b'; + case 't' -> '\t'; + case 'n' -> '\n'; + case 'f' -> '\f'; + case 'r' -> '\r'; + case '\"' -> '\"'; + case '\'' -> '\''; + case '\\' -> '\\'; + case '0', '1', '2', '3', '4', '5', '6', '7' -> (char) Integer + .parseInt(valStr.substring(1), 8); + case 'u' -> (char) Integer.parseInt(valStr.substring(2), 16); + default -> throw new NumberFormatException("Invalid char: " + sourceStr); + }; } else { return valStr.charAt(0); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExecCtxtSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExecCtxtSVWrapper.java index 3958ed20807..31b4797f03f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExecCtxtSVWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExecCtxtSVWrapper.java @@ -5,7 +5,6 @@ import de.uka.ilkd.key.logic.op.SchemaVariable; -import recoder.java.SourceElement; import recoder.java.SourceVisitor; public class ExecCtxtSVWrapper extends ExecutionContext implements KeYRecoderExtension, SVWrapper { @@ -37,10 +36,6 @@ public SchemaVariable getSV() { return sv; } - public SourceElement getFirstElement() { - return this; - } - public ExecutionContext deepClone() { return new ExecCtxtSVWrapper(sv); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExpressionSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExpressionSVWrapper.java index bf2a57d60cd..576e3d8d0dc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExpressionSVWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExpressionSVWrapper.java @@ -6,9 +6,7 @@ import de.uka.ilkd.key.logic.op.SchemaVariable; import recoder.java.Expression; -import recoder.java.ExpressionContainer; import recoder.java.LoopInitializer; -import recoder.java.NonTerminalProgramElement; import recoder.java.SourceVisitor; import recoder.java.StatementContainer; import recoder.java.expression.Literal; @@ -48,15 +46,6 @@ public ExpressionSVWrapper(SchemaVariable sv) { public void makeParentRoleValid() { } - /** - * Get AST parent. - * - * @return the non terminal program element. - */ - public NonTerminalProgramElement getASTParent() { - return expressionParent; - } - /** * sets the schema variable of sort statement @@ -73,24 +62,6 @@ public SchemaVariable getSV() { } - /** - * Get expression container. - * - * @return the expression container. - */ - public ExpressionContainer getExpressionContainer() { - return expressionParent; - } - - /** - * Set expression container. - * - * @param c an expression container. - */ - public void setExpressionContainer(ExpressionContainer c) { - expressionParent = c; - } - // don't think we need it public void accept(SourceVisitor v) { } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java index 4de44319c30..87c826ea835 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java @@ -28,7 +28,7 @@ * The Java DL requires some implicit fields, that are available in each Java class. The name of the * implicit fields is usually enclosed between two angle brackets. To access the fields in a uniform * way, they are added as usual fields to the classes, in particular this allows us to parse them in - * more easier. For further information see also + * easier. For further information see also *

    *
  • {@link ImplicitFieldAdder}
    • *
  • {@link CreateObjectBuilder}
    • @@ -43,7 +43,7 @@ public abstract class RecoderModelTransformer extends TwoPassTransformation { protected final TransformerCache cache; /** - * creates a transormder for the recoder model + * creates a transformer for the recoder model * * @param services the CrossReferenceServiceConfiguration to access model information * @param cache a cache object that stores information which is needed by and common to many @@ -67,45 +67,32 @@ public Expression getDefaultValue(Type type) { if (type instanceof ClassType || type instanceof ArrayType) { return new NullLiteral(); } else if (type instanceof PrimitiveType) { - switch (type.getName()) { - case "boolean": - return new BooleanLiteral(false); - case "byte": - case "short": - case "int": - case "\\bigint": - return new IntLiteral(0); - case "long": - return new LongLiteral(0); - case "\\real": - return new RealLiteral(); - case "char": - return new CharLiteral((char) 0); - case "float": - return new FloatLiteral(0.0F); - case "double": - return new DoubleLiteral(0.0D); - case "\\locset": - return EmptySetLiteral.INSTANCE; - case "\\seq": - return EmptySeqLiteral.INSTANCE; - case "\\set": - return new DLEmbeddedExpression("emptySet", Collections.emptyList()); - case "\\free": - return new DLEmbeddedExpression("atom", Collections.emptyList()); - case "\\map": - return EmptyMapLiteral.INSTANCE; - default: - if (type.getName().startsWith("\\dl_")) { - // The default value of a type is resolved later, then we know the Sort of the - // type - return new DLEmbeddedExpression( - "\\dl_DEFAULT_VALUE_" + type.getName().substring(4), - Collections.emptyList()); + return switch (type.getName()) { + case "boolean" -> new BooleanLiteral(false); + case "byte", "short", "int", "\\bigint" -> new IntLiteral(0); + case "long" -> new LongLiteral(0); + case "\\real" -> new RealLiteral(); + case "char" -> new CharLiteral((char) 0); + case "float" -> new FloatLiteral(0.0F); + case "double" -> new DoubleLiteral(0.0D); + case "\\locset" -> EmptySetLiteral.INSTANCE; + case "\\seq" -> EmptySeqLiteral.INSTANCE; + case "\\set" -> new DLEmbeddedExpression("emptySet", Collections.emptyList()); + case "\\free" -> new DLEmbeddedExpression("atom", Collections.emptyList()); + case "\\map" -> EmptyMapLiteral.INSTANCE; + default -> { + if (type.getName().startsWith("\\dl_")) { + // The default value of a type is resolved later, then we know the Sort of the + // type + yield new DLEmbeddedExpression( + "\\dl_DEFAULT_VALUE_" + type.getName().substring(4), + Collections.emptyList()); + } + Debug.fail("makeImplicitMembersExplicit: unknown primitive type" + type); + yield null; } - } + }; } - Debug.fail("makeImplicitMembersExplicit: unknown primitive type" + type); return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SpecialReferenceWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SpecialReferenceWrapper.java index 33e1bdc01ea..cd2d6630b33 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SpecialReferenceWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SpecialReferenceWrapper.java @@ -54,24 +54,6 @@ public NonTerminalProgramElement getASTParent() { } - /** - * Get expression container. - * - * @return the expression container. - */ - public ExpressionContainer getExpressionContainer() { - return expressionParent; - } - - /** - * Set expression container. - * - * @param c an expression container. - */ - public void setExpressionContainer(ExpressionContainer c) { - expressionParent = c; - } - // don't think we need it public void accept(SourceVisitor v) { } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/Intersect.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/Intersect.java index b0cd9859efe..c4797a78e2a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/Intersect.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/Intersect.java @@ -38,12 +38,6 @@ public int getArity() { } - @Override - public int getPrecedence() { - return 0; - } - - @Override public int getNotation() { return PREFIX; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/SchematicFieldReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/SchematicFieldReference.java index 8fd2827d609..9e4758638bd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/SchematicFieldReference.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/SchematicFieldReference.java @@ -76,15 +76,6 @@ public ProgramElement getChildAt(int index) { throw new ArrayIndexOutOfBoundsException(); } - /** - * Get reference prefix. - * - * @return the reference prefix. - */ - public ReferencePrefix getReferencePrefix() { - return prefix; - } - /** * Get reference prefix. * @@ -105,16 +96,6 @@ public ReferencePrefix setReferencePrefix(ReferencePrefix rp) { } - /** - * Get the number of type references in this container. - * - * @return the number of type references. - */ - - public int getTypeReferenceCount() { - return (prefix instanceof TypeReference) ? 1 : 0; - } - /** * Return the type reference at the specified index in this node's "virtual" type reference * array. @@ -130,15 +111,6 @@ public TypeReference getTypeReferenceAt(int index) { throw new ArrayIndexOutOfBoundsException(); } - /** - * Get the number of expressions in this container. - * - * @return the number of expressions. - */ - public int getExpressionCount() { - return (prefix instanceof Expression) ? 1 : 0; - } - /** * Return the expression at the specified index in this node's "virtual" expression array. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Do.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Do.java index 49cf1d19e0b..609ecaf1d38 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Do.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Do.java @@ -50,10 +50,6 @@ public Do(Expression guard, Statement body, PositionInfo pos) { super(guard, body, pos); } - public SourceElement getLastElement() { - return this; - } - /** * Is checked before iteration. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/DeclarationProgramVariableCollector.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/DeclarationProgramVariableCollector.java index 2ac2ec578c6..165a48b1190 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/DeclarationProgramVariableCollector.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/DeclarationProgramVariableCollector.java @@ -14,8 +14,6 @@ import de.uka.ilkd.key.java.declaration.ImplicitFieldSpecification; import de.uka.ilkd.key.java.declaration.VariableSpecification; import de.uka.ilkd.key.logic.op.IProgramVariable; -import de.uka.ilkd.key.logic.op.LocationVariable; -import de.uka.ilkd.key.logic.op.ProgramConstant; /** * The DeclarationProgramVariableCollector collects all top level declared program variables @@ -71,12 +69,4 @@ public void performActionOnImplicitFieldSpecification(ImplicitFieldSpecification addVariable(x.getProgramVariable()); } - public void performActionOnLocationVariable(LocationVariable x) { - performActionOnProgramVariable(x); - } - - public void performActionOnProgramConstant(ProgramConstant x) { - performActionOnProgramVariable(x); - } - } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramReplaceVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramReplaceVisitor.java index a5a36c0c8a1..a8a738e456f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramReplaceVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramReplaceVisitor.java @@ -38,14 +38,6 @@ public ProgramReplaceVisitor(ProgramElement root, Services services, SVInstantia svinsts = svi; } - /** - * the action that is performed just before leaving the node the last time - */ - @Override - protected void doAction(ProgramElement node) { - node.visit(this); - } - /** starts the walker */ @Override public void start() { @@ -68,11 +60,6 @@ public ProgramElement result() { return result; } - @Override - public String toString() { - return stack.peek().toString(); - } - /** * the implemented default action is called if a program element is, and if it has children all * its children too are left unchanged diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/CharListLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/CharListLDT.java index 5348f863eee..c2a9364d08d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/CharListLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/CharListLDT.java @@ -76,9 +76,9 @@ public CharListLDT(TermServices services) { // ------------------------------------------------------------------------- private String translateCharTerm(Term t) { - char charVal = 0; - int intVal = 0; - String result = printlastfirst(t.sub(0)).toString(); + char charVal; + int intVal; + String result = printLastFirst(t.sub(0)).toString(); try { intVal = Integer.parseInt(result); charVal = (char) intVal; @@ -93,11 +93,11 @@ private String translateCharTerm(Term t) { } - private StringBuffer printlastfirst(Term t) { + private StringBuffer printLastFirst(Term t) { if (t.op().arity() == 0) { return new StringBuffer(); } else { - return printlastfirst(t.sub(0)).append(t.op().name().toString()); + return printLastFirst(t.sub(0)).append(t.op().name().toString()); } } @@ -250,12 +250,10 @@ public Type getType(Term t) { @Nullable @Override public Function getFunctionFor(String operationName, Services services) { - switch (operationName) { // This is not very elegant; but seqConcat is actually in the SeqLDT. - case "add": + if (operationName.equals("add")) { return services.getNamespaces().functions().lookup("seqConcat"); - default: - return null; } + return null; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/DoubleLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/DoubleLDT.java index b30515b750e..3c9113b467e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/DoubleLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/DoubleLDT.java @@ -155,47 +155,29 @@ public Term translateLiteral(Literal lit, Services services) { @Override public Function getFunctionFor(String op, Services services) { - switch (op) { - case "gt": - return getGreaterThan(); - case "geq": - return getGreaterOrEquals(); - case "lt": - return getLessThan(); - case "leq": - return getLessOrEquals(); - case "div": - return getDiv(); - case "mul": - return getMul(); - case "add": - return getAdd(); - case "sub": - return getSub(); - case "neg": - return getNeg(); + return switch (op) { + case "gt" -> getGreaterThan(); + case "geq" -> getGreaterOrEquals(); + case "lt" -> getLessThan(); + case "leq" -> getLessOrEquals(); + case "div" -> getDiv(); + case "mul" -> getMul(); + case "add" -> getAdd(); + case "sub" -> getSub(); + case "neg" -> getNeg(); // Floating point extensions with "\fp_" - case "nan": - return getIsNaN(); - case "zero": - return getIsZero(); - case "infinite": - return getIsInfinite(); - case "nice": - return getIsNice(); - case "abs": - return getAbs(); - case "negative": - return getIsNegative(); - case "positive": - return getIsPositive(); - case "subnormal": - return getIsSubnormal(); - case "normal": - return getIsNormal(); - } - return null; + case "nan" -> getIsNaN(); + case "zero" -> getIsZero(); + case "infinite" -> getIsInfinite(); + case "nice" -> getIsNice(); + case "abs" -> getAbs(); + case "negative" -> getIsNegative(); + case "positive" -> getIsPositive(); + case "subnormal" -> getIsSubnormal(); + case "normal" -> getIsNormal(); + default -> null; + }; } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/FloatLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/FloatLDT.java index 8c694458b75..f4ea89fc7d6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/FloatLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/FloatLDT.java @@ -156,46 +156,28 @@ public Function getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Serv @Override public Function getFunctionFor(String op, Services services) { - switch (op) { - case "gt": - return getGreaterThan(); - case "geq": - return getGreaterOrEquals(); - case "lt": - return getLessThan(); - case "leq": - return getLessOrEquals(); - case "div": - return getDiv(); - case "mul": - return getMul(); - case "add": - return getAdd(); - case "sub": - return getSub(); - case "neg": - return getNeg(); + return switch (op) { + case "gt" -> getGreaterThan(); + case "geq" -> getGreaterOrEquals(); + case "lt" -> getLessThan(); + case "leq" -> getLessOrEquals(); + case "div" -> getDiv(); + case "mul" -> getMul(); + case "add" -> getAdd(); + case "sub" -> getSub(); + case "neg" -> getNeg(); // Floating point extensions with "\fp_" - case "nan": - return getIsNaN(); - case "zero": - return getIsZero(); - case "infinite": - return getIsInfinite(); - case "nice": - return getIsNice(); - case "abs": - return getAbs(); - case "negative": - return getIsNegative(); - case "positive": - return getIsPositive(); - case "subnormal": - return getIsSubnormal(); - case "normal": - return getIsNormal(); - } - return null; + case "nan" -> getIsNaN(); + case "zero" -> getIsZero(); + case "infinite" -> getIsInfinite(); + case "nice" -> getIsNice(); + case "abs" -> getAbs(); + case "negative" -> getIsNegative(); + case "positive" -> getIsPositive(); + case "subnormal" -> getIsSubnormal(); + case "normal" -> getIsNormal(); + default -> null; + }; } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/IntegerLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/IntegerLDT.java index 644ea234ab7..1df2ea60b98 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/IntegerLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/IntegerLDT.java @@ -718,29 +718,19 @@ public Function getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Serv @Nullable @Override public Function getFunctionFor(String op, Services services) { - switch (op) { - case "gt": - return getGreaterThan(); - case "geq": - return getGreaterOrEquals(); - case "lt": - return getLessThan(); - case "leq": - return getLessOrEquals(); - case "div": - return getDiv(); - case "mul": - return getMul(); - case "add": - return getAdd(); - case "sub": - return getSub(); - case "mod": - return getMod(); - case "neg": - return getNeg(); - } - return null; + return switch (op) { + case "gt" -> getGreaterThan(); + case "geq" -> getGreaterOrEquals(); + case "lt" -> getLessThan(); + case "leq" -> getLessOrEquals(); + case "div" -> getDiv(); + case "mul" -> getMul(); + case "add" -> getAdd(); + case "sub" -> getSub(); + case "mod" -> getMod(); + case "neg" -> getNeg(); + default -> null; + }; } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/LocSetLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/LocSetLDT.java index b91db6fce27..c8fc40887f9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/LocSetLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/LocSetLDT.java @@ -213,17 +213,12 @@ public Type getType(Term t) { @Nullable @Override public Function getFunctionFor(String operationName, Services services) { - switch (operationName) { - case "add": - return getUnion(); - case "sub": - return getSetMinus(); - case "mul": - return getIntersect(); - case "le": - return getSubset(); - default: - return null; - } + return switch (operationName) { + case "add" -> getUnion(); + case "sub" -> getSetMinus(); + case "mul" -> getIntersect(); + case "le" -> getSubset(); + default -> null; + }; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java index a78f133ef49..34487d51677 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java @@ -104,8 +104,6 @@ public Function getSeqDef() { /** * Placeholder for the sequence of values observed through the execution of an enhanced for * loop. Follows David Cok's proposal to adapt JML to Java5. - * - * @return */ public Function getValues() { return values; @@ -167,12 +165,10 @@ public Function getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Serv @Nullable @Override public Function getFunctionFor(String operationName, Services services) { - switch (operationName) { - case "add": + if (operationName.equals("add")) { return getSeqConcat(); - default: - return null; } + return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/FormulaTermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/FormulaTermLabel.java index 02bf571c002..9a4a79019f1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/FormulaTermLabel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/FormulaTermLabel.java @@ -134,14 +134,11 @@ public String toString() { */ @Override public Object getChild(int i) { - switch (i) { - case 0: - return getId(); - case 1: - return beforeIds; - default: - return null; - } + return switch (i) { + case 0 -> getId(); + case 1 -> beforeIds; + default -> null; + }; } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java index 028e69af9f8..a61b890cf76 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java @@ -369,11 +369,6 @@ public ProgramVariableSort() { super(new Name("Variable")); } - @Override - public boolean canStandFor(Term t) { - return t.op() instanceof ProgramVariable; - } - @Override protected boolean canStandFor(ProgramElement pe, Services services) { ProgramVariable accessedField = null; @@ -464,11 +459,6 @@ protected SimpleExpressionSort(Name n) { super(n); } - @Override - public boolean canStandFor(Term t) { - return true; - } - @Override protected boolean canStandFor(ProgramElement pe, Services services) { if (pe instanceof Negative) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EngineState.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EngineState.java index 2756439fa64..35d358ca81d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EngineState.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EngineState.java @@ -4,9 +4,9 @@ package de.uka.ilkd.key.macros.scripts; import java.io.File; -import java.io.StringReader; import java.util.Deque; import java.util.LinkedList; +import java.util.Objects; import java.util.Optional; import java.util.function.Consumer; import javax.annotation.Nonnull; @@ -16,7 +16,7 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.sort.Sort; import de.uka.ilkd.key.macros.scripts.meta.ValueInjector; -import de.uka.ilkd.key.parser.DefaultTermParser; +import de.uka.ilkd.key.nparser.KeyIO; import de.uka.ilkd.key.parser.ParserException; import de.uka.ilkd.key.pp.AbbrevMap; import de.uka.ilkd.key.proof.Goal; @@ -26,13 +26,13 @@ import org.key_project.util.collection.ImmutableList; +import org.antlr.v4.runtime.CharStreams; + /** * @author Alexander Weigl * @version 1 (28.03.17) */ public class EngineState { - private final static DefaultTermParser PARSER = new DefaultTermParser(); - // private final Map arbitraryVariables = new HashMap<>(); private final Proof proof; private final AbbrevMap abbrevMap = new AbbrevMap(); /** @@ -159,20 +159,16 @@ private Goal findGoalFromRoot(final Node rootNode, boolean checkAutomatic) { int childCount = node.childrenCount(); switch (childCount) { - case 0: + case 0 -> { result = getGoal(proof.openGoals(), node); - if (!checkAutomatic || result.isAutomatic()) { + if (!checkAutomatic || Objects.requireNonNull(result).isAutomatic()) { // We found our goal break loop; } node = choices.pollLast(); - break; - - case 1: - node = node.child(0); - break; - - default: + } + case 1 -> node = node.child(0); + default -> { Node next = null; for (int i = 0; i < childCount; i++) { Node child = node.child(i); @@ -186,31 +182,39 @@ private Goal findGoalFromRoot(final Node rootNode, boolean checkAutomatic) { } assert next != null; node = next; - break; + } } } return result; } + public Term toTerm(String string, Sort sort) throws ParserException, ScriptException { - StringReader reader = new StringReader(string); + final var io = getKeyIO(); + var term = io.parseExpression(string); + if (sort == null || term.sort().equals(sort)) + return term; + else + throw new IllegalStateException( + "Unexpected sort for term: " + term + ". Expected: " + sort); + } + + @Nonnull + private KeyIO getKeyIO() throws ScriptException { Services services = proof.getServices(); - return PARSER.parse(reader, sort, services, - getFirstOpenAutomaticGoal().getLocalNamespaces(), abbrevMap); + KeyIO io = new KeyIO(services, getFirstOpenAutomaticGoal().getLocalNamespaces()); + io.setAbbrevMap(abbrevMap); + return io; } - public Sort toSort(String sortName) throws ParserException, ScriptException { + public Sort toSort(String sortName) throws ScriptException { return (getFirstOpenAutomaticGoal() == null ? getProof().getServices().getNamespaces() : getFirstOpenAutomaticGoal().getLocalNamespaces()).sorts().lookup(sortName); } - public Sequent toSequent(String sequent) throws ParserException, ScriptException { - StringReader reader = new StringReader(sequent); - Services services = proof.getServices(); - - return PARSER.parseSeq(reader, services, - getFirstOpenAutomaticGoal().getLocalNamespaces(), getAbbreviations()); + public Sequent toSequent(String sequent) throws ScriptException { + return getKeyIO().parseSequent(CharStreams.fromString(sequent)); } public int getMaxAutomaticSteps() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptLineParser.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptLineParser.java index 22261286d39..4f4c84298b4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptLineParser.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptLineParser.java @@ -110,69 +110,62 @@ public ParsedCommand parseCommand() throws IOException, ScriptException { } switch (c) { - case -1: - if (sb.length() > 0 || key != null || !result.isEmpty()) { + case -1 -> { + if (!sb.isEmpty() || key != null || !result.isEmpty()) { throw new ScriptException("Trailing characters at end of script (missing ';'?)", getLocation()); } return null; - case '=': + } + case '=' -> { switch (state) { - case IN_ID: + case IN_ID -> { state = State.AFTER_EQ; key = sb.toString(); sb.setLength(0); - break; - case IN_QUOTE: - sb.append((char) c); - break; - case IN_COMMENT: - break; - default: - exc(c); } - break; - case ' ': - case '\t': - case '\n': + case IN_QUOTE -> sb.append((char) c); + case IN_COMMENT -> { + } + default -> exc(c); + } + } + case ' ', '\t', '\n' -> { switch (state) { - case IN_ID: + case IN_ID -> { state = State.INIT; result.put("#" + (impCounter++), sb.toString()); sb.setLength(0); - break; - case IN_QUOTE: - sb.append((char) c); - break; - case IN_UNQUOTE: + } + case IN_QUOTE -> sb.append((char) c); + case IN_UNQUOTE -> { state = State.INIT; result.put(key, sb.toString()); sb.setLength(0); - break; - case IN_COMMENT: + } + case IN_COMMENT -> { if (c == '\n') { state = stateBeforeComment; } - break; - default: - break; } - break; - case '\r': - break; - case '"': - case '\'': + default -> { + } + } + } + case '\r' -> { + } + case '"', '\'' -> { switch (state) { - case INIT: + case INIT -> { state = State.IN_QUOTE; stringInitChar = c; key = "#" + (impCounter++); - break; - case AFTER_EQ: + } + case AFTER_EQ -> { state = State.IN_QUOTE; stringInitChar = c; - break; - case IN_QUOTE: + } + case IN_QUOTE -> { if (stringInitChar == c) { state = State.INIT; result.put(key, sb.toString()); @@ -180,75 +173,62 @@ public ParsedCommand parseCommand() throws IOException, ScriptException { } else { sb.append((char) c); } - break; - case IN_COMMENT: - break; - default: - exc(c); } - break; - case '#': + case IN_COMMENT -> { + } + default -> exc(c); + } + } + case '#' -> { switch (state) { - case IN_QUOTE: - sb.append((char) c); - break; - case IN_COMMENT: - break; - default: + case IN_QUOTE -> sb.append((char) c); + case IN_COMMENT -> { + } + default -> { stateBeforeComment = state; state = State.IN_COMMENT; } - break; - case ';': + } + } + case ';' -> { switch (state) { - case IN_QUOTE: - sb.append((char) c); - break; - case IN_COMMENT: - break; - case IN_ID: - result.put("#" + (impCounter++), sb.toString()); - break; - case INIT: - break; - case IN_UNQUOTE: - result.put(key, sb.toString()); - break; - default: - exc(c); + case IN_QUOTE -> sb.append((char) c); + case IN_COMMENT, INIT -> { + } + case IN_ID -> result.put("#" + (impCounter++), sb.toString()); + case IN_UNQUOTE -> result.put(key, sb.toString()); + default -> exc(c); } if (state != State.IN_COMMENT && state != State.IN_QUOTE) { result.put(LITERAL_KEY, cmdBuilder.toString().trim()); var end = getLocation(); return new ParsedCommand(result, start, end); } - break; - default: + } + default -> { switch (state) { - case INIT: - case IN_ID: + case INIT, IN_ID -> { state = State.IN_ID; // fallthru intended! if (!isIDChar(c)) { exc(c); } sb.append((char) c); - break; - case IN_UNQUOTE: - case AFTER_EQ: + } + case IN_UNQUOTE, AFTER_EQ -> { state = State.IN_UNQUOTE; if (!isIDChar(c)) { exc(c); } sb.append((char) c); - break; - case IN_QUOTE: - sb.append((char) c); - break; - case IN_COMMENT: - break; - default: + } + case IN_QUOTE -> sb.append((char) c); + case IN_COMMENT -> { + } + default -> { assert false; } + } + } } if (state != State.IN_COMMENT) { cmdBuilder.append((char) c); diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SelectCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SelectCommand.java index e4cca9e09dc..0fb1b181bad 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SelectCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SelectCommand.java @@ -104,15 +104,9 @@ private Goal findGoalWith(Function filter, Function g } switch (childCount) { - case 0: - node = choices.pollLast(); - break; - - case 1: - node = node.child(0); - break; - - default: + case 0 -> node = choices.pollLast(); + case 1 -> node = node.child(0); + default -> { Node next = null; for (int i = 0; i < childCount; i++) { Node child = node.child(i); @@ -126,7 +120,7 @@ private Goal findGoalWith(Function filter, Function g } assert next != null; node = next; - break; + } } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/ValueInjector.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/ValueInjector.java index ef30a1b4954..a94da0c5e24 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/ValueInjector.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/ValueInjector.java @@ -31,7 +31,7 @@ public class ValueInjector { * T --> StringConverter * */ - private final Map converters = new HashMap<>(); + private final Map, StringConverter> converters = new HashMap<>(); /** * Injects the given {@code arguments} in the {@code obj}. For more details see @@ -163,7 +163,7 @@ private void injectIntoField(ProofScriptArgument meta, Map ar if (meta.isRequired()) { throw new ArgumentRequiredException(String.format( "Argument %s:%s is required, but %s was given. " + "For comamnd class: '%s'", - meta.getName(), meta.getField().getType(), val, meta.getCommand().getClass()), + meta.getName(), meta.getField().getType(), null, meta.getCommand().getClass()), meta); } } else { diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/ProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/ProofReplayer.java index 11522dc0664..c429e1fb7b7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/ProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/ProofReplayer.java @@ -4,8 +4,10 @@ package de.uka.ilkd.key.nparser; import java.net.URI; -import java.net.URL; -import java.util.*; +import java.util.ArrayDeque; +import java.util.Deque; +import java.util.LinkedHashMap; +import java.util.Map; import javax.annotation.Nonnull; import de.uka.ilkd.key.java.Position; @@ -25,7 +27,7 @@ * * @author Alexander Weigl * @version 1 (12/5/19) - * @see #run(Token, CharStream, IProofFileParser, URL) + * @see #run(Token, CharStream, IProofFileParser, URI) */ public class ProofReplayer { /** @@ -63,7 +65,7 @@ public static void run(@Nonnull Token token, CharStream input, IProofFileParser * Replays the proof behind the given {@code input}. This method uses the {@link KeYLexer} to * lex input stream, and parse them manually by consuming the tokens. It singals to the given * {@link IProofFileParser} at start or end of an expr. - * + *

    * Avoid the usage of a parser, avoids also the construction of an ASTs. * * @param input a valid input stream @@ -82,12 +84,11 @@ public static void run(CharStream input, IProofFileParser prl, final int startLi while (true) { int type = stream.LA(1); // current token type switch (type) { - case KeYLexer.LPAREN: + case KeYLexer.LPAREN -> { // expected "(" ["string"] stream.consume(); // consume the "(" Token idToken = stream.LT(1); // element id IProofFileParser.ProofElementID cur = proofSymbolElementId.get(idToken.getText()); - if (cur == null) { Location loc = new Location(source, Position.fromToken(idToken).offsetLine(startLine - 1)); @@ -95,7 +96,6 @@ public static void run(CharStream input, IProofFileParser prl, final int startLi loc); } stream.consume(); - String arg = null; int pos = idToken.getLine() + startLine; if (stream.LA(1) == KeYLexer.STRING_LITERAL) { @@ -104,19 +104,18 @@ public static void run(CharStream input, IProofFileParser prl, final int startLi arg = unescape(arg.substring(1, arg.length() - 1)); stream.consume();// throw string away } - prl.beginExpr(cur, arg); stack.push(cur); posStack.push(pos); - break; - case KeYLexer.RPAREN: + } + case KeYLexer.RPAREN -> { prl.endExpr(stack.pop(), posStack.pop()); stream.consume(); - break; - case KeYLexer.EOF: + } + case KeYLexer.EOF -> { return; - default: - stream.consume(); + } + default -> stream.consume(); } } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java index b9b6a6446cf..1d45254f8b2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java @@ -130,9 +130,6 @@ public static String trimJavaBlock(String raw) { /** * Given a raw modality string, this method determines the operator name. - * - * @param raw - * @return */ public static String operatorOfJavaBlock(String raw) { if (raw.startsWith("\\<")) { @@ -341,23 +338,12 @@ public Object visitWeak_arith_term(KeYParser.Weak_arith_termContext ctx) { for (int i = 0; i < terms.size(); i++) { String opname = ""; switch (ctx.op.get(i).getType()) { - case KeYLexer.UTF_INTERSECT: - opname = "intersect"; - break; - case KeYLexer.UTF_SETMINUS: - opname = "setMinus"; - break; - case KeYLexer.UTF_UNION: - opname = "union"; - break; - case KeYLexer.PLUS: - opname = "add"; - break; - case KeYLexer.MINUS: - opname = "sub"; - break; - default: - semanticError(ctx, "Unexpected token: %s", ctx.op.get(i)); + case KeYLexer.UTF_INTERSECT -> opname = "intersect"; + case KeYLexer.UTF_SETMINUS -> opname = "setMinus"; + case KeYLexer.UTF_UNION -> opname = "union"; + case KeYLexer.PLUS -> opname = "add"; + case KeYLexer.MINUS -> opname = "sub"; + default -> semanticError(ctx, "Unexpected token: %s", ctx.op.get(i)); } Term cur = terms.get(i); last = binaryLDTSpecificTerm(ctx, opname, last, cur); @@ -504,7 +490,7 @@ private LogicVariable bindVar(LogicVariable v) { } private void bindVar() { - namespaces().setVariables(new Namespace(variables())); + namespaces().setVariables(new Namespace<>(variables())); } private Term toZNotation(String literal, Namespace functions) { @@ -764,27 +750,15 @@ private String unescapeString(String string) { for (int i = 0; i < chars.length; i++) { if (chars[i] == '\\' && i < chars.length - 1) { switch (chars[++i]) { - case 'n': - sb.append("\n"); - break; - case 'f': - sb.append("\f"); - break; - case 'r': - sb.append("\r"); - break; - case 't': - sb.append("\t"); - break; - case 'b': - sb.append("\b"); - break; - case ':': - sb.append("\\:"); - break; // this is so in KeY ... - default: - sb.append(chars[i]); - break; // this more relaxed than before, \a becomes a ... + case 'n' -> sb.append("\n"); + case 'f' -> sb.append("\f"); + case 'r' -> sb.append("\r"); + case 't' -> sb.append("\t"); + case 'b' -> sb.append("\b"); + case ':' -> sb.append("\\:"); + // this is so in KeY ... + default -> sb.append(chars[i]); + // this more relaxed than before, \a becomes a ... } } else { sb.append(chars[i]); @@ -945,7 +919,7 @@ public Object visitPrimitive_labeled_term(KeYParser.Primitive_labeled_termContex Term t = accept(ctx.primitive_term()); if (ctx.LGUILLEMETS() != null) { ImmutableArray labels = accept(ctx.label()); - if (labels.size() > 0) { + if (!labels.isEmpty()) { t = getServices().getTermBuilder().addLabel(t, labels); } } @@ -955,7 +929,7 @@ public Object visitPrimitive_labeled_term(KeYParser.Primitive_labeled_termContex @Override public ImmutableArray visitLabel(KeYParser.LabelContext ctx) { List labels = mapOf(ctx.single_label()); - return new ImmutableArray(labels); + return new ImmutableArray<>(labels); } @Override @@ -1739,11 +1713,6 @@ private boolean isImplicitHeap(Term t) { /** * Guard for {@link #replaceHeap0(Term, Term, ParserRuleContext)} to protect the double * application of {@code @heap}. - * - * @param term - * @param heap - * @param ctx - * @return */ private Term replaceHeap(Term term, Term heap, ParserRuleContext ctx) { if (explicitHeap.contains(term)) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java index 4e18e476295..dbb441e2069 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java @@ -93,11 +93,7 @@ public Object visitRulesOrAxioms(KeYParser.RulesOrAxiomsContext ctx) { axiomMode = true; } ChoiceExpr choices = accept(ctx.choices); - if (choices != null) { - this.requiredChoices = choices; - } else { - this.requiredChoices = ChoiceExpr.TRUE; - } + this.requiredChoices = Objects.requireNonNullElse(choices, ChoiceExpr.TRUE); List seq = mapOf(ctx.taclet()); topLevelTaclets.addAll(seq); disableJavaSchemaMode(); @@ -310,22 +306,14 @@ private Object evaluateVarcondArgument(ArgumentType expectedType, Object prevVal return prevValue; // previous value is of suitable type, we do not re-evaluate } - switch (expectedType) { - case TYPE_RESOLVER: - return buildTypeResolver(ctx); - case SORT: - return visitSortId(ctx.term().getText(), ctx.term()); - case JAVA_TYPE: - return getOrCreateJavaType(ctx.term().getText(), ctx); - case VARIABLE: - return varId(ctx, ctx.getText()); - case STRING: - return ctx.getText(); - case TERM: - return accept(ctx.term()); - } - assert false; - return null; + return switch (expectedType) { + case TYPE_RESOLVER -> buildTypeResolver(ctx); + case SORT -> visitSortId(ctx.term().getText(), ctx.term()); + case JAVA_TYPE -> getOrCreateJavaType(ctx.term().getText(), ctx); + case VARIABLE -> varId(ctx, ctx.getText()); + case STRING -> ctx.getText(); + case TERM -> accept(ctx.term()); + }; } private Sort visitSortId(String text, ParserRuleContext ctx) { @@ -367,7 +355,7 @@ private KeYJavaType getOrCreateJavaType(String sortId, ParserRuleContext ctx) { if (t != null) { return t; } - return new KeYJavaType((Sort) visitSortId(sortId, ctx)); + return new KeYJavaType(visitSortId(sortId, ctx)); } @@ -504,19 +492,19 @@ private TacletBuilder createTacletBuilderFor(Object find, int applicationRest if (find == null) { return new NoFindTacletBuilder(); } else if (find instanceof Term) { - return new RewriteTacletBuilder().setFind((Term) find) + return new RewriteTacletBuilder<>().setFind((Term) find) .setApplicationRestriction(applicationRestriction); } else if (find instanceof Sequent findSeq) { if (findSeq.isEmpty()) { return new NoFindTacletBuilder(); - } else if (findSeq.antecedent().size() == 1 && findSeq.succedent().size() == 0) { + } else if (findSeq.antecedent().size() == 1 && findSeq.succedent().isEmpty()) { Term findFma = findSeq.antecedent().get(0).formula(); AntecTacletBuilder b = new AntecTacletBuilder(); b.setFind(findFma); b.setIgnoreTopLevelUpdates( (applicationRestriction & RewriteTaclet.IN_SEQUENT_STATE) == 0); return b; - } else if (findSeq.antecedent().size() == 0 && findSeq.succedent().size() == 1) { + } else if (findSeq.antecedent().isEmpty() && findSeq.succedent().size() == 1) { Term findFma = findSeq.succedent().get(0).formula(); SuccTacletBuilder b = new SuccTacletBuilder(); b.setFind(findFma); @@ -663,7 +651,7 @@ public Object visitOne_schema_var_decl(KeYParser.One_schema_var_declContext ctx) s = accept(ctx.sortId()); } - for (String id : ids) { + for (String id : Objects.requireNonNull(ids)) { declareSchemaVariable(ctx, id, s, makeVariableSV, makeSkolemTermSV, makeTermLabelSV, mods); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java index 770e765f810..bb55bca0593 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java @@ -1801,50 +1801,21 @@ public static String escapeHTML(String text, boolean escapeWhitespace) { for (int i = 0, sz = text.length(); i < sz; i++) { char c = text.charAt(i); switch (c) { - case '<': - sb.append("<"); - break; - case '>': - sb.append(">"); - break; - case '&': - sb.append("&"); - break; - case '\"': - sb.append("""); - break; - case '\'': - sb.append("'"); - break; - case '(': - sb.append("("); - break; - case ')': - sb.append(")"); - break; - case '#': - sb.append("#"); - break; - case '+': - sb.append("+"); - break; - case '-': - sb.append("-"); - break; - case '%': - sb.append("%"); - break; - case ';': - sb.append(";"); - break; - case '\n': - sb.append(escapeWhitespace ? "
    " : c); - break; - case ' ': - sb.append(escapeWhitespace ? " " : c); - break; - default: - sb.append(c); + case '<' -> sb.append("<"); + case '>' -> sb.append(">"); + case '&' -> sb.append("&"); + case '\"' -> sb.append("""); + case '\'' -> sb.append("'"); + case '(' -> sb.append("("); + case ')' -> sb.append(")"); + case '#' -> sb.append("#"); + case '+' -> sb.append("+"); + case '-' -> sb.append("-"); + case '%' -> sb.append("%"); + case ';' -> sb.append(";"); + case '\n' -> sb.append(escapeWhitespace ? "
    " : c); + case ' ' -> sb.append(escapeWhitespace ? " " : c); + default -> sb.append(c); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/PosTableLayouter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/PosTableLayouter.java index 8fe89ed03cb..63e268c1108 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/PosTableLayouter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/PosTableLayouter.java @@ -259,37 +259,19 @@ public enum MarkType { MARK_END_JAVA_BLOCK, } - public static final class Mark { - public final MarkType type; - public final int parameter; - - public Mark(MarkType type, int parameter) { - this.type = type; - this.parameter = parameter; - } + public record Mark(MarkType type, int parameter) { } /** - * Utility class for stack entries containing the position table and the position of the start - * of the subterm in the result. - */ - private static class StackEntry { - final PositionTable posTbl; - final int p; - - StackEntry(PositionTable posTbl, int p) { - this.posTbl = posTbl; - this.p = p; - } - - PositionTable posTbl() { - return posTbl; - } + * Utility class for stack entries containing the position table and the position of the start + * of the subterm in the result. + */ + private record StackEntry(PositionTable posTbl, int p) { int pos() { - return p; + return p; + } } - } /** * A {@link de.uka.ilkd.key.util.pp.Backend} which puts its result in a StringBuffer and builds @@ -381,7 +363,7 @@ public void mark(Mark pair) { // MU refactored this using enums which makes it a little less ugly // and more flexible. switch (markType) { - case MARK_START_SUB: + case MARK_START_SUB -> { if (parameter == -1) { // no parameter means subterms in normal order posTbl.setStart(count() - pos); @@ -391,21 +373,16 @@ public void mark(Mark pair) { } stack.push(new StackEntry(posTbl, pos)); pos = count(); - break; - - case MARK_END_SUB: + } + case MARK_END_SUB -> { StackEntry se = stack.peek(); stack.pop(); pos = se.pos(); se.posTbl().setEnd(count() - pos, posTbl); posTbl = se.posTbl(); - break; - - case MARK_MOD_POS_TBL: - need_modPosTable = true; - break; - - case MARK_START_TERM: + } + case MARK_MOD_POS_TBL -> need_modPosTable = true; + case MARK_START_TERM -> { // This is sent by startTerm if (need_modPosTable) { posTbl = new ModalityPositionTable(parameter); @@ -413,42 +390,26 @@ public void mark(Mark pair) { posTbl = new PositionTable(parameter); } need_modPosTable = false; - break; - - case MARK_START_FIRST_STMT: - firstStmtStart = count() - pos; - break; - - case MARK_END_FIRST_STMT: + } + case MARK_START_FIRST_STMT -> firstStmtStart = count() - pos; + case MARK_END_FIRST_STMT -> { if (posTbl instanceof ModalityPositionTable) { Range firstStmtRange = new Range(firstStmtStart, count() - pos); ((ModalityPositionTable) posTbl).setFirstStatementRange(firstStmtRange); } - break; - - case MARK_START_UPDATE: - updateStarts.push(count()); - break; - - case MARK_END_UPDATE: + } + case MARK_START_UPDATE -> updateStarts.push(count()); + case MARK_END_UPDATE -> { int updateStart = updateStarts.pop(); initPosTbl.addUpdateRange(new Range(updateStart, count())); - break; - case MARK_START_KEYWORD: - keywordStarts.push(count()); - break; - case MARK_END_KEYWORD: - initPosTbl.addKeywordRange(new Range(keywordStarts.pop(), count())); - break; - case MARK_START_JAVA_BLOCK: - javaBlockStarts.push(count()); - break; - case MARK_END_JAVA_BLOCK: - initPosTbl.addJavaBlockRange(new Range(javaBlockStarts.pop(), count())); - break; - - default: - LOGGER.error("Unexpected mark: {}", markType); + } + case MARK_START_KEYWORD -> keywordStarts.push(count()); + case MARK_END_KEYWORD -> initPosTbl + .addKeywordRange(new Range(keywordStarts.pop(), count())); + case MARK_START_JAVA_BLOCK -> javaBlockStarts.push(count()); + case MARK_END_JAVA_BLOCK -> initPosTbl + .addJavaBlockRange(new Range(javaBlockStarts.pop(), count())); + default -> LOGGER.error("Unexpected mark: {}", markType); } } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java index b5ed1c6fc32..bcf1e0932ea 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java @@ -185,27 +185,28 @@ protected void printOperator(Operator x, String symbol) { if (children != null) { l.beginC(); switch (x.getArity()) { - case 2: + case 2 -> { children.get(0).visit(this); l.print(" "); l.print(symbol); l.brk(); children.get(1).visit(this); - break; - case 1: + } + case 1 -> { switch (x.getNotation()) { - case Operator.PREFIX: + case Operator.PREFIX -> { l.print(symbol); children.get(0).visit(this); - break; - case Operator.POSTFIX: + } + case Operator.POSTFIX -> { children.get(0).visit(this); l.print(symbol); - break; - default: - break; + } + default -> { + } } } + } l.end(); } } @@ -654,7 +655,7 @@ public void performActionOnCompilationUnit(CompilationUnit x) { if (hasPackageSpec) { performActionOnPackageSpecification(x.getPackageSpecification()); } - boolean hasImports = (x.getImports() != null) && (x.getImports().size() > 0); + boolean hasImports = (x.getImports() != null) && (!x.getImports().isEmpty()); if (hasImports) { if (hasPackageSpec) { l.nl(); @@ -1010,10 +1011,6 @@ public void performActionOnFor(For x, boolean includeBody) { IForUpdates upd = x.getIForUpdates(); if (upd != null) { upd.visit(this); - if (upd instanceof ProgramSV) { - - } else { - } } endMultilineBracket(); @@ -1691,7 +1688,7 @@ public void performActionOnElse(Else x) { } private void printCaseBody(ImmutableArray body) { - if (body != null && body.size() > 0) { + if (body != null && !body.isEmpty()) { for (int i = 0; i < body.size(); i++) { Statement statement = body.get(i); if (statement instanceof StatementBlock) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java index 79d75ee0677..1f6c342dedc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java @@ -747,8 +747,8 @@ private ReplayResult replayProof(Proof proof) { : proof.root(); } catch (Exception e) { - if (parserResult == null || parserResult.getErrors() == null - || parserResult.getErrors().isEmpty() || replayer == null + if (parserResult == null || parserResult.errors() == null + || parserResult.errors().isEmpty() || replayer == null || replayResult == null || replayResult.getErrors() == null || replayResult.getErrors().isEmpty()) { // this exception was something unexpected @@ -756,8 +756,8 @@ private ReplayResult replayProof(Proof proof) { } } finally { if (parserResult != null) { - status = parserResult.getStatus(); - errors.addAll(parserResult.getErrors()); + status = parserResult.status(); + errors.addAll(parserResult.errors()); } status += (status.isEmpty() ? "Proof replayed successfully." : "\n\n") + (replayResult != null ? replayResult.getStatus() diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java index 0f1f4b1d260..9e9645a271d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java @@ -24,13 +24,13 @@ * be processed by {@link IntermediateProofReplayer}. This approach is more flexible than direct * parsing; for instance, it is capable of dealing with merge rule applications. *

    - * + *

    * The returned intermediate proof closely resembles the structure of the parsed proof file. * Specifically, branch nodes are explicitly stored and, as in the proof file, have exactly one * child (or zero in the case of an empty proof). The first node, that is also the main returned * result, is a branch node with the identifier "dummy ID" that is present in every proof. *

    - * + *

    * Example for parsed intermediate proof: *

    * @@ -48,11 +48,11 @@ * > ... * *

    - * + *

    * Note that the last open goal in an unfinished proof is not represented by a node in the * intermediate representation (since no rule has been applied on the goal yet). *

    - * + *

    * The results of the parser may be obtained by calling {@link #getResult()}. * * @author Dominic Scheurer @@ -60,7 +60,7 @@ public class IntermediatePresentationProofFileParser implements IProofFileParser { /* + The proof object for storing meta information */ - private Proof proof = null; + private final Proof proof; /* + Open Branches */ private final ArrayDeque stack = new ArrayDeque<>(); @@ -70,7 +70,7 @@ public class IntermediatePresentationProofFileParser implements IProofFileParser /* + State information that is returned after parsing */ private BranchNodeIntermediate root = null; // the "dummy ID" branch - private NodeIntermediate currNode = null; + private NodeIntermediate currNode; private final LinkedList errors = new LinkedList<>(); /** @@ -78,15 +78,13 @@ public class IntermediatePresentationProofFileParser implements IProofFileParser */ public IntermediatePresentationProofFileParser(Proof proof) { this.proof = proof; - this.currNode = this.root; } @Override @SuppressWarnings("unchecked") public void beginExpr(ProofElementID eid, String str) { switch (eid) { - case BRANCH: // branch - { + case BRANCH -> { final BranchNodeIntermediate newNode = new BranchNodeIntermediate(str); if (root == null) { @@ -99,37 +97,31 @@ public void beginExpr(ProofElementID eid, String str) { currNode = newNode; } } - break; - - case RULE: // rule (taclet) - { - final AppNodeIntermediate newNode = new AppNodeIntermediate(); - currNode.addChild(newNode); - currNode = newNode; - } - + case RULE -> { // rule (taclet) + { + final AppNodeIntermediate newNode = new AppNodeIntermediate(); + currNode.addChild(newNode); + currNode = newNode; + } ruleInfo = new TacletInformation(str); - break; - - case FORMULA: // formula + } + case FORMULA -> { // formula final int formula = Integer.parseInt(str); if (insideBuiltinIfInsts()) { ((BuiltinRuleInformation) ruleInfo).currIfInstFormula = formula; } else { ruleInfo.currFormula = formula; } - break; - - case TERM: // term + } + case TERM -> { // term final PosInTerm pos = PosInTerm.parseReverseString(str); if (insideBuiltinIfInsts()) { ((BuiltinRuleInformation) ruleInfo).currIfInstPosInTerm = pos; } else { ruleInfo.currPosInTerm = pos; } - break; - - case INSTANTIATION: // inst + } + case INSTANTIATION -> // inst { TacletInformation tacletInfo = (TacletInformation) ruleInfo; if (tacletInfo.loadedInsts == null) { @@ -137,138 +129,97 @@ public void beginExpr(ProofElementID eid, String str) { } tacletInfo.loadedInsts.add(str); } - break; - - case RULESET: // heuristics - break; - - case ASSUMES_FORMULA_IN_SEQUENT: // ifseqformula + case RULESET -> { + } // heuristics + case ASSUMES_FORMULA_IN_SEQUENT -> // ifseqformula { TacletInformation tacletInfo = (TacletInformation) ruleInfo; tacletInfo.ifSeqFormulaList = tacletInfo.ifSeqFormulaList.append(str); } - break; - - case ASSUMES_FORMULA_DIRECT: // ifdirectformula + case ASSUMES_FORMULA_DIRECT -> // ifdirectformula { TacletInformation tacletInfo = (TacletInformation) ruleInfo; tacletInfo.ifDirectFormulaList = tacletInfo.ifDirectFormulaList.append(str); } - break; - - case KeY_USER: // UserLog + case KeY_USER -> { // UserLog if (proof.userLog == null) { proof.userLog = new ArrayList<>(); } proof.userLog.add(str); - break; - - case KeY_VERSION: // Version log + } + case KeY_VERSION -> { // Version log if (proof.keyVersionLog == null) { proof.keyVersionLog = new ArrayList<>(); } proof.keyVersionLog.add(str); - break; - - case KeY_SETTINGS: // ProofSettings - loadPreferences(str); - break; - - case BUILT_IN_RULE: // BuiltIn rules - { - final AppNodeIntermediate newNode = new AppNodeIntermediate(); - currNode.addChild(newNode); - currNode = newNode; } - + case KeY_SETTINGS -> // ProofSettings + loadPreferences(str); + case BUILT_IN_RULE -> { // BuiltIn rules + { + final AppNodeIntermediate newNode = new AppNodeIntermediate(); + currNode.addChild(newNode); + currNode = newNode; + } ruleInfo = new BuiltinRuleInformation(str); - break; - - case CONTRACT: // contract - ((BuiltinRuleInformation) ruleInfo).currContract = str; - break; - - case MODALITY: + } + case CONTRACT -> ((BuiltinRuleInformation) ruleInfo).currContract = str; + case MODALITY -> // (additional information which can be used in external tools such as proof management) ((BuiltinRuleInformation) ruleInfo).currContractModality = str; - break; - - case ASSUMES_INST_BUILT_IN: // ifInst (for built in rules) + case ASSUMES_INST_BUILT_IN -> { // ifInst (for built in rules) BuiltinRuleInformation builtinInfo = (BuiltinRuleInformation) ruleInfo; - if (builtinInfo.builtinIfInsts == null) { builtinInfo.builtinIfInsts = ImmutableSLList.nil(); } builtinInfo.currIfInstFormula = 0; builtinInfo.currIfInstPosInTerm = PosInTerm.getTopLevel(); - break; - - case NEW_NAMES: // newnames + } + case NEW_NAMES -> { final String[] newNames = str.split(","); ruleInfo.currNewNames = ImmutableSLList.nil(); for (String newName : newNames) { ruleInfo.currNewNames = ruleInfo.currNewNames.append(new Name(newName)); } - break; - - case AUTOMODE_TIME: // autoModeTime + } + case AUTOMODE_TIME -> { try { proof.addAutoModeTime(Long.parseLong(str)); - } catch (NumberFormatException e) { - /* ignore */ + } catch (NumberFormatException ignore) { } - break; - - case MERGE_PROCEDURE: // merge procedure + } + case MERGE_PROCEDURE -> // merge procedure ((BuiltinRuleInformation) ruleInfo).currMergeProc = str; - break; - - case NUMBER_MERGE_PARTNERS: // number of merge partners + case NUMBER_MERGE_PARTNERS -> // number of merge partners ((BuiltinRuleInformation) ruleInfo).currNrPartners = Integer.parseInt(str); - break; - - case MERGE_NODE: // corresponding merge node id + case MERGE_NODE -> // corresponding merge node id ((BuiltinRuleInformation) ruleInfo).currCorrespondingMergeNodeId = Integer.parseInt(str); - break; - - case MERGE_ID: // merge node id + case MERGE_ID -> // merge node id ((BuiltinRuleInformation) ruleInfo).currMergeNodeId = Integer.parseInt(str); - break; - - case MERGE_DIST_FORMULA: // distinguishing formula for merges + case MERGE_DIST_FORMULA -> // distinguishing formula for merges ((BuiltinRuleInformation) ruleInfo).currDistFormula = str; - break; - - case MERGE_PREDICATE_ABSTRACTION_LATTICE_TYPE: // type of predicate - // abstraction lattice + case MERGE_PREDICATE_ABSTRACTION_LATTICE_TYPE -> { // type of predicate + // abstraction lattice try { ((BuiltinRuleInformation) ruleInfo).currPredAbstraLatticeType = (Class) Class.forName(str); } catch (ClassNotFoundException e) { errors.add(e); } - break; - - case MERGE_ABSTRACTION_PREDICATES: - ((BuiltinRuleInformation) ruleInfo).currAbstractionPredicates = str; - break; - - case MERGE_USER_CHOICES: - ((BuiltinRuleInformation) ruleInfo).currUserChoices = str; - break; - - case NOTES: + } + case MERGE_ABSTRACTION_PREDICATES -> ((BuiltinRuleInformation) ruleInfo).currAbstractionPredicates = + str; + case MERGE_USER_CHOICES -> ((BuiltinRuleInformation) ruleInfo).currUserChoices = str; + case NOTES -> { ruleInfo.notes = str; if (currNode != null) { ((AppNodeIntermediate) currNode).setNotes(ruleInfo.notes); } - break; - case SOLVERTYPE: - ((BuiltinRuleInformation) ruleInfo).solver = str; - break; - default: - break; + } + case SOLVERTYPE -> ((BuiltinRuleInformation) ruleInfo).solver = str; + default -> { + } } } @@ -276,41 +227,33 @@ public void beginExpr(ProofElementID eid, String str) { @Override public void endExpr(ProofElementID eid, int lineNr) { switch (eid) { - case BRANCH: // branch - currNode = stack.pop(); - break; - - case USER_INTERACTION: // userinteraction + case BRANCH -> currNode = stack.pop(); + case USER_INTERACTION -> { if (currNode != null) { ((AppNodeIntermediate) currNode).setInteractiveRuleApplication(true); } - break; - - case PROOF_SCRIPT: // proof script node + } + case PROOF_SCRIPT -> { if (currNode != null) { ((AppNodeIntermediate) currNode).setScriptRuleApplication(true); } - break; - - case RULE: // rule (taclet) + } + case RULE -> { // rule (taclet) ((AppNodeIntermediate) currNode).setIntermediateRuleApp(constructTacletApp()); ((AppNodeIntermediate) currNode).getIntermediateRuleApp().setLineNr(lineNr); - break; - - case BUILT_IN_RULE: // BuiltIn rules + } + case BUILT_IN_RULE -> { // BuiltIn rules ((AppNodeIntermediate) currNode).setIntermediateRuleApp(constructBuiltInApp()); ((AppNodeIntermediate) currNode).getIntermediateRuleApp().setLineNr(lineNr); - break; - - case ASSUMES_INST_BUILT_IN: // ifInst (for built in rules) + } + case ASSUMES_INST_BUILT_IN -> { // ifInst (for built in rules) BuiltinRuleInformation builtinInfo = (BuiltinRuleInformation) ruleInfo; builtinInfo.builtinIfInsts = builtinInfo.builtinIfInsts.append(new Pair<>( builtinInfo.currIfInstFormula, builtinInfo.currIfInstPosInTerm)); - break; - - default: - break; + } + default -> { + } } } @@ -356,33 +299,24 @@ private TacletAppIntermediate constructTacletApp() { */ private BuiltInAppIntermediate constructBuiltInApp() { BuiltinRuleInformation builtinInfo = (BuiltinRuleInformation) ruleInfo; - BuiltInAppIntermediate result = null; - - if (builtinInfo.currRuleName.equals("MergeRule")) { - result = - new MergeAppIntermediate(builtinInfo.currRuleName, - new Pair<>(builtinInfo.currFormula, - builtinInfo.currPosInTerm), - builtinInfo.currMergeNodeId, builtinInfo.currMergeProc, - builtinInfo.currNrPartners, builtinInfo.currNewNames, - builtinInfo.currDistFormula, builtinInfo.currPredAbstraLatticeType, - builtinInfo.currAbstractionPredicates, builtinInfo.currUserChoices); - } else if (builtinInfo.currRuleName.equals("CloseAfterMerge")) { - result = new MergePartnerAppIntermediate(builtinInfo.currRuleName, - new Pair<>(builtinInfo.currFormula, builtinInfo.currPosInTerm), - builtinInfo.currCorrespondingMergeNodeId, builtinInfo.currNewNames); - } else if (builtinInfo.currRuleName.equals("SMTRule")) { - result = new SMTAppIntermediate(builtinInfo.currRuleName, - new Pair<>(builtinInfo.currFormula, builtinInfo.currPosInTerm), - builtinInfo.solver); - } else { - result = new BuiltInAppIntermediate(builtinInfo.currRuleName, - new Pair<>(builtinInfo.currFormula, builtinInfo.currPosInTerm), - builtinInfo.currContract, builtinInfo.currContractModality, - builtinInfo.builtinIfInsts, builtinInfo.currNewNames); - } - - return result; + return switch (builtinInfo.currRuleName) { + case "MergeRule" -> new MergeAppIntermediate(builtinInfo.currRuleName, + new Pair<>(builtinInfo.currFormula, builtinInfo.currPosInTerm), + builtinInfo.currMergeNodeId, builtinInfo.currMergeProc, + builtinInfo.currNrPartners, builtinInfo.currNewNames, + builtinInfo.currDistFormula, builtinInfo.currPredAbstraLatticeType, + builtinInfo.currAbstractionPredicates, builtinInfo.currUserChoices); + case "CloseAfterMerge" -> new MergePartnerAppIntermediate(builtinInfo.currRuleName, + new Pair<>(builtinInfo.currFormula, builtinInfo.currPosInTerm), + builtinInfo.currCorrespondingMergeNodeId, builtinInfo.currNewNames); + case "SMTRule" -> new SMTAppIntermediate(builtinInfo.currRuleName, + new Pair<>(builtinInfo.currFormula, builtinInfo.currPosInTerm), + builtinInfo.solver); + default -> new BuiltInAppIntermediate(builtinInfo.currRuleName, + new Pair<>(builtinInfo.currFormula, builtinInfo.currPosInTerm), + builtinInfo.currContract, builtinInfo.currContractModality, + builtinInfo.builtinIfInsts, builtinInfo.currNewNames); + }; } /** @@ -411,7 +345,7 @@ private boolean insideBuiltinIfInsts() { */ private static abstract class RuleInformation { /* + General Information */ - protected String currRuleName = null; + protected String currRuleName; protected int currFormula = 0; protected PosInTerm currPosInTerm = PosInTerm.getTopLevel(); protected ImmutableList currNewNames = null; @@ -477,29 +411,8 @@ public BuiltinRuleInformation(String ruleName) { * * @author Dominic Scheurer */ - public static class Result { - private final List errors; - private final String status; - private BranchNodeIntermediate parsedResult = null; - - public Result(List errors, String status, BranchNodeIntermediate parsedResult) { - this.errors = errors; - this.status = status; - this.parsedResult = parsedResult; - } - - public List getErrors() { - return errors; - } - - public String getStatus() { - return status; - } - - public BranchNodeIntermediate getParsedResult() { - return parsedResult; - } - + public record Result(List errors, String status, + BranchNodeIntermediate parsedResult) { } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java index b6a1c17b6a5..e0f791f1f3a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java @@ -130,7 +130,7 @@ public IntermediateProofReplayer(AbstractProblemLoader loader, Proof proof, this.loader = loader; queue.addFirst( - new Pair<>(proof.root(), parserResult.getParsedResult())); + new Pair<>(proof.root(), parserResult.parsedResult())); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java index 9e795b0fff1..12b9d7030d1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java @@ -229,10 +229,9 @@ public Instantiator(final Term formula, final Goal goal, final Services services public Instantiation instantiate() { final Term update = extractUpdate(); final Term target = extractUpdateTarget(); - if (!(target.op() instanceof Modality)) { + if (!(target.op() instanceof Modality modality)) { return null; } - final Modality modality = (Modality) target.op(); final JavaStatement statement = getFirstStatementInPrefixWithAtLeastOneApplicableContract(modality, target.javaBlock(), goal); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeComparisonCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeComparisonCondition.java index da69483d8c2..c48cb977213 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeComparisonCondition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeComparisonCondition.java @@ -93,25 +93,20 @@ private boolean checkSorts(final Sort fstSort, final Sort sndSort, final Service if (!proxy1 && !proxy2) { // This is the standard case where no proxy sorts are involved - switch (mode) { - case SAME: - return fstSort == sndSort; - case NOT_SAME: - return fstSort != sndSort; - case IS_SUBTYPE: - return fstSort.extendsTrans(sndSort); - case STRICT_SUBTYPE: - return fstSort != sndSort && fstSort.extendsTrans(sndSort); - case NOT_IS_SUBTYPE: - return !fstSort.extendsTrans(sndSort); - case DISJOINTMODULONULL: - return checkDisjointness(fstSort, sndSort, services); - } + return switch (mode) { + case SAME -> fstSort == sndSort; + case NOT_SAME -> fstSort != sndSort; + case IS_SUBTYPE -> fstSort.extendsTrans(sndSort); + case STRICT_SUBTYPE -> fstSort != sndSort && fstSort.extendsTrans(sndSort); + case NOT_IS_SUBTYPE -> !fstSort.extendsTrans(sndSort); + case DISJOINTMODULONULL -> checkDisjointness(fstSort, sndSort, services); + }; } else { switch (mode) { - case SAME: + case SAME -> { return fstSort == sndSort; - case IS_SUBTYPE: + } + case IS_SUBTYPE -> { if (proxy2) { return false; } @@ -124,7 +119,8 @@ private boolean checkSorts(final Sort fstSort, final Sort sndSort, final Service } } return false; - case STRICT_SUBTYPE: + } + case STRICT_SUBTYPE -> { if (proxy2) { return false; } @@ -137,14 +133,13 @@ private boolean checkSorts(final Sort fstSort, final Sort sndSort, final Service } } return false; - - case NOT_SAME: - case DISJOINTMODULONULL: - case NOT_IS_SUBTYPE: + } + case NOT_SAME, DISJOINTMODULONULL, NOT_IS_SUBTYPE -> { // There are cases where - based on the bounds - true could be returned. // Implement them if needed. There is the Null type to consider as subtype. return false; } + } } assert false : "All cases should have been covered"; @@ -266,21 +261,14 @@ private boolean checkDisjointness(Sort fstSort, Sort sndSort, Services services) @Override public String toString() { - switch (mode) { - case SAME: - return "\\same(" + fst + ", " + snd + ")"; - case NOT_SAME: - return "\\not\\same(" + fst + ", " + snd + ")"; - case IS_SUBTYPE: - return "\\sub(" + fst + ", " + snd + ")"; - case STRICT_SUBTYPE: - return "\\strict\\sub(" + fst + ", " + snd + ")"; - case NOT_IS_SUBTYPE: - return "\\not\\sub(" + fst + ", " + snd + ")"; - case DISJOINTMODULONULL: - return "\\disjointModuloNull(" + fst + ", " + snd + ")"; - default: - return "invalid type comparison mode"; - } + return switch (mode) { + case SAME -> "\\same(" + fst + ", " + snd + ")"; + case NOT_SAME -> "\\not\\same(" + fst + ", " + snd + ")"; + case IS_SUBTYPE -> "\\sub(" + fst + ", " + snd + ")"; + case STRICT_SUBTYPE -> "\\strict\\sub(" + fst + ", " + snd + ")"; + case NOT_IS_SUBTYPE -> "\\not\\sub(" + fst + ", " + snd + ")"; + case DISJOINTMODULONULL -> "\\disjointModuloNull(" + fst + ", " + snd + ")"; + default -> "invalid type comparison mode"; + }; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ReplaceWhileLoop.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ReplaceWhileLoop.java index 3b5e9535ba9..20eaae2941d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ReplaceWhileLoop.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ReplaceWhileLoop.java @@ -114,10 +114,6 @@ public Statement getTheLoop() { return theLoop; } - public String toString() { - return stack.peek().toString(); - } - public void performActionOnMethodFrame(MethodFrame x) { if (lastMethodFrameBeforeLoop == depth()) { IProgramVariable res = x.getProgramVariable(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/ModelExtractor.java b/key.core/src/main/java/de/uka/ilkd/key/smt/ModelExtractor.java index 165f846a38e..ac2ced2ca92 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/ModelExtractor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/ModelExtractor.java @@ -23,22 +23,16 @@ interface Query { /** * Stores the result from the z3 solver. - * - * @param s */ void setResult(String s); /** * Returns the command that is to be handed over to the z3 solver. - * - * @return */ String getQuery(); /** * Returns the stored result. - * - * @return */ String getResult(); } @@ -671,29 +665,15 @@ public class ModelExtractor { public void addFunction(SMTFunction f) { - if (f.getDomainSorts().size() == 0) { + if (f.getDomainSorts().isEmpty()) { switch (f.getImageSort().getId()) { - case SMTObjTranslator.HEAP_SORT: - heaps.add(f); - break; - case SMTObjTranslator.FIELD_SORT: - fields.add(f); - break; - case SMTObjTranslator.LOCSET_SORT: - locsets.add(f); - break; - case SMTObjTranslator.OBJECT_SORT: - objects.add(f); - break; - case SMTObjTranslator.BINT_SORT: - ints.add(f); - break; - case SMTObjTranslator.SEQ_SORT: - seqs.add(f); - break; - default: - bools.add(f); - break; + case SMTObjTranslator.HEAP_SORT -> heaps.add(f); + case SMTObjTranslator.FIELD_SORT -> fields.add(f); + case SMTObjTranslator.LOCSET_SORT -> locsets.add(f); + case SMTObjTranslator.OBJECT_SORT -> objects.add(f); + case SMTObjTranslator.BINT_SORT -> ints.add(f); + case SMTObjTranslator.SEQ_SORT -> seqs.add(f); + default -> bools.add(f); } } else if (f.getDomainSorts().size() == 2) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTObjTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTObjTranslator.java index fa2cb4ba435..230b578750a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTObjTranslator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTObjTranslator.java @@ -670,25 +670,19 @@ private void generateWellFormedAssertions() throws IllegalFormulaException { SMTTerm selectArr = SMTTerm.call(selectFunction, h, o, arr); SMTTerm typeReq; switch (single) { - case "int": - case "char": - case "byte": - typeReq = SMTTerm.call(getIsFunction(sorts.get(BINT_SORT)), selectArr); - break; - case "java.lang.Object": - typeReq = SMTTerm.call(getIsFunction(sorts.get(OBJECT_SORT)), selectArr); - break; - case "boolean": - typeReq = SMTTerm.call(getIsFunction(SMTSort.BOOL), selectArr); - break; - default: + case "int", "char", "byte" -> typeReq = + SMTTerm.call(getIsFunction(sorts.get(BINT_SORT)), selectArr); + case "java.lang.Object" -> typeReq = + SMTTerm.call(getIsFunction(sorts.get(OBJECT_SORT)), selectArr); + case "boolean" -> typeReq = SMTTerm.call(getIsFunction(SMTSort.BOOL), selectArr); + default -> { typeReq = SMTTerm.call(getIsFunction(sorts.get(OBJECT_SORT)), selectArr); Sort singleSort = services.getJavaInfo().getKeYJavaType(single).getSort(); addTypePredicate(singleSort); SMTFunction tps = getTypePredicate(singleSort.name().toString()); SMTTerm selectObjArr = castTermIfNecessary(selectArr, sorts.get(OBJECT_SORT)); typeReq = typeReq.and(SMTTerm.call(tps, selectObjArr)); - break; + } } assertion4 = assertion4.and(premise.implies(typeReq)); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java index fb52a52373b..5754a602046 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java @@ -48,11 +48,6 @@ public SMTRuleApp replacePos(PosInOccurrence newPos) { return new SMTRuleApp(RULE, newPos, ifInsts, successfulSolverName); } - @Override - public boolean complete() { - return true; - } - public String getTitle() { return title; } @@ -61,11 +56,6 @@ public String getSuccessfulSolverName() { return successfulSolverName; } - @Override - public PosInOccurrence posInOccurrence() { - return pio; - } - @Override public BuiltInRule rule() { return RULE; diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java index 044152bb3a1..0201e0772eb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java @@ -290,17 +290,12 @@ private void interruptionOccurred(Throwable e) { ReasonOfInterruption reason = getReasonOfInterruption(); setReasonOfInterruption(ReasonOfInterruption.Exception, e); switch (reason) { - case Exception: - case NoInterruption: + case Exception, NoInterruption -> { setReasonOfInterruption(ReasonOfInterruption.Exception, e); listener.processInterrupted(this, problem, e); - break; - case Timeout: - listener.processTimeout(this, problem); - break; - case User: - listener.processUser(this, problem); - break; + } + case Timeout -> listener.processTimeout(this, problem); + case User -> listener.processUser(this, problem); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3CESocket.java b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3CESocket.java index 49d56f94742..ffc1b7c272c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3CESocket.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3CESocket.java @@ -33,7 +33,7 @@ public void messageIncoming(@Nonnull Pipe pipe, @Nonnull String msg) throws IOEx } switch (sc.getState()) { - case WAIT_FOR_RESULT: + case WAIT_FOR_RESULT -> { if (msg.equals("unsat")) { sc.setFinalResult(SMTSolverResult.createValidResult(getName())); pipe.sendMessage("(exit)"); @@ -50,21 +50,17 @@ public void messageIncoming(@Nonnull Pipe pipe, @Nonnull String msg) throws IOEx sc.setState(WAIT_FOR_DETAILS); pipe.sendMessage("(exit)"); } - - break; - - case WAIT_FOR_DETAILS: - // Currently we rely on the solver to terminate after receiving "(exit)". If this does - // not work in future, it may be that we have to forcibly close the pipe. - break; - - case WAIT_FOR_QUERY: + } + case WAIT_FOR_DETAILS -> { + } + // Currently we rely on the solver to terminate after receiving "(exit)". If this does + // not work in future, it may be that we have to forcibly close the pipe. + case WAIT_FOR_QUERY -> { if (!msg.equals("success")) { getQuery().messageIncoming(pipe, msg); } - break; - - case WAIT_FOR_MODEL: + } + case WAIT_FOR_MODEL -> { if (msg.equals("endmodel")) { if (getQuery() != null && getQuery().getState() == ModelExtractor.DEFAULT) { getQuery().getModel().setEmpty(false); @@ -75,9 +71,8 @@ public void messageIncoming(@Nonnull Pipe pipe, @Nonnull String msg) throws IOEx sc.setState(WAIT_FOR_DETAILS); } } - break; - default: - throw new IllegalStateException("Unexpected value: " + sc.getState()); + } + default -> throw new IllegalStateException("Unexpected value: " + sc.getState()); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3Socket.java b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3Socket.java index f03a9624079..0a8b9a8c1f0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3Socket.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3Socket.java @@ -32,7 +32,7 @@ public void messageIncoming(@Nonnull Pipe pipe, @Nonnull String msg) throws IOEx } switch (sc.getState()) { - case WAIT_FOR_RESULT: + case WAIT_FOR_RESULT -> { if (msg.equals("unsat")) { sc.setFinalResult(SMTSolverResult.createValidResult(getName())); // TODO: proof production is currently completely disabled, since it does not work @@ -55,16 +55,15 @@ public void messageIncoming(@Nonnull Pipe pipe, @Nonnull String msg) throws IOEx pipe.sendMessage("(exit)\n"); sc.setState(WAIT_FOR_DETAILS); } - break; - - case WAIT_FOR_DETAILS: - // Currently we rely on the solver to terminate after receiving "(exit)". If this does - // not work in future, it may be that we have to forcibly close the pipe. - // if (msg.equals("success")) { - // pipe.sendMessage("(exit)"); - // pipe.close(); - // } - break; + } + case WAIT_FOR_DETAILS -> { + } + // Currently we rely on the solver to terminate after receiving "(exit)". If this does + // not work in future, it may be that we have to forcibly close the pipe. + // if (msg.equals("success")) { + // pipe.sendMessage("(exit)"); + // pipe.close(); + // } } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTerm.java b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTerm.java index 6b28cb74ff3..d3e8cabd6aa 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTerm.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTerm.java @@ -291,12 +291,10 @@ public static SMTTerms terms(List terms) { */ public SMTTerm unaryOp(SMTTermUnaryOp.Op op) { - switch (op) { - case NOT: - return this.not(); - default: - return new SMTTermUnaryOp(op, this); - } + return switch (op) { + case NOT -> this.not(); + default -> new SMTTermUnaryOp(op, this); + }; } public SMTTerm sign(boolean pol) { @@ -326,51 +324,29 @@ public SMTTerm not() { } public SMTTerm multOp(SMTTermMultOp.Op op, SMTTerm t) { - - switch (op) { - case AND: - return this.and(t); - case OR: - return this.or(t); - case IMPLIES: - return this.implies(t); - case IFF: - return this.iff(t); - case EQUALS: - return this.equal(t); - case LT: - return this.lt(t); - case LTE: - return this.lte(t); - case DIV: - return this.div(t); - case GT: - return this.gt(t); - case GTE: - return this.gte(t); - case MINUS: - return this.minus(t); - case MUL: - return this.mul(t); - case PLUS: - return this.plus(t); - case REM: - return this.rem(t); - - default: - return defaultMultOp(op, t); + return switch (op) { + case AND -> this.and(t); + case OR -> this.or(t); + case IMPLIES -> this.implies(t); + case IFF -> this.iff(t); + case EQUALS -> this.equal(t); + case LT -> this.lt(t); + case LTE -> this.lte(t); + case DIV -> this.div(t); + case GT -> this.gt(t); + case GTE -> this.gte(t); + case MINUS -> this.minus(t); + case MUL -> this.mul(t); + case PLUS -> this.plus(t); + case REM -> this.rem(t); + default -> defaultMultOp(op, t); // TODO implement bitvec cases if necessary // throw new // RuntimeException("Unexpected: binOp as arg for the method binOp(): "+op); - } + }; } - /** - * @param op - * @param f - * @return - */ private SMTTerm defaultMultOp(SMTTermMultOp.Op op, SMTTerm f) { List args = this.toList(); args.add(f); @@ -721,26 +697,18 @@ public SMTTerm minus(SMTTerm right) { } public SMTTerm quant(SMTTermQuant.Quant quant, List bindVars) { - switch (quant) { - case FORALL: - return this.forall(bindVars); - case EXISTS: - return this.exists(bindVars); - default: - return this; - } + return switch (quant) { + case FORALL -> this.forall(bindVars); + case EXISTS -> this.exists(bindVars); + }; } public SMTTerm quant(SMTTermQuant.Quant quant, List bindVars, List> pats) { - switch (quant) { - case FORALL: - return this.forall(bindVars, pats); - case EXISTS: - return this.exists(bindVars, pats); - default: - return this; - } + return switch (quant) { + case FORALL -> this.forall(bindVars, pats); + case EXISTS -> this.exists(bindVars, pats); + }; } public SMTTerm forall(List bindVars) { @@ -941,12 +909,7 @@ public String toString() { @Override public String toString(int nestPos) { - StringBuffer tab = new StringBuffer(); - for (int i = 0; i < nestPos; i++) { - tab = tab.append(" "); - } - - return tab + "true"; + return " ".repeat(Math.max(0, nestPos)) + "true"; } @Override @@ -1041,12 +1004,7 @@ public String toString() { @Override public String toString(int nestPos) { - StringBuffer tab = new StringBuffer(); - for (int i = 0; i < nestPos; i++) { - tab = tab.append(" "); - } - - return tab + "false"; + return " ".repeat(Math.max(0, nestPos)) + "false"; } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermBinOp.java b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermBinOp.java index 698991eb9ad..90000511b0a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermBinOp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermBinOp.java @@ -6,6 +6,7 @@ import java.util.HashMap; import java.util.LinkedList; import java.util.List; +import java.util.Map; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -19,8 +20,8 @@ public class SMTTermBinOp extends SMTTerm { private static final Logger LOGGER = LoggerFactory.getLogger(SMTTermBinOp.class); - private static HashMap bvSymbols; - private static HashMap intSymbols; + private static Map bvSymbols; + private static Map intSymbols; public enum OpProperty { NONE, LEFTASSOC, RIGHTASSOC, FULLASSOC, CHAINABLE, PAIRWISE @@ -52,28 +53,15 @@ public SMTTermBinOp(Op operator, SMTTerm left, SMTTerm right) { } public static OpProperty getProperty(SMTTermBinOp.Op op) { - - - switch (op) { - case AND: - case OR: - case PLUS: - case MUL: - return OpProperty.FULLASSOC; - case MINUS: - case XOR: - case DIV: - return OpProperty.LEFTASSOC; - case IMPLIES: - return OpProperty.RIGHTASSOC; - case EQUALS: - /* case LT: case LTE: case GT: case GTE: */ return OpProperty.CHAINABLE; - case DISTINCT: - return OpProperty.PAIRWISE; - default: - return OpProperty.NONE; - } - + return switch (op) { + case AND, OR, PLUS, MUL -> OpProperty.FULLASSOC; + case MINUS, XOR, DIV -> OpProperty.LEFTASSOC; + case IMPLIES -> OpProperty.RIGHTASSOC; + case EQUALS -> + /* case LT: case LTE: case GT: case GTE: */ OpProperty.CHAINABLE; + case DISTINCT -> OpProperty.PAIRWISE; + default -> OpProperty.NONE; + }; } private static void initMaps() { @@ -169,33 +157,22 @@ public List getVars() { /** {@inheritDoc} */ @Override public SMTSort sort() { + return switch (operator) { + case PLUS, MINUS, MUL, DIV, REM, BVASHR, BVSHL, BVSMOD, BVSREM -> { + if (!left.sort().equals(right.sort())) { - switch (operator) { - case PLUS: - case MINUS: - case MUL: - case DIV: - case REM: - case BVASHR: - case BVSHL: - case BVSMOD: - case BVSREM: - if (!left.sort().equals(right.sort())) { - - String error = "Unexpected: binary operation with two diff. arg sorts"; - error += "\n"; - error += this.toSting() + "\n"; - error += "Left sort: " + left.sort() + "\n"; - error += "Right sort: " + right.sort() + "\n"; - throw new RuntimeException(error); + String error = "Unexpected: binary operation with two diff. arg sorts"; + error += "\n"; + error += this.toSting() + "\n"; + error += "Left sort: " + left.sort() + "\n"; + error += "Right sort: " + right.sort() + "\n"; + throw new RuntimeException(error); + } + yield left.sort(); } - - - return left.sort(); - default: - return SMTSort.BOOL; - } + default -> SMTSort.BOOL; + }; } /** {@inheritDoc} */ @@ -241,8 +218,6 @@ public SMTTerm replace(SMTTermCall a, SMTTerm b) { /** {@inheritDoc} */ @Override public SMTTerm instantiate(SMTTermVariable a, SMTTerm b) { - // return new TermBinOp(operator, (Term) left.instantiate(a, b), (Term) right.instantiate(a, - // b)); //TODO return left.instantiate(a, b).binOp(operator, right.instantiate(a, b)); } @@ -358,10 +333,8 @@ public boolean isChainableBinOp(SMTTerm t) { public String toString(int nestPos) { LOGGER.warn("Warning: somehow a binop was created. {}", this.getOperator()); - StringBuffer tab = new StringBuffer(); - for (int i = 0; i < nestPos; i++) { - tab = tab.append(" "); - } + StringBuilder tab = new StringBuilder(); + tab.append(" ".repeat(Math.max(0, nestPos))); String symbol = getSymbol(operator, left); @@ -405,7 +378,7 @@ public String toString(int nestPos) { if (this.operator.equals(Op.AND)) { List chainStrings = checkChainable(nestPos, args); - if (chainStrings.size() == 1 && args.size() == 0) { + if (chainStrings.size() == 1 && args.isEmpty()) { return tab + chainStrings.get(0); } for (String s : chainStrings) { @@ -470,11 +443,6 @@ private List extractChain(int start, List args, List ops, return chain; } - /** - * @param nestPos - * @param args - * @return - */ private List checkChainable(int nestPos, List args) { List ops = new LinkedList<>(); List> chains = searchChains(args, ops); @@ -492,12 +460,9 @@ private List checkChainable(int nestPos, List args) { return chainStrings; } - /** - * @return - */ private String getSymbol(Op operator, SMTTerm first) { boolean isInt = first.sort().equals(SMTSort.INT) && first.sort().getBitSize() == -1; - String symbol = null; + String symbol; if (isInt) { symbol = intSymbols.get(operator); } else { diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermMultOp.java b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermMultOp.java index 69d7c4ed77f..8442bcf81c7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermMultOp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermMultOp.java @@ -35,58 +35,45 @@ public enum Op { BVSLE, BVSGT, BVSGE, BVSDIV; public SMTTerm getIdem() { - switch (this) { - case AND: - return SMTTerm.TRUE; - case OR: - return SMTTerm.FALSE; - default: - throw new RuntimeException( - "Unexpected: getIdem() is only app. to the Operators 'AND' and 'OR': " + this); - } + return switch (this) { + case AND -> SMTTerm.TRUE; + case OR -> SMTTerm.FALSE; + default -> throw new RuntimeException( + "Unexpected: getIdem() is only app. to the Operators 'AND' and 'OR': " + this); + }; } public Op sign(boolean pol) { - switch (this) { - case AND: - if (pol) { - return this; + return switch (this) { + case AND -> { + if (pol) { + yield this; + } + yield OR; } - return OR; - case OR: - if (pol) { - return this; + case OR -> { + if (pol) { + yield this; + } + yield AND; } - return AND; - default: - throw new RuntimeException( - "Unexpected: sign(Boolean pol) is only app. to the Operators 'AND' and 'OR': " - + this); - } + default -> throw new RuntimeException( + "Unexpected: sign(Boolean pol) is only app. to the Operators 'AND' and 'OR': " + + this); + }; } } public static OpProperty getProperty(SMTTermMultOp.Op op) { - switch (op) { - case AND: - case OR: - case PLUS: - case MUL: - return OpProperty.FULLASSOC; - case MINUS: - case XOR: - case DIV: - return OpProperty.LEFTASSOC; - case IMPLIES: - return OpProperty.RIGHTASSOC; - case IFF: - case EQUALS: - /* case LT: case LTE: case GT: case GTE: */ return OpProperty.CHAINABLE; - case DISTINCT: - return OpProperty.PAIRWISE; - default: - return OpProperty.NONE; - } + return switch (op) { + case AND, OR, PLUS, MUL -> OpProperty.FULLASSOC; + case MINUS, XOR, DIV -> OpProperty.LEFTASSOC; + case IMPLIES -> OpProperty.RIGHTASSOC; + case IFF, EQUALS -> + /* case LT: case LTE: case GT: case GTE: */ OpProperty.CHAINABLE; + case DISTINCT -> OpProperty.PAIRWISE; + default -> OpProperty.NONE; + }; } private static void initMaps() { @@ -223,32 +210,23 @@ public List getVars() { @Override public SMTSort sort() { - switch (operator) { - case PLUS: - case MINUS: - case MUL: - case DIV: - case REM: - case BVASHR: - case BVSHL: - case BVSMOD: - case BVSREM: - case BVSDIV: - // Sanity check - if (subs.size() > 1) { - if (!subs.get(0).sort().equals(subs.get(1).sort())) { - String error = "Unexpected: binary operation with two diff. arg sorts"; - error += "\n"; - error += this.toSting() + "\n"; - error += "First sort: " + subs.get(0).sort() + "\n"; - error += "Second sort: " + subs.get(1).sort() + "\n"; - throw new RuntimeException(error); + return switch (operator) { + case PLUS, MINUS, MUL, DIV, REM, BVASHR, BVSHL, BVSMOD, BVSREM, BVSDIV -> { + // Sanity check + if (subs.size() > 1) { + if (!subs.get(0).sort().equals(subs.get(1).sort())) { + String error = "Unexpected: binary operation with two diff. arg sorts"; + error += "\n"; + error += this.toSting() + "\n"; + error += "First sort: " + subs.get(0).sort() + "\n"; + error += "Second sort: " + subs.get(1).sort() + "\n"; + throw new RuntimeException(error); + } } + yield subs.get(0).sort(); } - return subs.get(0).sort(); - default: - return SMTSort.BOOL; - } + default -> SMTSort.BOOL; + }; } /** {@inheritDoc} */ @@ -494,7 +472,7 @@ public String toString(int nestPos) { StringBuilder buff = new StringBuilder(); buff.append(tab); - if (subs.size() == 0) { + if (subs.isEmpty()) { throw new RuntimeException("Unexpected: Empty args for TermLogicalOp "); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermQuant.java b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermQuant.java index 70e9f1018ec..60379932f39 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermQuant.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermQuant.java @@ -18,20 +18,21 @@ public enum Quant { FORALL, EXISTS; public Quant sign(boolean pol) { - switch (this) { - case FORALL: - if (pol) { - return this; + return switch (this) { + case FORALL -> { + if (pol) { + yield this; + } + yield EXISTS; } - return EXISTS; - case EXISTS: - if (pol) { - return this; + case EXISTS -> { + if (pol) { + yield this; + } + yield FORALL; } - return FORALL; - default: - throw new RuntimeException("Unexpected: Quant in neg() : " + this); - } + default -> throw new RuntimeException("Unexpected: Quant in neg() : " + this); + }; } } @@ -96,7 +97,7 @@ public List> getPats() { } /** - * @param pat the pat to set + * @param pats the pat to set */ public void setPats(List> pats) { this.pats = pats; @@ -231,13 +232,13 @@ public SMTTerm instantiate(SMTTermVariable a, SMTTerm b) { } if (newVars.size() < bindVars.size()) - /** + /* * 1. Some SMT solvers like Z3 requires patterns to contains all binded variables 2. * Some terms of the patterns can contains more that one variable 3. Instantiation of * quantified variables should can destroy the well-sortedness of patterns term. Because * of 1-3 and for simplicity, we just drop the entry pattern its the quantifier is * instantiated. - **/ + */ { return sub.instantiate(a, b).quant(quant, newVars); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermUnaryOp.java b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermUnaryOp.java index bd128a76fd9..e4cbc209461 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermUnaryOp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/lang/SMTTermUnaryOp.java @@ -198,17 +198,12 @@ public String toString(int nestPos) { tab = tab.append(" "); } - switch (operator) { - case NOT: - return tab + "(not" + "\n" + sub.toString(nestPos + 1) + "\n" + tab + ")"; - case BVNOT: - return tab + "(bvnot" + "\n" + sub.toString(nestPos + 1) + "\n" + tab + ")"; - case BVNEG: - return tab + "(bvneg" + "\n" + sub.toString(nestPos + 1) + "\n" + tab + ")"; - default: - throw new RuntimeException("Unexpected: supported unaryOp={NOT}"); - } - + return switch (operator) { + case NOT -> tab + "(not" + "\n" + sub.toString(nestPos + 1) + "\n" + tab + ")"; + case BVNOT -> tab + "(bvnot" + "\n" + sub.toString(nestPos + 1) + "\n" + tab + ")"; + case BVNEG -> tab + "(bvneg" + "\n" + sub.toString(nestPos + 1) + "\n" + tab + ")"; + default -> throw new RuntimeException("Unexpected: supported unaryOp={NOT}"); + }; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/MasterHandler.java b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/MasterHandler.java index 0453702a493..cbc58e552f6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/MasterHandler.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/MasterHandler.java @@ -27,10 +27,10 @@ /** * Instances of this class are the controlling units of the translation. They control how the * translation is delegated to different {@link SMTHandler}s and collects the translations. - * + *

    * It keeps track of the actual translation of an expression but collects also the declarations and * axioms that occur during the translation. - * + *

    * It has measures to ensure that symbols are defined and axiomatized at most once. This allows us * to add these entries on the fly and on demand. * @@ -116,7 +116,7 @@ public void addDeclarationsAndAxioms(Properties snippets) { /** * This interface is used for routines that can be used to flexibly introduce function symbols. - * + *

    * An instance can be stored in the {@link #translationState} with a key suffixed with ".intro". * It is then invoked when a symbol is to be introduced. */ @@ -127,11 +127,11 @@ public interface SymbolIntroducer { /** * Translate a single term to an SMTLib S-Expression. - * + *

    * This method may modify the state of the handler (by adding symbols e.g.). - * + *

    * It tries to find a {@link SMTHandler} that can deal with the argument and delegates to that. - * + *

    * A default translation is triggered if no handler can be found. * * @param problem the non-null term to translate @@ -149,14 +149,16 @@ public SExpr translate(Term problem) { for (SMTHandler smtHandler : handlers) { Capability response = smtHandler.canHandle(problem); switch (response) { - case YES_THIS_INSTANCE: + case YES_THIS_INSTANCE -> { // handle this but do not cache. return smtHandler.handle(this, problem); - case YES_THIS_OPERATOR: + } + case YES_THIS_OPERATOR -> { // handle it and cache it for future instances of the op. handlerMap.put(problem.op(), smtHandler); return smtHandler.handle(this, problem); } + } } return handleAsUnknownValue(problem); @@ -168,14 +170,14 @@ public SExpr translate(Term problem) { /** * Translate a single term to an SMTLib S-Expression. - * + *

    * The result is ensured to have the SExpr-Type given as argument. If the type coercion fails, * then the translation falls back to translating the argument as an unknown function. - * + *

    * This method may modify the state of the handler (by adding symbols e.g.). - * + *

    * It tries to find a {@link SMTHandler} that can deal with the argument and delegates to that. - * + *

    * A default translation is triggered if no handler can be found. * * @param problem the non-null term to translate @@ -218,7 +220,7 @@ private SExpr handleAsUnknownValue(Term problem) { /** * Treats the given term as a function call. - * + *

    * This means that an expression of the form * * 

    @@ -237,7 +239,7 @@ SExpr handleAsFunctionCall(String functionName, Term term) {
 
     /**
      * Treats the given term as a function call.
-     *
+     * 
    
      * This means that an expression of the form
      *
      * 
    diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SExprs.java b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SExprs.java
index 636e081efff..dbbf995a716 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SExprs.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SExprs.java
@@ -54,14 +54,11 @@ private SExprs() {
      * @return an SExpr equivalent to the conjunction of the clauses.
      */
     public static SExpr and(List clauses) {
-        switch (clauses.size()) {
-        case 0:
-            return TRUE;
-        case 1:
-            return clauses.get(0);
-        default:
-            return new SExpr("and", Type.BOOL, clauses);
-        }
+        return switch (clauses.size()) {
+        case 0 -> TRUE;
+        case 1 -> clauses.get(0);
+        default -> new SExpr("and", Type.BOOL, clauses);
+        };
     }
 
     /**
diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTTacletTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTTacletTranslator.java
index d29de5ae414..22a92cf034b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTTacletTranslator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTTacletTranslator.java
@@ -63,9 +63,7 @@ public Term translate(Taclet taclet) throws SMTTranslationException {
         return quantify(skeleton, variables);
     }
 
-    private Term quantify(Term smt, Map variables)
-            throws SMTTranslationException {
-
+    private Term quantify(Term smt, Map variables) {
         if (variables.isEmpty()) {
             return smt;
         }
@@ -102,7 +100,7 @@ private Term variablify(Term term, Map variables)
         }
 
         List qvars = new ArrayList<>();
-        if (op instanceof Quantifier q) {
+        if (op instanceof Quantifier) {
             for (QuantifiableVariable boundVar : term.boundVars()) {
                 if (boundVar instanceof SchemaVariable sv) {
                     LogicVariable lv =
@@ -116,7 +114,7 @@ private Term variablify(Term term, Map variables)
         }
 
         if (changes) {
-            ImmutableArray bvars = new ImmutableArray(qvars);
+            var bvars = new ImmutableArray<>(qvars);
             return services.getTermFactory().createTerm(op, subs, bvars, null, term.getLabels());
         } else {
             return term;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SumProdHandler.java b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SumProdHandler.java
index 4311a2ac092..2b636e81103 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SumProdHandler.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SumProdHandler.java
@@ -3,11 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.smt.newsmt2;
 
-import java.util.HashMap;
-import java.util.LinkedHashMap;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.Properties;
+import java.util.*;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.Term;
@@ -21,10 +17,10 @@ public class SumProdHandler implements SMTHandler {
     private Function bsumOp, bprodOp;
 
     // key is the term to identify the bsum, value is the name used for that function.
-    private final HashMap usedBsumTerms = new LinkedHashMap();
+    private final Map usedBsumTerms = new LinkedHashMap<>();
 
     // key is the term to identify the bprod, value is the name used for that function.
-    private final HashMap usedBprodTerms = new LinkedHashMap();
+    private final Map usedBprodTerms = new LinkedHashMap<>();
 
     @Override
     public void init(MasterHandler masterHandler, Services services, Properties handlerSnippets,
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalBlockContract.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalBlockContract.java
index 6af2aa727ce..dabb6ca7ad6 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalBlockContract.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalBlockContract.java
@@ -51,12 +51,6 @@ public ContractPO createProofObl(InitConfig initConfig) {
         return new FunctionalBlockContractPO(initConfig, this);
     }
 
-    @Override
-    public ProofOblInput createProofObl(InitConfig initConfig, Contract contract) {
-        assert contract instanceof FunctionalBlockContract;
-        return new FunctionalBlockContractPO(initConfig, (FunctionalBlockContract) contract);
-    }
-
     @Override
     public ProofOblInput createProofObl(InitConfig initConfig, Contract contract,
             boolean supportSymbolicExecutionAPI) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java
index 134711d1d30..ff2ae281ed4 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java
@@ -581,20 +581,16 @@ private static void replaceVariable(ProgramVariable var, Expression init,
             Map preReplacementMap, Map postReplacementMap,
             LoopContractImpl r, Services services) {
         switch (ReplaceTypes.fromClass(init.getClass())) {
-        case PROGRAM_VARIABLE:
-            replaceVariable(var, (ProgramVariable) init, preReplacementMap, postReplacementMap, r,
-                services);
-            break;
-        case ABSTRACT_INTEGER_LITERAL:
-            replaceVariable(var, (AbstractIntegerLiteral) init, preReplacementMap,
-                postReplacementMap, r, services);
-            break;
-        case EMPTY_SEQ_LITERAL:
-            replaceVariable(var, (EmptySeqLiteral) init, preReplacementMap, postReplacementMap, r,
-                services);
-            break;
-        default:
-            throw new AssertionError();
+        case PROGRAM_VARIABLE -> replaceVariable(var, (ProgramVariable) init, preReplacementMap,
+            postReplacementMap, r,
+            services);
+        case ABSTRACT_INTEGER_LITERAL -> replaceVariable(var, (AbstractIntegerLiteral) init,
+            preReplacementMap,
+            postReplacementMap, r, services);
+        case EMPTY_SEQ_LITERAL -> replaceVariable(var, (EmptySeqLiteral) init, preReplacementMap,
+            postReplacementMap, r,
+            services);
+        default -> throw new AssertionError();
         }
     }
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/PredicateAbstractionMergeContract.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/PredicateAbstractionMergeContract.java
index 65c03d0b2b0..f7e22b22022 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/PredicateAbstractionMergeContract.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/PredicateAbstractionMergeContract.java
@@ -148,17 +148,13 @@ private Map getReplaceMap(Map atPres, Servic
 
     private static Class latticeTypeFromString(
             String latticeTypeStr) {
-        switch (latticeTypeStr) {
-        case "simple":
-            return SimplePredicateAbstractionLattice.class;
-        case "conjunctive":
-            return ConjunctivePredicateAbstractionLattice.class;
-        case "disjunctive":
-            return DisjunctivePredicateAbstractionLattice.class;
-        default:
-            throw new RuntimeException(
-                "PredicateAbstractionMergeContract: Unexpected lattice type: " + latticeTypeStr);
-        }
+        return switch (latticeTypeStr) {
+        case "simple" -> SimplePredicateAbstractionLattice.class;
+        case "conjunctive" -> ConjunctivePredicateAbstractionLattice.class;
+        case "disjunctive" -> DisjunctivePredicateAbstractionLattice.class;
+        default -> throw new RuntimeException(
+            "PredicateAbstractionMergeContract: Unexpected lattice type: " + latticeTypeStr);
+        };
     }
 
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/OverloadedOperatorHandler.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/OverloadedOperatorHandler.java
index afa088210c4..a9bb592cbb0 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/OverloadedOperatorHandler.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/OverloadedOperatorHandler.java
@@ -17,9 +17,9 @@
 /**
  * This class is used to resolve arithmetic operations to {@link SLExpression}s. These are overladed
  * for different primitive types.
- *
+ * 
    
  * It delegates to the {@link JMLOperatorHandler}s registered in the class.
- *
+ * 
    
  * Numeric promotion plays into it, too.
  *
  * @author Alexander Weigl
@@ -175,23 +175,16 @@ public SLExpression build(JMLOperator op, SLExpression left, SLExpression right)
             final var l = left.getTerm();
             final var r = right.getTerm();
             if (l.sort() == ldt.targetSort() && r.sort() == ldt.targetSort()) {
-                switch (op) {
-                case ADD:
-                case BITWISE_OR:
-                    return new SLExpression(tb.union(l, r));
-                case SUBTRACT:
-                    return new SLExpression(tb.setMinus(l, r));
-                case BITWISE_AND:
-                    return new SLExpression(tb.intersect(l, r));
-                case LT:
-                    return new SLExpression(tb.subset(l, r));
-                case LTE:
-                    return new SLExpression(tb.and(tb.subset(l, r), tb.equals(l, r)));
-                case GT:
-                    return new SLExpression(tb.subset(r, l));
-                case GTE:
-                    return new SLExpression(tb.and(tb.subset(r, l), tb.equals(l, r)));
-                }
+                return switch (op) {
+                case ADD, BITWISE_OR -> new SLExpression(tb.union(l, r));
+                case SUBTRACT -> new SLExpression(tb.setMinus(l, r));
+                case BITWISE_AND -> new SLExpression(tb.intersect(l, r));
+                case LT -> new SLExpression(tb.subset(l, r));
+                case LTE -> new SLExpression(tb.and(tb.subset(l, r), tb.equals(l, r)));
+                case GT -> new SLExpression(tb.subset(r, l));
+                case GTE -> new SLExpression(tb.and(tb.subset(r, l), tb.equals(l, r)));
+                default -> null;
+                };
             }
             return null;
         }
@@ -208,21 +201,19 @@ public BinaryBooleanHandler(Services services) {
 
         @Nullable
         @Override
-        public SLExpression build(JMLOperator op, SLExpression left, SLExpression right)
-                throws SLTranslationException {
+        public SLExpression build(JMLOperator op, SLExpression left, SLExpression right) {
             if ((left.getTerm().sort() == sortBoolean || left.getTerm().sort() == Sort.FORMULA)
                     && (right.getTerm().sort() == sortBoolean
                             || right.getTerm().sort() == Sort.FORMULA)) {
                 final var t1 = tb.convertToFormula(left.getTerm());
                 final var t2 = tb.convertToFormula(right.getTerm());
-                switch (op) {
-                case BITWISE_AND:
-                    return new SLExpression(tb.and(t1, t2));
-                case BITWISE_OR:
-                    return new SLExpression(tb.or(t1, t2));
-                case BITWISE_XOR:
-                    return new SLExpression(tb.or(tb.and(t1, tb.not(t2)), tb.and(tb.not(t1), t2)));
-                }
+                return switch (op) {
+                case BITWISE_AND -> new SLExpression(tb.and(t1, t2));
+                case BITWISE_OR -> new SLExpression(tb.or(t1, t2));
+                case BITWISE_XOR -> new SLExpression(
+                    tb.or(tb.and(t1, tb.not(t2)), tb.and(tb.not(t1), t2)));
+                default -> null;
+                };
             }
             return null;
         }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
index ba37105c5c1..44f3d4a8087 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
@@ -41,59 +41,34 @@ public static JMLModifier modifierFromToken(Token token) {
             return null;
         }
 
-        switch (token.getType()) {
-        case JmlLexer.ABSTRACT:
-            return JMLModifier.ABSTRACT;
-        case JmlLexer.FINAL:
-            return JMLModifier.FINAL;
-        case JmlLexer.GHOST:
-            return JMLModifier.GHOST;
-        case JmlLexer.HELPER:
-            return JMLModifier.HELPER;
-        case JmlLexer.INSTANCE:
-            return JMLModifier.INSTANCE;
-        case JmlLexer.MODEL:
-            return JMLModifier.MODEL;
-        case JmlLexer.NON_NULL:
-            return JMLModifier.NON_NULL;
-        case JmlLexer.NULLABLE:
-            return JMLModifier.NULLABLE;
-        case JmlLexer.NULLABLE_BY_DEFAULT:
-            return JMLModifier.NULLABLE_BY_DEFAULT;
-        case JmlLexer.PRIVATE:
-            return JMLModifier.PRIVATE;
-        case JmlLexer.PROTECTED:
-            return JMLModifier.PROTECTED;
-        case JmlLexer.PUBLIC:
-            return JMLModifier.PUBLIC;
-        case JmlLexer.PURE:
-            return JMLModifier.PURE;
-        case JmlLexer.STRICTLY_PURE:
-            return JMLModifier.STRICTLY_PURE;
-        case JmlLexer.SPEC_PROTECTED:
-            return JMLModifier.SPEC_PROTECTED;
-        case JmlLexer.SPEC_PUBLIC:
-            return JMLModifier.SPEC_PUBLIC;
-        case JmlLexer.STATIC:
-            return JMLModifier.STATIC;
-        case JmlLexer.TWO_STATE:
-            return JMLModifier.TWO_STATE;
-        case JmlLexer.NO_STATE:
-            return JMLModifier.NO_STATE;
-        case JmlLexer.SPEC_JAVA_MATH:
-            return JMLModifier.SPEC_JAVA_MATH;
-        case JmlLexer.SPEC_SAFE_MATH:
-            return JMLModifier.SPEC_SAFE_MATH;
-        case JmlLexer.SPEC_BIGINT_MATH:
-            return JMLModifier.SPEC_BIGINT_MATH;
-        case JmlLexer.CODE_JAVA_MATH:
-            return JMLModifier.CODE_JAVA_MATH;
-        case JmlLexer.CODE_SAFE_MATH:
-            return JMLModifier.CODE_SAFE_MATH;
-        case JmlLexer.CODE_BIGINT_MATH:
-            return JMLModifier.CODE_BIGINT_MATH;
-        }
-        throw new IllegalStateException("Illegal token is given");
+        return switch (token.getType()) {
+        case JmlLexer.ABSTRACT -> JMLModifier.ABSTRACT;
+        case JmlLexer.FINAL -> JMLModifier.FINAL;
+        case JmlLexer.GHOST -> JMLModifier.GHOST;
+        case JmlLexer.HELPER -> JMLModifier.HELPER;
+        case JmlLexer.INSTANCE -> JMLModifier.INSTANCE;
+        case JmlLexer.MODEL -> JMLModifier.MODEL;
+        case JmlLexer.NON_NULL -> JMLModifier.NON_NULL;
+        case JmlLexer.NULLABLE -> JMLModifier.NULLABLE;
+        case JmlLexer.NULLABLE_BY_DEFAULT -> JMLModifier.NULLABLE_BY_DEFAULT;
+        case JmlLexer.PRIVATE -> JMLModifier.PRIVATE;
+        case JmlLexer.PROTECTED -> JMLModifier.PROTECTED;
+        case JmlLexer.PUBLIC -> JMLModifier.PUBLIC;
+        case JmlLexer.PURE -> JMLModifier.PURE;
+        case JmlLexer.STRICTLY_PURE -> JMLModifier.STRICTLY_PURE;
+        case JmlLexer.SPEC_PROTECTED -> JMLModifier.SPEC_PROTECTED;
+        case JmlLexer.SPEC_PUBLIC -> JMLModifier.SPEC_PUBLIC;
+        case JmlLexer.STATIC -> JMLModifier.STATIC;
+        case JmlLexer.TWO_STATE -> JMLModifier.TWO_STATE;
+        case JmlLexer.NO_STATE -> JMLModifier.NO_STATE;
+        case JmlLexer.SPEC_JAVA_MATH -> JMLModifier.SPEC_JAVA_MATH;
+        case JmlLexer.SPEC_SAFE_MATH -> JMLModifier.SPEC_SAFE_MATH;
+        case JmlLexer.SPEC_BIGINT_MATH -> JMLModifier.SPEC_BIGINT_MATH;
+        case JmlLexer.CODE_JAVA_MATH -> JMLModifier.CODE_JAVA_MATH;
+        case JmlLexer.CODE_SAFE_MATH -> JMLModifier.CODE_SAFE_MATH;
+        case JmlLexer.CODE_BIGINT_MATH -> JMLModifier.CODE_BIGINT_MATH;
+        default -> throw new IllegalStateException("Illegal token is given");
+        };
     }
 
     @Override
@@ -130,24 +105,16 @@ private Behavior getBehavior(Token behavior) {
         if (behavior == null) {
             return Behavior.NONE; // lightweight specification
         }
-
-        switch (behavior.getType()) {
-        case JmlLexer.BEHAVIOR:
-            return Behavior.BEHAVIOR;
-        case JmlLexer.NORMAL_BEHAVIOR:
-            return Behavior.NORMAL_BEHAVIOR;
-        case JmlLexer.BREAK_BEHAVIOR:
-            return Behavior.BREAK_BEHAVIOR;
-        case JmlLexer.EXCEPTIONAL_BEHAVIOUR:
-            return Behavior.EXCEPTIONAL_BEHAVIOR;
-        case JmlLexer.MODEL_BEHAVIOUR:
-            return Behavior.MODEL_BEHAVIOR;
-        case JmlLexer.RETURN_BEHAVIOR:
-            return Behavior.RETURN_BEHAVIOR;
-        case JmlLexer.CONTINUE_BEHAVIOR:
-            return Behavior.CONTINUE_BEHAVIOR;
-        }
-        throw new IllegalStateException("No behavior is given");
+        return switch (behavior.getType()) {
+        case JmlLexer.BEHAVIOR -> Behavior.BEHAVIOR;
+        case JmlLexer.NORMAL_BEHAVIOR -> Behavior.NORMAL_BEHAVIOR;
+        case JmlLexer.BREAK_BEHAVIOR -> Behavior.BREAK_BEHAVIOR;
+        case JmlLexer.EXCEPTIONAL_BEHAVIOUR -> Behavior.EXCEPTIONAL_BEHAVIOR;
+        case JmlLexer.MODEL_BEHAVIOUR -> Behavior.MODEL_BEHAVIOR;
+        case JmlLexer.RETURN_BEHAVIOR -> Behavior.RETURN_BEHAVIOR;
+        case JmlLexer.CONTINUE_BEHAVIOR -> Behavior.CONTINUE_BEHAVIOR;
+        default -> throw new IllegalStateException("No behavior is given");
+        };
     }
 
     @Override
@@ -174,7 +141,7 @@ public Object visitSpec_body(JmlParser.Spec_bodyContext ctx) {
 
     @Override
     public Name[] visitTargetHeap(JmlParser.TargetHeapContext ctx) {
-        if (ctx == null || ctx.SPECIAL_IDENT().size() == 0) {
+        if (ctx == null || ctx.SPECIAL_IDENT().isEmpty()) {
             return new Name[] { HeapLDT.BASE_HEAP_NAME };
         }
         Name[] heaps = new Name[ctx.SPECIAL_IDENT().size()];
@@ -445,7 +412,7 @@ public Object visitClass_axiom(JmlParser.Class_axiomContext ctx) {
 
     @Override
     public Object visitField_declaration(JmlParser.Field_declarationContext ctx) {
-        assert mods.size() > 0;
+        assert !mods.isEmpty();
         TextualJMLFieldDecl inv = new TextualJMLFieldDecl(mods, ctx);
         constructs = constructs.append(inv);
         return null;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
index a5873acb47e..b8a497afa50 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
@@ -1702,18 +1702,15 @@ public Object visitSequenceFuncs(JmlParser.SequenceFuncsContext ctx) {
 
         final Term t2 = e2.getTerm();
         final Term t1 = e1.getTerm();
-        switch (ctx.op.getType()) {
-        case JmlLexer.SEQCONCAT:
-            return termFactory.seqConcat(t1, t2);
-        case JmlLexer.SEQGET:
-            return termFactory.seqGet(t1, t2);
-        case JmlLexer.INDEXOF:
-            return termFactory.createIndexOf(t1, t2);
-        default:
-            raiseError(ctx, "Unexpected syntax case.");
-        }
-        raiseError(ctx, "Unknown operator: %s", ctx.op);
-        return null;
+        return switch (ctx.op.getType()) {
+            case JmlLexer.SEQCONCAT -> termFactory.seqConcat(t1, t2);
+            case JmlLexer.SEQGET -> termFactory.seqGet(t1, t2);
+            case JmlLexer.INDEXOF -> termFactory.createIndexOf(t1, t2);
+            default -> {
+                raiseError(ctx, "Unknown operator: %s", ctx.op);
+                yield null;
+            }
+        };
     }
 
     @Override
@@ -1738,42 +1735,37 @@ public SLExpression visitSpecquantifiedexpression(
             guard = a.getTerm();
         }
         SLExpression expr =
-            ctx.expression().size() == 2 ? accept(ctx.expression(1)) : accept(ctx.expression(0));
+                ctx.expression().size() == 2 ? accept(ctx.expression(1)) : accept(ctx.expression(0));
 
         resolverManager.popLocalVariablesNamespace();
         assert guard != null;
         guard = tb.convertToFormula(guard);
         assert expr != null;
         final Term body = expr.getTerm();
-        switch (ctx.quantifier().start.getType()) {
-        case JmlLexer.FORALL:
-            return termFactory.forall(guard, body, declVars.first, declVars.second, nullable,
-                expr.getType());
-        case JmlLexer.EXISTS:
-            return termFactory.exists(guard, body, declVars.first, declVars.second, nullable,
-                expr.getType());
-        case JmlLexer.MAX:
-            return termFactory.quantifiedMax(guard, body, declVars.first, nullable,
-                declVars.second);
-        case JmlLexer.MIN:
-            return termFactory.quantifiedMin(guard, body, declVars.first, nullable,
-                declVars.second);
-        case JmlLexer.NUM_OF:
-            KeYJavaType kjtInt =
-                services.getTypeConverter().getKeYJavaType(PrimitiveType.JAVA_BIGINT);
-            return termFactory.quantifiedNumOf(guard, body, declVars.first, nullable,
-                declVars.second, kjtInt);
-        case JmlLexer.SUM:
-            return termFactory.quantifiedSum(declVars.first, nullable, declVars.second, guard, body,
-                expr.getType());
-        case JmlLexer.PRODUCT:
-            return termFactory.quantifiedProduct(declVars.first, nullable, declVars.second, guard,
-                body, expr.getType());
-        default:
-            raiseError(ctx, "Unexpected syntax case.");
-        }
-        raiseError(ctx, "Unexpected syntax case.");
-        return null;
+        return switch (ctx.quantifier().start.getType()) {
+            case JmlLexer.FORALL -> termFactory.forall(guard, body, declVars.first, declVars.second, nullable,
+                    expr.getType());
+            case JmlLexer.EXISTS -> termFactory.exists(guard, body, declVars.first, declVars.second, nullable,
+                    expr.getType());
+            case JmlLexer.MAX -> termFactory.quantifiedMax(guard, body, declVars.first, nullable,
+                    declVars.second);
+            case JmlLexer.MIN -> termFactory.quantifiedMin(guard, body, declVars.first, nullable,
+                    declVars.second);
+            case JmlLexer.NUM_OF -> {
+                KeYJavaType kjtInt =
+                        services.getTypeConverter().getKeYJavaType(PrimitiveType.JAVA_BIGINT);
+                yield termFactory.quantifiedNumOf(guard, body, declVars.first, nullable,
+                        declVars.second, kjtInt);
+            }
+            case JmlLexer.SUM -> termFactory.quantifiedSum(declVars.first, nullable, declVars.second, guard, body,
+                    expr.getType());
+            case JmlLexer.PRODUCT -> termFactory.quantifiedProduct(declVars.first, nullable, declVars.second, guard,
+                    body, expr.getType());
+            default -> {
+                raiseError(ctx, "Unexpected syntax case.");
+                yield null;
+            }
+        };
     }
 
     @Override
@@ -1903,8 +1895,7 @@ public KeYJavaType visitTypespec(JmlParser.TypespecContext ctx) {
             try {
                 javaInfo.readJavaBlock("{" + fullName + " k;}");
                 t = javaInfo.getKeYJavaType(fullName);
-            } catch (Exception e) {
-                t = null;
+            } catch (Exception ignored) {
             }
         }
         return t;
@@ -1961,9 +1952,7 @@ public LogicVariable visitQuantifiedvariabledeclarator(
             } else {
                 fullName.append(t.getFullName());
             }
-            for (int i = 0; i < dim; i++) {
-                fullName.append("[]");
-            }
+            fullName.append("[]".repeat(dim));
             varType = javaInfo.getKeYJavaType(fullName.toString());
         } else {
             varType = t;
@@ -2132,14 +2121,9 @@ private void insertSimpleClause(String type, LocationVariable heap, Term t,
             ContractClauses.Clauses free,
             ContractClauses.Clauses redundantly) {
         switch (subType(type)) {
-        case FREE:
-            contractClauses.add(free, heap, t);
-            break;
-        case REDUNDANT:
-            contractClauses.add(redundantly, heap, t);
-            break;
-        default:
-            contractClauses.add(none, heap, t);
+        case FREE -> contractClauses.add(free, heap, t);
+        case REDUNDANT -> contractClauses.add(redundantly, heap, t);
+        default -> contractClauses.add(none, heap, t);
         }
     }
 
@@ -2531,19 +2515,10 @@ public LocationVariable[] visitTargetHeap(JmlParser.TargetHeapContext ctx) {
         for (int i = 0; i < ctx.SPECIAL_IDENT().size(); i++) {
             String heapName = ctx.SPECIAL_IDENT(i).getText();
             switch (heapName) {
-            case "":
-            case "":
-                heaps[i] = getPermissionHeap();
-                break;
-            case "":
-            case "":
-                heaps[i] = getSavedHeap();
-                break;
-            case "":
-                heaps[i] = getBaseHeap();
-                break;
-            default:
-                heaps[i] = heapLDT.getHeapForName(new Name(heapName));
+            case "", "" -> heaps[i] = getPermissionHeap();
+            case "", "" -> heaps[i] = getSavedHeap();
+            case "" -> heaps[i] = getBaseHeap();
+            default -> heaps[i] = heapLDT.getHeapForName(new Name(heapName));
             }
         }
         return heaps;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLResolverManager.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLResolverManager.java
index 174706502cd..65ed989a381 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLResolverManager.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLResolverManager.java
@@ -35,11 +35,10 @@ public abstract class SLResolverManager {
     private final boolean useLocalVarsAsImplicitReceivers;
     private final TermBuilder tb;
 
-    private ImmutableList> /* ParsableVariable */
-    localVariablesNamespaces = ImmutableSLList.nil();
+    private ImmutableList> localVariablesNamespaces =
+        ImmutableSLList.nil();
 
-    private final Map kjts =
-        new LinkedHashMap<>();
+    private final Map kjts = new LinkedHashMap<>();
 
     // -------------------------------------------------------------------------
     // constructors
@@ -122,8 +121,7 @@ private SLExpression resolveImplicit(String name, SLParameters parameters)
         // (e.g. for static attributes or static methods)
         if (specInClass != null) {
             SLExpression receiver = new SLExpression(specInClass);
-            SLExpression result = resolveExplicit(receiver, name, parameters);
-            return result;
+            return resolveExplicit(receiver, name, parameters);
         }
 
         return null;
@@ -152,7 +150,7 @@ private SLExpression resolveExplicit(SLExpression receiver, String name, SLParam
      */
     private SLExpression resolveIt(SLExpression receiver, String name, SLParameters parameters)
             throws SLTranslationException {
-        SLExpression result = null;
+        SLExpression result;
 
         if (receiver != null) {
             result = resolveExplicit(receiver, name, parameters);
@@ -181,7 +179,6 @@ private SLExpression resolveIt(SLExpression receiver, String name, SLParameters
      * @param name name of the property
      * @param parameters actual parameters of the property call, or null
      * @return corresponding term, type or collection if successful, null otherwise
-     * @throws SLTranslationException
      */
     public SLExpression resolve(SLExpression receiver, String name, SLParameters parameters)
             throws SLTranslationException {
@@ -203,8 +200,7 @@ public SLExpression resolve(SLExpression receiver, String name, SLParameters par
      * Pushes a new, empty namespace onto the stack.
      */
     public void pushLocalVariablesNamespace() {
-        // FIXME: This breaks the generics of namespaces.
-        Namespace ns = new Namespace();
+        var ns = new Namespace();
         localVariablesNamespaces = localVariablesNamespaces.prepend(ns);
     }
 
@@ -213,8 +209,7 @@ public void pushLocalVariablesNamespace() {
      * Puts a local variable into the topmost namespace on the stack
      */
     public void putIntoTopLocalVariablesNamespace(ParsableVariable pv, KeYJavaType kjt) {
-        // FIXME: This breaks the generics of Namespaces.
-        ((Namespace) localVariablesNamespaces.head()).addSafely(pv);
+        localVariablesNamespaces.head().addSafely(pv);
         kjts.put(pv, kjt);
     }
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java
index 25611a27205..d6c8d662444 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java
@@ -124,32 +124,32 @@ protected Feature setupGlobalF(Feature dispatcher) {
         final Feature methodSpecF;
         final String methProp =
             strategyProperties.getProperty(StrategyProperties.METHOD_OPTIONS_KEY);
-        if (methProp.equals(StrategyProperties.METHOD_CONTRACT)) {
-            methodSpecF = methodSpecFeature(longConst(-20));
-        } else if (methProp.equals(StrategyProperties.METHOD_EXPAND)) {
-            methodSpecF = methodSpecFeature(inftyConst());
-        } else if (methProp.equals(StrategyProperties.METHOD_NONE)) {
-            methodSpecF = methodSpecFeature(inftyConst());
-        } else {
+        switch (methProp) {
+        case StrategyProperties.METHOD_CONTRACT -> methodSpecF = methodSpecFeature(longConst(-20));
+        case StrategyProperties.METHOD_EXPAND -> methodSpecF = methodSpecFeature(inftyConst());
+        case StrategyProperties.METHOD_NONE -> methodSpecF = methodSpecFeature(inftyConst());
+        default -> {
             methodSpecF = null;
             assert false;
         }
+        }
 
         final String queryProp =
             strategyProperties.getProperty(StrategyProperties.QUERY_OPTIONS_KEY);
         final Feature queryF;
-        if (queryProp.equals(StrategyProperties.QUERY_ON)) {
-            queryF = querySpecFeature(new QueryExpandCost(200, 1, 1, false));
-        } else if (queryProp.equals(StrategyProperties.QUERY_RESTRICTED)) {
+        switch (queryProp) {
+        case StrategyProperties.QUERY_ON -> queryF =
+            querySpecFeature(new QueryExpandCost(200, 1, 1, false));
+        case StrategyProperties.QUERY_RESTRICTED ->
             // All tests in the example directory pass with this strategy.
             // Hence, the old query_on strategy is obsolete.
             queryF = querySpecFeature(new QueryExpandCost(500, 0, 1, true));
-        } else if (queryProp.equals(StrategyProperties.QUERY_OFF)) {
-            queryF = querySpecFeature(inftyConst());
-        } else {
+        case StrategyProperties.QUERY_OFF -> queryF = querySpecFeature(inftyConst());
+        default -> {
             queryF = null;
             assert false;
         }
+        }
 
         final Feature depSpecF;
         final String depProp = strategyProperties.getProperty(StrategyProperties.DEP_OPTIONS_KEY);
@@ -383,56 +383,39 @@ private RuleSetDispatchFeature setupCostComputationF() {
             strategyProperties.getProperty(StrategyProperties.METHOD_OPTIONS_KEY);
 
         switch (methProp) {
-        case StrategyProperties.METHOD_CONTRACT:
+        case StrategyProperties.METHOD_CONTRACT ->
             /*
              * If method treatment by contracts is chosen, this does not mean that method expansion
              * is disabled. The original cost was 200 and is now increased to 2000 in order to
              * repress method expansion stronger when method treatment by contracts is chosen.
              */
             bindRuleSet(d, "method_expand", longConst(2000));
-            break;
-        case StrategyProperties.METHOD_EXPAND:
-            bindRuleSet(d, "method_expand", longConst(100));
-            break;
-        case StrategyProperties.METHOD_NONE:
-            bindRuleSet(d, "method_expand", inftyConst());
-            break;
-        default:
-            throw new RuntimeException("Unexpected strategy property " + methProp);
+        case StrategyProperties.METHOD_EXPAND -> bindRuleSet(d, "method_expand", longConst(100));
+        case StrategyProperties.METHOD_NONE -> bindRuleSet(d, "method_expand", inftyConst());
+        default -> throw new RuntimeException("Unexpected strategy property " + methProp);
         }
 
         final String mpsProp = strategyProperties.getProperty(StrategyProperties.MPS_OPTIONS_KEY);
 
         switch (mpsProp) {
-        case StrategyProperties.MPS_MERGE:
+        case StrategyProperties.MPS_MERGE ->
             /*
              * For this case, we use a special feature, since deleting merge points should only be
              * done after a merge rule application.
              */
             bindRuleSet(d, "merge_point", DeleteMergePointRuleFeature.INSTANCE);
-            break;
-        case StrategyProperties.MPS_SKIP:
-            bindRuleSet(d, "merge_point", longConst(-5000));
-            break;
-        case StrategyProperties.MPS_NONE:
-            bindRuleSet(d, "merge_point", inftyConst());
-            break;
-        default:
-            throw new RuntimeException("Unexpected strategy property " + methProp);
+        case StrategyProperties.MPS_SKIP -> bindRuleSet(d, "merge_point", longConst(-5000));
+        case StrategyProperties.MPS_NONE -> bindRuleSet(d, "merge_point", inftyConst());
+        default -> throw new RuntimeException("Unexpected strategy property " + methProp);
         }
 
 
         final String queryAxProp =
             strategyProperties.getProperty(StrategyProperties.QUERYAXIOM_OPTIONS_KEY);
         switch (queryAxProp) {
-        case StrategyProperties.QUERYAXIOM_ON:
-            bindRuleSet(d, "query_axiom", longConst(-3000));
-            break;
-        case StrategyProperties.QUERYAXIOM_OFF:
-            bindRuleSet(d, "query_axiom", inftyConst());
-            break;
-        default:
-            throw new RuntimeException("Unexpected strategy property " + queryAxProp);
+        case StrategyProperties.QUERYAXIOM_ON -> bindRuleSet(d, "query_axiom", longConst(-3000));
+        case StrategyProperties.QUERYAXIOM_OFF -> bindRuleSet(d, "query_axiom", inftyConst());
+        default -> throw new RuntimeException("Unexpected strategy property " + queryAxProp);
         }
 
         if (classAxiomApplicationEnabled()) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NonDuplicateAppModPositionFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NonDuplicateAppModPositionFeature.java
index 7919f201d07..9c8de611c8b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NonDuplicateAppModPositionFeature.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NonDuplicateAppModPositionFeature.java
@@ -5,7 +5,6 @@
 
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.rule.TacletApp;
 import de.uka.ilkd.key.rule.inst.SVInstantiations.UpdateLabelPair;
 
@@ -19,15 +18,6 @@ public class NonDuplicateAppModPositionFeature extends NonDuplicateAppFeature {
 
     public static final Feature INSTANCE = new NonDuplicateAppModPositionFeature();
 
-    @Override
-    public boolean filter(TacletApp app, PosInOccurrence pos, Goal goal) {
-        if (!app.ifInstsComplete()) {
-            return true;
-        }
-
-        return noDuplicateFindTaclet(app, pos, goal);
-    }
-
     @Override
     protected boolean comparePio(TacletApp newApp, TacletApp oldApp, PosInOccurrence newPio,
             PosInOccurrence oldPio) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/SortComparisonFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/SortComparisonFeature.java
index a0e6ed622d5..947180e9da8 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/SortComparisonFeature.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/SortComparisonFeature.java
@@ -42,12 +42,10 @@ protected boolean filter(RuleApp app, PosInOccurrence pos, Goal goal) {
      * @param sort2
      */
     protected boolean compare(final Sort sort1, final Sort sort2) {
-        switch (comparator) {
-        case SUBSORT:
+        if (comparator == SUBSORT) {
             return sort1.extendsTrans(sort2);
-        default:
-            return false;
         }
+        return false;
     }
 
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/RootsGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/RootsGenerator.java
index 4438935d470..2030daafa5c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/RootsGenerator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/RootsGenerator.java
@@ -99,30 +99,28 @@ private Term breakDownEq(Term var, BigInteger lit, int pow, TermServices service
 
         if ((pow % 2 == 0)) {
             // the even case
-
-            switch (lit.signum()) {
-            case -1:
-                // no solutions
-                return tb.ff();
-            case 0:
-                // exactly one solution
-                return tb.equals(var, zero);
-            case 1:
-                final BigInteger r = root(lit, pow);
-                if (power(r, pow).equals(lit)) {
-                    // two solutions
-                    final Term rTerm = tb.zTerm(r.toString());
-                    final Term rNegTerm = tb.zTerm(r.negate().toString());
-                    return tb.or(tb.or(tb.lt(var, rNegTerm), tb.gt(var, rTerm)),
-                        tb.and(tb.gt(var, rNegTerm), tb.lt(var, rTerm)));
-                } else {
-                    // no solution
-                    return tb.ff();
+            return switch (lit.signum()) {
+                case -1 -> // no solutions
+                        tb.ff();
+                case 0 -> // exactly one solution
+                        tb.equals(var, zero);
+                case 1 -> {
+                    final BigInteger r = root(lit, pow);
+                    if (power(r, pow).equals(lit)) {
+                        // two solutions
+                        final Term rTerm = tb.zTerm(r.toString());
+                        final Term rNegTerm = tb.zTerm(r.negate().toString());
+                        yield tb.or(tb.or(tb.lt(var, rNegTerm), tb.gt(var, rTerm)),
+                                tb.and(tb.gt(var, rNegTerm), tb.lt(var, rTerm)));
+                    } else {
+                        // no solution
+                        yield tb.ff();
+                    }
                 }
-            }
+                default -> null;
+            };
         } else {
             // the odd case
-
             final BigInteger r = root(lit, pow);
             if (power(r, pow).equals(lit)) {
                 // one solution
@@ -133,60 +131,49 @@ private Term breakDownEq(Term var, BigInteger lit, int pow, TermServices service
                 return tb.ff();
             }
         }
-
-        assert false; // unreachable
-        return null;
     }
 
     private Term breakDownGeq(Term var, BigInteger lit, int pow, TermServices services) {
         if ((pow % 2 == 0)) {
             // the even case
 
-            switch (lit.signum()) {
-            case -1:
-            case 0:
-                // the inequation is no restriction
-                return tb.ff();
-            case 1:
-                final BigInteger r = rootRoundingUpwards(lit, pow);
-                final Term rTerm = tb.zTerm(r.toString());
-                final Term rNegTerm = tb.zTerm(r.negate().toString());
-                return tb.or(tb.leq(var, rNegTerm), tb.geq(var, rTerm));
-            }
+            return switch (lit.signum()) {
+                case -1, 0 -> // the inequation is no restriction
+                        tb.ff();
+                case 1 -> {
+                    final BigInteger r = rootRoundingUpwards(lit, pow);
+                    final Term rTerm = tb.zTerm(r.toString());
+                    final Term rNegTerm = tb.zTerm(r.negate().toString());
+                    yield tb.or(tb.leq(var, rNegTerm), tb.geq(var, rTerm));
+                }
+                default -> throw new IllegalStateException("Unexpected value: " + lit.signum());
+            };
         } else {
             // the odd case
-
             return tb.geq(var, tb.zTerm(rootRoundingUpwards(lit, pow).toString()));
         }
-
-        assert false; // unreachable
-        return null;
     }
 
     private Term breakDownLeq(Term var, BigInteger lit, int pow, TermServices services) {
         if ((pow % 2 == 0)) {
             // the even case
 
-            switch (lit.signum()) {
-            case -1:
-                // no solutions
-                return tb.ff();
-            case 0:
-                return tb.equals(var, tb.zero());
-            case 1:
-                final BigInteger r = root(lit, pow);
-                final Term rTerm = tb.zTerm(r.toString());
-                final Term rNegTerm = tb.zTerm(r.negate().toString());
-                return tb.and(tb.geq(var, rNegTerm), tb.leq(var, rTerm));
-            }
+            return switch (lit.signum()) {
+                case -1 -> // no solutions
+                        tb.ff();
+                case 0 -> tb.equals(var, tb.zero());
+                case 1 -> {
+                    final BigInteger r = root(lit, pow);
+                    final Term rTerm = tb.zTerm(r.toString());
+                    final Term rNegTerm = tb.zTerm(r.negate().toString());
+                    yield tb.and(tb.geq(var, rNegTerm), tb.leq(var, rTerm));
+                }
+                default -> throw new IllegalStateException("Unexpected value: " + lit.signum());
+            };
         } else {
             // the odd case
-
             return tb.leq(var, tb.zTerm(root(lit, pow).toString()));
         }
-
-        assert false; // unreachable
-        return null;
     }
 
     /**
diff --git a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/DefaultTacletTranslator.java b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/DefaultTacletTranslator.java
index 237622b58fa..b98c32a8df0 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/DefaultTacletTranslator.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/DefaultTacletTranslator.java
@@ -69,8 +69,7 @@ private Term translateReplaceAndAddTerm(TacletGoalTemplate template, Term find,
             replace = TacletSections.REPLACE.getDefaultValue(services);
         }
 
-        Term term = tb.imp(tb.equals(find, replace), add);
-        return term;
+        return tb.imp(tb.equals(find, replace), add);
     }
 
     /**
@@ -105,29 +104,23 @@ private Term translateReplaceAndAddFormula(TacletGoalTemplate template, Term fin
         assert polarity == 0 || add == TacletSections.ADD.getDefaultValue(services)
                 : "add() commands not allowed in polarity rules (syntactically forbidden)";
 
-        Term term = tb.imp(translateEquivalence(find, replace, polarity, services), add);
-        return term;
+        return tb.imp(translateEquivalence(find, replace, polarity, services), add);
 
     }
 
     private Term translateEquivalence(Term find, Term replace, int polarity,
             TermServices services) {
         TermBuilder tb = services.getTermBuilder();
-        switch (polarity) {
-        case 0:
-            return tb.equals(find, replace);
-        case 1:
-            return tb.imp(replace, find);
-        case -1:
-            return tb.imp(find, replace);
-        default:
-            throw new IllegalArgumentException();
-        }
+        return switch (polarity) {
+        case 0 -> tb.equals(find, replace);
+        case 1 -> tb.imp(replace, find);
+        case -1 -> tb.imp(find, replace);
+        default -> throw new IllegalArgumentException();
+        };
     }
 
     private Term translateReplaceAndAddSequent(TacletGoalTemplate template, int type,
             TermServices services) {
-
         TermBuilder tb = services.getTermBuilder();
         Sequent replace = null;
         if (template instanceof AntecSuccTacletGoalTemplate) {
@@ -144,8 +137,7 @@ private Term translateReplaceAndAddSequent(TacletGoalTemplate template, int type
         if (rep == null) {
             rep = TacletSections.REPLACE.getDefaultValue(services);
         }
-        Term term = tb.or(rep, add);
-        return term;
+        return tb.or(rep, add);
     }
 
     /**
@@ -215,7 +207,7 @@ public Term translate(Taclet taclet, TermServices services) throws IllegalTaclet
 
     /**
      * Retrieve the "find" Term from a FindTaclet.
-     *
+     * 
    
      * Originally, this simply calls {@link FindTaclet#find()}. Overriding classes may choose to
      * garnish the result with additional information.
      *
diff --git a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/UserDefinedSymbols.java b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/UserDefinedSymbols.java
index 8ae2adfa0bd..5fe559c193a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/UserDefinedSymbols.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/UserDefinedSymbols.java
@@ -54,7 +54,7 @@ public UserDefinedSymbols(UserDefinedSymbols parent) {
         this.referenceNamespaces = parent.referenceNamespaces;
     }
 
-    private  void addUserDefiniedSymbol(T symbol, Set set,
+    private  void addUserDefinedSymbol(T symbol, Set set,
             Namespace excludeNamespace) {
         if (!contains(symbol, set)) {
             if (symbol instanceof SchemaVariable
@@ -74,11 +74,11 @@ private  boolean contains(T symbol, Set set) {
     }
 
     public void addFunction(Function symbol) {
-        addUserDefiniedSymbol(symbol, usedExtraFunctions, referenceNamespaces.functions());
+        addUserDefinedSymbol(symbol, usedExtraFunctions, referenceNamespaces.functions());
     }
 
     public void addPredicate(Function symbol) {
-        addUserDefiniedSymbol(symbol, usedExtraPredicates, referenceNamespaces.functions());
+        addUserDefinedSymbol(symbol, usedExtraPredicates, referenceNamespaces.functions());
     }
 
     public void addSort(Named symbol) {
@@ -89,17 +89,18 @@ public void addSort(Named symbol) {
                     addSort(parentSort);
                 }
             }
-            addUserDefiniedSymbol(sort, usedExtraSorts, referenceNamespaces.sorts());
+            addUserDefinedSymbol(sort, usedExtraSorts, referenceNamespaces.sorts());
         }
     }
 
     public void addVariable(QuantifiableVariable symbol) {
-        addUserDefiniedSymbol(symbol, usedExtraVariables, referenceNamespaces.variables());
+        addUserDefinedSymbol(symbol, usedExtraVariables, referenceNamespaces.variables());
     }
 
+    @SuppressWarnings({ "rawtypes", "unchecked" })
     public void addSchemaVariable(SchemaVariable symbol) {
         // FIXME: This breaks the generics of namespace
-        addUserDefiniedSymbol(symbol, usedSchemaVariables,
+        addUserDefinedSymbol(symbol, usedSchemaVariables,
             (Namespace) referenceNamespaces.variables());
     }
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java b/key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java
index 42c58beb19a..5eeecfc3891 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java
@@ -59,9 +59,11 @@
  */
 public final class MiscTools {
 
-    /** Pattern to parse URL scheme (capture group 1) and scheme specific part (group 2). */
+    /**
+     * Pattern to parse URL scheme (capture group 1) and scheme specific part (group 2).
+     */
     private static final Pattern URL_PATTERN =
-        Pattern.compile("(^[a-zA-Z][a-zA-Z0-9\\+\\-\\.]*):(.*)");
+        Pattern.compile("(^[a-zA-Z][a-zA-Z0-9+\\-.]*):(.*)");
 
     private MiscTools() {
     }
@@ -362,12 +364,11 @@ public static Name toValidVariableName(String s) {
     /**
      * Join the string representations of a collection of objects into onw string. The individual
      * elements are separated by a delimiter.
-     *
+     * 
    
      * {@link Object#toString()} is used to turn the objects into strings.
      *
      * @param collection an arbitrary non-null collection
      * @param delimiter a non-null string which is put between the elements.
-     *
      * @return the concatenation of all string representations separated by the delimiter
      */
     public static String join(Iterable collection, String delimiter) {
@@ -377,12 +378,11 @@ public static String join(Iterable collection, String delimiter) {
     /**
      * Join the string representations of an array of objects into one string. The individual
      * elements are separated by a delimiter.
-     *
+     * 
    
      * {@link Object#toString()} is used to turn the objects into strings.
      *
      * @param collection an arbitrary non-null array of objects
      * @param delimiter a non-null string which is put between the elements.
-     *
      * @return the concatenation of all string representations separated by the delimiter
      */
     public static String join(Object[] collection, String delimiter) {
@@ -392,13 +392,12 @@ public static String join(Object[] collection, String delimiter) {
     /**
      * Takes a string and returns a string which is potentially shorter and contains a
      * sub-collection of the original characters.
-     *
+     * 
    
      * All alphabetic characters (A-Z and a-z) are copied to the result while all other characters
      * are removed.
      *
      * @param string an arbitrary string
      * @return a string which is a sub-structure of the original character sequence
-     *
      * @author Mattias Ulbrich
      */
     public static /* @ non_null @ */ String filterAlphabetic(/* @ non_null @ */ String string) {
@@ -420,9 +419,6 @@ public static boolean containsWholeWord(String s, String word) {
     /**
      * There are different kinds of JML markers. See Section 4.4 "Annotation markers" of the JML
      * reference manual.
-     *
-     * @param comment
-     * @return
      */
     public static boolean isJMLComment(String comment) {
         return Strings.isJMLComment(comment);
@@ -733,31 +729,32 @@ public static Optional extractURI(DataLocation loc) {
         }
 
         try {
-            switch (loc.getType()) {
-            case "URL": // URLDataLocation
-                return Optional.of(((URLDataLocation) loc).url().toURI());
-            case "ARCHIVE": // ArchiveDataLocation
-                // format: "ARCHIVE:?"
-                ArchiveDataLocation adl = (ArchiveDataLocation) loc;
-
-                // extract item name and zip file
-                int qmindex = adl.toString().lastIndexOf('?');
-                String itemName = adl.toString().substring(qmindex + 1);
-                ZipFile zip = adl.getFile();
-
-                // use special method to ensure that path separators are correct
-                return Optional.of(getZipEntryURI(zip, itemName));
-            case "FILE": // DataFileLocation
-                // format: "FILE:"
-                return Optional.of(((DataFileLocation) loc).getFile().toURI());
-            default: // SpecDataLocation
-                // format "://"
-                // wrap into URN to ensure URI encoding is correct (no spaces!)
-                return Optional.empty();
-            }
+            return switch (loc.getType()) {
+                case "URL" -> // URLDataLocation
+                        Optional.of(((URLDataLocation) loc).url().toURI());
+                case "ARCHIVE" -> { // ArchiveDataLocation
+                    // format: "ARCHIVE:?"
+                    ArchiveDataLocation adl = (ArchiveDataLocation) loc;
+
+                    // extract item name and zip file
+                    int qmindex = adl.toString().lastIndexOf('?');
+                    String itemName = adl.toString().substring(qmindex + 1);
+                    ZipFile zip = adl.getFile();
+
+                    // use special method to ensure that path separators are correct
+                    yield Optional.of(getZipEntryURI(zip, itemName));
+                }
+                case "FILE" -> // DataFileLocation
+                    // format: "FILE:"
+                        Optional.of(((DataFileLocation) loc).getFile().toURI());
+                default -> // SpecDataLocation
+                    // format "://"
+                    // wrap into URN to ensure URI encoding is correct (no spaces!)
+                        Optional.empty();
+            };
         } catch (URISyntaxException | IOException e) {
             throw new IllegalArgumentException(
-                "The given DataLocation can not be converted into a valid URI: " + loc, e);
+                    "The given DataLocation can not be converted into a valid URI: " + loc, e);
         }
     }
 
@@ -844,7 +841,7 @@ public static URI getURIFromTokenSource(String source) {
      *
* * - * + *

* A NullPointerException is thrown if null is given. If the input is "", ".", or a relative * path in general, the path is resolved against the current working directory (see system * property "user.dir") consistently to the behaviour of {@link Paths#get(String, String...)}. @@ -867,16 +864,16 @@ public static URL parseURL(final String input) throws MalformedURLException { schemeSpecPart = m.group(2); } switch (scheme) { - case "URL": + case "URL" -> { // schemeSpecPart actually contains a URL again return new URL(schemeSpecPart); - case "ARCHIVE": + } + case "ARCHIVE" -> { // format: "ARCHIVE:?" // extract item name and zip file int qmindex = schemeSpecPart.lastIndexOf('?'); String zipName = schemeSpecPart.substring(0, qmindex); String itemName = schemeSpecPart.substring(qmindex + 1); - try { ZipFile zip = new ZipFile(zipName); // use special method to ensure that path separators are correct @@ -887,15 +884,18 @@ public static URL parseURL(final String input) throws MalformedURLException { me.initCause(e); throw me; } - case "FILE": + } + case "FILE" -> { // format: "FILE:" Path path = Paths.get(schemeSpecPart).toAbsolutePath().normalize(); return path.toUri().toURL(); - case "": + } + case "" -> { // only file/path without protocol Path p = Paths.get(input).toAbsolutePath().normalize(); return p.toUri().toURL(); - default: + } + default -> { // may still be Windows path starting with : if (scheme.length() == 1) { // TODO: Theoretically, a protocol with only a single letter is allowed. @@ -907,5 +907,6 @@ public static URL parseURL(final String input) throws MalformedURLException { // if this also fails, there is an unknown protocol -> MalformedURLException return new URL(input); } + } } } diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/GenerateUnitTests.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/GenerateUnitTests.java index 06f8d3ce048..b8dbbaf79b3 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/GenerateUnitTests.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/GenerateUnitTests.java @@ -5,7 +5,6 @@ import java.io.File; import java.io.IOException; -import java.nio.charset.StandardCharsets; import java.nio.file.Files; import java.nio.file.Paths; import java.util.Map; @@ -29,7 +28,7 @@ * {@code generateRunAllProofs}. *

* The considered proof collections files are configured statically in - * {@link #collections}. + * {@link ProofCollections}. * * @author Alexander Weigl * @version 1 (6/14/20) @@ -57,41 +56,60 @@ public static void main(String[] args) throws IOException { for (var col : collections) { for (RunAllProofsTestUnit unit : col.createRunAllProofsTestUnits()) { - createUnitClass(col, unit); + createUnitClass(unit); } } } + // "import de.uka.ilkd.key.util.NamedRunner;\n" + + // "import de.uka.ilkd.key.util.TestName;\n" + + // "@org.junit.experimental.categories.Category(org.key_project.util.testcategories.ProofTestCategory.class)\n" + // + + // "@RunWith(NamedRunner.class)\n" + private static final String TEMPLATE_CONTENT = - "package $packageName;\n" + "\n" + "import org.junit.*;\n" + - // "import de.uka.ilkd.key.util.NamedRunner;\n" + - // "import de.uka.ilkd.key.util.TestName;\n" + - "import org.junit.rules.Timeout;\n" + "import org.junit.runner.RunWith;\n" + "\n" + - // "@org.junit.experimental.categories.Category(org.key_project.util.testcategories.ProofTestCategory.class)\n" - // + - // "@RunWith(NamedRunner.class)\n" + - "public class $className extends de.uka.ilkd.key.proof.runallproofs.ProveTest {\n" - + "\n" + " public static final String STATISTIC_FILE = \"$statisticsFile\";\n\n" - + " @Before public void setUp() {\n" + " this.baseDirectory = \"$baseDirectory\";\n" - + " this.statisticsFile = STATISTIC_FILE;\n" + " this.name = \"$name\";\n" - + " this.reloadEnabled = $reloadEnabled;\n" + " this.tempDir = \"$tempDir\";\n" - + "\n" + " this.globalSettings = \"$keySettings\";\n" - + " this.localSettings = \"$localSettings\";\n" + " }\n" + "\n" + " $timeout\n" - + "\n" + " $methods\n" + "\n" + "}\n"; + """ + /* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ + + package $packageName; + + import org.junit.jupiter.api.*; + import static org.junit.jupiter.api.Assertions.*; + + public class $className extends de.uka.ilkd.key.proof.runallproofs.ProveTest { + public static final String STATISTIC_FILE = "$statisticsFile"; + + { // initialize during construction + this.baseDirectory = "$baseDirectory"; + this.statisticsFile = STATISTIC_FILE; + this.name = "$name"; + this.reloadEnabled = $reloadEnabled; + this.tempDir = "$tempDir"; + + this.globalSettings = "$keySettings"; + this.localSettings = "$localSettings"; + } + + $timeout + $methods + } + """; /** * Generates the test classes for the given proof collection, and writes the * java files. * - * @param col - * @param unit + * @param unit a group of proof collection units * @throws IOException if the file is not writable */ - private static void createUnitClass(ProofCollection col, RunAllProofsTestUnit unit) + private static void createUnitClass(RunAllProofsTestUnit unit) throws IOException { String packageName = "de.uka.ilkd.key.proof.runallproofs.gen"; String name = unit.getTestName(); - String className = name.replaceAll("\\.java", "").replaceAll("\\.key", "") + String className = '_' + name // avoids name clashes, i.e., group "switch" + .replaceAll("\\.java", "") + .replaceAll("\\.key", "") .replaceAll("[^a-zA-Z0-9]+", "_"); ProofCollectionSettings settings = unit.getSettings(); @@ -126,7 +144,9 @@ private static void createUnitClass(ProofCollection col, RunAllProofsTestUnit un for (TestFile file : unit.getTestFiles()) { File keyFile = file.getKeYFile(); - String testName = keyFile.getName().replaceAll("\\.java", "").replaceAll("\\.key", "") + String testName = keyFile.getName() + .replaceAll("\\.java", "") + .replaceAll("\\.key", "") .replaceAll("[^a-zA-Z0-9]+", "_"); if (usedMethodNames.contains(testName)) { @@ -139,26 +159,18 @@ private static void createUnitClass(ProofCollection col, RunAllProofsTestUnit un methods.append("\n"); methods.append("@Test(").append(to).append(")") // .append("@TestName(\"").append(keyFile.getName()).append("\")") - .append("public void test").append(testName).append("() throws Exception {\n"); + .append("void test").append(testName).append("() throws Exception {\n"); // "// This tests is based on").append(keyFile.getAbsolutePath()).append("\n"); switch (file.getTestProperty()) { - case PROVABLE: - methods.append("assertProvability(\"").append(keyFile.getAbsolutePath()) - .append("\");"); - break; - case NOTPROVABLE: - methods.append("assertUnProvability(\"").append(keyFile.getAbsolutePath()) - .append("\");"); - break; - case LOADABLE: - methods.append("assertLoadability(\"").append(keyFile.getAbsolutePath()) - .append("\");"); - break; - case NOTLOADABLE: - methods.append("assertUnLoadability(\"").append(keyFile.getAbsolutePath()) - .append("\");"); - break; + case PROVABLE -> methods.append("assertProvability(\"") + .append(keyFile.getAbsolutePath()).append("\");"); + case NOTPROVABLE -> methods.append("assertUnProvability(\"") + .append(keyFile.getAbsolutePath()).append("\");"); + case LOADABLE -> methods.append("assertLoadability(\"") + .append(keyFile.getAbsolutePath()).append("\");"); + case NOTLOADABLE -> methods.append("assertUnLoadability(\"") + .append(keyFile.getAbsolutePath()).append("\");"); } methods.append("}"); } @@ -174,7 +186,7 @@ private static void createUnitClass(ProofCollection col, RunAllProofsTestUnit un m.appendTail(sb); File folder = new File(outputFolder, packageName.replace('.', '/')); folder.mkdirs(); - Files.write(Paths.get(folder.getAbsolutePath(), className + ".java"), - sb.toString().getBytes(StandardCharsets.UTF_8)); + Files.writeString(Paths.get(folder.getAbsolutePath(), className + ".java"), + sb.toString()); } } diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestUnit.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestUnit.java index 1c913abe7f1..c5d44556514 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestUnit.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestUnit.java @@ -86,29 +86,24 @@ public TestResult runTest(JunitXmlWriter xml) throws Exception { ForkMode forkMode = settings.getForkMode(); switch (forkMode) { - case PERGROUP: - testResults = ForkedTestFileRunner.processTestFiles(testFiles, getTempDir()); - break; - - case NOFORK: + case PERGROUP -> testResults = + ForkedTestFileRunner.processTestFiles(testFiles, getTempDir()); + case NOFORK -> { testResults = new ArrayList<>(); for (TestFile testFile : testFiles) { TestResult testResult = testFile.runKey(); testResults.add(testResult); } - break; - - case PERFILE: + } + case PERFILE -> { testResults = new ArrayList<>(); for (TestFile testFile : testFiles) { TestResult testResult = ForkedTestFileRunner.processTestFile(testFile, getTempDir()); testResults.add(testResult); } - break; - - default: - throw new RuntimeException("Unexpected value for fork mode: " + forkMode); + } + default -> throw new RuntimeException("Unexpected value for fork mode: " + forkMode); } if (verbose) { diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java index 7ac7351c856..6987844858d 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java @@ -59,7 +59,8 @@ public class MasterHandlerTest { * If this variable is set when running this test class, then those cases with expected result * "weak_valid" will raise an exception unless they can be proved using the solver. *

- * Otherwise a "timeout" or "unknown" is accepted. This can be used to deal with test cases that + * Otherwise, a "timeout" or "unknown" is accepted. This can be used to deal with test cases + * that * should verify but do not yet do so. *

* (Default false) @@ -106,72 +107,60 @@ public static List data() return result; } - public static class TestData { - public final String name; - public final Path path; - private final String translation; - private final LineProperties props; - - public TestData(String name, Path path, LineProperties props, String translation) { - this.name = name; - this.path = path; - this.translation = translation; - this.props = props; - } - + public record TestData(String name, Path path, LineProperties props, String translation) { @Nullable - public static TestData create(Path path) throws IOException, ProblemLoaderException { - var name = path.getFileName().toString(); - var props = new LineProperties(); - try (BufferedReader reader = Files.newBufferedReader(path)) { - props.read(reader); - } + public static TestData create(Path path) throws IOException, ProblemLoaderException { + var name = path.getFileName().toString(); + var props = new LineProperties(); + try (BufferedReader reader = Files.newBufferedReader(path)) { + props.read(reader); + } - if ("ignore".equals(props.get("state"))) { - LOGGER.info("Test case has been marked ignore"); - return null; - } + if ("ignore".equals(props.get("state"))) { + LOGGER.info("Test case has been marked ignore"); + return null; + } - List sources = props.getLines("sources"); - List lines = new ArrayList<>(props.getLines("KeY")); + List sources = props.getLines("sources"); + List lines = new ArrayList<>(props.getLines("KeY")); - if (!sources.isEmpty()) { - Path srcDir = Files.createTempDirectory("SMT_key_" + name); - Path tmpSrc = srcDir.resolve("src.java"); - Files.write(tmpSrc, sources); - lines.add(0, "\\javaSource \"" + srcDir + "\";\n"); - } + if (!sources.isEmpty()) { + Path srcDir = Files.createTempDirectory("SMT_key_" + name); + Path tmpSrc = srcDir.resolve("src.java"); + Files.write(tmpSrc, sources); + lines.add(0, "\\javaSource \"" + srcDir + "\";\n"); + } - Path tmpKey = Files.createTempFile("SMT_key_" + name, ".key"); - Files.write(tmpKey, lines); + Path tmpKey = Files.createTempFile("SMT_key_" + name, ".key"); + Files.write(tmpKey, lines); - KeYEnvironment env = KeYEnvironment.load(tmpKey.toFile()); + KeYEnvironment env = KeYEnvironment.load(tmpKey.toFile()); - Proof proof = env.getLoadedProof(); - Sequent sequent = proof.root().sequent(); + Proof proof = env.getLoadedProof(); + Sequent sequent = proof.root().sequent(); - SMTSettings settings = new DefaultSMTSettings(proof.getSettings().getSMTSettings(), - ProofIndependentSettings.DEFAULT_INSTANCE.getSMTSettings(), - proof.getSettings().getNewSMTSettings(), proof); + SMTSettings settings = new DefaultSMTSettings(proof.getSettings().getSMTSettings(), + ProofIndependentSettings.DEFAULT_INSTANCE.getSMTSettings(), + proof.getSettings().getNewSMTSettings(), proof); - String updates = props.get("smt-settings"); - if (updates != null) { - Properties map = new Properties(); - map.load(new StringReader(updates)); - settings.getNewSettings().readSettings(map); - } + String updates = props.get("smt-settings"); + if (updates != null) { + Properties map = new Properties(); + map.load(new StringReader(updates)); + settings.getNewSettings().readSettings(map); + } - ModularSMTLib2Translator translator = new ModularSMTLib2Translator(); - var translation = - translator.translateProblem(sequent, env.getServices(), settings).toString(); - return new TestData(name, path, props, translation); - } + ModularSMTLib2Translator translator = new ModularSMTLib2Translator(); + var translation = + translator.translateProblem(sequent, env.getServices(), settings).toString(); + return new TestData(name, path, props, translation); + } - @Override - public String toString() { - return name; + @Override + public String toString() { + return name; + } } - } @ParameterizedTest @MethodSource("data") @@ -180,7 +169,7 @@ public void testTranslation(TestData data) throws Exception { Path tmpSmt = Files.createTempFile("SMT_key_" + data.name, ".smt2"); // FIXME This is beyond Java 8: add as soon as switched to Java 11: // Files.writeString(tmpSmt, translation); - Files.write(tmpSmt, data.translation.getBytes(StandardCharsets.UTF_8)); + Files.writeString(tmpSmt, data.translation); LOGGER.info("SMT2 for {} saved in: {}", data.name, tmpSmt); } @@ -225,16 +214,11 @@ public void testZ3(TestData data) throws Exception { try { String lookFor = null; switch (expectation) { - case "valid": - lookFor = "unsat"; - break; - case "fail": - lookFor = "(sat|timeout)"; - break; - case "irrelevant": - break; - default: - fail("Unexpected expectation: " + expectation); + case "valid" -> lookFor = "unsat"; + case "fail" -> lookFor = "(sat|timeout)"; + case "irrelevant" -> { + } + default -> fail("Unexpected expectation: " + expectation); } if (lookFor != null) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java index f96ad58769c..72bc9e54fd0 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java @@ -805,9 +805,6 @@ public void selectedProofChanged(KeYSelectionEvent e) { public void enableWhenProofLoaded(final Action a) { a.setEnabled(getSelectedProof() != null); addKeYSelectionListener(new KeYSelectionListener() { - @Override - public void selectedNodeChanged(KeYSelectionEvent e) { - } @Override public void selectedProofChanged(KeYSelectionEvent e) { @@ -824,9 +821,6 @@ public void selectedProofChanged(KeYSelectionEvent e) { public void enableWhenProofLoaded(final javax.swing.AbstractButton a) { a.setEnabled(getSelectedProof() != null); addKeYSelectionListener(new KeYSelectionListener() { - @Override - public void selectedNodeChanged(KeYSelectionEvent e) { - } @Override public void selectedProofChanged(KeYSelectionEvent e) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java index bd2cc4cb37f..957bd2192ed 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java @@ -221,15 +221,15 @@ private void findNext() { nextOne = null; while (nextOne == null) { switch (currentPos) { - case POS_START: + case POS_START -> { currentPos = POS_LEAVES; if (selectedNode != null) { nodeIt = selectedNode.leavesIterator(); } else { nodeIt = null; } - break; - case POS_LEAVES: + } + case POS_LEAVES -> { if (nodeIt == null || !nodeIt.hasNext()) { currentPos = POS_GOAL_LIST; if (!proof.openGoals().isEmpty()) { @@ -240,16 +240,15 @@ private void findNext() { } else { nextOne = proof.getOpenGoal(nodeIt.next()); } - break; - - case POS_GOAL_LIST: + } + case POS_GOAL_LIST -> { if (goalIt == null || !goalIt.hasNext()) { // no more items return; } else { nextOne = goalIt.next(); } - break; + } } } } @@ -278,14 +277,10 @@ public void remove() { */ public void defaultSelection() { Goal g = null; - Goal firstG = null; Iterator it = new DefaultSelectionIterator(); while (g == null && it.hasNext()) { g = it.next(); - if (firstG == null) { - firstG = g; - } } /* @@ -295,11 +290,7 @@ public void defaultSelection() { if (g != null) { setSelectedGoal(g); } else { - if (firstG != null) { - setSelectedGoal(firstG); - } else { - setSelectedNode(proof.root().leavesIterator().next()); - } + setSelectedNode(proof.root().leavesIterator().next()); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/Log.java b/key.ui/src/main/java/de/uka/ilkd/key/core/Log.java index d6a624842e3..c37783fb436 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/Log.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/core/Log.java @@ -59,24 +59,12 @@ public static void configureLogging(@Nullable Integer verbosity) { var filter = new ThresholdFilter(); consoleAppender.addFilter(filter); switch (verbosity.byteValue()) { - case Verbosity.TRACE: - filter.setLevel("TRACE"); - break; - case Verbosity.DEBUG: - filter.setLevel("DEBUG"); - break; - case Verbosity.INFO: - filter.setLevel("INFO"); - break; - case Verbosity.NORMAL: - filter.setLevel("ERROR"); - break; - case Verbosity.SILENT: - filter.setLevel("OFF"); - break; - default: - filter.setLevel("WARN"); - break; + case Verbosity.TRACE -> filter.setLevel("TRACE"); + case Verbosity.DEBUG -> filter.setLevel("DEBUG"); + case Verbosity.INFO -> filter.setLevel("INFO"); + case Verbosity.NORMAL -> filter.setLevel("ERROR"); + case Verbosity.SILENT -> filter.setLevel("OFF"); + default -> filter.setLevel("WARN"); } filter.start(); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/Watchdog.java b/key.ui/src/main/java/de/uka/ilkd/key/core/Watchdog.java index b9fd8ba04ad..0439c08fd52 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/Watchdog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/core/Watchdog.java @@ -81,19 +81,13 @@ private static void run() { continue; } switch (thread.getState()) { - case NEW: - case RUNNABLE: - anyProgress = true; - break; - case WAITING: - case BLOCKED: - case TIMED_WAITING: - case TERMINATED: + case NEW, RUNNABLE -> anyProgress = true; + case WAITING, BLOCKED, TIMED_WAITING, TERMINATED -> { if (thread.getName().equals("AWT-EventQueue-0") && EventQueue.getCurrentEvent() == null) { anyProgress = true; // nothing to do } - break; + } } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java index 93971de9bbd..465e335ccaa 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java @@ -8,10 +8,12 @@ import java.awt.event.MouseAdapter; import java.awt.event.MouseEvent; import java.awt.event.MouseListener; +import java.io.Serial; import java.util.ArrayList; import java.util.EventObject; import java.util.List; import java.util.WeakHashMap; +import javax.annotation.Nonnull; import javax.swing.*; import javax.swing.event.ListDataEvent; import javax.swing.event.ListDataListener; @@ -44,9 +46,8 @@ public class GoalList extends JList implements TabPanel { public static final Icon GOAL_LIST_ICON = IconFontSwing .buildIcon(FontAwesomeSolid.FLAG_CHECKERED, MainWindow.TAB_ICON_SIZE); - /** - * - */ + + @Serial private static final long serialVersionUID = 1632264315383703798L; private final static ImageIcon keyIcon = IconFactory.keyHole(20, 20); private final static Icon disabledGoalIcon = IconFactory.keyHoleInteractive(20, 20); @@ -110,6 +111,7 @@ public void mouseReleased(MouseEvent e) { KeYGuiExtension.KeyboardShortcuts.GOAL_LIST); } + @Nonnull @Override public String getTitle() { return "Goals"; @@ -120,6 +122,7 @@ public Icon getIcon() { return GOAL_LIST_ICON; } + @Nonnull @Override public JComponent getComponent() { return new JScrollPane(this); @@ -177,11 +180,6 @@ private void unregister() { } } - public void removeNotify() { // not used? - // unregister(); - // super.removeNotify(); - } - private KeYMediator mediator() { return mediator; } @@ -236,6 +234,7 @@ private String seqToString(Sequent seq) { } private static class GoalListModel extends AbstractListModel { + @Serial private static final long serialVersionUID = 3754243473284250930L; /** * listens to the proof @@ -282,7 +281,7 @@ public boolean isAttentive() { } /** - * Sets whether this object should respond to changes in the the proof immediately. + * Sets whether this object should respond to changes in the proof immediately. */ private void setAttentive(boolean b) { if ((b != attentive) && (proof != null) && !proof.isDisposed()) { @@ -332,6 +331,7 @@ public Goal getElementAt(int i) { class GoalListProofTreeListener implements ProofTreeListener, java.io.Serializable { + @Serial private static final long serialVersionUID = 3090011700136463120L; private boolean pruningInProcess; @@ -370,7 +370,7 @@ public void proofPruned(ProofTreeEvent e) { } /** - * invoked if the list of goals changed (goals were added, removed etc. + * invoked if the list of goals changed (goals were added, removed etc.) */ public void proofGoalRemoved(ProofTreeEvent e) { if (pruningInProcess) { @@ -408,9 +408,6 @@ public void proofStructureChanged(ProofTreeEvent e) { add(e.getSource().openGoals()); } - @Override - public void notesChanged(ProofTreeEvent e) { - } } } @@ -420,10 +417,7 @@ public void notesChanged(ProofTreeEvent e) { * @author Richard Bubel */ private final class DisableSingleGoal extends DisableGoal { - - /** - * - */ + @Serial private static final long serialVersionUID = -2035187175105625072L; DisableSingleGoal() { @@ -472,10 +466,7 @@ public void actionPerformed(ActionEvent e) { * @author Richard Bubel */ private final class DisableOtherGoals extends DisableGoal { - - /** - * - */ + @Serial private static final long serialVersionUID = 4077876260098617901L; DisableOtherGoals() { @@ -535,9 +526,8 @@ public void valueChanged(ListSelectionEvent e) { } private class GoalListGUIListener implements GUIListener, java.io.Serializable { - /** - * - */ + + @Serial private static final long serialVersionUID = -1826501525753975124L; /** @@ -607,10 +597,7 @@ public void autoModeStopped(ProofEvent e) { * used to prevent the display of goals that appear closed for the present user constraint. */ private class SelectingGoalListModel extends AbstractListModel { - - /** - * - */ + @Serial private static final long serialVersionUID = 7395134147866131926L; private final GoalListModel delegate; /** @@ -661,9 +648,8 @@ protected void setProof(Proof p) { private boolean isHiddenGoal(final Goal goal) { return proof != null - && /* - * that afterwards should always be false as goals exist only for open nodes - */goal.node().isClosed(); + && // that afterwards should always be false as goals exist only for open nodes + goal.node().isClosed(); } private void setup() { @@ -766,10 +752,9 @@ public void contentsChanged(ListDataEvent e) { updateDelegateSize(); - final int changeBegin = begin; final int changeEnd = end - 1; - if (changeEnd >= changeBegin) { - fireContentsChanged(this, changeBegin, changeEnd); + if (changeEnd >= begin) { + fireContentsChanged(this, begin, changeEnd); } } @@ -794,10 +779,9 @@ public void intervalRemoved(ListDataEvent e) { updateDelegateSize(); - final int remBegin = begin; final int remEnd = begin + (oldSize - entries.size()) - 1; - if (remEnd >= remBegin) { - fireIntervalRemoved(this, remBegin, remEnd); + if (remEnd >= begin) { + fireIntervalRemoved(this, begin, remEnd); } } } @@ -805,10 +789,7 @@ public void intervalRemoved(ListDataEvent e) { } private class IconCellRenderer extends DefaultListCellRenderer implements java.io.Serializable { - - /** - * - */ + @Serial private static final long serialVersionUID = -8178991338906184819L; public IconCellRenderer() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/KeyboardTacletExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/KeyboardTacletExtension.java index a10c18b86b0..2f24be1750a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/KeyboardTacletExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/KeyboardTacletExtension.java @@ -67,11 +67,6 @@ public Collection getPanels(@Nonnull MainWindow window, public void selectedNodeChanged(KeYSelectionEvent e) { panel.setGoal(mediator.getSelectedGoal()); } - - @Override - public void selectedProofChanged(KeYSelectionEvent e) { - - } }); /* @@ -192,7 +187,7 @@ private void applyRule(RuleApp ruleApp) { TacletApp tacletApp = (TacletApp) ruleApp; ImmutableSet seq = ImmutableSet.singleton(tacletApp); pc.selectedTaclet(seq, lastGoal); - } catch (ClassCastException e) { + } catch (ClassCastException ignored) { } } else { @@ -459,17 +454,16 @@ public void addPropertyChangeListener(String propertyName, PropertyChangeListene public void processChar(char c) { switch (c) { - case '\u001B': // escape + case '\u001B' -> // escape reset(); - break; - case '\b': + case '\b' -> { if (currentPrefix.length() <= 1) { setCurrentPrefix(""); } else { setCurrentPrefix(currentPrefix.substring(0, currentPrefix.length() - 1)); } - break; - default: + } + default -> { if ('0' <= c && c <= '9') { setCurrentPos(c - '0'); } @@ -477,6 +471,7 @@ public void processChar(char c) { setCurrentPrefix(currentPrefix + c); } } + } } public int getCurrentPos() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java index 1582d72d09c..b90981570f4 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java @@ -95,8 +95,6 @@ public final class StrategySelectionView extends JPanel implements TabPanel { * Observe changes on {@link #mediator}. */ private final KeYSelectionListener mediatorListener = new KeYSelectionListener() { - public void selectedNodeChanged(KeYSelectionEvent e) { - } public void selectedProofChanged(KeYSelectionEvent e) { refresh(e.getSource().getSelectedProof()); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java index 5ca7a9175c2..e90f2a7267d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java @@ -11,7 +11,6 @@ import java.io.File; import java.io.IOException; import java.net.URI; -import java.nio.charset.StandardCharsets; import java.nio.file.Files; import java.nio.file.Paths; import java.util.Optional; @@ -240,7 +239,7 @@ private JPanel createButtonPanel(final URI sourceURI, final JTextPane textPane, // workaround for #1641: replace "\n" with system dependent line separators when // saving String text = textPane.getText().replace("\n", System.lineSeparator()); - Files.write(sourceFile.toPath(), text.getBytes(StandardCharsets.UTF_8)); + Files.writeString(sourceFile.toPath(), text); } catch (IOException ioe) { String message = "Cannot write to file:\n" + ioe.getMessage(); JOptionPane.showMessageDialog(parent, message); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveBundleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveBundleAction.java index 7678105608f..871225b47fa 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveBundleAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveBundleAction.java @@ -41,8 +41,6 @@ public SaveBundleAction(MainWindow mainWindow) { // react to changes of proof selection mainWindow.getMediator().addKeYSelectionListener(new KeYSelectionListener() { - @Override - public void selectedNodeChanged(KeYSelectionEvent e) {} @Override public void selectedProofChanged(KeYSelectionEvent e) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java index f867c0a5a7d..6dae2505c25 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java @@ -117,15 +117,12 @@ public String getColumnName(int column) { @Override public Object getValueAt(int rowIndex, int columnIndex) { - switch (columnIndex) { - case 0: - return colorData.get(rowIndex).property.getKey(); - case 1: - return colorData.get(rowIndex).property.getDescription(); - case 2: - return colorData.get(rowIndex).color; - } - return ""; + return switch (columnIndex) { + case 0 -> colorData.get(rowIndex).property.getKey(); + case 1 -> colorData.get(rowIndex).property.getDescription(); + case 2 -> colorData.get(rowIndex).color; + default -> ""; + }; } @Override diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/ExtensionManager.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/ExtensionManager.java index e7d1f7d4b55..1b709394453 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/ExtensionManager.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/ExtensionManager.java @@ -26,9 +26,8 @@ * @version 1 (08.04.19) */ public class ExtensionManager extends SettingsPanel implements SettingsProvider { - private static final long serialVersionUID = 6682677093231975786L; private static final ExtensionSettings EXTENSION_SETTINGS = new ExtensionSettings(); - private HashMap map; + private HashMap> map; private String keywords = ""; public ExtensionManager() { @@ -91,7 +90,7 @@ private void refresh() { }); } - private String getSupportLabel(Extension it) { + private String getSupportLabel(Extension it) { return "Provides: " + (it.supportsContextMenu() ? "ContextMenu " : "") + (it.supportsLeftPanel() ? "LeftPanel " : "") + (it.supportsMainMenu() ? "MainMenu " : "") diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/ContextMenuAdapter.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/ContextMenuAdapter.java index 84d4cbb6071..845879559c4 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/ContextMenuAdapter.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/ContextMenuAdapter.java @@ -5,6 +5,7 @@ import java.util.Collections; import java.util.List; +import javax.annotation.Nonnull; import javax.swing.*; import de.uka.ilkd.key.core.KeYMediator; @@ -18,21 +19,17 @@ * @version 1 (16.04.19) */ public abstract class ContextMenuAdapter implements KeYGuiExtension.ContextMenu { + @Nonnull @Override - public final List getContextActions(KeYMediator mediator, ContextMenuKind kind, - Object underlyingObject) { - switch ((DefaultContextMenuKind) kind) { - case PROOF_LIST: - return getContextActions(mediator, kind, (Proof) underlyingObject); - case PROOF_TREE: - return getContextActions(mediator, kind, (Node) underlyingObject); - case TACLET_INFO: - return getContextActions(mediator, kind, (Rule) underlyingObject); - case SEQUENT_VIEW: - return getContextActions(mediator, kind, (PosInSequent) underlyingObject); - default: - throw new IllegalArgumentException("unexpected kind"); - } + public final List getContextActions(@Nonnull KeYMediator mediator, + @Nonnull ContextMenuKind kind, + @Nonnull Object underlyingObject) { + return switch ((DefaultContextMenuKind) kind) { + case PROOF_LIST -> getContextActions(mediator, kind, (Proof) underlyingObject); + case PROOF_TREE -> getContextActions(mediator, kind, (Node) underlyingObject); + case TACLET_INFO -> getContextActions(mediator, kind, (Rule) underlyingObject); + case SEQUENT_VIEW -> getContextActions(mediator, kind, (PosInSequent) underlyingObject); + }; } public List getContextActions(KeYMediator mediator, ContextMenuKind kind, diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/ExtensionSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/ExtensionSettings.java index b30186412f1..47227814fe8 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/ExtensionSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/ExtensionSettings.java @@ -27,7 +27,7 @@ public PropertyEntry> forbiddenClasses() { } - public void setForbiddenClass(Class type, boolean activated) { + public void setForbiddenClass(Class type, boolean activated) { String text = type.getName(); Collection classes = getForbiddenClasses(); if (activated) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/ShortcutSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/ShortcutSettings.java index 55f500be85c..1dc26a2ab93 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/ShortcutSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/ShortcutSettings.java @@ -5,6 +5,7 @@ import java.awt.event.KeyAdapter; import java.awt.event.KeyEvent; +import java.io.Serial; import java.util.ArrayList; import java.util.List; import java.util.Properties; @@ -24,6 +25,7 @@ * @version 1 (09.05.19) */ public class ShortcutSettings extends SimpleSettingsPanel implements SettingsProvider { + @Serial private static final long serialVersionUID = -7609149706562761596L; private final JTable tblShortcuts = new JTable(); private ShortcutsTableModel modelShortcuts; @@ -147,6 +149,7 @@ public void applySettings(MainWindow window) { } private static class ShortcutsTableModel extends AbstractTableModel { + @Serial private static final long serialVersionUID = -2854179933936417703L; private static final String[] COLUMNS = new String[] { "Name", "Description", "Shortcut" }; private final List actionName; @@ -178,20 +181,23 @@ public String getColumnName(int column) { @Override public Object getValueAt(int rowIndex, int columnIndex) { switch (columnIndex) { - case 0: + case 0 -> { return actionName.get(rowIndex) // remove common package prefixes .replaceAll("([a-z]\\w*\\.)*", ""); - case 1: + } + case 1 -> { Action a = actions.get(rowIndex); if (a == null) { return ""; } Object val = a.getValue(Action.SHORT_DESCRIPTION); return val != null ? val.toString() : ""; - case 2: + } + case 2 -> { return shortcut.get(rowIndex); } + } return ""; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java index 871a2ad2d3d..cf21eccce45 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java @@ -5,6 +5,7 @@ import java.awt.*; import java.awt.event.ActionEvent; +import java.io.Serial; import java.util.ArrayList; import java.util.Collection; import java.util.Comparator; @@ -55,10 +56,11 @@ /** * The menu shown by a {@link CurrentGoalViewListener} when the user clicks on a * {@link CurrentGoalView}, i.e. when the user clicks on the sequent. - * + *

* Shows all {@link Taclet}s that are applicable at a selected position. */ public final class CurrentGoalViewMenu extends SequentViewMenu { + @Serial private static final long serialVersionUID = 8151230546928796116L; private static final String INTRODUCE_AXIOM_TACLET_NAME = "introduceAxiom"; @@ -537,23 +539,19 @@ public void actionPerformed(ActionEvent e) { PosInOccurrence occ = getPos().getPosInOccurrence(); switch (((JMenuItem) e.getSource()).getText()) { - case DISABLE_ABBREVIATION: + case DISABLE_ABBREVIATION -> { if (occ != null && occ.posInTerm() != null) { mediator.getNotationInfo().getAbbrevMap().setEnabled(occ.subTerm(), false); getSequentView().printSequent(); } - - break; - - case ENABLE_ABBREVIATION: + } + case ENABLE_ABBREVIATION -> { if (occ != null && occ.posInTerm() != null) { mediator.getNotationInfo().getAbbrevMap().setEnabled(occ.subTerm(), true); getSequentView().printSequent(); } - - break; - - case CREATE_ABBREVIATION: + } + case CREATE_ABBREVIATION -> { if (occ != null && occ.posInTerm() != null) { // trim string, otherwise window gets too large (bug #1430) final String oldTerm = occ.subTerm().toString(); @@ -580,10 +578,8 @@ public void actionPerformed(ActionEvent e) { JOptionPane.INFORMATION_MESSAGE); } } - - break; - - case CHANGE_ABBREVIATION: + } + case CHANGE_ABBREVIATION -> { if (occ != null && occ.posInTerm() != null) { String abbreviation = (String) JOptionPane.showInputDialog(new JFrame(), "Enter abbreviation for term: \n" + occ.subTerm().toString(), @@ -608,11 +604,8 @@ public void actionPerformed(ActionEvent e) { JOptionPane.INFORMATION_MESSAGE); } } - - break; - - default: - super.actionPerformed(e); + } + default -> super.actionPerformed(e); } } } @@ -621,9 +614,8 @@ public void actionPerformed(ActionEvent e) { static class FocussedRuleApplicationMenuItem extends JMenuItem { private static final String APPLY_RULES_AUTOMATICALLY_HERE = "Apply rules automatically here"; - /** - * - */ + + @Serial private static final long serialVersionUID = -6486650015103963268L; public FocussedRuleApplicationMenuItem() { @@ -732,7 +724,7 @@ public LinkedHashMap score(TacletApp o1) { final Taclet taclet1 = o1.taclet(); - map.put("closing", taclet1.goalTemplates().size() == 0 ? -1 : 1); + map.put("closing", taclet1.goalTemplates().isEmpty() ? -1 : 1); boolean calc = false; for (RuleSet rs : taclet1.getRuleSets()) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DefaultTacletMenuItem.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DefaultTacletMenuItem.java index 9b0bc588f3c..0c406e6241f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DefaultTacletMenuItem.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DefaultTacletMenuItem.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.nodeviews; +import java.io.Serial; import javax.swing.*; import de.uka.ilkd.key.gui.MainWindow; @@ -22,10 +23,7 @@ * easier access to the Taclet if the item has been selected */ class DefaultTacletMenuItem extends JMenuItem implements TacletMenuItem { - - /** - * - */ + @Serial private static final long serialVersionUID = -5537139155045230424L; private final TacletApp connectedTo; @@ -114,20 +112,11 @@ protected static StringBuilder ascii2html(String sb) { int sbl = asb.length(); for (int i = 0; i < sbl; i++) { switch (asb.charAt(i)) { - case '<': - nsb.append("<"); - break; - case '>': - nsb.append(">"); - break; - case '&': - nsb.append("&"); - break; - case '\n': - nsb.append("
"); - break; - default: - nsb.append(asb.charAt(i)); + case '<' -> nsb.append("<"); + case '>' -> nsb.append(">"); + case '&' -> nsb.append("&"); + case '\n' -> nsb.append("
"); + default -> nsb.append(asb.charAt(i)); } } return nsb; @@ -141,11 +130,6 @@ private static String removeEmptyLines(String string) { return string.replaceAll("(?m)^[ \t]*\r?\n|\n$", ""); } - /* - * (non-Javadoc) - * - * @see de.uka.ilkd.key.gui.TacletMenuItem#connectedTo() - */ @Override public TacletApp connectedTo() { return connectedTo; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewSearchBar.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewSearchBar.java index aec9d295d2a..91149a652f7 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewSearchBar.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewSearchBar.java @@ -5,8 +5,10 @@ import java.awt.*; import java.awt.event.ItemEvent; +import java.io.Serial; import java.util.ArrayList; import java.util.List; +import java.util.Objects; import java.util.regex.Matcher; import java.util.regex.Pattern; import javax.annotation.Nonnull; @@ -25,7 +27,7 @@ */ public class SequentViewSearchBar extends SearchBar { - + @Serial private static final long serialVersionUID = 9102464983776181771L; public static final ColorSettings.ColorProperty SEARCH_HIGHLIGHT_COLOR_1 = ColorSettings.define("[sequentSearchBar]highlight_1", "", new Color(0, 140, 255, 178)); @@ -100,24 +102,22 @@ public void createUI() { searchModeBox.addItemListener(e -> { if (e.getStateChange() == ItemEvent.SELECTED) { // search always does a repaint, therefore don't force update in setFilter - switch ((SearchMode) searchModeBox.getSelectedItem()) { - case HIDE: + switch ((SearchMode) Objects.requireNonNull(searchModeBox.getSelectedItem())) { + case HIDE -> { sequentView.setFilter(new HideSequentPrintFilter( sequentView.getLogicPrinter(), regExpCheckBox.isSelected()), false); search(); - break; - case REGROUP: + } + case REGROUP -> { sequentView.setFilter(new RegroupSequentPrintFilter( sequentView.getLogicPrinter(), regExpCheckBox.isSelected()), false); search(); - break; - case HIGHLIGHT: + } + case HIGHLIGHT -> { sequentView.setFilter(new IdentitySequentPrintFilter(), false); search(); - break; - default: - sequentView.setFilter(new IdentitySequentPrintFilter(), true); - break; + } + default -> sequentView.setFilter(new IdentitySequentPrintFilter(), true); } } }); @@ -178,7 +178,7 @@ public boolean search(@Nonnull String search) { sequentView.printSequent(); - if (sequentView == null || sequentView.getText() == null || search.equals("") + if (sequentView == null || sequentView.getText() == null || search.isEmpty() || !this.isVisible()) { return true; } @@ -198,17 +198,17 @@ public boolean search(@Nonnull String search) { return false; } - Matcher m = p.matcher(sequentView.getText().replace("\u00A0", "\u0020")); + Matcher m = p.matcher(sequentView.getText().replace("\u00A0", " ")); - boolean loopEnterd = false; + boolean loopEntered = false; while (m.find()) { int foundAt = m.start(); Object highlight = sequentView.getColorHighlight(SEARCH_HIGHLIGHT_COLOR_2.get()); searchResults.add(new Pair<>(foundAt, highlight)); sequentView.paintHighlight(new Range(foundAt, m.end()), highlight); - loopEnterd = true; + loopEntered = true; } - return loopEnterd; + return loopEntered; } /** @@ -219,7 +219,7 @@ public boolean search(@Nonnull String search) { public void searchFor(String searchTerm) { if (regExpCheckBox.isSelected()) { // https://stackoverflow.com/questions/60160/how-to-escape-text-for-regular-expression-in-java - String escaped = searchTerm.replaceAll("[-\\[\\]{}()*+?.,\\\\\\\\^$|#\\\\s]", "\\\\$0"); + String escaped = searchTerm.replaceAll("[-\\[\\]{}()*+?.,\\\\^$|#s]", "\\\\$0"); searchField.setText(escaped); } else { searchField.setText(searchTerm); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java index 27fc959e3f4..645a539f746 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java @@ -76,14 +76,11 @@ public int getColumnCount() { @Override public String getColumnName(int column) { - switch (column) { - case 0: - return "Goal"; - case 1: - return "Reference"; - default: - return "??"; - } + return switch (column) { + case 0 -> "Goal"; + case 1 -> "Reference"; + default -> "??"; + }; } @Override diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDiffFrame.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDiffFrame.java index 21aacdbdfee..83b0971547e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDiffFrame.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDiffFrame.java @@ -19,7 +19,7 @@ /** * Proof-of-concept implementation of a textual sequent comparison. - * + *

* This class provides a frame which allows the user to display a in-place comparison of two * sequents. The comparison happens on the pretty-printed text only, no sophisticated tree * comparison. The algorithm is taken from a google library. @@ -29,15 +29,10 @@ */ public class ProofDiffFrame extends JFrame { - - private static final long serialVersionUID = -1593379776744771923L; - /** * The action to show a new frame of this class. Is used in {@link MainWindow}. */ public static class Action extends MainWindowAction { - - private static final long serialVersionUID = -1745515272350810787L; private final MainWindow mainWindow; public Action(MainWindow mainWindow) { @@ -166,7 +161,7 @@ private void setSelectedNode() { /** * Initiate a diff calculation and set the content of the text area. - * + *

* It uses the result of {@link diff_match_patch#diff_main(String, String, boolean)} and html * markup to show the text. */ @@ -177,7 +172,7 @@ private void showDiff() { try { int toNo; String toText = to.getText(); - if (toText.length() == 0) { + if (toText.isEmpty()) { throw new IllegalArgumentException( "At least the second proof node must be specified"); } else { @@ -186,7 +181,7 @@ private void showDiff() { } String fromText = from.getText(); - if (fromText.length() == 0) { + if (fromText.isEmpty()) { sFrom = getProofNodeText(getParent(toNo)); } else { int fromNo = Integer.parseInt(fromText); @@ -209,25 +204,23 @@ private void showDiff() { sb.append("

");
         for (Diff diff : diffs) {
             switch (diff.operation) {
-            case EQUAL:
-                sb.append(toHtml(diff.text));
-                break;
-            case DELETE:
+            case EQUAL -> sb.append(toHtml(diff.text));
+            case DELETE -> {
                 if (onlySpaces(diff.text)) {
                     sb.append(diff.text);
                 } else {
                     sb.append("").append(toHtml(diff.text))
                             .append("");
                 }
-                break;
-            case INSERT:
+            }
+            case INSERT -> {
                 if (onlySpaces(diff.text)) {
                     sb.append(diff.text);
                 } else {
                     sb.append("").append(toHtml(diff.text))
                             .append("");
                 }
-                break;
+            }
             }
         }
         sb.append("
"); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java index 13a8bb0d6eb..7ce51ee87d4 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java @@ -214,7 +214,7 @@ private JButton getStopButton() { public void setModus(Modus m) { modus = m; switch (modus) { - case SOLVERS_DONE: + case SOLVERS_DONE -> { stopButton.setText("Discard"); if (applyButton != null) { applyButton.setEnabled(true); @@ -222,14 +222,13 @@ public void setModus(Modus m) { if (focusButton != null) { focusButton.setEnabled(true); } - break; - case SOLVERS_RUNNING: + } + case SOLVERS_RUNNING -> { stopButton.setText("Stop"); if (applyButton != null) { applyButton.setEnabled(false); } - break; - + } } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/SolverListener.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/SolverListener.java index 2da795d3a1d..7dc063f6bc3 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/SolverListener.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/SolverListener.java @@ -379,19 +379,20 @@ private float calculateRemainingTime(InternSMTProblem problem) { private boolean refreshProgessOfProblem(InternSMTProblem problem) { SolverState state = problem.solver.getState(); - switch (state) { - case Running: - running(problem); - return true; - case Stopped: - stopped(problem); - return false; - case Waiting: - waiting(problem); - return true; - - } - return true; + return switch (state) { + case Running -> { + running(problem); + yield true; + } + case Stopped -> { + stopped(problem); + yield false; + } + case Waiting -> { + waiting(problem); + yield true; + } + }; } @@ -456,24 +457,17 @@ private void interrupted(InternSMTProblem problem) { int x = problem.getSolverIndex(); int y = problem.getProblemIndex(); switch (reason) { - case Exception: + case Exception -> { progressModel.setProgress(0, x, y); progressModel.setTextColor(RED.get(), x, y); progressModel.setText("Exception!", x, y); - - - break; - case NoInterruption: - throw new RuntimeException("This position should not be reachable!"); - - case Timeout: + } + case NoInterruption -> throw new RuntimeException("This position should not be reachable!"); + case Timeout -> { progressModel.setProgress(0, x, y); progressModel.setText("Timeout.", x, y); - - break; - case User: - progressModel.setText("Interrupted by user.", x, y); - break; + } + case User -> progressModel.setText("Interrupted by user.", x, y); } } @@ -580,11 +574,12 @@ private String finalizePath(String path, SMTSolver solver, Goal goal) { public static String computeSolverTypeWarningMessage(SolverType type) { - String message = "You are using a version of " + type.getName() - + " which has not been tested for this version of KeY.\nIt can therefore be that" - + " errors occur that would not occur\nusing the following version or higher:\n" + - type.getMinimumSupportedVersion(); - return message; + return (""" + You are using a version of %s which has not been tested for this version of KeY. + It can therefore be that errors occur that would not occur + using the following version or higher: + %s""") + .formatted(type.getName(), type.getMinimumSupportedVersion()); } private class ProgressDialogListenerImpl implements ProgressDialogListener { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java index 4b7abca4070..81dda805d8e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java @@ -7,7 +7,6 @@ import java.util.ArrayList; import java.util.Collection; import java.util.List; -import java.util.ResourceBundle; import javax.swing.*; import de.uka.ilkd.key.core.Main; @@ -28,22 +27,79 @@ * @version 1 (08.04.19) */ public class SMTSettingsProvider extends SettingsPanel implements SettingsProvider { - // de/uka/ilkd/key/gui/smt/settings/messages.xml - public static final ResourceBundle BUNDLE = - ResourceBundle.getBundle("de.uka.ilkd.key.gui.smt.settings.messages"); - - public static final String PROGRESS_MODE_USER = "PROGRESS_MODE_USER"; - public static final String PROGRESS_MODE_CLOSE = "PROGRESS_MODE_CLOSE"; - public static final String PROGRESS_MODE_CLOSE_FIRST = "PROGRESS_MODE_CLOSE_FIRST"; - private static final String INFO_BOUND = "infoBound"; - private static final String INFO_SAVE_TO_FILE_PANEL = "infoSaveToFilePanel"; - private static final String INFO_PROGRESS_MODE_BOX = "infoProgressModeBox"; - private static final String INFO_CHECK_FOR_SUPPORT = "infoCheckForSupport"; - private static final String INFO_MAX_PROCESSES = "infoMaxProcesses"; - private static final String INFO_TIMEOUT_FIELD = "infoTimeoutField"; + public static final String PROGRESS_MODE_USER = + "Progress dialog remains open after executing solvers"; + public static final String PROGRESS_MODE_CLOSE = + "Close progress dialog after all solvers have finished"; + public static final String PROGRESS_MODE_CLOSE_FIRST = + "Close progress dialog after the first solver has finished"; + public static final String INFO_BOUND = + "Bitvector size for this type. Use a value larger than 0."; + public static final String INFO_SAVE_TO_FILE_PANEL = + """ + Activate this option to store the translations that are handed over to the externals solvers: + 1. Choose the folder. + 2. Specify the filename: + %s: the solver's name + %d: date + %t: time + %i: the goal's number + Example: /home/translations/%d_%t_%i_%s.txt" + Remark: After every restart of KeY this option\ + is deactivated."""; - private final JTextField saveToFilePanel; + public static final String INFO_SOLVER_NAME = + """ + There are two ways to make supported provers applicable for KeY: + 1. Specify the absolute path of the prover in the field 'Command'. + 2. Change the environment variable $PATH of your system, so that it + refers to the installed prover. In that case you must specify the name of the solver in 'Command'"""; + public static final String INFO_PROGRESS_MODE_BOX = + """ + 1. Option: The progress dialog remains open after executing the solvers so that the user\ + can decide whether he wants to accept the results. + 2. Option: The progress dialog is closed once the external provers have done their work or the time limit\ + has been exceeded."""; + public static final String INFO_CHECK_FOR_SUPPORT = + """ + If this option is activated, each time before a solver is started\ + it is checked whether the version of that solver is supported. If the version is not supported, a warning is\ + presented in the progress dialog."""; + public static final String INFO_MAX_PROCESSES = + "Maximal number or processes that are allowed to run concurrently"; + public static final String INFO_TIMEOUT_FIELD = + """ + Timeout for the external solvers in seconds. Fractions of a second are allowed. Example: 6.5 + """; + public static final String INFO_SOLVER_COMMAND = """ + The command for the solver. + + Either you specify the absolute path of your solver or just the command for starting it. + In the latter case you have to modify the PATH-variable of your system. + Please note that you also have to specify the filename extension. + For example: z3.exe"""; + + public static final String INFO_SOLVER_PARAMETERS = + """ + In this field you can specify which parameters are passed to the \ + solver when the solver is started. Note that the default parameters are crucial for a stable run of the\ + solver."""; + + public static final String INFO_SOLVER_SUPPORT = + """ + For the KeY system only some particular versions of this solver + have been tested. It is highly recommended to use those versions, because otherwise it is not guaranteed that + the connection to this solver is stable. + If you want to check whether the installed solver is supported, please click on the button below."""; + public static final String SOLVER_SUPPORTED = "Version of solver is supported."; + public static final String SOLVER_MAY_SUPPORTED = "Version of solver may not be supported."; + public static final String SOLVER_UNSUPPORTED = "Support has not been checked, yet."; + public static final String INFO_SOLVER_TIMEOUT = + "Overrides timeout for this solver. Values in seconds. If value <= 0, global timeout is used."; + public static final String INFO_SOLVER_INFO = "Information about this solver."; + + private final JTextField saveToFilePanel; private final JComboBox progressModeBox; private final JSpinner maxProcesses; private final JSpinner timeoutField; @@ -121,12 +177,12 @@ public void applySettings(MainWindow window) { private JSpinner createLocSetBoundField() { return addNumberField("Locset bound:", 0L, (long) Integer.MAX_VALUE, 1, - BUNDLE.getString(INFO_BOUND), e -> settings.setLocsetBound(e.longValue())); + INFO_BOUND, e -> settings.setLocsetBound(e.longValue())); } private JSpinner createMaxProcesses() { return addNumberField("Concurrent processes:", 0, Integer.MAX_VALUE, 1, - BUNDLE.getString(INFO_MAX_PROCESSES), + INFO_MAX_PROCESSES, e -> settings.setMaxConcurrentProcesses(e.intValue())); } @@ -134,7 +190,7 @@ private JSpinner createTimeoutField() { // Use doubles so that the formatter doesn't make every entered String into integers. // [see NumberFormatter#stringToValue()]. JSpinner timeoutSpinner = addNumberField("Timeout:", 0.0, (double) Long.MAX_VALUE, 1, - BUNDLE.getString(INFO_TIMEOUT_FIELD), + INFO_TIMEOUT_FIELD, e -> settings.setTimeout((long) Math.floor(e.doubleValue() * 1000))); // Set the editor so that entered Strings only have three decimal places. JSpinner.NumberEditor editor = new JSpinner.NumberEditor(timeoutSpinner, "#.###"); @@ -146,21 +202,21 @@ private JSpinner createTimeoutField() { private JSpinner createIntBoundField() { return addNumberField("Integer bound:", 0L, (long) Integer.MAX_VALUE, 1, - BUNDLE.getString(INFO_BOUND), e -> settings.setIntBound(e.longValue())); + INFO_BOUND, e -> settings.setIntBound(e.longValue())); } private JSpinner createSeqBoundField() { return addNumberField("Seq bound:", 0L, (long) Integer.MAX_VALUE, 1, - BUNDLE.getString(INFO_BOUND), e -> settings.setSeqBound(e.longValue())); + INFO_BOUND, e -> settings.setSeqBound(e.longValue())); } private JSpinner createObjectBoundField() { return addNumberField("Object bound:", 0L, (long) Integer.MAX_VALUE, 1, - BUNDLE.getString(INFO_BOUND), e -> settings.setObjectBound(e.longValue())); + INFO_BOUND, e -> settings.setObjectBound(e.longValue())); } private JComboBox getProgressModeBox() { - return addComboBox("", BUNDLE.getString(INFO_PROGRESS_MODE_BOX), 0, + return addComboBox("", INFO_PROGRESS_MODE_BOX, 0, e -> settings.setModeOfProgressDialog( ProgressMode.values()[progressModeBox.getSelectedIndex()]), getProgressMode(ProgressMode.USER), getProgressMode(ProgressMode.CLOSE)); @@ -168,7 +224,7 @@ private JComboBox getProgressModeBox() { private JCheckBox createSolverSupportCheck() { return addCheckBox("Check for support when a solver is started", - BUNDLE.getString(INFO_CHECK_FOR_SUPPORT), false, + INFO_CHECK_FOR_SUPPORT, false, e -> settings.setCheckForSupport(solverSupportCheck.isSelected())); } @@ -180,20 +236,16 @@ private JCheckBox createEnableOnLoad() { private JTextField getSaveToFilePanel() { return addFileChooserPanel("Store translation to file:", "", - BUNDLE.getString(INFO_SAVE_TO_FILE_PANEL), true, + INFO_SAVE_TO_FILE_PANEL, true, e -> settings.setPathForSMTTranslation(saveToFilePanel.getText())); } private String getProgressMode(ProgressMode index) { - switch (index) { - case USER: - return BUNDLE.getString(PROGRESS_MODE_USER); - case CLOSE: - return BUNDLE.getString(PROGRESS_MODE_CLOSE); - case CLOSE_FIRST: - return BUNDLE.getString(PROGRESS_MODE_CLOSE_FIRST); - } - return ""; + return switch (index) { + case USER -> PROGRESS_MODE_USER; + case CLOSE -> PROGRESS_MODE_CLOSE; + case CLOSE_FIRST -> PROGRESS_MODE_CLOSE_FIRST; + }; } public void setSmtSettings(ProofIndependentSMTSettings settings) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SolverOptions.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SolverOptions.java index e65252b3c60..baea011a54d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SolverOptions.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SolverOptions.java @@ -13,22 +13,13 @@ import de.uka.ilkd.key.settings.ProofIndependentSMTSettings; import de.uka.ilkd.key.smt.solvertypes.SolverType; -import static de.uka.ilkd.key.gui.smt.settings.SMTSettingsProvider.BUNDLE; - /** * @author Alexander Weigl * @version 1 (08.04.19) */ class SolverOptions extends SettingsPanel implements SettingsProvider { - private static final String INFO_SOLVER_NAME = "infoSolverName"; - private static final String INFO_SOLVER_PARAMETERS = "infoSolverParameters"; - private static final String INFO_SOLVER_COMMAND = "infoSolverCommand"; - private static final String INFO_SOLVER_SUPPORT = "infoSolverSupport"; - private static final String INFO_SOLVER_INFO = "SOLVER_INFO"; - private static final String[] SOLVER_SUPPORT_TEXT = { BUNDLE.getString("SOLVER_SUPPORTED"), - BUNDLE.getString("SOLVER_MAY_SUPPORTED"), BUNDLE.getString("SOLVER_UNSUPPORTED") }; - private static final String INFO_SOLVER_TIMEOUT = "SOLVER_TIMEOUT"; - + private static final String[] SOLVER_SUPPORT_TEXT = { SMTSettingsProvider.SOLVER_SUPPORTED, + SMTSettingsProvider.SOLVER_MAY_SUPPORTED, SMTSettingsProvider.SOLVER_UNSUPPORTED }; private static final int SOLVER_SUPPORTED = 0; private static final int SOLVER_NOT_SUPPOTED = 1; @@ -58,12 +49,7 @@ public SolverOptions(SolverType solverType) { } private static String versionInfo(String info, String versionString) { - String builder = info + - " " + - "(" + - versionString + - ")"; - return builder; + return info + " " + "(" + versionString + ")"; } protected JButton createDefaultButton() { @@ -90,9 +76,9 @@ private String getSolverSupportText() { private JTextArea createSolverInformation() { String info = solverType.getInfo(); - if (info != null && !info.equals("")) { + if (info != null && !info.isEmpty()) { JTextArea solverInfo = - addTextAreaWithoutScroll("Info", info, BUNDLE.getString(INFO_SOLVER_INFO), null); + addTextAreaWithoutScroll("Info", info, SMTSettingsProvider.INFO_SOLVER_INFO, null); solverInfo.setLineWrap(true); solverInfo.setWrapStyleWord(true); solverInfo.setEditable(false); @@ -111,7 +97,8 @@ private JTextArea createSolverInformation() { protected JTextField createSolverSupported() { JTextField txt = addTextField("Support", getSolverSupportText(), - BUNDLE.getString(INFO_SOLVER_SUPPORT) + createSupportedVersionText(), emptyValidator()); + SMTSettingsProvider.INFO_SOLVER_SUPPORT + createSupportedVersionText(), + emptyValidator()); txt.setEditable(false); return txt; } @@ -126,7 +113,7 @@ private JSpinner createSolverTimeout() { // Use floor rounding to be consistent with the value that will be set for the timeout. editor.getFormat().setRoundingMode(RoundingMode.FLOOR); jsp.setEditor(editor); - addTitledComponent("Timeout", jsp, BUNDLE.getString(INFO_SOLVER_TIMEOUT)); + addTitledComponent("Timeout", jsp, SMTSettingsProvider.INFO_SOLVER_TIMEOUT); return jsp; } @@ -143,13 +130,13 @@ protected JButton createCheckSupportButton() { protected JTextField createSolverParameters() { return addTextField("Parameters", solverType.getSolverParameters(), - BUNDLE.getString(INFO_SOLVER_PARAMETERS), e -> { + SMTSettingsProvider.INFO_SOLVER_PARAMETERS, e -> { }); } public JTextField createSolverCommand() { return addTextField("Command", solverType.getSolverCommand(), - BUNDLE.getString(INFO_SOLVER_COMMAND), e -> { + SMTSettingsProvider.INFO_SOLVER_COMMAND, e -> { }); } @@ -178,7 +165,7 @@ protected JTextField createSolverInstalled() { protected JTextField createSolverName() { JTextField txt = addTextField("Name", solverType.getName(), - BUNDLE.getString(INFO_SOLVER_NAME), emptyValidator()); + SMTSettingsProvider.INFO_SOLVER_NAME, emptyValidator()); txt.setEditable(false); return txt; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java index f8a45d9613c..2eb275be4c5 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java @@ -5,6 +5,7 @@ import java.awt.Color; import java.beans.PropertyChangeListener; +import java.io.Serial; import java.util.*; import java.util.regex.Pattern; import javax.swing.text.*; @@ -16,15 +17,16 @@ /** * This document performs syntax highlighting when strings are inserted. However, only inserting the * whole String at once is supported, otherwise the syntax highlighting will be faulty. - * + *

* Note that tab characters have to be replaced by spaces before inserting into the document. - * + *

* The document currently only works when newlines are represented by "\n"! * * @author Wolfram Pfeifer */ public class JavaDocument extends DefaultStyledDocument { + @Serial private static final long serialVersionUID = -1856296532743892931L; // highlighting colors (same as in HTMLSyntaxHighlighter of SequentView for consistency) @@ -56,7 +58,7 @@ public class JavaDocument extends DefaultStyledDocument { * COMMENT (/* ... */), JML (/*@ ... */ ), ... */ private enum Mode { - /** parser is currently inside a String */ + /* parser is currently inside a String */ // STRING, // currently not in use /** parser is currently inside normal java code */ NORMAL, @@ -125,7 +127,7 @@ private enum CommentState { * Stores the Java keywords which have to be highlighted. The list is taken from * * https://docs.oracle.com/javase/tutorial/java/nutsandbolts/_keywords.html . - * + *

* To add additional keywords, simply add them to the array. Note that the keywords must not * contain any of the characters defined by the DELIM regex. */ @@ -140,7 +142,7 @@ private enum CommentState { /** * Stores the JML keywords which have to be highlighted. - * + *

* To add additional keywords, simply add them to the array. Note that the keywords must not * contain any of the characters defined by the DELIM regex. */ @@ -200,7 +202,7 @@ private enum CommentState { /** the style of annotations */ private final SimpleAttributeSet annotation = new SimpleAttributeSet(); - /** the style of strings */ + /* the style of strings */ // private SimpleAttributeSet string = new SimpleAttributeSet(); /** default style */ @@ -441,61 +443,26 @@ private void checkDelimiter(char c) { private void processChar(char strChar) throws BadLocationException { switch (strChar) { - case ('@'): - checkAt(); - break; - case '\n': - checkLinefeed(); - break; - case '\t': // all tabs should have been replaced earlier! - case ' ': - checkSpaceTab(strChar); - break; - case '*': - checkStar(); - break; - case '/': - checkSlash(); - break; - case '"': - checkQuote(); - break; + case ('@') -> checkAt(); + case '\n' -> checkLinefeed(); + // all tabs should have been replaced earlier! + case '\t', ' ' -> checkSpaceTab(strChar); + case '*' -> checkStar(); + case '/' -> checkSlash(); + case '"' -> checkQuote(); + // keyword delimiters: +-*/(){}[]%!^~.;?:&|<>="'\n(space) - case '+': - case '-': - checkPlusMinus(strChar); - break; + case '+', '-' -> checkPlusMinus(strChar); + // case '*': // case '/': - case '(': - case ')': - case '[': - case ']': - case '{': - case '}': - case '%': - case '!': - case '^': - case '~': - case '&': - case '|': - case '.': - case ':': - case ';': - case '?': - case '<': - case '>': - case '=': - case '\'': + case '(', ')', '[', ']', '{', '}', '%', '!', '^', '~', '&', '|', '.', ':', ';', '?', '<', '>', '=', '\'' -> // case ' ': // case '"': // case '\'': // case '\n': checkDelimiter(strChar); - break; - default: - checkOther(strChar); - break; + default -> checkOther(strChar); } } diff --git a/key.ui/src/main/resources/de/uka/ilkd/key/gui/smt/settings/messages.properties b/key.ui/src/main/resources/de/uka/ilkd/key/gui/smt/settings/messages.properties deleted file mode 100644 index f1dda118031..00000000000 --- a/key.ui/src/main/resources/de/uka/ilkd/key/gui/smt/settings/messages.properties +++ /dev/null @@ -1,48 +0,0 @@ -PROGRESS_MODE_USER=Progress dialog remains open after executing solvers -PROGRESS_MODE_CLOSE=Close progress dialog after all solvers have finished -PROGRESS_MODE_CLOSE_FIRST=Close progress dialog after the first solver has finished -infoBound=Bitvector size for this type. Use a value larger than 0. -infoSaveToFilePanel=Activate this option to store the translations \ - that are handed over to the externals solvers: \n\ - 1. Choose the folder.\n\ - 2. Specify the filename:\n\ - \t%s: the solver's name\n\ - \t%d: date\n\ - \t%t: time\n\ - \t%i: the goal's number\n\ - \n\ - Example: /home/translations/%d_%t_%i_%s.txt"\n\ - \n\ - Remark: After every restart of KeY this option\ - is deactivated. -infoProgressModeBox=1. Option: The progress dialog remains open after executing the solvers so that the user\ - can decide whether he wants to accept the results.\n\ - \n\ - 2. Option: The progress dialog is closed once the external provers have done their work or the time limit\ - has been exceeded. -infoCheckForSupport=If this option is activated, each time before a solver is started\ - it is checked whether the version of that solver is supported. If the version is not supported, a warning is\ - presented in the progress dialog. -infoMaxProcesses=Maximal number or processes that are allowed to run concurrently -infoTimeoutField=Timeout for the external solvers in seconds. Fractions of a second are allowed. Example: 6.5 -infoSolverName=There are two ways to make supported provers applicable for KeY:\n\ - 1. Specify the absolute path of the prover in the field 'Command'.\n\ - 2. Change the environment variable $PATH of your system, so that it\n\ - refers to the installed prover. In that case you must specify the name of the solver in 'Command' -infoSolverParameters=In this field you can specify which parameters are passed to the \ - solver when the solver is started. Note that the default parameters are crucial for a stable run of the\ - solver. -infoSolverCommand=The command for the solver.\ - Either you specify the absolute path of your solver or just the command for starting it.\ - In the latter case you have to modify the PATH-variable of your system.\ - Please note that you also have to specify the filename extension.\n\ - For example: z3.exe -infoSolverSupport=For the KeY system only some particular versions of this solver \ - have been tested. It is highly recommended to use those versions, because otherwise it is not guaranteed that\ - the connection to this solver is stable.\ -If you want to check whether the installed solver is supported, please click on the button below. -SOLVER_SUPPORTED=Version of solver is supported. -SOLVER_MAY_SUPPORTED=Version of solver may not be supported. -SOLVER_UNSUPPORTED=Support has not been checked, yet. -SOLVER_TIMEOUT=Overrides timeout for this solver. Values in seconds. If value <= 0, global timeout is used. -SOLVER_INFO=Information about this solver. \ No newline at end of file diff --git a/keyext.exploration/src/main/java/org/key_project/exploration/actions/ToggleExplorationAction.java b/keyext.exploration/src/main/java/org/key_project/exploration/actions/ToggleExplorationAction.java index afda9851da6..e46442f4f2e 100644 --- a/keyext.exploration/src/main/java/org/key_project/exploration/actions/ToggleExplorationAction.java +++ b/keyext.exploration/src/main/java/org/key_project/exploration/actions/ToggleExplorationAction.java @@ -43,8 +43,6 @@ public void selectedProofChanged(KeYSelectionEvent e) { updateEnable(mainWindow); } - @Override - public void selectedNodeChanged(KeYSelectionEvent e) {} }); updateEnable(mainWindow); diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java index a850e742f56..6d445482155 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java @@ -385,8 +385,8 @@ private static ReplayResult replayProof(CheckerData.ProofEntry line, EnvInput en lastTouchedNode = lastGoal != null ? lastGoal.node() : proof.root(); } catch (Exception e) { - if (parserResult == null || parserResult.getErrors() == null - || parserResult.getErrors().isEmpty() || + if (parserResult == null || parserResult.errors() == null + || parserResult.errors().isEmpty() || replayer == null || replayResult == null || replayResult.getErrors() == null || replayResult.getErrors().isEmpty()) { // this exception was something unexpected @@ -395,8 +395,8 @@ private static ReplayResult replayProof(CheckerData.ProofEntry line, EnvInput en } finally { String status = ""; if (parserResult != null) { - status = parserResult.getStatus(); - errors.addAll(parserResult.getErrors()); + status = parserResult.status(); + errors.addAll(parserResult.errors()); } status += (status.isEmpty() ? "" : "\n\n") + (replayResult != null ? replayResult.getStatus() diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/DependencyGraphBuilder.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/DependencyGraphBuilder.java index 46f448e727a..38931951162 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/DependencyGraphBuilder.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/DependencyGraphBuilder.java @@ -52,7 +52,7 @@ public static DependencyGraph buildGraph(List proofEntri // get current node and root of proof Proof proof = line.proof; DependencyNode currentNode = graph.getNodeByName(proof.name().toString()); - BranchNodeIntermediate node = line.parseResult.getParsedResult(); + BranchNodeIntermediate node = line.parseResult.parsedResult(); // collect all contracts the current proof refers to Services services = proof.getServices(); diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/HTMLReport.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/HTMLReport.java index 4b1eedc1e27..171056afa64 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/HTMLReport.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/HTMLReport.java @@ -6,7 +6,6 @@ import java.io.IOException; import java.lang.reflect.Method; import java.net.URL; -import java.nio.charset.StandardCharsets; import java.nio.file.Files; import java.nio.file.Path; import java.util.Map; @@ -56,7 +55,7 @@ public static void print(CheckerData data, Path target) throws IOException { data.print("Generating html report ..."); try { String output = st.render(); - Files.write(target, output.getBytes(StandardCharsets.UTF_8)); + Files.writeString(target, output); data.print("Report generated at " + target.normalize()); } catch (IOException e) { data.print("Unable to generate report: " + e.getMessage()); @@ -69,6 +68,7 @@ public static void print(CheckerData data, Path target) throws IOException { * @return the ST object for rendering the HTML report * @throws IOException if an error occurs accessing the StringTemplate resources */ + @SuppressWarnings("rawtypes") private static ST prepareStringTemplate() throws IOException { ClassLoader classLoader = HTMLReport.class.getClassLoader(); URL url = classLoader.getResource("report/html"); diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ui/SliceToFixedPointWorker.java b/keyext.slicing/src/main/java/org/key_project/slicing/ui/SliceToFixedPointWorker.java index dbda182e018..1c9837d03d3 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ui/SliceToFixedPointWorker.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ui/SliceToFixedPointWorker.java @@ -91,11 +91,6 @@ protected Void doInBackground() { return null; } - @Override - protected void done() { - - } - /** * @return the proof sliced by this worker */ diff --git a/recoder/src/main/java/recoder/service/DefaultConstantEvaluator.java b/recoder/src/main/java/recoder/service/DefaultConstantEvaluator.java index c120fbabcf7..a9e8e43a386 100644 --- a/recoder/src/main/java/recoder/service/DefaultConstantEvaluator.java +++ b/recoder/src/main/java/recoder/service/DefaultConstantEvaluator.java @@ -723,26 +723,17 @@ static int translateType(PrimitiveType t, NameInfo ni) { } static PrimitiveType translateType(int t, NameInfo ni) { - switch (t) { - case INT_TYPE: - return ni.getIntType(); - case BOOLEAN_TYPE: - return ni.getBooleanType(); - case LONG_TYPE: - return ni.getLongType(); - case FLOAT_TYPE: - return ni.getFloatType(); - case DOUBLE_TYPE: - return ni.getDoubleType(); - case BYTE_TYPE: - return ni.getByteType(); - case CHAR_TYPE: - return ni.getCharType(); - case SHORT_TYPE: - return ni.getShortType(); - default: - return null; - } + return switch (t) { + case INT_TYPE -> ni.getIntType(); + case BOOLEAN_TYPE -> ni.getBooleanType(); + case LONG_TYPE -> ni.getLongType(); + case FLOAT_TYPE -> ni.getFloatType(); + case DOUBLE_TYPE -> ni.getDoubleType(); + case BYTE_TYPE -> ni.getByteType(); + case CHAR_TYPE -> ni.getCharType(); + case SHORT_TYPE -> ni.getShortType(); + default -> null; + }; } /** @@ -750,94 +741,57 @@ static PrimitiveType translateType(int t, NameInfo ni) { */ static void promoteNumericTypeToInt(ConstantEvaluator.EvaluationResult res) { switch (res.getTypeCode()) { - case BYTE_TYPE: - res.setInt(res.getByte()); - break; - case CHAR_TYPE: - res.setInt(res.getChar()); - break; - case SHORT_TYPE: - res.setInt(res.getShort()); - break; + case BYTE_TYPE -> res.setInt(res.getByte()); + case CHAR_TYPE -> res.setInt(res.getChar()); + case SHORT_TYPE -> res.setInt(res.getShort()); } } /** * Asumes that both values are widened to at least int type. This is done by - * {@link #promoteNumericType}. Ensures that both values have equal types, or throws an + * {@link #promoteNumericTypeToInt(EvaluationResult)}. Ensures that both values have equal + * types, or throws an * exception if this is not possible given the set of allowed transformations. */ static void matchTypes(ConstantEvaluator.EvaluationResult lhs, ConstantEvaluator.EvaluationResult rhs) { switch (lhs.getTypeCode()) { - case INT_TYPE: + case INT_TYPE -> { switch (rhs.getTypeCode()) { - case LONG_TYPE: - lhs.setLong(lhs.getInt()); - break; - case FLOAT_TYPE: - lhs.setFloat(lhs.getInt()); - break; - case DOUBLE_TYPE: - lhs.setDouble(lhs.getInt()); - break; + case LONG_TYPE -> lhs.setLong(lhs.getInt()); + case FLOAT_TYPE -> lhs.setFloat(lhs.getInt()); + case DOUBLE_TYPE -> lhs.setDouble(lhs.getInt()); } - break; - case LONG_TYPE: + } + case LONG_TYPE -> { switch (rhs.getTypeCode()) { - case INT_TYPE: - rhs.setLong(rhs.getInt()); - break; - case FLOAT_TYPE: - lhs.setFloat(lhs.getLong()); - break; - case DOUBLE_TYPE: - lhs.setDouble(lhs.getLong()); - break; + case INT_TYPE -> rhs.setLong(rhs.getInt()); + case FLOAT_TYPE -> lhs.setFloat(lhs.getLong()); + case DOUBLE_TYPE -> lhs.setDouble(lhs.getLong()); } - break; - case FLOAT_TYPE: + } + case FLOAT_TYPE -> { switch (rhs.getTypeCode()) { - case INT_TYPE: - rhs.setFloat(rhs.getInt()); - break; - case LONG_TYPE: - rhs.setFloat(rhs.getLong()); - break; - case DOUBLE_TYPE: - lhs.setDouble(lhs.getFloat()); - break; + case INT_TYPE -> rhs.setFloat(rhs.getInt()); + case LONG_TYPE -> rhs.setFloat(rhs.getLong()); + case DOUBLE_TYPE -> lhs.setDouble(lhs.getFloat()); } - break; - case DOUBLE_TYPE: + } + case DOUBLE_TYPE -> { switch (rhs.getTypeCode()) { - case INT_TYPE: - rhs.setDouble(rhs.getInt()); - break; - case LONG_TYPE: - rhs.setDouble(rhs.getLong()); - break; - case FLOAT_TYPE: - rhs.setDouble(rhs.getFloat()); - break; + case INT_TYPE -> rhs.setDouble(rhs.getInt()); + case LONG_TYPE -> rhs.setDouble(rhs.getLong()); + case FLOAT_TYPE -> rhs.setDouble(rhs.getFloat()); } - break; - case STRING_TYPE: + } + case STRING_TYPE -> { switch (rhs.getTypeCode()) { - case INT_TYPE: - rhs.setString(String.valueOf(rhs.getInt())); - break; - case LONG_TYPE: - rhs.setString(String.valueOf(rhs.getLong())); - break; - case FLOAT_TYPE: - rhs.setString(String.valueOf(rhs.getFloat())); - break; - case DOUBLE_TYPE: - rhs.setString(String.valueOf(rhs.getDouble())); - break; + case INT_TYPE -> rhs.setString(String.valueOf(rhs.getInt())); + case LONG_TYPE -> rhs.setString(String.valueOf(rhs.getLong())); + case FLOAT_TYPE -> rhs.setString(String.valueOf(rhs.getFloat())); + case DOUBLE_TYPE -> rhs.setString(String.valueOf(rhs.getDouble())); } - break; + } } // if the rules above did not produce equal types, // something is wrong, e.g. boolean + non-boolean, @@ -857,9 +811,9 @@ static void matchAssignmentTypes(ConstantEvaluator.EvaluationResult lhs, ConstantEvaluator.EvaluationResult rhs) { int value; switch (lhs.getTypeCode()) { - case INT_TYPE: + case INT_TYPE -> { switch (rhs.getTypeCode()) { - case BYTE_TYPE: + case BYTE_TYPE -> { value = lhs.getInt(); if (Byte.MIN_VALUE <= value && value <= Byte.MAX_VALUE) { lhs.setByte((byte) value); @@ -867,7 +821,8 @@ static void matchAssignmentTypes(ConstantEvaluator.EvaluationResult lhs, rhs.setInt(rhs.getByte()); } return; - case CHAR_TYPE: + } + case CHAR_TYPE -> { value = lhs.getInt(); if (Character.MIN_VALUE <= value && value <= Character.MAX_VALUE) { lhs.setChar((char) value); @@ -875,7 +830,8 @@ static void matchAssignmentTypes(ConstantEvaluator.EvaluationResult lhs, rhs.setInt(rhs.getChar()); } return; - case SHORT_TYPE: + } + case SHORT_TYPE -> { value = lhs.getInt(); if (Short.MIN_VALUE <= value && value <= Short.MAX_VALUE) { lhs.setShort((short) value); @@ -884,8 +840,9 @@ static void matchAssignmentTypes(ConstantEvaluator.EvaluationResult lhs, } return; } - break; - case BYTE_TYPE: + } + } + case BYTE_TYPE -> { if (rhs.getTypeCode() == INT_TYPE) { value = rhs.getInt(); if (Byte.MIN_VALUE <= value && value <= Byte.MAX_VALUE) { @@ -895,8 +852,8 @@ static void matchAssignmentTypes(ConstantEvaluator.EvaluationResult lhs, } return; } - break; - case SHORT_TYPE: + } + case SHORT_TYPE -> { if (rhs.getTypeCode() == INT_TYPE) { value = rhs.getInt(); if (Short.MIN_VALUE <= value && value <= Short.MAX_VALUE) { @@ -906,8 +863,8 @@ static void matchAssignmentTypes(ConstantEvaluator.EvaluationResult lhs, } return; } - break; - case CHAR_TYPE: + } + case CHAR_TYPE -> { if (rhs.getTypeCode() == INT_TYPE) { value = rhs.getInt(); if (Character.MIN_VALUE <= value && value <= Character.MAX_VALUE) { @@ -917,7 +874,7 @@ static void matchAssignmentTypes(ConstantEvaluator.EvaluationResult lhs, } return; } - break; + } } matchTypes(lhs, rhs); } @@ -930,37 +887,41 @@ static void matchAssignmentTypes(ConstantEvaluator.EvaluationResult lhs, static void matchConditionalTypes(ConstantEvaluator.EvaluationResult lhs, ConstantEvaluator.EvaluationResult rhs) { switch (lhs.getTypeCode()) { - case BYTE_TYPE: + case BYTE_TYPE -> { switch (rhs.getTypeCode()) { - case SHORT_TYPE: // byte x short -> short x short + case SHORT_TYPE -> { // byte x short -> short x short lhs.setShort(lhs.getByte()); return; - case CHAR_TYPE: // byte x char -> int x int + } + case CHAR_TYPE -> { // byte x char -> int x int promoteNumericTypeToInt(lhs); promoteNumericTypeToInt(rhs); return; } - break; - case CHAR_TYPE: - switch (rhs.getTypeCode()) { - case BYTE_TYPE: // char x byte, char x short -> int x int - case SHORT_TYPE: + } + } + case CHAR_TYPE -> { + switch (rhs.getTypeCode()) { // char x byte, char x short -> int x int + case BYTE_TYPE, SHORT_TYPE -> { promoteNumericTypeToInt(lhs); promoteNumericTypeToInt(rhs); return; } - break; - case SHORT_TYPE: + } + } + case SHORT_TYPE -> { switch (rhs.getTypeCode()) { - case BYTE_TYPE: // short x byte -> short x short + case BYTE_TYPE -> { // short x byte -> short x short rhs.setShort(rhs.getByte()); return; - case CHAR_TYPE: // short x char -> int x int + } + case CHAR_TYPE -> { // short x char -> int x int promoteNumericTypeToInt(lhs); promoteNumericTypeToInt(rhs); return; } - break; + } + } } matchAssignmentTypes(lhs, rhs); } @@ -975,31 +936,15 @@ static String parseJavaString(String text) { } else { i += 1; switch (text.charAt(i)) { - case 'b': - buf.append('\b'); - break; - case 't': - buf.append('\t'); - break; - case 'n': - buf.append('\n'); - break; - case 'f': - buf.append('\f'); - break; - case 'r': - buf.append('\r'); - break; - case '\"': - buf.append('\"'); - break; - case '\'': - buf.append('\''); - break; - case '\\': - buf.append('\\'); - break; - case 'u': + case 'b' -> buf.append('\b'); + case 't' -> buf.append('\t'); + case 'n' -> buf.append('\n'); + case 'f' -> buf.append('\f'); + case 'r' -> buf.append('\r'); + case '\"' -> buf.append('\"'); + case '\'' -> buf.append('\''); + case '\\' -> buf.append('\\'); + case 'u' -> { // skip an arbitrary number of u's i += 1; while (text.charAt(i) == 'u') { @@ -1008,24 +953,16 @@ static String parseJavaString(String text) { // the following must be a 4-digit hex value buf.append((char) Integer.parseInt(text.substring(i, i + 4), 16)); i += 4; - break; - case '0': - case '1': - case '2': - case '3': - case '4': - case '5': - case '6': - case '7': + } + case '0', '1', '2', '3', '4', '5', '6', '7' -> { int j = i + 1; while (j < len && text.charAt(j) >= '0' && text.charAt(j) <= '7') { j += 1; } buf.append((char) Integer.parseInt(text.substring(i, j), 8)); i = j; - break; - default: - throw new ModelException("Bad character representation: " + text); + } + default -> throw new ModelException("Bad character representation: " + text); } } } @@ -1041,160 +978,76 @@ static void doPrimitiveTypeCast(int newType, ConstantEvaluator.EvaluationResult throw new ModelException("Cast not allowed"); } switch (oldType) { - case BYTE_TYPE: + case BYTE_TYPE -> { switch (newType) { - case SHORT_TYPE: - res.setShort(res.getByte()); - return; - case CHAR_TYPE: - res.setChar((char) res.getByte()); - return; - case INT_TYPE: - res.setInt(res.getByte()); - return; - case LONG_TYPE: - res.setLong(res.getByte()); - return; - case FLOAT_TYPE: - res.setFloat(res.getByte()); - return; - case DOUBLE_TYPE: - res.setDouble(res.getByte()); - return; + case SHORT_TYPE -> res.setShort(res.getByte()); + case CHAR_TYPE -> res.setChar((char) res.getByte()); + case INT_TYPE -> res.setInt(res.getByte()); + case LONG_TYPE -> res.setLong(res.getByte()); + case FLOAT_TYPE -> res.setFloat(res.getByte()); + case DOUBLE_TYPE -> res.setDouble(res.getByte()); } - break; - case SHORT_TYPE: + } + case SHORT_TYPE -> { switch (newType) { - case BYTE_TYPE: - res.setByte((byte) res.getShort()); - return; - case CHAR_TYPE: - res.setChar((char) res.getShort()); - return; - case INT_TYPE: - res.setInt(res.getShort()); - return; - case LONG_TYPE: - res.setLong(res.getShort()); - return; - case FLOAT_TYPE: - res.setFloat(res.getShort()); - return; - case DOUBLE_TYPE: - res.setDouble(res.getShort()); - return; + case BYTE_TYPE -> res.setByte((byte) res.getShort()); + case CHAR_TYPE -> res.setChar((char) res.getShort()); + case INT_TYPE -> res.setInt(res.getShort()); + case LONG_TYPE -> res.setLong(res.getShort()); + case FLOAT_TYPE -> res.setFloat(res.getShort()); + case DOUBLE_TYPE -> res.setDouble(res.getShort()); } - break; - case CHAR_TYPE: + } + case CHAR_TYPE -> { switch (newType) { - case BYTE_TYPE: - res.setByte((byte) res.getChar()); - return; - case SHORT_TYPE: - res.setShort((short) res.getChar()); - return; - case INT_TYPE: - res.setInt(res.getChar()); - return; - case LONG_TYPE: - res.setLong(res.getChar()); - return; - case FLOAT_TYPE: - res.setFloat(res.getChar()); - return; - case DOUBLE_TYPE: - res.setDouble(res.getChar()); - return; + case BYTE_TYPE -> res.setByte((byte) res.getChar()); + case SHORT_TYPE -> res.setShort((short) res.getChar()); + case INT_TYPE -> res.setInt(res.getChar()); + case LONG_TYPE -> res.setLong(res.getChar()); + case FLOAT_TYPE -> res.setFloat(res.getChar()); + case DOUBLE_TYPE -> res.setDouble(res.getChar()); } - break; - case INT_TYPE: + } + case INT_TYPE -> { switch (newType) { - case BYTE_TYPE: - res.setByte((byte) res.getInt()); - return; - case SHORT_TYPE: - res.setShort((short) res.getInt()); - return; - case CHAR_TYPE: - res.setChar((char) res.getInt()); - return; - case LONG_TYPE: - res.setLong(res.getInt()); - return; - case FLOAT_TYPE: - res.setFloat((float) res.getInt()); - return; - case DOUBLE_TYPE: - res.setDouble(res.getInt()); - return; + case BYTE_TYPE -> res.setByte((byte) res.getInt()); + case SHORT_TYPE -> res.setShort((short) res.getInt()); + case CHAR_TYPE -> res.setChar((char) res.getInt()); + case LONG_TYPE -> res.setLong(res.getInt()); + case FLOAT_TYPE -> res.setFloat((float) res.getInt()); + case DOUBLE_TYPE -> res.setDouble(res.getInt()); } - break; - case LONG_TYPE: + } + case LONG_TYPE -> { switch (newType) { - case BYTE_TYPE: - res.setByte((byte) res.getLong()); - return; - case SHORT_TYPE: - res.setShort((short) res.getLong()); - return; - case CHAR_TYPE: - res.setChar((char) res.getLong()); - return; - case INT_TYPE: - res.setInt((int) res.getLong()); - return; - case FLOAT_TYPE: - res.setFloat((float) res.getLong()); - return; - case DOUBLE_TYPE: - res.setDouble((double) res.getLong()); - return; + case BYTE_TYPE -> res.setByte((byte) res.getLong()); + case SHORT_TYPE -> res.setShort((short) res.getLong()); + case CHAR_TYPE -> res.setChar((char) res.getLong()); + case INT_TYPE -> res.setInt((int) res.getLong()); + case FLOAT_TYPE -> res.setFloat((float) res.getLong()); + case DOUBLE_TYPE -> res.setDouble((double) res.getLong()); } - break; - case FLOAT_TYPE: + } + case FLOAT_TYPE -> { switch (newType) { - case BYTE_TYPE: - res.setByte((byte) res.getFloat()); - return; - case SHORT_TYPE: - res.setShort((short) res.getFloat()); - return; - case CHAR_TYPE: - res.setChar((char) res.getFloat()); - return; - case INT_TYPE: - res.setInt((int) res.getFloat()); - return; - case LONG_TYPE: - res.setLong((long) res.getFloat()); - return; - case DOUBLE_TYPE: - res.setDouble(res.getFloat()); - return; + case BYTE_TYPE -> res.setByte((byte) res.getFloat()); + case SHORT_TYPE -> res.setShort((short) res.getFloat()); + case CHAR_TYPE -> res.setChar((char) res.getFloat()); + case INT_TYPE -> res.setInt((int) res.getFloat()); + case LONG_TYPE -> res.setLong((long) res.getFloat()); + case DOUBLE_TYPE -> res.setDouble(res.getFloat()); } - break; - case DOUBLE_TYPE: + } + case DOUBLE_TYPE -> { switch (newType) { - case BYTE_TYPE: - res.setByte((byte) res.getDouble()); - return; - case SHORT_TYPE: - res.setShort((short) res.getDouble()); - return; - case CHAR_TYPE: - res.setChar((char) res.getDouble()); - return; - case INT_TYPE: - res.setInt((int) res.getDouble()); - return; - case LONG_TYPE: - res.setLong((long) res.getDouble()); - return; - case FLOAT_TYPE: - res.setFloat((float) res.getDouble()); - return; + case BYTE_TYPE -> res.setByte((byte) res.getDouble()); + case SHORT_TYPE -> res.setShort((short) res.getDouble()); + case CHAR_TYPE -> res.setChar((char) res.getDouble()); + case INT_TYPE -> res.setInt((int) res.getDouble()); + case LONG_TYPE -> res.setLong((long) res.getDouble()); + case FLOAT_TYPE -> res.setFloat((float) res.getDouble()); } - break; + } } } @@ -1327,12 +1180,11 @@ public boolean isCompileTimeConstant(Expression expr, ConstantEvaluator.Evaluati BinaryBooleanOperation bbo = null; switch (op.getArity()) { - case 1: // unary operations + case 1 -> { // unary operations if (!isCompileTimeConstant(op.getExpressionAt(0), res)) { return false; } - if (op instanceof Positive) { uno = POSITIVE; } else if (op instanceof Negative) { @@ -1342,8 +1194,8 @@ public boolean isCompileTimeConstant(Expression expr, ConstantEvaluator.Evaluati } else if (op instanceof LogicalNot) { ubo = LOGICAL_NOT; } - break; - case 2: // binary operations + } + case 2 -> { // binary operations if (!isCompileTimeConstant(op.getExpressionAt(0), res)) { return false; } @@ -1355,7 +1207,7 @@ public boolean isCompileTimeConstant(Expression expr, ConstantEvaluator.Evaluati * would be stored locally and res would be reused for the rhs call. However, * performance is not critical here. */ - rhs = new ConstantEvaluator.EvaluationResult(); + rhs = new EvaluationResult(); // evaluate right-hand side; finish if not constant if (!isCompileTimeConstant(op.getExpressionAt(1), rhs)) { return false; @@ -1365,7 +1217,6 @@ public boolean isCompileTimeConstant(Expression expr, ConstantEvaluator.Evaluati // widen the remaining types to match both argument types matchTypes(lhs, rhs); - if (op instanceof ComparativeOperator) { if (op instanceof Equals) { bbo = EQUALS; @@ -1411,8 +1262,8 @@ public boolean isCompileTimeConstant(Expression expr, ConstantEvaluator.Evaluati } else if (op instanceof LogicalOr) { bbo = LOGICAL_OR; } - break; - case 3: + } + case 3 -> { // this must be the conditional (?:) if (!isCompileTimeConstant(op.getExpressionAt(0), res)) { return false; @@ -1427,136 +1278,70 @@ public boolean isCompileTimeConstant(Expression expr, ConstantEvaluator.Evaluati if (!isCompileTimeConstant(op.getExpressionAt(1), lhs)) { return false; } - rhs = new ConstantEvaluator.EvaluationResult(); + rhs = new EvaluationResult(); if (!isCompileTimeConstant(op.getExpressionAt(2), rhs)) { return false; } matchConditionalTypes(lhs, rhs); - switch (lhs.getTypeCode()) { // matches type of rhs - case BOOLEAN_TYPE: - res.setBoolean(cond ? lhs.getBoolean() : rhs.getBoolean()); - break; - case BYTE_TYPE: - res.setByte(cond ? lhs.getByte() : rhs.getByte()); - break; - case SHORT_TYPE: - res.setShort(cond ? lhs.getShort() : rhs.getShort()); - break; - case CHAR_TYPE: - res.setChar(cond ? lhs.getChar() : rhs.getChar()); - break; - case INT_TYPE: - res.setInt(cond ? lhs.getInt() : rhs.getInt()); - break; - case LONG_TYPE: - res.setLong(cond ? lhs.getLong() : rhs.getLong()); - break; - case FLOAT_TYPE: - res.setFloat(cond ? lhs.getFloat() : rhs.getFloat()); - break; - case DOUBLE_TYPE: - res.setDouble(cond ? lhs.getDouble() : rhs.getDouble()); - break; - case STRING_TYPE: - res.setString(cond ? lhs.getString() : rhs.getString()); - break; + case BOOLEAN_TYPE -> res.setBoolean(cond ? lhs.getBoolean() : rhs.getBoolean()); + case BYTE_TYPE -> res.setByte(cond ? lhs.getByte() : rhs.getByte()); + case SHORT_TYPE -> res.setShort(cond ? lhs.getShort() : rhs.getShort()); + case CHAR_TYPE -> res.setChar(cond ? lhs.getChar() : rhs.getChar()); + case INT_TYPE -> res.setInt(cond ? lhs.getInt() : rhs.getInt()); + case LONG_TYPE -> res.setLong(cond ? lhs.getLong() : rhs.getLong()); + case FLOAT_TYPE -> res.setFloat(cond ? lhs.getFloat() : rhs.getFloat()); + case DOUBLE_TYPE -> res.setDouble(cond ? lhs.getDouble() : rhs.getDouble()); + case STRING_TYPE -> res.setString(cond ? lhs.getString() : rhs.getString()); } return true; } + } if (bno != null) { switch (lhs.getTypeCode()) { - case BOOLEAN_TYPE: - lhs.setBoolean(bno.eval(lhs.getBoolean(), rhs.getBoolean())); - break; - case INT_TYPE: - lhs.setInt(bno.eval(lhs.getInt(), rhs.getInt())); - break; - case LONG_TYPE: - lhs.setLong(bno.eval(lhs.getLong(), rhs.getLong())); - break; - case FLOAT_TYPE: - lhs.setFloat(bno.eval(lhs.getFloat(), rhs.getFloat())); - break; - case DOUBLE_TYPE: - lhs.setDouble(bno.eval(lhs.getDouble(), rhs.getDouble())); - break; - case STRING_TYPE: - lhs.setString(bno.eval(lhs.getString(), rhs.getString())); - break; + case BOOLEAN_TYPE -> lhs.setBoolean(bno.eval(lhs.getBoolean(), rhs.getBoolean())); + case INT_TYPE -> lhs.setInt(bno.eval(lhs.getInt(), rhs.getInt())); + case LONG_TYPE -> lhs.setLong(bno.eval(lhs.getLong(), rhs.getLong())); + case FLOAT_TYPE -> lhs.setFloat(bno.eval(lhs.getFloat(), rhs.getFloat())); + case DOUBLE_TYPE -> lhs.setDouble(bno.eval(lhs.getDouble(), rhs.getDouble())); + case STRING_TYPE -> lhs.setString(bno.eval(lhs.getString(), rhs.getString())); } return true; } if (bbo != null) { switch (lhs.getTypeCode()) { - case BOOLEAN_TYPE: - lhs.setBoolean(bbo.eval(lhs.getBoolean(), rhs.getBoolean())); - break; - case INT_TYPE: - lhs.setBoolean(bbo.eval(lhs.getInt(), rhs.getInt())); - break; - case LONG_TYPE: - lhs.setBoolean(bbo.eval(lhs.getLong(), rhs.getLong())); - break; - case FLOAT_TYPE: - lhs.setBoolean(bbo.eval(lhs.getFloat(), rhs.getFloat())); - break; - case DOUBLE_TYPE: - lhs.setBoolean(bbo.eval(lhs.getDouble(), rhs.getDouble())); - break; - case STRING_TYPE: - lhs.setBoolean(bbo.eval(lhs.getString(), rhs.getString())); - break; + case BOOLEAN_TYPE -> lhs.setBoolean(bbo.eval(lhs.getBoolean(), rhs.getBoolean())); + case INT_TYPE -> lhs.setBoolean(bbo.eval(lhs.getInt(), rhs.getInt())); + case LONG_TYPE -> lhs.setBoolean(bbo.eval(lhs.getLong(), rhs.getLong())); + case FLOAT_TYPE -> lhs.setBoolean(bbo.eval(lhs.getFloat(), rhs.getFloat())); + case DOUBLE_TYPE -> lhs.setBoolean(bbo.eval(lhs.getDouble(), rhs.getDouble())); + case STRING_TYPE -> lhs.setBoolean(bbo.eval(lhs.getString(), rhs.getString())); } return true; } if (uno != null) { switch (res.getTypeCode()) { - case BOOLEAN_TYPE: - res.setBoolean(uno.eval(res.getBoolean())); - break; - case INT_TYPE: - res.setInt(uno.eval(res.getInt())); - break; - case LONG_TYPE: - res.setLong(uno.eval(res.getLong())); - break; - case FLOAT_TYPE: - res.setFloat(uno.eval(res.getFloat())); - break; - case DOUBLE_TYPE: - res.setDouble(uno.eval(res.getDouble())); - break; - case STRING_TYPE: - res.setString(uno.eval(res.getString())); - break; + case BOOLEAN_TYPE -> res.setBoolean(uno.eval(res.getBoolean())); + case INT_TYPE -> res.setInt(uno.eval(res.getInt())); + case LONG_TYPE -> res.setLong(uno.eval(res.getLong())); + case FLOAT_TYPE -> res.setFloat(uno.eval(res.getFloat())); + case DOUBLE_TYPE -> res.setDouble(uno.eval(res.getDouble())); + case STRING_TYPE -> res.setString(uno.eval(res.getString())); } return true; } if (ubo != null) { switch (res.getTypeCode()) { - case BOOLEAN_TYPE: - res.setBoolean(ubo.eval(res.getBoolean())); - break; - case INT_TYPE: - res.setBoolean(ubo.eval(res.getInt())); - break; - case LONG_TYPE: - res.setBoolean(ubo.eval(res.getLong())); - break; - case FLOAT_TYPE: - res.setBoolean(ubo.eval(res.getFloat())); - break; - case DOUBLE_TYPE: - res.setBoolean(ubo.eval(res.getDouble())); - break; - case STRING_TYPE: - res.setBoolean(ubo.eval(res.getString())); - break; + case BOOLEAN_TYPE -> res.setBoolean(ubo.eval(res.getBoolean())); + case INT_TYPE -> res.setBoolean(ubo.eval(res.getInt())); + case LONG_TYPE -> res.setBoolean(ubo.eval(res.getLong())); + case FLOAT_TYPE -> res.setBoolean(ubo.eval(res.getFloat())); + case DOUBLE_TYPE -> res.setBoolean(ubo.eval(res.getDouble())); + case STRING_TYPE -> res.setBoolean(ubo.eval(res.getString())); } return true; } @@ -1627,43 +1412,29 @@ public boolean isCompileTimeConstant(Expression expr, ConstantEvaluator.Evaluati return false; } switch (vtype) { - case BOOLEAN_TYPE: - res.setBoolean(Integer.parseInt(val) != 0); - break; - case BYTE_TYPE: - res.setByte((byte) Integer.parseInt(val)); - break; - case SHORT_TYPE: - res.setShort((short) Integer.parseInt(val)); - break; - case CHAR_TYPE: - res.setChar((char) Integer.parseInt(val)); - break; - case INT_TYPE: - res.setInt(Integer.parseInt(val)); - break; - case LONG_TYPE: - res.setLong(Long.parseLong(val)); - break; - case FLOAT_TYPE: + case BOOLEAN_TYPE -> res.setBoolean(Integer.parseInt(val) != 0); + case BYTE_TYPE -> res.setByte((byte) Integer.parseInt(val)); + case SHORT_TYPE -> res.setShort((short) Integer.parseInt(val)); + case CHAR_TYPE -> res.setChar((char) Integer.parseInt(val)); + case INT_TYPE -> res.setInt(Integer.parseInt(val)); + case LONG_TYPE -> res.setLong(Long.parseLong(val)); + case FLOAT_TYPE -> { if (val.equals("NaN")) { // may occur in byte code?! res.setFloat(Float.NaN); } else { res.setFloat(Float.valueOf(val)); } - break; - case DOUBLE_TYPE: + } + case DOUBLE_TYPE -> { if (val.equals("NaN")) { // may occur in byte code?! res.setDouble(Double.NaN); } else { res.setDouble(Double.valueOf(val)); } - break; - case STRING_TYPE: - res.setString(val); - break; + } + case STRING_TYPE -> res.setString(val); } return true; } diff --git a/recoder/src/main/java/recoder/service/DefaultProgramModelInfo.java b/recoder/src/main/java/recoder/service/DefaultProgramModelInfo.java index 9814b29c124..cd48ec0e173 100644 --- a/recoder/src/main/java/recoder/service/DefaultProgramModelInfo.java +++ b/recoder/src/main/java/recoder/service/DefaultProgramModelInfo.java @@ -31,23 +31,16 @@ protected DefaultProgramModelInfo(ServiceConfiguration config) { super(config); } - // TODO move to where it belongs ?! - private static void removeRange(List list, int from) { - for (int i = list.size() - 1; i >= from; i--) { - list.remove(i); + private static void removeRange(List list, int from) { + if (list.size() > from) { + list.subList(from, list.size()).clear(); } } - // TODO move to where it belongs ?! - private static void removeRange(List list, int from, int to) { - // TODO improve speed! - if (from > to) { - to ^= from ^= to ^= from; - } - int cnt = to - from; - while (cnt-- > 0) { - list.remove(from); - } + private static void removeRange(List list, int from, int to) { + int start = Math.min(from, to); + int end = Math.max(from, to); + list.subList(start, end).clear(); } final ChangeHistory getChangeHistory() { @@ -118,9 +111,7 @@ public List getSubtypes(ClassType ct) { } int s = ctce.subtypes.size(); List result = new ArrayList<>(s); - for (ClassType subct : ctce.subtypes) { - result.add(subct); - } + result.addAll(ctce.subtypes); return result; } @@ -184,13 +175,12 @@ private void computeAllFields(ClassType ct, ClassTypeCacheEntry ctce) { if (fl == null) { continue; } - int fs = fl.size(); add_fields: for (Field f : fl) { if (isVisibleFor(f, ct)) { String fname = f.getName(); for (int k = 0; k < result_size; k++) { Field rf = result.get(k); - if (rf.getName() == fname) { + if (Objects.equals(rf.getName(), fname)) { continue add_fields; } } @@ -234,7 +224,6 @@ private void computeAllMethods(ClassType ct, ClassTypeCacheEntry ctce) { if (ml == null) { continue; } - int ms = ml.size(); add_methods: for (Method m : ml) { // if (m.isPublic() || m.isProtected() || c == ct || // (!m.isPrivate() && c.getPackage() == ct.getPackage())) { @@ -264,7 +253,7 @@ private void computeAllMethods(ClassType ct, ClassTypeCacheEntry ctce) { String mname = m.getName(); for (int k = 0; k < result_size; k++) { Method rm = result.get(k); - if (rm.getName() == mname) { + if (Objects.equals(rm.getName(), mname)) { List rsig = rm.getSignature(); if (rsig.equals(msig)) { // skip this method: we already had it @@ -282,18 +271,11 @@ private void computeAllMethods(ClassType ct, ClassTypeCacheEntry ctce) { } private Type makeParameterizedType(TypeArgument ta) { - Type bt = null; - switch (ta.getWildcardMode()) { - case Super: - case Any: - bt = getNameInfo().getJavaLangObject(); - break; - case None: - case Extends: - bt = getBaseType(ta); - break; - } - if (ta.getTypeArguments() == null || ta.getTypeArguments().size() == 0) { + Type bt = switch (ta.getWildcardMode()) { + case Super, Any -> getNameInfo().getJavaLangObject(); + case None, Extends -> getBaseType(ta); + }; + if (ta.getTypeArguments() == null || ta.getTypeArguments().isEmpty()) { return bt; } return new ParameterizedType((ClassType) bt, ta.getTypeArguments()); @@ -329,7 +311,6 @@ private void computeAllMemberTypes(ClassType ct, ClassTypeCacheEntry ctce) { if (cl == null) { continue; } - int cs = cl.size(); add_ClassTypes: for (ClassType hc : cl) { // hc == ct may occur as it is admissible for a member class // to extend its parent class @@ -337,7 +318,7 @@ private void computeAllMemberTypes(ClassType ct, ClassTypeCacheEntry ctce) { String cname = hc.getName(); for (int k = 0; k < result_size; k++) { ClassType rc = result.get(k); - if (rc.getName() == cname) { + if (Objects.equals(rc.getName(), cname)) { continue add_ClassTypes; } } @@ -444,8 +425,7 @@ public boolean isWidening(Type from, Type to) { if (to instanceof ClassType) { return isWidening((ClassType) from, (ClassType) to); } else { - return (from instanceof NullType) - && (to instanceof ArrayType || to instanceof TypeParameter); + return from instanceof NullType && to instanceof ArrayType; } } else if (from instanceof PrimitiveType) { if (to instanceof PrimitiveType) { @@ -509,7 +489,7 @@ public boolean isSupertype(ClassType a, ClassType b) { return isSubtype(b, a); } - private final boolean paramMatches(Type ta, Type tb, boolean allowAutoboxing) { + private boolean paramMatches(Type ta, Type tb, boolean allowAutoboxing) { if (ta == tb) { return true; } @@ -585,7 +565,7 @@ private ClassType getClassTypeFromTypeParameter(TypeParameter tp, int i) { return t; } - private final boolean internalIsCompatibleSignature(List a, List b, + private boolean internalIsCompatibleSignature(List a, List b, boolean allowAutoboxing, boolean isVarArgMethod) { int s = b.size(); int n = a.size(); @@ -896,9 +876,7 @@ private void internalFilterApplicableMethods(List list, String name, private List replaceTypeArguments(List methodSig, List typeArguments, Method m) { List res = new ArrayList<>(methodSig.size()); - for (Type type : methodSig) { - res.add(type); - } + res.addAll(methodSig); for (int l = 0; l < m.getTypeParameters().size(); l++) { TypeParameter tp = m.getTypeParameters().get(l); for (int k = 0; k < methodSig.size(); k++) { @@ -1025,7 +1003,7 @@ private List internalGetMostSpecificMethods(ClassType ct, String name, List signature, List meths, List typeArgs, ClassType context) { Debug.assertNonnull(ct, name, signature); - boolean allowJava5 = Boolean.valueOf( + boolean allowJava5 = Boolean.parseBoolean( getServiceConfiguration().getProjectSettings().getProperty(PropertyNames.JAVA_5)); List result; @@ -1059,13 +1037,13 @@ public List doThreePhaseFilter(List methods, List 0) { + if (!result.isEmpty()) { return result; } result.addAll(applicableMethods); // result is empty at this point filterMostSpecificMethodsPhase2(result); - if (result.size() > 0) { + if (!result.isEmpty()) { return result; } result.addAll(applicableMethods); // once again, result is empty @@ -1084,7 +1062,6 @@ public void reset() { /** * Takes an (Array|Class)Type and adds type arguments to it. * - * @return * @throws AssertionError if t is neither a Class or Array Type * @throws ClassCastException if t is an array type with a primitive type as base type. */ diff --git a/recoder/src/main/java/recoder/service/DefaultSourceInfo.java b/recoder/src/main/java/recoder/service/DefaultSourceInfo.java index 8842e3a81a8..89f5265b610 100644 --- a/recoder/src/main/java/recoder/service/DefaultSourceInfo.java +++ b/recoder/src/main/java/recoder/service/DefaultSourceInfo.java @@ -89,7 +89,6 @@ static boolean isPartOf(ProgramElement pe, Class c) { /** * looks for the next variable scope that is a parent of the given element * - * @param pe a program element * @return the outer variable scope of the program element or null */ private static VariableScope findOuterVariableScope(VariableScope ts) { @@ -160,7 +159,7 @@ private static LoopStatement findInnermostLoop(Statement s) { /** * Initializes the new service; called by the configuration. * - * @param config the configuration this services becomes part of. + * @param cfg the configuration this services becomes part of. */ public void initialize(ServiceConfiguration cfg) { super.initialize(cfg); @@ -198,8 +197,6 @@ protected NameInfo getNameInfo() { /** * Change notification callback method. - * - * @param config the configuration this services becomes part of. */ public void modelChanged(ChangeHistoryEvent changes) { List changed = changes.getChanges(); diff --git a/recoder/src/main/java/recoder/util/OptionManager.java b/recoder/src/main/java/recoder/util/OptionManager.java index 390b7f318a9..004b6036bca 100644 --- a/recoder/src/main/java/recoder/util/OptionManager.java +++ b/recoder/src/main/java/recoder/util/OptionManager.java @@ -117,10 +117,8 @@ int parseArg(String[] args, int offset) throws UnknownOptionException, } Object optval = null; switch (descr.type) { - case SIMPLE: - optval = TRUE; - break; - case SWITCH: + case SIMPLE -> optval = TRUE; + case SWITCH -> { if ("on".equals(sval)) { optval = ON; } else if ("off".equals(sval)) { @@ -128,8 +126,8 @@ int parseArg(String[] args, int offset) throws UnknownOptionException, } else { throw new IllegalOptionValueException(opt, sval); } - break; - case BOOL: + } + case BOOL -> { if ("true".equals(sval)) { optval = TRUE; } else if ("false".equals(sval)) { @@ -137,17 +135,15 @@ int parseArg(String[] args, int offset) throws UnknownOptionException, } else { throw new IllegalOptionValueException(opt, sval); } - break; - case NUM: + } + case NUM -> { try { optval = Integer.valueOf(sval); } catch (NumberFormatException nfe) { throw new IllegalOptionValueException(opt, sval); } - break; - case STRING: - optval = sval; - break; + } + case STRING -> optval = sval; } Debug.assertNonnull(optval); descr.values.addElement(optval); @@ -168,7 +164,7 @@ public String[] parseArgs(String[] args) // check if all mandatory arguments have been set for (Enumeration mand = mandatories.elements(); mand.hasMoreElements();) { OptionDescription descr = (OptionDescription) mand.nextElement(); - if (descr.values.size() == 0) { + if (descr.values.isEmpty()) { throw new MissingArgumentException(descr.shortOpt); } } @@ -332,7 +328,7 @@ public String getStringVal(String opt, String defaultVal) { /** * describes a single command line option. */ - private static class OptionDescription { + public static class OptionDescription { int type; int multiplicity;