diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/JmlAssert.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/JmlAssert.java index 14c8a6c1946..8e18cfc3048 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/JmlAssert.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/JmlAssert.java @@ -5,7 +5,6 @@ import java.util.Objects; -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.PositionInfo; import de.uka.ilkd.key.java.ast.ProgramElement; import de.uka.ilkd.key.java.visitor.Visitor; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java index f626877d436..6044caf6cbd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java @@ -514,7 +514,7 @@ public Object visit(EmptyStmt n, Void arg) { var construct = n.getData(JMLTransformer.KEY_CONSTRUCT); if (construct instanceof TextualJMLAssertStatement) { var a = (TextualJMLAssertStatement) construct; - return new JmlAssert(a.getKind(), a.getContext(), pi, services); + return new JmlAssert(a.getKind(), a.getContext(), pi); } if (construct instanceof TextualJMLMergePointDecl) { var a = (TextualJMLMergePointDecl) construct; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SetStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SetStatement.java deleted file mode 100644 index 2f509951666..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SetStatement.java +++ /dev/null @@ -1,93 +0,0 @@ -/* 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 de.uka.ilkd.key.java.recoderext; - -import de.uka.ilkd.key.nparser.KeyAst.SetStatementContext; - -import recoder.java.ProgramElement; -import recoder.java.SourceVisitor; -import recoder.java.statement.JavaStatement; - -/** - * Wrapper for JML set statements which lifts the contained parse tree to the Translator. - * - * @author Julian Wiesler - */ -public class SetStatement extends JavaStatement { - /** - * Parser context of the assignment - */ - private final SetStatementContext context; - - /** - * Primary constructor - * - * @param context the context of the assignment - */ - public SetStatement(SetStatementContext context) { - this.context = context; - } - - /** - * copy constructor - * - * @param proto the orginal JML set statement to copy - */ - public SetStatement(SetStatement proto) { - super(proto); - this.context = proto.context; - } - - /** - * {@inheritDoc} - */ - @Override - public SetStatement deepClone() { - return new SetStatement(this); - } - - /** - * Gets the contained parser context - * - * @return the parser context - */ - public SetStatementContext getParserContext() { - return context; - } - - /** - * A set statement has no recorder AST children - */ - @Override - public int getChildCount() { - return 0; - } - - /** - * {@inheritDoc} - * - * There are no recorder AST children. - * - * @throws IndexOutOfBoundsException always - */ - @Override - public ProgramElement getChildAt(int index) { - throw new IndexOutOfBoundsException("JmlAssert has no program children"); - } - - @Override - public int getChildPositionCode(ProgramElement child) { - return -1; - } - - @Override - public boolean replaceChild(ProgramElement p, ProgramElement q) { - return false; - } - - @Override - public void accept(SourceVisitor v) { - // should be fine to leave blank - } -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/SeqPut.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/SeqPut.java deleted file mode 100644 index 579f1355bdb..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/SeqPut.java +++ /dev/null @@ -1,49 +0,0 @@ -/* 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 de.uka.ilkd.key.java.recoderext.adt; - -import recoder.java.Expression; -import recoder.list.generic.ASTArrayList; - - -public class SeqPut extends ADTPrefixConstruct { - - private static final long serialVersionUID = -4836079248155746383L; - - public SeqPut(Expression seq, Expression idx, Expression val) { - children = new ASTArrayList<>(getArity()); - children.add(seq); - children.add(idx); - children.add(val); - makeParentRoleValid(); - } - - protected SeqPut(SeqPut proto) { - super(proto); - makeParentRoleValid(); - } - - @Override - public SeqPut deepClone() { - return new SeqPut(this); - } - - - @Override - public int getArity() { - return 3; - } - - - @Override - public int getNotation() { - return PREFIX; - } - - @Override - public String toSource() { - return "\\seq_upd(" + children.get(0).toSource() + ", " + children.get(1).toSource() + ", " - + children.get(2).toSource() + ")"; - } -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/package-info.java deleted file mode 100644 index 4ee9164bded..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/package-info.java +++ /dev/null @@ -1,7 +0,0 @@ -/** - * This package contains RecodeR Operators - * which represent algebraic data type functions. (See also the - * ldt package description.) - */ -package de.uka.ilkd.key.java.recoderext.adt; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgVarReplaceVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgVarReplaceVisitor.java index 0ff581dca25..e64c3d48162 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgVarReplaceVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgVarReplaceVisitor.java @@ -12,13 +12,11 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.Label; import de.uka.ilkd.key.java.ast.ProgramElement; +import de.uka.ilkd.key.java.ast.Statement; import de.uka.ilkd.key.java.ast.StatementBlock; import de.uka.ilkd.key.java.ast.declaration.LocalVariableDeclaration; import de.uka.ilkd.key.java.ast.declaration.VariableSpecification; -import de.uka.ilkd.key.java.ast.statement.JavaStatement; -import de.uka.ilkd.key.java.ast.statement.JmlAssert; -import de.uka.ilkd.key.java.ast.statement.LoopStatement; -import de.uka.ilkd.key.java.ast.statement.MergePointStatement; +import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; @@ -608,44 +606,6 @@ public void performActionOnJmlAssert(final JmlAssert x) { @Override public void performActionOnSetStatement(final SetStatement x) { - /* - * var spec = - * Objects.requireNonNull(services.getSpecificationRepository().getStatementSpec(x)); - * ProgramVariableCollection vars = spec.vars(); - * Map atPres = vars.atPres; - * Map newAtPres = new LinkedHashMap<>(atPres); - * Map atPreVars = vars.atPreVars; - * Map newAtPreVars = new LinkedHashMap<>(atPreVars); - * - * for (Entry e : atPres.entrySet()) { - * LocationVariable pv = e.getKey(); - * final Term t = e.getValue(); - * if (t == null) { - * continue; - * } - * if (replaceMap.containsKey(pv)) { - * newAtPres.remove(pv); - * pv = (LocationVariable) replaceMap.get(pv); - * newAtPreVars.put(pv, atPreVars.get(e.getKey())); - * } - * newAtPres.put(pv, replaceVariablesInTerm(t)); - * } - * final ProgramVariableCollection newVars = - * new ProgramVariableCollection(vars.selfVar, vars.paramVars, vars.resultVar, vars.excVar, - * newAtPreVars, newAtPres, vars.atBeforeVars, vars.atBefores); - * - * - * var newTerms = spec.terms().map(this::replaceVariablesInTerm); - * var newSpec = new SpecificationRepository.JmlStatementSpec(newVars, newTerms); - * - * services.getSpecificationRepository().addStatementSpec(x, newSpec); - * - * /* - * if (!newAtPres.equals(vars.atPres)) { - * changed(); - * } - * doDefaultAction(x); - */ handleJmlStatements(x, SetStatement::new); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramVariableCollector.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramVariableCollector.java index f6ebe80e615..635d341e764 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramVariableCollector.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramVariableCollector.java @@ -12,7 +12,9 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.ProgramElement; import de.uka.ilkd.key.java.ast.SourceElement; +import de.uka.ilkd.key.java.ast.Statement; import de.uka.ilkd.key.java.ast.statement.JmlAssert; +import de.uka.ilkd.key.java.ast.statement.SetStatement; import de.uka.ilkd.key.ldt.HeapLDT; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.LocationVariable; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java index e0036ecb368..a937a1d4191 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java @@ -14,7 +14,6 @@ import de.uka.ilkd.key.java.ast.expression.operator.adt.*; import de.uka.ilkd.key.java.ast.reference.*; import de.uka.ilkd.key.java.ast.statement.*; -import de.uka.ilkd.key.java.statement.SetStatement; import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.logic.op.IProgramMethod; import de.uka.ilkd.key.logic.op.IProgramVariable; @@ -81,7 +80,7 @@ public interface Visitor { void performActionOnSeqReverse(SeqReverse x); - //void performActionOnSeqPut(SeqPut seqPut); + void performActionOnSeqPut(SeqPut seqPut); void performActionOnDLEmbeddedExpression(DLEmbeddedExpression x); @@ -185,7 +184,7 @@ public interface Visitor { void performActionOnCopyAssignment(CopyAssignment x); - //void performActionOnSetStatement(SetStatement x); + void performActionOnSetStatement(SetStatement x); void performActionOnDivideAssignment(DivideAssignment x); 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 bfdbf3cbe0f..4d34c5b8300 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 @@ -3,7 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.ldt; -import de.uka.ilkd.key.java.Expression; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.abstraction.Type; import de.uka.ilkd.key.java.ast.expression.Expression; @@ -11,7 +10,7 @@ import de.uka.ilkd.key.java.ast.expression.literal.EmptySeqLiteral; import de.uka.ilkd.key.java.ast.expression.literal.Literal; import de.uka.ilkd.key.java.ast.expression.operator.adt.*; -import de.uka.ilkd.key.java.expression.operator.adt.SeqPut; +import de.uka.ilkd.key.java.ast.expression.operator.adt.SeqPut; import de.uka.ilkd.key.java.ast.reference.ExecutionContext; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermServices; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java b/key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java index 7759cb56f5c..cd57b9b6480 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java @@ -3,7 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.logic; -import de.uka.ilkd.key.java.NameAbstractionTable; import de.uka.ilkd.key.java.ast.JavaProgramElement; import de.uka.ilkd.key.java.ast.StatementBlock; import de.uka.ilkd.key.pp.PrettyPrinter; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java index 3a49c3002b9..d9efa02540e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java @@ -5,7 +5,7 @@ import java.util.concurrent.atomic.AtomicInteger; -import de.uka.ilkd.key.java.PositionInfo; +import de.uka.ilkd.key.java.ast.PositionInfo; import de.uka.ilkd.key.logic.equality.TermProperty; import de.uka.ilkd.key.logic.label.TermLabel; import de.uka.ilkd.key.logic.op.*; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingProperty.java index 4e2c9488dc4..ba4d8b4f0a4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingProperty.java @@ -3,8 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.logic.equality; -import de.uka.ilkd.key.java.JavaProgramElement; import de.uka.ilkd.key.java.NameAbstractionTable; +import de.uka.ilkd.key.java.ast.JavaProgramElement; import de.uka.ilkd.key.logic.JavaBlock; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.*; 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 b2cf4836d58..03842ce278e 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 @@ -5,14 +5,13 @@ import java.util.Objects; +import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.*; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.abstraction.Type; import de.uka.ilkd.key.java.ast.ccatch.*; -import de.uka.ilkd.key.java.ast.declaration.ArrayInitializer; +import de.uka.ilkd.key.java.ast.declaration.*; import de.uka.ilkd.key.java.ast.expression.*; -import de.uka.ilkd.key.java.expression.ParenthesizedExpression; -import de.uka.ilkd.key.java.expression.PassiveExpression; import de.uka.ilkd.key.java.ast.expression.Operator; import de.uka.ilkd.key.java.ast.expression.literal.*; import de.uka.ilkd.key.java.ast.expression.operator.*; @@ -61,8 +60,8 @@ public class PrettyPrinter implements Visitor { private final SVInstantiations instantiations; @Nullable private final Services services; - private boolean usePrettyPrinting; - private boolean useUnicodeSymbols; + private final boolean usePrettyPrinting; + private final boolean useUnicodeSymbols; /** creates a new PrettyPrinter */ public PrettyPrinter(PosTableLayouter out) { @@ -237,14 +236,14 @@ private void endMultilineBracket() { layouter.print(")"); } - private void printReferencePrefix(ReferencePrefix p) { + private void printReferencePrefix(@Nullable ReferencePrefix p) { if (p != null) { p.visit(this); layouter.print("."); } } - private void printArguments(ImmutableArray args) { + private void printArguments(@Nullable ImmutableArray args) { beginMultilineBracket(); if (args != null) { writeCommaList(args); @@ -402,8 +401,7 @@ public void performActionOnSeqReverse( } @Override - public void performActionOnSeqPut( - de.uka.ilkd.key.java.expression.operator.adt.SeqPut x) { + public void performActionOnSeqPut(SeqPut x) { printDLFunctionOperator("\\seq_upd", x); } @@ -505,7 +503,7 @@ public void performActionOnSuperArrayDeclaration(SuperArrayDeclaration x) { } @Override - public void performActionOnParameterDeclaration(ParameterDeclaration x) { + public void performActionOnParameterDeclaration(@Nullable ParameterDeclaration x) { performActionOnVariableDeclaration(x); } @@ -587,15 +585,14 @@ public void performActionOnMergeContract(MergeContract x) { layouter.print("//@ merge-contract"); } - private void performActionOnType(Type type) { + private void performActionOnType(@Nullable Type type) { if (type == null) { - l.print("unknown"); - } else if (type instanceof ArrayDeclaration) { - var arr = (ArrayDeclaration) type; + layouter.print("unknown"); + } else if (type instanceof ArrayDeclaration arr) { performActionOnType(arr.getBaseType().getKeYJavaType().getJavaType()); - l.print("[]"); + layouter.print("[]"); } else { - l.print(type.getFullName()); + layouter.print(type.getFullName()); } } @@ -619,10 +616,10 @@ public void performActionOnTypeReference(TypeReference x, boolean fullTypeNames) } } - private void printTypeReference(ReferencePrefix prefix, KeYJavaType type, + private void printTypeReference(ReferencePrefix prefix, @Nullable KeYJavaType type, ProgramElementName name, boolean fullTypeNames) { printReferencePrefix(prefix); - if (fullTypeNames) { + if (fullTypeNames && type != null) { layouter.print(type.getFullName()); } else { performActionOnProgramElementName(name); @@ -688,9 +685,9 @@ public void performActionOnCompilationUnit(CompilationUnit x) { } for (int i = 0; i < x.getDeclarations().size(); i++) { if (i != 0) { - l.nl(); + layouter.nl(); } - l.nl(); + layouter.nl(); x.getDeclarations().get(i).visit(this); } } @@ -698,8 +695,8 @@ public void performActionOnCompilationUnit(CompilationUnit x) { @Override public void performActionOnClassDeclaration(ClassDeclaration x) { - l.beginC(); - l.beginC(0); + layouter.beginC(); + layouter.beginC(0); ImmutableArray mods = x.getModifiers(); boolean hasMods = mods != null && !mods.isEmpty(); if (hasMods) { @@ -712,33 +709,34 @@ public void performActionOnClassDeclaration(ClassDeclaration x) { layouter.keyWord("class").print(" "); performActionOnProgramElementName(x.getProgramElementName()); } - l.end(); + layouter.end(); if (x.getExtendedTypes() != null && x.getExtendedTypes().getChildCount() != 0) { - l.brk().beginC(0); + layouter.brk().beginC(0); performActionOnExtends(x.getExtendedTypes()); - l.end(); + layouter.end(); } if (x.getImplementedTypes() != null && x.getImplementedTypes().getChildCount() != 0) { - l.brk(); + layouter.brk(); performActionOnImplements(x.getImplementedTypes()); } // not an anonymous class if (x.getProgramElementName() != null) { layouter.print(" "); } - l.end(); + layouter.end(); performActionOnMemberDeclarations(x.getMembers()); } - private void performActionOnMemberDeclarations(ImmutableArray members) { + private void performActionOnMemberDeclarations( + @Nullable ImmutableArray members) { if (members != null && !members.isEmpty()) { beginBlock(); for (int i = 0; i < members.size(); ++i) { if (i != 0) { - l.nl(); + layouter.nl(); } - l.nl(); + layouter.nl(); members.get(i).visit(this); } endBlock(); @@ -763,11 +761,11 @@ public void performActionOnInterfaceDeclaration(InterfaceDeclaration x) { performActionOnProgramElementName(x.getProgramElementName()); } if (x.getExtendedTypes() != null && x.getExtendedTypes().getChildCount() != 0) { - l.print(" "); + layouter.print(" "); performActionOnExtends(x.getExtendedTypes()); } - l.print(" "); - l.end(); + layouter.print(" "); + layouter.end(); performActionOnMemberDeclarations(x.getMembers()); } @@ -783,7 +781,7 @@ public void performActionOnLocalVariableDeclaration(LocalVariableDeclaration x) } @Override - public void performActionOnVariableDeclaration(VariableDeclaration x) { + public void performActionOnVariableDeclaration(@Nullable VariableDeclaration x) { layouter.beginI(); ImmutableArray modifiers = x.getModifiers(); if (modifiers != null && !modifiers.isEmpty()) { @@ -801,7 +799,7 @@ public void performActionOnVariableDeclaration(VariableDeclaration x) { @Override public void performActionOnMethodDeclaration(MethodDeclaration x) { - l.beginC(0); + layouter.beginC(0); ImmutableArray mods = x.getModifiers(); boolean hasMods = mods != null && !mods.isEmpty(); if (hasMods) { @@ -827,10 +825,10 @@ public void performActionOnMethodDeclaration(MethodDeclaration x) { performActionOnThrows(x.getThrown()); } if (x.getBody() != null) { - l.print(" ").end(); + layouter.print(" ").end(); printStatementBlock(x.getBody()); } else { - l.print(";").end(); + layouter.print(";").end(); } } @@ -848,7 +846,7 @@ public void performActionOnClassInitializer(ClassInitializer x) { } protected void performActionOnStatement(SourceElement s) { - l.beginRelativeC(0); + layouter.beginRelativeC(0); boolean validStatement = !(s instanceof CatchAllStatement || s instanceof ProgramPrefix || s instanceof TypeDeclarationContainer); if (validStatement) { @@ -860,7 +858,7 @@ protected void performActionOnStatement(SourceElement s) { } if (!(s instanceof BranchStatement) && !(s instanceof StatementContainer) && !(s instanceof TypeDeclarationContainer)) { - l.print(";"); + layouter.print(";"); } layouter.end(); } @@ -880,7 +878,7 @@ private void endBlock() { } public boolean printStatementBlock(StatementBlock x) { - boolean emptyBlock = x.getBody() == null || x.getBody().isEmpty(); + boolean emptyBlock = x.getBody().isEmpty(); if (emptyBlock) { // We have an empty statement block ... markStart(x); @@ -900,9 +898,9 @@ public boolean printStatementBlock(StatementBlock x) { @Override public void performActionOnBreak(Break x) { - l.keyWord("break"); + layouter.keyWord("break"); if (x.getLabel() != null) { - l.brk(); + layouter.brk(); x.getLabel().visit(this); } } @@ -955,7 +953,7 @@ private boolean handleBlockOrSingleStatement(Statement body) { } } - private boolean handleBlockStatementOrEmpty(Statement body, boolean includeBody) { + private boolean handleBlockStatementOrEmpty(@Nullable Statement body, boolean includeBody) { if (includeBody) { if (body == null || body instanceof EmptyStatement) { layouter.print(";"); @@ -978,9 +976,7 @@ public void performActionOnDo(Do x, boolean includeBody) { layouter.keyWord("while"); layouter.print(" "); beginMultilineBracket(); - if (x.getGuard() != null) { - x.getGuard().visit(this); - } + x.getGuard().visit(this); endMultilineBracket(); layouter.print(";"); } @@ -1003,9 +999,7 @@ public void performActionOnEnhancedFor(EnhancedFor x, boolean includeBody) { layouter.print(" :"); layouter.brk(); - if (x.getGuard() != null) { - x.getGuardExpression().visit(this); - } + x.getGuardExpression().visit(this); endMultilineBracket(); @@ -1120,7 +1114,9 @@ public void performActionOnSwitch(Switch x, boolean includeBranches) { } } - private void printTryLike(String name, StatementBlock body, ImmutableArray branches) { + private void printTryLike(String name, + @Nullable StatementBlock body, + @Nullable ImmutableArray branches) { layouter.keyWord(name); layouter.print(" "); if (body != null) { @@ -1258,20 +1254,20 @@ public void performActionOnImport(Import x) { @Override public void performActionOnExtends(Extends x) { if (x.getSupertypes() != null) { - l.beginC(); - l.keyWord("extends").brk(); + layouter.beginC(); + layouter.keyWord("extends").brk(); writeCommaList(x.getSupertypes()); - l.end(); + layouter.end(); } } @Override public void performActionOnImplements(Implements x) { if (x.getSupertypes() != null) { - l.beginC(); - l.keyWord("implements").brk(); + layouter.beginC(); + layouter.keyWord("implements").brk(); writeCommaList(x.getSupertypes()); - l.end(); + layouter.end(); } } @@ -1659,11 +1655,11 @@ public void performActionOnExecutionContext(ExecutionContext x) { layouter.beginRelativeC(); layouter.print("source="); if (x.getMethodContext() == null) { - l.print("null"); + layouter.print("null"); } else { writeFullMethodSignature(x.getMethodContext()); } - l.print("@"); + layouter.print("@"); x.getTypeReference().visit(this); if (x.getRuntimeInstance() != null) { layouter.print(",").end().brk().beginRelativeC().print("this="); @@ -1722,7 +1718,7 @@ public void performActionOnElse(Else x) { } } - private void printCaseBody(ImmutableArray body) { + private void printCaseBody(@Nullable ImmutableArray body) { if (body != null && !body.isEmpty()) { for (int i = 0; i < body.size(); i++) { Statement statement = body.get(i); @@ -1816,11 +1812,12 @@ public void performActionOnSchemaVariable(SchemaVariable x) { } @Override - public void performActionOnEmptyStatement(EmptyStatement x) {} + public void performActionOnEmptyStatement(EmptyStatement x) { + } @Override public void performActionOnComment(Comment x) { - // l.print("/* " + x.getText().trim() + " */"); + // layouter.print("/* " + x.getText().trim() + " */"); } @Override @@ -1929,7 +1926,7 @@ public void performActionOnCcatchBreakWildcardParameterDeclaration( @Override public void performActionOnCcatchContinueWildcardParameterDeclaration( CcatchContinueWildcardParameterDeclaration x) { - l.keyWord("\\Continue").brk().print("*"); + layouter.keyWord("\\Continue").brk().print("*"); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java index b4105efdb91..a206b4b0cbb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java @@ -10,7 +10,7 @@ import de.uka.ilkd.key.java.JavaInfo; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.java.Statement; +import de.uka.ilkd.key.java.ast.Statement; import de.uka.ilkd.key.java.ast.StatementBlock; import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; import de.uka.ilkd.key.java.ast.declaration.ClassDeclaration; @@ -1878,12 +1878,12 @@ public JmlStatementSpec addStatementSpec(Statement statement, JmlStatementSpec s *

* Note: There is a immutability hole in {@link ProgramVariableCollection} due to mutable {@link Map} *

- * For {@link de.uka.ilkd.key.java.statement.JmlAssert} this is the formula behind the assert. - * For {@link de.uka.ilkd.key.java.statement.SetStatement} this is the target and the value terms. + * For {@link de.uka.ilkd.key.java.ast.statement.JmlAssert} this is the formula behind the assert. + * For {@link de.uka.ilkd.key.java.ast.statement.SetStatement} this is the target and the value terms. * You may want to use the index constant for accessing them: - * {@link de.uka.ilkd.key.java.statement.SetStatement#INDEX_TARGET}, - * {@link de.uka.ilkd.key.java.statement.SetStatement#INDEX_VALUE}, - * {@link de.uka.ilkd.key.java.statement.JmlAssert#INDEX_CONDITION} + * {@link de.uka.ilkd.key.java.ast.statement.SetStatement#INDEX_TARGET}, + * {@link de.uka.ilkd.key.java.ast.statement.SetStatement#INDEX_VALUE}, + * {@link de.uka.ilkd.key.java.ast.statement.JmlAssert#INDEX_CONDITION} * * @param vars * @param terms diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/SetStatementRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/SetStatementRule.java index 4cbf982d056..3d4464c0fed 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/SetStatementRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/SetStatementRule.java @@ -7,9 +7,9 @@ import de.uka.ilkd.key.java.JavaTools; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.java.SourceElement; -import de.uka.ilkd.key.java.statement.MethodFrame; -import de.uka.ilkd.key.java.statement.SetStatement; +import de.uka.ilkd.key.java.ast.SourceElement; +import de.uka.ilkd.key.java.ast.statement.MethodFrame; +import de.uka.ilkd.key.java.ast.statement.SetStatement; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.op.Modality; import de.uka.ilkd.key.logic.op.Transformer; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java index b0340b50909..14e9e75c1e8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java @@ -9,12 +9,9 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.ast.ProgramElement; import de.uka.ilkd.key.java.ast.SourceElement; +import de.uka.ilkd.key.java.ast.Statement; import de.uka.ilkd.key.java.ast.StatementBlock; -import de.uka.ilkd.key.java.ast.statement.JavaStatement; -import de.uka.ilkd.key.java.ast.statement.JmlAssert; -import de.uka.ilkd.key.java.ast.statement.LoopStatement; -import de.uka.ilkd.key.java.ast.statement.MergePointStatement; -import de.uka.ilkd.key.java.ast.statement.MethodFrame; +import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.java.visitor.JavaASTVisitor; import de.uka.ilkd.key.ldt.HeapLDT; import de.uka.ilkd.key.logic.Term; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java index c2b596da09d..2c8df2c3ce7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java @@ -16,11 +16,7 @@ import de.uka.ilkd.key.java.ast.declaration.ClassDeclaration; import de.uka.ilkd.key.java.ast.declaration.InterfaceDeclaration; import de.uka.ilkd.key.java.ast.declaration.TypeDeclaration; -import de.uka.ilkd.key.java.ast.statement.JmlAssert; -import de.uka.ilkd.key.java.ast.statement.LabeledStatement; -import de.uka.ilkd.key.java.ast.statement.LoopStatement; -import de.uka.ilkd.key.java.ast.statement.MergePointStatement; -import de.uka.ilkd.key.java.statement.SetStatement; +import de.uka.ilkd.key.java.ast.statement.*; import de.uka.ilkd.key.java.visitor.JavaASTCollector; import de.uka.ilkd.key.java.visitor.JavaASTWalker; import de.uka.ilkd.key.logic.op.IProgramMethod; diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java index 0e2969608b0..91d82aa52cc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java @@ -19,7 +19,6 @@ import de.uka.ilkd.key.java.ast.declaration.modifier.Public; import de.uka.ilkd.key.java.ast.declaration.modifier.VisibilityModifier; import de.uka.ilkd.key.java.ast.statement.*; -import de.uka.ilkd.key.java.statement.SetStatement; import de.uka.ilkd.key.ldt.HeapLDT; import de.uka.ilkd.key.ldt.HeapLDT.SplitFieldName; import de.uka.ilkd.key.ldt.JavaDLTheory; diff --git a/key.core/src/test/java/de/uka/ilkd/key/nparser/AdtTests.java b/key.core/src/test/java/de/uka/ilkd/key/nparser/AdtTests.java index 99c5972b1ab..500a5c78278 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/nparser/AdtTests.java +++ b/key.core/src/test/java/de/uka/ilkd/key/nparser/AdtTests.java @@ -3,7 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.nparser; -import java.io.File; import java.nio.file.Paths; import java.util.Collection; diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollection.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollection.java index ad6e1d764b4..ebe5753dbd8 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollection.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollection.java @@ -4,10 +4,7 @@ package de.uka.ilkd.key.proof.runallproofs.proofcollection; import java.io.IOException; -import java.util.LinkedHashSet; -import java.util.LinkedList; -import java.util.List; -import java.util.Set; +import java.util.*; import java.util.function.Predicate; import de.uka.ilkd.key.proof.runallproofs.RunAllProofsTestUnit; diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java index 368277bc1dc..63a913f06d7 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java @@ -3,9 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.smt.newsmt2; -import java.io.File; import java.nio.file.Path; -import java.nio.file.Paths; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; @@ -59,7 +57,7 @@ public class TestSMTMod { @Test public void testModSpec() throws ProblemLoaderException { KeYEnvironment env = - KeYEnvironment.load(testCaseDirectory.resolve("smt/modSpec.key")); + KeYEnvironment.load(testCaseDirectory.resolve("smt/modSpec.key")); try { Proof proof = env.getLoadedProof(); assertNotNull(proof); diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/SetStatementTest.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/SetStatementTest.java index 514d89e0392..88caedb1306 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/speclang/SetStatementTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/SetStatementTest.java @@ -8,8 +8,8 @@ import de.uka.ilkd.key.java.JavaInfo; import de.uka.ilkd.key.java.Position; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.java.abstraction.KeYJavaType; -import de.uka.ilkd.key.java.abstraction.PrimitiveType; +import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.ast.abstraction.PrimitiveType; import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.LocationVariable; @@ -69,7 +69,7 @@ public class SetStatementTest { public synchronized void setUp() { if (javaInfo == null) { javaInfo = - new HelperClassForTests().parse(new File(TEST_FILE)).getFirstProof().getJavaInfo(); + HelperClassForTests.parse(new File(TEST_FILE)).getFirstProof().getJavaInfo(); services = javaInfo.getServices(); testClassType = javaInfo.getKeYJavaType("testPackage.TestClass"); } diff --git a/key.java/src/test/java/TranslationTest.java b/key.java/src/test/java/TranslationTest.java index 14cdd5d11d6..29b29c24e52 100644 --- a/key.java/src/test/java/TranslationTest.java +++ b/key.java/src/test/java/TranslationTest.java @@ -61,7 +61,8 @@ void expressions(String javaExpr) { expr.setParentNode(parent); var converted = converter.process(expr); Assertions.assertNotEquals(null, converted); - Assertions.assertInstanceOf(Expression.class, converted, "Unexpected type: " + converted.getClass()); + Assertions.assertInstanceOf(Expression.class, converted, + "Unexpected type: " + converted.getClass()); System.out.println(converted); } } diff --git a/settings.gradle b/settings.gradle index 2c1d4a7a4e4..3aae1eb560a 100644 --- a/settings.gradle +++ b/settings.gradle @@ -10,7 +10,7 @@ include "key.core.testgen" include "key.core.proof_references" include "key.core.example" include "key.core.symbolic_execution.example" -include 'recoder' +//include 'recoder' include 'keyext.ui.testgen' include 'keyext.proofmanagement' include 'keyext.exploration'