From f8d5a1c4abf1639d70390210d730bacf10767d9e Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Fri, 3 May 2024 17:53:55 +0200 Subject: [PATCH 1/6] wip --- key.core/build.gradle | 17 ++ .../java/declaration/ArrayDeclaration.java | 3 +- .../key/java/reference/FieldReference.java | 3 +- .../java/de/uka/ilkd/key/ldt/BooleanLDT.java | 12 +- .../java/de/uka/ilkd/key/ldt/CharListLDT.java | 14 +- .../java/de/uka/ilkd/key/ldt/DoubleLDT.java | 7 +- .../java/de/uka/ilkd/key/ldt/FloatLDT.java | 60 +++--- .../java/de/uka/ilkd/key/ldt/FreeLDT.java | 10 +- .../java/de/uka/ilkd/key/ldt/HeapLDT.java | 82 ++++----- .../java/de/uka/ilkd/key/ldt/IntegerLDT.java | 28 ++- .../de/uka/ilkd/key/ldt/JavaDLTheory.java | 16 +- .../main/java/de/uka/ilkd/key/ldt/LDT.java | 27 ++- .../java/de/uka/ilkd/key/ldt/LocSetLDT.java | 11 +- .../main/java/de/uka/ilkd/key/ldt/MapLDT.java | 13 +- .../de/uka/ilkd/key/ldt/PermissionLDT.java | 12 +- .../java/de/uka/ilkd/key/ldt/RealLDT.java | 8 +- .../main/java/de/uka/ilkd/key/ldt/SeqLDT.java | 11 +- .../java/de/uka/ilkd/key/ldt/SortLDT.java | 9 +- .../de/uka/ilkd/key/ldt/package-info.java | 4 +- .../uka/ilkd/key/macros/AlternativeMacro.java | 7 +- .../ilkd/key/macros/DoWhileFinallyMacro.java | 4 +- .../de/uka/ilkd/key/macros/ProofMacro.java | 3 +- .../ilkd/key/macros/SequentialProofMacro.java | 2 +- .../ilkd/key/macros/scripts/EngineState.java | 12 +- .../ilkd/key/macros/scripts/FocusCommand.java | 7 +- .../ilkd/key/macros/scripts/MacroCommand.java | 53 +++--- .../key/macros/scripts/RewriteCommand.java | 2 + .../ilkd/key/macros/scripts/RuleCommand.java | 77 ++++---- .../ilkd/key/macros/scripts/ScriptNode.java | 24 +-- .../ilkd/key/macros/scripts/SetCommand.java | 8 +- .../scripts/meta/DescriptionFacade.java | 3 +- .../key/macros/scripts/meta/package-info.java | 7 + .../ilkd/key/macros/scripts/package-info.java | 12 +- .../nparser/builder/ExpressionBuilder.java | 2 +- .../java/de/uka/ilkd/key/pp/LogicPrinter.java | 171 +++++++++--------- .../key/proof/io/OutputStreamProofSaver.java | 7 +- .../rule/metaconstruct/MemberPVToField.java | 3 +- .../settings/AbstractPropertiesSettings.java | 16 +- .../uka/ilkd/key/settings/ChoiceSettings.java | 3 +- .../uka/ilkd/key/settings/Configuration.java | 114 ++++++------ .../ilkd/key/settings/FeatureSettings.java | 18 +- .../key/speclang/DependencyContractImpl.java | 3 +- .../uka/ilkd/key/speclang/LoopSpecImpl.java | 3 +- .../key/speclang/WellDefinednessCheck.java | 3 +- .../ilkd/key/speclang/njml/Translator.java | 3 +- .../java/de/uka/ilkd/key/util/MiscTools.java | 37 ++-- .../key/util/parsing/BuildingException.java | 8 +- .../key/util/parsing/SyntaxErrorReporter.java | 43 +++-- .../ilkd/key/util/parsing/package-info.java | 7 + .../key/gui/DependencyContractCompletion.java | 3 +- keyext.exploration/build.gradle | 19 +- 51 files changed, 526 insertions(+), 505 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/package-info.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/util/parsing/package-info.java diff --git a/key.core/build.gradle b/key.core/build.gradle index 80e648e785c..464a3b9233a 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -266,3 +266,20 @@ task generateRAPUnitTests(type: JavaExec) { sourceSets.test.java.srcDirs("$buildDir/generated-src/rap/") sourcesJar.dependsOn(runAntlr4Jml, runAntlr4Key, compileJavacc, generateGrammarSource) + + +checkerFramework { + if(System.getProperty("ENABLE_NULLNESS")) { + checkers = [ + "org.checkerframework.checker.nullness.NullnessChecker", + ] + extraJavacArgs = [ + "-AonlyDefs=^de\\.uka\\.ilkd\\.key\\.(ldt|macros|settings)", + "-Xmaxerrs", "10000", + "-Astubs=$rootDir/key.util/src/main/checkerframework:permit-nullness-assertion-exception.astub", + "-AstubNoWarnIfNotFound", + "-Werror", + "-Aversion", + ] + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ArrayDeclaration.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ArrayDeclaration.java index c432502f14d..092dfe36610 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ArrayDeclaration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/ArrayDeclaration.java @@ -207,8 +207,7 @@ public static ProgramElementName createName(TypeReference basetype) { } else if (javaBasetype instanceof PrimitiveType) { return ((PrimitiveType) javaBasetype).getArrayElementName(); } - assert false; - return null; + throw new RuntimeException("Not Implemented"); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/FieldReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/FieldReference.java index 0616f1b3c7e..9f904b577b7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/FieldReference.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/FieldReference.java @@ -8,6 +8,7 @@ import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.op.ProgramVariable; +import org.jspecify.annotations.Nullable; import org.key_project.util.ExtList; @@ -28,7 +29,7 @@ protected FieldReference(ReferencePrefix prefix) { this.prefix = prefix; } - public FieldReference(ProgramVariable pv, ReferencePrefix prefix) { + public FieldReference(ProgramVariable pv, @Nullable ReferencePrefix prefix) { this(pv, prefix, PositionInfo.UNDEFINED); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/BooleanLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/BooleanLDT.java index 1167d63cb49..f1d9169f977 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/BooleanLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/BooleanLDT.java @@ -15,6 +15,7 @@ import de.uka.ilkd.key.logic.op.JFunction; import de.uka.ilkd.key.util.Debug; +import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; import org.key_project.util.ExtList; @@ -106,7 +107,7 @@ public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term s @Override - public Term translateLiteral(Literal lit, Services services) { + public @Nullable Term translateLiteral(Literal lit, Services services) { if (lit instanceof BooleanLiteral) { return (((BooleanLiteral) lit).getValue() ? term_bool_true : term_bool_false); } @@ -119,8 +120,7 @@ public Term translateLiteral(Literal lit, Services services) { public JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Services services, ExecutionContext ec) { - assert false; - return null; + throw new RuntimeException("Not Implemented"); } @@ -137,8 +137,7 @@ public Expression translateTerm(Term t, ExtList children, Services services) { } else if (t.op() == bool_false) { return BooleanLiteral.FALSE; } else { - assert false : "BooleanLDT: Cannot convert term to program: " + t; - return null; + throw new AssertionError("BooleanLDT: Cannot convert term to program: " + t); } } @@ -148,8 +147,7 @@ public Type getType(Term t) { if (t.sort() == targetSort()) { return PrimitiveType.JAVA_BOOLEAN; } else { - assert false : "BooleanLDT: Cannot get Java type for term: " + t; - return null; + throw new AssertionError("BooleanLDT: Cannot get Java type for term: " + t); } } } 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 19f537f4601..a22348b9420 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 @@ -22,6 +22,8 @@ import org.jspecify.annotations.Nullable; +import java.util.Objects; + public final class CharListLDT extends LDT { @@ -56,7 +58,7 @@ public final class CharListLDT extends LDT { // ------------------------------------------------------------------------- public CharListLDT(TermServices services) { - super(NAME, services.getNamespaces().sorts().lookup(SeqLDT.NAME), services); + super(NAME, Objects.requireNonNull(services.getNamespaces().sorts().lookup(SeqLDT.NAME)), services); clIndexOfChar = addFunction(services, "clIndexOfChar"); clIndexOfCl = addFunction(services, "clIndexOfCl"); clLastIndexOfChar = addFunction(services, "clLastIndexOfChar"); @@ -98,7 +100,7 @@ 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()); } } @@ -186,7 +188,7 @@ public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term s @Override - public Term translateLiteral(Literal lit, Services services) { + public @Nullable Term translateLiteral(Literal lit, Services services) { final SeqLDT seqLDT = services.getTypeConverter().getSeqLDT(); final TermBuilder tb = services.getTermBuilder(); final Term term_empty = tb.func(seqLDT.getSeqEmpty()); @@ -219,8 +221,7 @@ public Term translateLiteral(Literal lit, Services services) { @Override public JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Services serv, ExecutionContext ec) { - assert false; - return null; + throw new RuntimeException("Not Implemented"); } @@ -244,8 +245,7 @@ public Expression translateTerm(Term t, ExtList children, Services services) { @Override public Type getType(Term t) { - assert false; - return null; + throw new RuntimeException("Not Implemented"); } @Nullable 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 57319dc0fba..8e50312eb24 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 @@ -14,6 +14,7 @@ import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.JFunction; +import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; import org.key_project.util.ExtList; @@ -154,7 +155,7 @@ public Term translateLiteral(Literal lit, Services services) { } @Override - public JFunction getFunctionFor(String op, Services services) { + public @Nullable JFunction getFunctionFor(String op, Services services) { return switch (op) { case "gt" -> getGreaterThan(); case "geq" -> getGreaterOrEquals(); @@ -181,7 +182,7 @@ public JFunction getFunctionFor(String op, Services services) { } @Override - public JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, + public @Nullable JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Services services, ExecutionContext ec) { if (op instanceof Negative) { @@ -215,7 +216,7 @@ public DoubleLiteral translateTerm(Term t, ExtList children, Services services) @Override - public Type getType(Term t) { + public @Nullable Type getType(Term t) { if (t.sort() == targetSort()) { return PrimitiveType.JAVA_DOUBLE; } else { 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 e209a5772fe..cf38887fc93 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 @@ -13,7 +13,7 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.JFunction; - +import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; import org.key_project.logic.op.Function; import org.key_project.util.ExtList; @@ -96,7 +96,7 @@ public FloatLDT(TermServices services) { @Override public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term[] subs, - Services services, ExecutionContext ec) { + Services services, ExecutionContext ec) { if (subs.length == 1) { return isResponsible(op, subs[0], services, ec); } else if (subs.length == 2) { @@ -107,7 +107,7 @@ public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term[] @Override public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term left, Term right, - Services services, ExecutionContext ec) { + Services services, ExecutionContext ec) { return left != null && left.sort().extendsTrans(targetSort()) && right != null && right.sort().extendsTrans(targetSort()) && getFunctionFor(op, services, ec) != null; @@ -115,7 +115,7 @@ public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term l @Override public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term sub, - TermServices services, ExecutionContext ec) { + TermServices services, ExecutionContext ec) { return sub != null && sub.sort().extendsTrans(targetSort()) && op instanceof Negative; } @@ -128,9 +128,9 @@ public Term translateLiteral(Literal lit, Services services) { } @Override - public JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, - Services services, - ExecutionContext ec) { + public @Nullable JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, + Services services, + ExecutionContext ec) { if (op instanceof GreaterThan) { return getGreaterThan(); } else if (op instanceof LessThan) { @@ -157,28 +157,28 @@ public JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, } @Override - public JFunction getFunctionFor(String op, Services services) { + public @Nullable JFunction getFunctionFor(String op, Services services) { 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" -> 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; + 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" -> 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; }; } @@ -189,7 +189,7 @@ public boolean hasLiteralFunction(JFunction f) { @Override - public FloatLiteral translateTerm(Term t, ExtList children, Services services) { + public @Nullable FloatLiteral translateTerm(Term t, ExtList children, Services services) { if (!containsFunction((Function) t.op())) { return null; } @@ -209,7 +209,7 @@ public FloatLiteral translateTerm(Term t, ExtList children, Services services) { @Override - public Type getType(Term t) { + public @Nullable Type getType(Term t) { if (t.sort() == targetSort()) { return PrimitiveType.JAVA_FLOAT; } else { diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/FreeLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/FreeLDT.java index 58b49471584..5965a591f3a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/FreeLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/FreeLDT.java @@ -64,9 +64,7 @@ public Term translateLiteral(Literal lit, Services services) { @Override public JFunction getFunctionFor(Operator op, Services services, ExecutionContext ec) { - // TODO Auto-generated method stub - assert false; - return null; + throw new RuntimeException("Not implemented"); } @Override @@ -79,14 +77,12 @@ public Expression translateTerm(Term t, ExtList children, Services services) { if (t.op() instanceof JFunction && hasLiteralFunction((JFunction) t.op())) { return FreeLiteral.INSTANCE; } - assert false; - return null; + throw new RuntimeException("Not implemented"); } @Override public Type getType(Term t) { - assert false; - return null; + throw new RuntimeException("Not implemented"); } public Function getAtom() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/HeapLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/HeapLDT.java index 1e93af66fc3..6428c3c8f53 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/HeapLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/HeapLDT.java @@ -17,7 +17,7 @@ import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.proof.init.JavaProfile; import de.uka.ilkd.key.proof.io.ProofSaver; - +import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; import org.key_project.logic.Named; import org.key_project.logic.op.Function; @@ -27,7 +27,7 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; -import org.jspecify.annotations.Nullable; +import java.util.Objects; /** @@ -45,8 +45,7 @@ public final class HeapLDT extends LDT { public static final Name SAVED_HEAP_NAME = new Name("savedHeap"); public static final Name PERMISSION_HEAP_NAME = new Name("permissions"); public static final Name[] VALID_HEAP_NAMES = - { BASE_HEAP_NAME, SAVED_HEAP_NAME, PERMISSION_HEAP_NAME }; - + {BASE_HEAP_NAME, SAVED_HEAP_NAME, PERMISSION_HEAP_NAME}; // additional sorts @@ -80,11 +79,15 @@ public final class HeapLDT extends LDT { private final JFunction reach; private final Function prec; + // heaps + final LocationVariable heapBase; + final LocationVariable heapSaved; + final @Nullable LocationVariable heapPermission; + // heap pv private ImmutableList heaps; - // ------------------------------------------------------------------------- // constructors // ------------------------------------------------------------------------- @@ -94,7 +97,7 @@ public HeapLDT(TermServices services) { final Namespace sorts = services.getNamespaces().sorts(); final Namespace progVars = services.getNamespaces().programVariables(); - fieldSort = sorts.lookup(new Name("Field")); + fieldSort = Objects.requireNonNull(sorts.lookup(new Name("Field"))); select = addSortDependingFunction(services, SELECT_NAME.toString()); store = addFunction(services, "store"); create = addFunction(services, "create"); @@ -106,22 +109,23 @@ public HeapLDT(TermServices services) { classPrepared = addSortDependingFunction(services, ""); classInitialized = addSortDependingFunction(services, ""); classInitializationInProgress = - addSortDependingFunction(services, ""); + addSortDependingFunction(services, ""); classErroneous = addSortDependingFunction(services, ""); length = addFunction(services, "length"); nullFunc = addFunction(services, "null"); acc = addFunction(services, "acc"); reach = addFunction(services, "reach"); prec = addFunction(services, "prec"); + heapBase = (LocationVariable) Objects.requireNonNull(progVars.lookup(BASE_HEAP_NAME)); + heapSaved = (LocationVariable) Objects.requireNonNull(progVars.lookup(SAVED_HEAP_NAME)); heaps = ImmutableSLList.nil() - .append((LocationVariable) progVars.lookup(BASE_HEAP_NAME)) - .append((LocationVariable) progVars.lookup(SAVED_HEAP_NAME)); - if (services instanceof Services s) { - if (s.getProfile() instanceof JavaProfile) { - if (((JavaProfile) s.getProfile()).withPermissions()) { - heaps = heaps.append((LocationVariable) progVars.lookup(PERMISSION_HEAP_NAME)); - } - } + .append(heapBase) + .append(heapSaved); + if (services instanceof Services s && s.getProfile() instanceof JavaProfile jp && jp.withPermissions()) { + heapPermission = (LocationVariable) progVars.lookup(PERMISSION_HEAP_NAME); + heaps = heaps.append(Objects.requireNonNull(heapPermission)); + } else { + heapPermission = null; } wellFormed = addFunction(services, "wellFormed"); } @@ -142,7 +146,6 @@ private String getFieldSymbolName(LocationVariable fieldPV) { } - // ------------------------------------------------------------------------- // public interface // ------------------------------------------------------------------------- @@ -150,10 +153,11 @@ private String getFieldSymbolName(LocationVariable fieldPV) { /** * Wrapper class * - * @param className the class name + * @param className the class name * @param attributeName the attribute name */ - public record SplitFieldName(String className, String attributeName) {} + public record SplitFieldName(String className, String attributeName) { + } /** * Splits a field name. @@ -207,7 +211,7 @@ public static String getPrettyFieldName(Named fieldSymbol) { * Extracts the name of the enclosing class from the name of a constant symbol representing a * field. */ - public static String getClassName(Function fieldSymbol) { + public static @Nullable String getClassName(Function fieldSymbol) { String name = fieldSymbol.name().toString(); int index = name.indexOf("::"); if (index == -1) { @@ -238,7 +242,7 @@ public SortDependingFunction getSelect(Sort instanceSort, TermServices services) * If the passed operator is an instance of "select", this method returns the sort of the * function (identical to its return type); otherwise, returns null. */ - public Sort getSortOfSelect(Operator op) { + public @Nullable Sort getSortOfSelect(Operator op) { if (isSelectOp(op)) { return ((SortDependingFunction) op).getSortDependingOn(); } else { @@ -298,7 +302,7 @@ public JFunction getClassInitialized(Sort instanceSort, TermServices services) { public JFunction getClassInitializationInProgress(Sort instanceSort, - TermServices services) { + TermServices services) { return classInitializationInProgress.getInstanceFor(instanceSort, services); } @@ -338,19 +342,18 @@ public Function getPrec() { public LocationVariable getHeap() { - return heaps.head(); + return heapBase; } public LocationVariable getSavedHeap() { - return heaps.tail().head(); + return heapSaved; } - public ImmutableList getAllHeaps() { return heaps; } - public LocationVariable getHeapForName(Name name) { + public @Nullable LocationVariable getHeapForName(Name name) { for (LocationVariable h : getAllHeaps()) { if (h.name().equals(name)) { return h; @@ -359,7 +362,7 @@ public LocationVariable getHeapForName(Name name) { return null; } - public LocationVariable getPermissionHeap() { + public @Nullable LocationVariable getPermissionHeap() { return heaps.size() > 2 ? heaps.tail().tail().head() : null; } @@ -382,7 +385,7 @@ public JFunction getFieldSymbolForPV(LocationVariable fieldPV, Services services final Name kind = new Name(name.toString().substring(index + 2)); SortDependingFunction firstInstance = - SortDependingFunction.getFirstInstance(kind, services); + SortDependingFunction.getFirstInstance(kind, services); if (firstInstance != null) { Sort sortDependingOn = fieldPV.getContainerType().getSort(); result = firstInstance.getInstanceFor(sortDependingOn, services); @@ -396,8 +399,8 @@ public JFunction getFieldSymbolForPV(LocationVariable fieldPV, Services services heapCount++; } result = new ObserverFunction(kind.toString(), fieldPV.sort(), - fieldPV.getKeYJavaType(), targetSort(), fieldPV.getContainerType(), - fieldPV.isStatic(), new ImmutableArray<>(), heapCount, 1); + fieldPV.getKeYJavaType(), targetSort(), fieldPV.getContainerType(), + fieldPV.isStatic(), new ImmutableArray<>(), heapCount, 1); } else { result = new JFunction(name, fieldSort, new Sort[0], null, true); } @@ -429,37 +432,35 @@ public boolean containsFunction(Function op) { @Override public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term[] subs, - Services services, ExecutionContext ec) { + Services services, ExecutionContext ec) { return false; } @Override public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term left, Term right, - Services services, ExecutionContext ec) { + Services services, ExecutionContext ec) { return false; } @Override public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term sub, - TermServices services, ExecutionContext ec) { + TermServices services, ExecutionContext ec) { return false; } @Override public Term translateLiteral(Literal lit, Services services) { - assert false; - return null; + throw new IllegalStateException("Not implemented"); } @Override public JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Services serv, - ExecutionContext ec) { - assert false; - return null; + ExecutionContext ec) { + throw new IllegalStateException("Not implemented"); } @@ -487,17 +488,16 @@ public Expression translateTerm(Term t, ExtList children, Services services) { } else if (t.sort() == getFieldSort() && t.op() instanceof JFunction && ((Function) t.op()).isUnique()) { return services.getJavaInfo().getAttribute(getPrettyFieldName(t.op()), - getClassName((Function) t.op())); + Objects.requireNonNull(getClassName((Function) t.op()))); } throw new IllegalArgumentException( - "Could not translate " + ProofSaver.printTerm(t, null) + " to program."); + "Could not translate " + ProofSaver.printTerm(t, null) + " to program."); } @Override public Type getType(Term t) { - assert false; - return null; + throw new IllegalStateException("Not implemented"); } 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 a8a37770859..75867035963 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 @@ -19,6 +19,7 @@ import de.uka.ilkd.key.logic.op.Operator; import de.uka.ilkd.key.util.Debug; +import org.checkerframework.checker.initialization.qual.UnknownInitialization; import org.key_project.logic.Name; import org.key_project.logic.op.Function; import org.key_project.util.ExtList; @@ -169,7 +170,7 @@ public IntegerLDT(Services services) { } neglit = addFunction(services, NEGATIVE_LITERAL_STRING); numbers = addFunction(services, NUMBERS_NAME.toString()); - assert sharp.sort() == numbers.argSort(0); + if (sharp.sort() != numbers.argSort(0)) throw new AssertionError(); charID = addFunction(services, CHAR_ID_NAME.toString()); add = addFunction(services, "add"); neg = addFunction(services, "neg"); @@ -290,7 +291,7 @@ private boolean isNumberLiteral(Operator f) { return false; } - private Term makeDigit(int digit, TermBuilder tb) { + private Term makeDigit(@UnknownInitialization IntegerLDT this, int digit, TermBuilder tb) { return tb.func(getNumberSymbol(), tb.func(getNumberLiteralFor(digit), tb.func(getNumberTerminator()))); } @@ -300,12 +301,12 @@ private Term makeDigit(int digit, TermBuilder tb) { // public interface // ------------------------------------------------------------------------- - public JFunction getNumberTerminator() { + public JFunction getNumberTerminator(@UnknownInitialization IntegerLDT this) { return sharp; } - public JFunction getNumberLiteralFor(int number) { + public JFunction getNumberLiteralFor(@UnknownInitialization IntegerLDT this, int number) { if (number < 0 || number > 9) { throw new IllegalArgumentException( "Number literal symbols range from 0 to 9. Requested was:" + number); @@ -320,7 +321,7 @@ public JFunction getNegativeNumberSign() { } - public JFunction getNumberSymbol() { + public JFunction getNumberSymbol(@UnknownInitialization IntegerLDT this) { return numbers; } @@ -631,15 +632,13 @@ public JFunction getCheckedBitwiseXOrLong() { /** * Placeholder for the loop index variable in an enhanced for loop over arrays. Follows the * proposal by David Cok to adapt JML to Java5. - * - * @return */ public JFunction getIndex() { return index; } - public JFunction getInBounds(Type t) { + public @Nullable JFunction getInBounds(Type t) { if (t == PrimitiveType.JAVA_BYTE) { return inByte; } else if (t == PrimitiveType.JAVA_CHAR) { @@ -661,7 +660,7 @@ public JFunction getInBounds(Type t) { * @param t the type * @return in range function */ - public JFunction getSpecInBounds(Type t) { + public @Nullable JFunction getSpecInBounds(Type t) { if (t == PrimitiveType.JAVA_BYTE) { return inRangeByte; } else if (t == PrimitiveType.JAVA_CHAR) { @@ -683,7 +682,7 @@ public JFunction getSpecInBounds(Type t) { * @param t the type * @return the cast */ - public JFunction getSpecCast(Type t) { + public @Nullable JFunction getSpecCast(Type t) { if (t == PrimitiveType.JAVA_BYTE) { return moduloByte; } else if (t == PrimitiveType.JAVA_CHAR) { @@ -712,7 +711,7 @@ public JFunction getSpecCast(Type t) { public JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Services serv, ExecutionContext ec) { // Dead in all examples, removed in commit 1e72a5709053a87cae8d2 - return null; + throw new RuntimeException("Not implemented"); } @Nullable @@ -791,7 +790,7 @@ public String toNumberString(Term t) { } @Override - public Expression translateTerm(Term t, ExtList children, Services services) { + public @Nullable Expression translateTerm(Term t, ExtList children, Services services) { if (!containsFunction((Function) t.op())) { return null; } @@ -811,12 +810,9 @@ public Expression translateTerm(Term t, ExtList children, Services services) { @Override public Type getType(Term t) { - assert false : "IntegerLDT: Cannot get Java type for term: " + t; - return null; + throw new AssertionError("IntegerLDT: Cannot get Java type for term: " + t); } - - /** * returns the function symbol used to represent java-like division of the arithmetical integers * diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java index ce57a7afebb..49e6095c5cd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java @@ -14,7 +14,6 @@ import de.uka.ilkd.key.logic.op.JFunction; import de.uka.ilkd.key.logic.op.SortDependingFunction; import de.uka.ilkd.key.logic.sort.SortImpl; - import org.key_project.logic.Name; import org.key_project.logic.sort.Sort; import org.key_project.util.ExtList; @@ -170,31 +169,26 @@ public boolean isResponsible(Operator op, Term sub, TermServices services, @Override public Term translateLiteral(Literal lit, Services services) { - assert false; - return null; + throw new IllegalStateException("Not implemented."); } @Override public JFunction getFunctionFor(Operator op, Services services, ExecutionContext ec) { - assert false; - return null; + throw new IllegalStateException("Not implemented."); } @Override public boolean hasLiteralFunction(JFunction f) { - assert false; - return false; + throw new IllegalStateException("Not implemented."); } @Override public Expression translateTerm(Term t, ExtList children, Services services) { - assert false; - return null; + throw new IllegalStateException("Not implemented."); } @Override public Type getType(Term t) { - assert false; - return null; + throw new IllegalStateException("Not implemented."); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java index f6c8e741ca6..b2b1321c62d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java @@ -18,6 +18,8 @@ import de.uka.ilkd.key.logic.op.Operator; import de.uka.ilkd.key.logic.op.SortDependingFunction; +import org.checkerframework.checker.initialization.qual.UnderInitialization; +import org.checkerframework.checker.initialization.qual.UnknownInitialization; import org.key_project.logic.Name; import org.key_project.logic.Named; import org.key_project.logic.op.Function; @@ -47,21 +49,18 @@ public abstract class LDT implements Named { // ------------------------------------------------------------------------- protected LDT(Name name, TermServices services) { - sort = services.getNamespaces().sorts().lookup(name); - if (sort == null) { + var s = services.getNamespaces().sorts().lookup(name); + if (s == null) { throw new RuntimeException("LDT " + name + " not found.\n" + "It seems that there are definitions missing from the .key files."); } + this.sort = s; this.name = name; } protected LDT(Name name, Sort targetSort, TermServices services) { sort = targetSort; - if (sort == null) { - throw new RuntimeException("LDT " + name + " not found.\n" - + "It seems that there are definitions missing from the .key files."); - } this.name = name; } @@ -74,7 +73,7 @@ protected LDT(Name name, Sort targetSort, TermServices services) { * * @return the added function (for convenience reasons) */ - protected final JFunction addFunction(JFunction f) { + protected final JFunction addFunction(@UnknownInitialization LDT this, JFunction f) { functions.addSafely(f); return f; } @@ -85,7 +84,7 @@ protected final JFunction addFunction(JFunction f) { * @param funcName the String with the name of the function to look up * @return the added function (for convenience reasons) */ - protected final JFunction addFunction(TermServices services, String funcName) { + protected final JFunction addFunction(@UnknownInitialization LDT this, TermServices services, String funcName) { final Namespace funcNS = services.getNamespaces().functions(); final JFunction f = funcNS.lookup(new Name(funcName)); if (f == null) { @@ -95,8 +94,8 @@ protected final JFunction addFunction(TermServices services, String funcName) { return addFunction(f); } - protected final SortDependingFunction addSortDependingFunction(TermServices services, - String kind) { + protected final SortDependingFunction addSortDependingFunction(@UnknownInitialization LDT this, + TermServices services, String kind) { final SortDependingFunction f = SortDependingFunction.getFirstInstance(new Name(kind), services); assert f != null : "LDT: Sort depending function " + kind + " not found"; @@ -221,7 +220,7 @@ public abstract boolean isResponsible(de.uka.ilkd.key.java.expression.Operator o * @param lit the Literal to be translated * @return the Term that represents the given literal in its logic form */ - public abstract Term translateLiteral(Literal lit, Services services); + public abstract @Nullable Term translateLiteral(Literal lit, Services services); /** * returns the function symbol for the given Java operator. @@ -229,7 +228,7 @@ public abstract boolean isResponsible(de.uka.ilkd.key.java.expression.Operator o * @return the function symbol for the given operation, null if not supported in general or not * supported for this particular operator. */ - public abstract JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, + public abstract @Nullable JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Services services, ExecutionContext ec); /** @@ -253,7 +252,7 @@ public abstract JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operato public abstract boolean hasLiteralFunction(JFunction f); /** Is called whenever hasLiteralFunction() returns true. */ - public abstract Expression translateTerm(Term t, ExtList children, Services services); + public abstract @Nullable Expression translateTerm(Term t, ExtList children, Services services); - public abstract Type getType(Term t); + public abstract @Nullable Type getType(Term t); } 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 5b309635ec6..f3327bcb7d2 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 @@ -155,7 +155,7 @@ public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term l @Override - public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term sub, + public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, @Nullable Term sub, TermServices services, ExecutionContext ec) { return op instanceof Singleton || op instanceof SetUnion || op instanceof Intersect || op instanceof SetMinus || op instanceof AllFields; @@ -183,8 +183,7 @@ public JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Ser } else if (op instanceof AllFields) { return allFields; } - assert false; - return null; + throw new RuntimeException("Not Implemented"); } @@ -199,15 +198,13 @@ public Expression translateTerm(Term t, ExtList children, Services services) { if (t.op().equals(empty)) { return EmptySetLiteral.LOCSET; } - assert false; - return null; + throw new RuntimeException("Not Implemented"); } @Override public Type getType(Term t) { - assert false; - return null; + throw new RuntimeException("Not Implemented"); } @Nullable diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/MapLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/MapLDT.java index b163184b5bc..51056a7aced 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/MapLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/MapLDT.java @@ -14,6 +14,7 @@ import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.JFunction; +import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; import org.key_project.logic.op.Function; import org.key_project.util.ExtList; @@ -47,8 +48,7 @@ public boolean isResponsible(Operator op, Term left, Term right, Services servic } @Override - public boolean isResponsible(Operator op, Term sub, TermServices services, - ExecutionContext ec) { + public boolean isResponsible(Operator op, @Nullable Term sub, TermServices services, ExecutionContext ec) { return false; } @@ -60,8 +60,7 @@ public Term translateLiteral(Literal lit, Services services) { @Override public JFunction getFunctionFor(Operator op, Services serv, ExecutionContext ec) { - assert false; - return null; + throw new RuntimeException("Not Implemented"); } @Override @@ -74,14 +73,12 @@ public Expression translateTerm(Term t, ExtList children, Services services) { if (t.op().equals(mapEmpty)) { return EmptyMapLiteral.INSTANCE; } - assert false; - return null; + throw new RuntimeException("Not Implemented"); } @Override public Type getType(Term t) { - assert false; - return null; + throw new RuntimeException("Not Implemented"); } public Function getMapEmpty() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/PermissionLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/PermissionLDT.java index d2d65597aea..0303223315a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/PermissionLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/PermissionLDT.java @@ -50,14 +50,12 @@ public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term s @Override public Term translateLiteral(Literal lit, Services services) { - assert false : "PermissionLDT: there are no permission literals: " + lit; - return null; + throw new AssertionError("PermissionLDT: there are no permission literals: " + lit); } @Override public JFunction getFunctionFor(Operator op, Services services, ExecutionContext ec) { - assert false : "PermissionLDT: there are no permission operators: " + op; - return null; + throw new AssertionError("PermissionLDT: there are no permission operators: " + op); } @Override @@ -67,13 +65,11 @@ public boolean hasLiteralFunction(JFunction f) { @Override public Expression translateTerm(Term t, ExtList children, Services services) { - assert false : "PermissionLDT: Cannot convert term to program: " + t; - return null; + throw new AssertionError("PermissionLDT: Cannot convert term to program: " + t); } @Override public Type getType(Term t) { - assert false : "PermissionLDT: there are no types associated with permissions " + t; - return null; + throw new AssertionError("PermissionLDT: there are no types associated with permissions " + t); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/RealLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/RealLDT.java index 0d1ab8d120d..9346fcaca56 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/RealLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/RealLDT.java @@ -13,6 +13,7 @@ import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.JFunction; +import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; import org.key_project.util.ExtList; @@ -81,8 +82,7 @@ public Term translateLiteral(Literal lit, Services services) { public JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Services services, ExecutionContext ec) { - assert false; - return null; + throw new RuntimeException("Not Implemented"); } @@ -93,13 +93,13 @@ public boolean hasLiteralFunction(JFunction f) { @Override - public Expression translateTerm(Term t, ExtList children, Services services) { + public @Nullable Expression translateTerm(Term t, ExtList children, Services services) { return null; } @Override - public Type getType(Term t) { + public @Nullable Type getType(Term t) { if (t.sort() == targetSort()) { return PrimitiveType.JAVA_REAL; } else { 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 21122c0e7da..50196862274 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 @@ -131,7 +131,7 @@ public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term l @Override - public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term sub, + public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, @Nullable Term sub, TermServices services, ExecutionContext ec) { return op instanceof SeqSingleton || op instanceof SeqConcat || op instanceof SeqSub || op instanceof SeqReverse || op instanceof SeqIndexOf || op instanceof SeqGet @@ -166,8 +166,7 @@ public JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Ser } else if (op instanceof SeqLength) { return seqLen; } - assert false; - return null; + throw new RuntimeException("Not Implemented"); } @Nullable @@ -191,15 +190,13 @@ public Expression translateTerm(Term t, ExtList children, Services services) { if (t.op().equals(seqEmpty)) { return EmptySeqLiteral.INSTANCE; } - assert false; - return null; + throw new RuntimeException("Not Implemented"); } @Override public Type getType(Term t) { - assert false; - return null; + throw new RuntimeException("Not Implemented"); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/SortLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/SortLDT.java index 734625993e4..dc560b7ceee 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/SortLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/SortLDT.java @@ -61,8 +61,7 @@ public boolean isResponsible(Operator op, Term sub, TermServices services, @Override public Term translateLiteral(Literal lit, Services services) { - assert false; - return null; + throw new RuntimeException("Not Implemented"); } @Override @@ -71,8 +70,7 @@ public JFunction getFunctionFor(Operator op, Services services, ExecutionContext return ssubsort; } - assert false; - return null; + throw new RuntimeException("Not Implemented"); } @Override @@ -92,7 +90,6 @@ public Expression translateTerm(Term t, ExtList children, Services services) { @Override public Type getType(Term t) { - assert false; - return null; + throw new RuntimeException("Not Implemented"); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/package-info.java index 4edf3521570..dd5425badab 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/package-info.java @@ -4,4 +4,6 @@ * programming interface to access the entities declared in these * rule files. */ -package de.uka.ilkd.key.ldt; +@NullMarked package de.uka.ilkd.key.ldt; + +import org.jspecify.annotations.NullMarked; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/AlternativeMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/AlternativeMacro.java index 443052df359..f3cab1b92d7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/AlternativeMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/AlternativeMacro.java @@ -3,8 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.macros; -import java.util.List; - import de.uka.ilkd.key.control.UserInterfaceControl; import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.proof.Goal; @@ -12,9 +10,10 @@ import de.uka.ilkd.key.prover.ProverTaskListener; import de.uka.ilkd.key.prover.TaskStartedInfo.TaskKind; import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; - import org.key_project.util.collection.ImmutableList; +import java.util.List; + /** * The abstract class AlternativeMacro can be used to create compound macros which apply the first * applicable macro (similar to a shortcut disjunction) and then it returns. @@ -28,7 +27,7 @@ public abstract class AlternativeMacro extends AbstractProofMacro { * * This array is created on demand using {@link #createProofMacroArray()}. */ - private ProofMacro[] proofMacros = null; + private ProofMacro[] proofMacros = new ProofMacro[0]; /** * Creates the proof macro array. diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/DoWhileFinallyMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/DoWhileFinallyMacro.java index 78a10143177..b6a2af95183 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/DoWhileFinallyMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/DoWhileFinallyMacro.java @@ -11,6 +11,7 @@ import de.uka.ilkd.key.prover.TaskStartedInfo.TaskKind; import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; +import org.jspecify.annotations.Nullable; import org.key_project.util.collection.ImmutableList; /** @@ -58,7 +59,8 @@ public boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrenc @Override public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, - ImmutableList goals, PosInOccurrence posInOcc, ProverTaskListener listener) + ImmutableList goals, + @Nullable PosInOccurrence posInOcc, ProverTaskListener listener) throws Exception { ProofMacroFinishedInfo info = new ProofMacroFinishedInfo(this, goals); int steps = getMaxSteps(proof); diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacro.java index 29ab3712133..237f9e73d1d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacro.java @@ -14,6 +14,7 @@ import de.uka.ilkd.key.prover.TaskStartedInfo.TaskKind; import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; +import org.jspecify.annotations.Nullable; import org.key_project.util.collection.ImmutableList; /** @@ -91,7 +92,7 @@ public interface ProofMacro { * * @return a constant string, or null */ - String getCategory(); + @Nullable String getCategory(); /** * Gets the description of this macro. diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/SequentialProofMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/SequentialProofMacro.java index 65c3d9f91f4..172ceb50a35 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/SequentialProofMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/SequentialProofMacro.java @@ -36,7 +36,7 @@ public abstract class SequentialProofMacro extends AbstractProofMacro { * * This array is created on demand using {@link #createProofMacroArray()}. */ - private ProofMacro[] proofMacros = null; + private ProofMacro[] proofMacros = new ProofMacro[0]; /** * Creates the proof macro array. 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 7437ebe7c4f..9675dc0c6e4 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 @@ -22,6 +22,7 @@ import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.settings.ProofSettings; +import org.jspecify.annotations.Nullable; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableList; @@ -35,14 +36,11 @@ public class EngineState { private final Proof proof; private final AbbrevMap abbrevMap = new AbbrevMap(); - /** - * nullable - */ - private Consumer observer; + private @Nullable Consumer observer; private File baseFileName = new File("."); private final ValueInjector valueInjector = ValueInjector.createDefault(); - private Goal goal; - private Node lastSetGoalNode; + private @Nullable Goal goal; + private @Nullable Node lastSetGoalNode; /** * If set to true, outputs all commands to observers and console. Otherwise, only shows explicit @@ -91,7 +89,7 @@ public Proof getProof() { * @throws ScriptException If there is no such {@link Goal}, or something else goes wrong. */ @SuppressWarnings("unused") - public @NonNull Goal getFirstOpenGoal(boolean checkAutomatic) throws ScriptException { + public Goal getFirstOpenGoal(boolean checkAutomatic) throws ScriptException { if (proof.closed()) { throw new ProofAlreadyClosedException("The proof is closed already"); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusCommand.java index a27f4613191..01c41db1bb4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusCommand.java @@ -41,19 +41,14 @@ public FocusCommand() { super(Parameters.class); } - static class Parameters { + public static class Parameters { @Option("#2") public Sequent toKeep; } @Override public void execute(Parameters s) throws ScriptException, InterruptedException { - if (s == null) { - throw new ScriptException("Missing 'sequent' argument for focus"); - } - Sequent toKeep = s.toKeep; - hideAll(toKeep); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java index 2a431b1cad5..7a696a9d4e1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java @@ -3,10 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.macros.scripts; -import java.util.HashMap; -import java.util.Map; -import java.util.ServiceLoader; - import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.PosInOccurrence; @@ -20,6 +16,11 @@ import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.prover.TaskStartedInfo; import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; +import org.jspecify.annotations.Nullable; + +import java.util.HashMap; +import java.util.Map; +import java.util.ServiceLoader; public class MacroCommand extends AbstractCommand { private static final Map macroMap = loadMacroMap(); @@ -72,29 +73,29 @@ public void execute(AbstractUserInterfaceControl uiControl, Parameters args, Eng macro.setParameter(macroParam.getKey(), macroParam.getValue()); } catch (IllegalArgumentException e) { throw new ScriptException(String.format( - "Wrong format for parameter %s of macro %s: %s.\nMessage: %s", - macroParam.getKey(), args.macroName, macroParam.getValue(), - e.getMessage())); + "Wrong format for parameter %s of macro %s: %s.\nMessage: %s", + macroParam.getKey(), args.macroName, macroParam.getValue(), + e.getMessage())); } } else { throw new ScriptException(String.format("Unknown parameter %s for macro %s", - macroParam.getKey(), args.macroName)); + macroParam.getKey(), args.macroName)); } } } Goal g = state.getFirstOpenAutomaticGoal(); ProofMacroFinishedInfo info = - ProofMacroFinishedInfo.getDefaultInfo(macro, state.getProof()); + ProofMacroFinishedInfo.getDefaultInfo(macro, state.getProof()); try { uiControl.taskStarted( - new DefaultTaskStartedInfo(TaskStartedInfo.TaskKind.Macro, macro.getName(), 0)); + new DefaultTaskStartedInfo(TaskStartedInfo.TaskKind.Macro, macro.getName(), 0)); final Sequent sequent = g.node().sequent(); PosInOccurrence pio = null; if (args.occ > -1) { pio = new PosInOccurrence(sequent.getFormulabyNr(args.occ + 1), - PosInTerm.getTopLevel(), args.occ + 1 <= sequent.antecedent().size()); + PosInTerm.getTopLevel(), args.occ + 1 <= sequent.antecedent().size()); } final String matchRegEx = args.matches; @@ -107,7 +108,7 @@ public void execute(AbstractUserInterfaceControl uiControl, Parameters args, Eng } } catch (Exception e) { throw new ScriptException( - "Macro '" + args.macroName + "' raised an exception: " + e.getMessage(), e); + "Macro '" + args.macroName + "' raised an exception: " + e.getMessage(), e); } finally { uiControl.taskFinished(info); macro.resetParams(); @@ -124,27 +125,27 @@ public void execute(AbstractUserInterfaceControl uiControl, Parameters args, Eng * @throws ScriptException */ public static PosInOccurrence extractMatchingPio(final Sequent sequent, final String matchRegEx, - final Services services) throws ScriptException { + final Services services) throws ScriptException { PosInOccurrence pio = null; boolean matched = false; for (int i = 1; i < sequent.size() + 1; i++) { final boolean matchesRegex = formatTermString( - LogicPrinter.quickPrintTerm(sequent.getFormulabyNr(i).formula(), services)) - .matches(".*" + matchRegEx + ".*"); + LogicPrinter.quickPrintTerm(sequent.getFormulabyNr(i).formula(), services)) + .matches(".*" + matchRegEx + ".*"); if (matchesRegex) { if (matched) { throw new ScriptException("More than one occurrence of a matching term."); } matched = true; pio = new PosInOccurrence(sequent.getFormulabyNr(i), PosInTerm.getTopLevel(), - i <= sequent.antecedent().size()); + i <= sequent.antecedent().size()); } } if (!matched) { throw new ScriptException( - String.format("Did not find a formula matching regex %s", matchRegEx)); + String.format("Did not find a formula matching regex %s", matchRegEx)); } return pio; @@ -163,16 +164,26 @@ private static String formatTermString(String str) { } public static class Parameters { - /** Macro name parameter */ + /** + * Macro name parameter + */ @Option("#2") public String macroName; - /** Run on formula number "occ" parameter */ + /** + * Run on formula number "occ" parameter + */ @Option(value = "occ", required = false) + @Nullable public Integer occ = -1; - /** Run on formula matching the given regex */ + /** + * Run on formula matching the given regex + */ @Option(value = "matches", required = false) + @Nullable public String matches = null; - /** Variable macro parameters */ + /** + * Variable macro parameters + */ @Varargs(as = String.class, prefix = "arg_") public Map instantiations = new HashMap<>(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RewriteCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RewriteCommand.java index 4c15504162b..6b4ee86087f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RewriteCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RewriteCommand.java @@ -19,6 +19,7 @@ import de.uka.ilkd.key.rule.RewriteTaclet; import de.uka.ilkd.key.rule.TacletApp; +import org.jspecify.annotations.Nullable; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -254,6 +255,7 @@ public static class Parameters { * Formula, where to find {@see find}. */ @Option(value = "formula", required = false) + @Nullable public Term formula; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RuleCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RuleCommand.java index a107e4c8c96..6f2a4582362 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RuleCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RuleCommand.java @@ -3,11 +3,12 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.macros.scripts; -import java.util.*; - import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.*; +import de.uka.ilkd.key.logic.PosInOccurrence; +import de.uka.ilkd.key.logic.PosInTerm; +import de.uka.ilkd.key.logic.SequentFormula; +import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.macros.scripts.meta.Option; import de.uka.ilkd.key.macros.scripts.meta.Varargs; @@ -18,11 +19,13 @@ import de.uka.ilkd.key.proof.RuleAppIndex; import de.uka.ilkd.key.proof.rulefilter.TacletFilter; import de.uka.ilkd.key.rule.*; - +import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; +import java.util.*; + import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY; import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY; @@ -74,21 +77,21 @@ private RuleApp makeRuleApp(Parameters p, EngineState state) throws ScriptExcept final Proof proof = state.getProof(); final Optional maybeBuiltInRule = - proof.getInitConfig().getProfile().getStandardRules().standardBuiltInRules().stream() - .filter(r -> r.name().toString().equals(p.rulename)).findAny(); + proof.getInitConfig().getProfile().getStandardRules().standardBuiltInRules().stream() + .filter(r -> r.name().toString().equals(p.rulename)).findAny(); final Optional maybeTaclet = Optional.ofNullable( - proof.getEnv().getInitConfigForEnvironment().lookupActiveTaclet(new Name(p.rulename))); + proof.getEnv().getInitConfigForEnvironment().lookupActiveTaclet(new Name(p.rulename))); if (!maybeBuiltInRule.isPresent() && !maybeTaclet.isPresent()) { /* * (DS, 2019-01-31): Might be a locally introduced taclet, e.g., by hide_left etc. */ final Optional maybeApp = Optional.ofNullable( - state.getFirstOpenAutomaticGoal().indexOfTaclets().lookup(p.rulename)); + state.getFirstOpenAutomaticGoal().indexOfTaclets().lookup(p.rulename)); TacletApp app = maybeApp.orElseThrow( - () -> new ScriptException("Taclet '" + p.rulename + "' not known.")); + () -> new ScriptException("Taclet '" + p.rulename + "' not known.")); if (app.taclet() instanceof FindTaclet) { app = findTacletApp(p, state); @@ -108,7 +111,7 @@ private RuleApp makeRuleApp(Parameters p, EngineState state) throws ScriptExcept return instantiateTacletApp(p, state, proof, theApp); } else { IBuiltInRuleApp builtInRuleApp = // - builtInRuleApp(p, state, maybeBuiltInRule.get()); + builtInRuleApp(p, state, maybeBuiltInRule.get()); if (builtInRuleApp.isSufficientlyComplete()) { builtInRuleApp = builtInRuleApp.forceInstantiate(state.getFirstOpenAutomaticGoal()); } @@ -116,9 +119,9 @@ private RuleApp makeRuleApp(Parameters p, EngineState state) throws ScriptExcept } } - private TacletApp instantiateTacletApp(final Parameters p, final EngineState state, - final Proof proof, final TacletApp theApp) throws ScriptException { - TacletApp result = theApp; + private @Nullable TacletApp instantiateTacletApp(final Parameters p, final EngineState state, + final Proof proof, final TacletApp theApp) throws ScriptException { + TacletApp result; Services services = proof.getServices(); ImmutableList assumesCandidates = theApp @@ -147,7 +150,7 @@ private TacletApp instantiateTacletApp(final Parameters p, final EngineState sta * "\newPV", Skolem terms etc. */ final TacletApp maybeInstApp = result.tryToInstantiateAsMuchAsPossible( - services.getOverlay(state.getFirstOpenAutomaticGoal().getLocalNamespaces())); + services.getOverlay(state.getFirstOpenAutomaticGoal().getLocalNamespaces())); if (maybeInstApp != null) { result = maybeInstApp; @@ -172,7 +175,7 @@ private TacletApp instantiateTacletApp(final Parameters p, final EngineState sta // try to instantiate remaining symbols result = result.tryToInstantiate( - services.getOverlay(state.getFirstOpenAutomaticGoal().getLocalNamespaces())); + services.getOverlay(state.getFirstOpenAutomaticGoal().getLocalNamespaces())); if (result == null) { throw new ScriptException("Cannot instantiate this rule"); @@ -180,7 +183,7 @@ private TacletApp instantiateTacletApp(final Parameters p, final EngineState sta if (recheckMatchConditions) { final MatchConditions appMC = - result.taclet().getMatcher().checkConditions(result.matchConditions(), services); + result.taclet().getMatcher().checkConditions(result.matchConditions(), services); if (appMC == null) { return null; } else { @@ -192,15 +195,14 @@ private TacletApp instantiateTacletApp(final Parameters p, final EngineState sta } private TacletApp makeNoFindTacletApp(Taclet taclet) { - TacletApp app = NoPosTacletApp.createNoPosTacletApp(taclet); - return app; + return NoPosTacletApp.createNoPosTacletApp(taclet); } private IBuiltInRuleApp builtInRuleApp(Parameters p, EngineState state, BuiltInRule rule) throws ScriptException { final List matchingApps = // - findBuiltInRuleApps(p, state).stream().filter(r -> r.rule().name().equals(rule.name())) - .toList(); + findBuiltInRuleApps(p, state).stream().filter(r -> r.rule().name().equals(rule.name())) + .toList(); if (matchingApps.isEmpty()) { throw new ScriptException("No matching applications."); @@ -215,7 +217,7 @@ private IBuiltInRuleApp builtInRuleApp(Parameters p, EngineState state, BuiltInR } else { if (p.occ >= matchingApps.size()) { throw new ScriptException("Occurence " + p.occ - + " has been specified, but there are only " + matchingApps.size() + " hits."); + + " has been specified, but there are only " + matchingApps.size() + " hits."); } return matchingApps.get(p.occ); @@ -239,7 +241,7 @@ private TacletApp findTacletApp(Parameters p, EngineState state) throws ScriptEx } else { if (p.occ >= matchingApps.size()) { throw new ScriptException("Occurence " + p.occ - + " has been specified, but there are only " + matchingApps.size() + " hits."); + + " has been specified, but there are only " + matchingApps.size() + " hits."); } return matchingApps.get(p.occ); } @@ -248,8 +250,6 @@ private TacletApp findTacletApp(Parameters p, EngineState state) throws ScriptEx private ImmutableList findBuiltInRuleApps(Parameters p, EngineState state) throws ScriptException { final Services services = state.getProof().getServices(); - assert services != null; - final Goal g = state.getFirstOpenAutomaticGoal(); final BuiltInRuleAppIndex index = g.ruleAppIndex().builtInRuleAppIndex(); @@ -260,7 +260,7 @@ private ImmutableList findBuiltInRuleApps(Parameters p, EngineS } allApps = allApps.append( - index.getBuiltInRule(g, new PosInOccurrence(sf, PosInTerm.getTopLevel(), true))); + index.getBuiltInRule(g, new PosInOccurrence(sf, PosInTerm.getTopLevel(), true))); } for (SequentFormula sf : g.node().sequent().succedent()) { @@ -269,7 +269,7 @@ private ImmutableList findBuiltInRuleApps(Parameters p, EngineS } allApps = allApps.append( - index.getBuiltInRule(g, new PosInOccurrence(sf, PosInTerm.getTopLevel(), false))); + index.getBuiltInRule(g, new PosInOccurrence(sf, PosInTerm.getTopLevel(), false))); } return allApps; @@ -278,7 +278,6 @@ private ImmutableList findBuiltInRuleApps(Parameters p, EngineS private ImmutableList findAllTacletApps(Parameters p, EngineState state) throws ScriptException { Services services = state.getProof().getServices(); - assert services != null; TacletFilter filter = new TacletNameFilter(p.rulename); Goal g = state.getFirstOpenAutomaticGoal(); RuleAppIndex index = g.ruleAppIndex(); @@ -291,7 +290,7 @@ private ImmutableList findAllTacletApps(Parameters p, EngineState sta } allApps = allApps.append(index.getTacletAppAtAndBelow(filter, - new PosInOccurrence(sf, PosInTerm.getTopLevel(), true), services)); + new PosInOccurrence(sf, PosInTerm.getTopLevel(), true), services)); } for (SequentFormula sf : g.node().sequent().succedent()) { @@ -300,7 +299,7 @@ private ImmutableList findAllTacletApps(Parameters p, EngineState sta } allApps = allApps.append(index.getTacletAppAtAndBelow(filter, - new PosInOccurrence(sf, PosInTerm.getTopLevel(), false), services)); + new PosInOccurrence(sf, PosInTerm.getTopLevel(), false), services)); } return allApps; @@ -311,18 +310,17 @@ private ImmutableList findAllTacletApps(Parameters p, EngineState sta * {@link Parameters#formula} parameter or its String representation matches the * {@link Parameters#matches} regex. If both parameters are not supplied, always returns true. * - * @param p The {@link Parameters} object. + * @param p The {@link Parameters} object. * @param sf The {@link SequentFormula} to check. * @return true if sf matches. */ - private boolean isFormulaSearchedFor(Parameters p, SequentFormula sf, Services services) - throws ScriptException { + private boolean isFormulaSearchedFor(Parameters p, SequentFormula sf, Services services) { final boolean satisfiesFormulaParameter = - p.formula != null && sf.formula().equalsModProperty(p.formula, RENAMING_PROPERTY); + p.formula != null && sf.formula().equalsModProperty(p.formula, RENAMING_PROPERTY); final boolean satisfiesMatchesParameter = p.matches != null && formatTermString(LogicPrinter.quickPrintTerm(sf.formula(), services)) - .matches(".*" + p.matches + ".*"); + .matches(".*" + p.matches + ".*"); return (p.formula == null && p.matches == null) || satisfiesFormulaParameter || satisfiesMatchesParameter; @@ -348,15 +346,15 @@ private List filterList(Parameters p, ImmutableList list) for (TacletApp tacletApp : list) { if (tacletApp instanceof PosTacletApp pta) { boolean add = - p.on == null || pta.posInOccurrence().subTerm() - .equalsModProperty(p.on, RENAMING_PROPERTY); + p.on == null || pta.posInOccurrence().subTerm() + .equalsModProperty(p.on, RENAMING_PROPERTY); Iterator it = pta.instantiations().svIterator(); while (it.hasNext()) { SchemaVariable sv = it.next(); Term userInst = p.instantiations.get(sv.name().toString()); Object ptaInst = - pta.instantiations().getInstantiationEntry(sv).getInstantiation(); + pta.instantiations().getInstantiationEntry(sv).getInstantiation(); add &= userInst == null || userInst.equalsModProperty(ptaInst, IRRELEVANT_TERM_LABELS_PROPERTY); @@ -374,17 +372,20 @@ public static class Parameters { @Option(value = "#2") public String rulename; @Option(value = "on", required = false) + @Nullable public Term on; @Option(value = "formula", required = false) + @Nullable public Term formula; @Option(value = "occ", required = false) + @Nullable public int occ = -1; /** * Represents a part of a formula (may use Java regular expressions as long as supported by * proof script parser). Rule is applied to the sequent formula which matches that string. */ @Option(value = "matches", required = false) - public String matches = null; + public @Nullable String matches = null; @Varargs(as = Term.class, prefix = "inst_") public Map instantiations = new HashMap<>(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptNode.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptNode.java index 18531d0516b..0c1501e1dba 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptNode.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptNode.java @@ -3,27 +3,27 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.macros.scripts; -import java.util.LinkedList; -import java.util.List; -import java.util.Map; - import de.uka.ilkd.key.proof.Node; - +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import java.util.LinkedList; +import java.util.List; +import java.util.Map; + public class ScriptNode { private static final Logger LOGGER = LoggerFactory.getLogger(ScriptNode.class); private final Map command; private final int fromPos; private final int toPos; - private final ScriptNode parent; + private final @Nullable ScriptNode parent; private final List children = new LinkedList<>(); - private Node proofNode; - private Throwable encounteredException; + private @Nullable Node proofNode; + private @Nullable Throwable encounteredException; - public ScriptNode(ScriptNode parent, Map command, int fromPos, int toPos) { + public ScriptNode(@Nullable ScriptNode parent, Map command, int fromPos, int toPos) { this.parent = parent; this.command = command; this.fromPos = fromPos; @@ -36,7 +36,7 @@ public void addNode(ScriptNode node) { public void dump(int indent) { LOGGER.debug("{} {} {}", " ".repeat(indent), - proofNode == null ? "xxx" : proofNode.serialNr(), command); + proofNode == null ? "xxx" : proofNode.serialNr(), command); for (ScriptNode child : children) { child.dump(indent + 1); } @@ -46,7 +46,7 @@ public Map getCommand() { return command; } - public Node getProofNode() { + public @Nullable Node getProofNode() { return proofNode; } @@ -70,7 +70,7 @@ public void clearChildren() { children.clear(); } - public Throwable getEncounteredException() { + public @Nullable Throwable getEncounteredException() { return encounteredException; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetCommand.java index 9ccd3c2c274..b9b1193c361 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetCommand.java @@ -13,6 +13,7 @@ import de.uka.ilkd.key.strategy.Strategy; import de.uka.ilkd.key.strategy.StrategyFactory; import de.uka.ilkd.key.strategy.StrategyProperties; +import org.jspecify.annotations.Nullable; public class SetCommand extends AbstractCommand { @@ -86,8 +87,7 @@ private Strategy getStrategy(StrategyProperties properties) { // (DS, 2020-04-08) This should not happen -- we already have a proof with that // strategy, there should be a factory for it. - assert false; - return null; + throw new RuntimeException("Not Implemented"); } @Override @@ -98,18 +98,22 @@ public String getName() { public static class Parameters { /** One Step Simplification parameter */ @Option(value = "oss", required = false) + @Nullable public Boolean oneStepSimplification; /** Maximum number of proof steps parameter */ @Option(value = "steps", required = false) + @Nullable public Integer proofSteps; /** Normal key-value setting -- key */ @Option(value = "key", required = false) + @Nullable public String key; /** Normal key-value setting -- value */ @Option(value = "value", required = false) + @Nullable public String value; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/DescriptionFacade.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/DescriptionFacade.java index c1f6c7fda90..ddfd0ff19bc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/DescriptionFacade.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/DescriptionFacade.java @@ -8,6 +8,7 @@ import de.uka.ilkd.key.macros.scripts.ProofScriptCommand; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -32,7 +33,7 @@ public final class DescriptionFacade { * * @see #getProperties */ - private static Properties properties = null; + private static @Nullable Properties properties = null; private DescriptionFacade() { } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/package-info.java new file mode 100644 index 00000000000..5c6f5617587 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/package-info.java @@ -0,0 +1,7 @@ +/** + * @author Alexander Weigl + * @version 1 (03.05.24) + */ +@NullMarked package de.uka.ilkd.key.macros.scripts.meta; + +import org.jspecify.annotations.NullMarked; \ No newline at end of file diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/package-info.java index 232a2bf0b62..9164279fdfe 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/package-info.java @@ -1,13 +1,7 @@ /** - * Proof script commands are a simple proof automation facility. - * - * @see de.uka.ilkd.key.macros.scripts.ProofScriptCommand - * @see de.uka.ilkd.key.macros.scripts.ProofScriptEngine - * @see de.uka.ilkd.key.macros.scripts.EngineState - * - * - * @author Mattias Ulbrich * @author Alexander Weigl * @version 1 (29.03.17) */ -package de.uka.ilkd.key.macros.scripts; +@NullMarked package de.uka.ilkd.key.macros.scripts; + +import org.jspecify.annotations.NullMarked; \ No newline at end of file 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 2b5ce808052..674b471b78f 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 @@ -813,7 +813,7 @@ private void markHeapAsExplicit(Term a) { * pm.name().toString().equals(kjt.getFullName() + "::" + mn)) { List arguments = * mapOf(suffix.attribute_or_query_suffix().result.args.argument()); Term[] args = * arguments.toArray(new Term[0]); return getJavaInfo().getStaticProgramMethodTerm(mn, args, - * kjt.getFullName()); } } } assert false; return null; } + * kjt.getFullName()); } } } throw new RuntimeException("Not Implemented"); } */ @Override 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 356b3ed7cb5..1629b12bb76 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 @@ -3,9 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.pp; -import java.util.Iterator; -import java.util.Set; - import de.uka.ilkd.key.control.TermLabelVisibilityManager; import de.uka.ilkd.key.java.JavaInfo; import de.uka.ilkd.key.java.ProgramElement; @@ -26,16 +23,18 @@ import de.uka.ilkd.key.rule.tacletbuilder.TacletGoalTemplate; import de.uka.ilkd.key.util.UnicodeHelper; import de.uka.ilkd.key.util.pp.UnbalancedBlocksException; - +import org.jspecify.annotations.Nullable; import org.key_project.logic.op.Function; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSet; - import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import java.util.Iterator; +import java.util.Set; + import static de.uka.ilkd.key.pp.PosTableLayouter.DEFAULT_LINE_WIDTH; @@ -77,7 +76,7 @@ public class LogicPrinter { private final StorePrinter storePrinter; private QuantifiableVariablePrintMode quantifiableVariablePrintMode = - QuantifiableVariablePrintMode.NORMAL; + QuantifiableVariablePrintMode.NORMAL; private enum QuantifiableVariablePrintMode { NORMAL, WITH_OUT_DECLARATION @@ -88,8 +87,8 @@ private enum QuantifiableVariablePrintMode { * Java programs and a NotationInfo which determines the concrete syntax. * * @param notationInfo the NotationInfo for the concrete syntax - * @param services services. - * @param layouter the layouter to use + * @param services services. + * @param layouter the layouter to use */ public LogicPrinter(NotationInfo notationInfo, Services services, PosTableLayouter layouter) { this.notationInfo = notationInfo; @@ -106,9 +105,9 @@ public LogicPrinter(NotationInfo notationInfo, Services services, PosTableLayout * Creates a LogicPrinter that does not create a position table. * * @param notationInfo the NotationInfo for the concrete syntax - * @param services The Services object + * @param services The Services object */ - public static LogicPrinter purePrinter(NotationInfo notationInfo, Services services) { + public static LogicPrinter purePrinter(NotationInfo notationInfo, @Nullable Services services) { return new LogicPrinter(notationInfo, services, PosTableLayouter.pure()); } @@ -120,7 +119,7 @@ public PosTableLayouter layouter() { } public static SequentViewLogicPrinter quickPrinter(Services services, - boolean usePrettyPrinting, boolean useUnicodeSymbols) { + boolean usePrettyPrinting, boolean useUnicodeSymbols) { final NotationInfo ni = new NotationInfo(); if (services != null) { ni.refresh(services, usePrettyPrinting, useUnicodeSymbols); @@ -135,26 +134,26 @@ public static SequentViewLogicPrinter quickPrinter(Services services, /** * Converts a term to a string. * - * @param t a term. + * @param t a term. * @param services services. * @return the printed term. */ public static String quickPrintTerm(Term t, Services services) { return quickPrintTerm(t, services, NotationInfo.DEFAULT_PRETTY_SYNTAX, - NotationInfo.DEFAULT_UNICODE_ENABLED); + NotationInfo.DEFAULT_UNICODE_ENABLED); } /** * Converts a term to a string. * - * @param t a term. - * @param services services. + * @param t a term. + * @param services services. * @param usePrettyPrinting whether to use pretty-printing. * @param useUnicodeSymbols whether to use unicode symbols. * @return the printed term. */ public static String quickPrintTerm(Term t, Services services, boolean usePrettyPrinting, - boolean useUnicodeSymbols) { + boolean useUnicodeSymbols) { var p = quickPrinter(services, usePrettyPrinting, useUnicodeSymbols); p.printTerm(t); return p.result(); @@ -163,13 +162,13 @@ public static String quickPrintTerm(Term t, Services services, boolean usePretty /** * Converts a semisequent to a string. * - * @param s a semisequent. + * @param s a semisequent. * @param services services. * @return the printed semisequent. */ public static String quickPrintSemisequent(Semisequent s, Services services) { var p = quickPrinter(services, NotationInfo.DEFAULT_PRETTY_SYNTAX, - NotationInfo.DEFAULT_UNICODE_ENABLED); + NotationInfo.DEFAULT_UNICODE_ENABLED); p.printSemisequent(s); return p.result(); } @@ -177,13 +176,13 @@ public static String quickPrintSemisequent(Semisequent s, Services services) { /** * Converts a sequent to a string. * - * @param s a sequent. + * @param s a sequent. * @param services services. * @return the printed sequent. */ public static String quickPrintSequent(Sequent s, Services services) { var p = quickPrinter(services, NotationInfo.DEFAULT_PRETTY_SYNTAX, - NotationInfo.DEFAULT_UNICODE_ENABLED); + NotationInfo.DEFAULT_UNICODE_ENABLED); p.printSequent(s); return p.result(); } @@ -217,9 +216,9 @@ public void setLineWidth(int lineWidth) { * Reprints the sequent. This can be useful if settings like PresentationFeatures or * abbreviations have changed. * - * @param filter The SequentPrintFilter for seq + * @param filter The SequentPrintFilter for seq * @param lineWidth the max. number of character to put on one line (the actual taken linewidth - * is the max of {@link PosTableLayouter#DEFAULT_LINE_WIDTH} and the given value + * is the max of {@link PosTableLayouter#DEFAULT_LINE_WIDTH} and the given value */ public void update(SequentPrintFilter filter, int lineWidth) { setLineWidth(lineWidth); @@ -239,14 +238,14 @@ public void setInstantiation(SVInstantiations instantiations) { /** * Pretty-print a taclet. Line-breaks are taken care of. * - * @param taclet The Taclet to be pretty-printed. - * @param sv The instantiations of the SchemaVariables - * @param showWholeTaclet Should the find, varcond and heuristic part be pretty-printed? + * @param taclet The Taclet to be pretty-printed. + * @param sv The instantiations of the SchemaVariables + * @param showWholeTaclet Should the find, varcond and heuristic part be pretty-printed? * @param declareSchemaVars Should declarations for the schema variables used in the taclet be - * pretty-printed? + * pretty-printed? */ public void printTaclet(Taclet taclet, SVInstantiations sv, boolean showWholeTaclet, - boolean declareSchemaVars) { + boolean declareSchemaVars) { instantiations = sv; quantifiableVariablePrintMode = QuantifiableVariablePrintMode.WITH_OUT_DECLARATION; @@ -432,7 +431,7 @@ protected void printHeuristics(Taclet taclet) { return; } layouter.nl().beginRelativeC().print("\\heuristics(").brk(0); - for (Iterator it = taclet.getRuleSets().iterator(); it.hasNext();) { + for (Iterator it = taclet.getRuleSets().iterator(); it.hasNext(); ) { RuleSet tgt = it.next(); printHeuristic(tgt); if (it.hasNext()) { @@ -505,7 +504,7 @@ protected void printGoalTemplates(Taclet taclet) { } for (final Iterator it = taclet.goalTemplates().reverse().iterator(); it - .hasNext();) { + .hasNext(); ) { printGoalTemplate(it.next()); if (it.hasNext()) { layouter.print(";"); @@ -597,15 +596,15 @@ protected void printSchemaVariable(SchemaVariable sv) { private void printSourceElement(SourceElement element) { new PrettyPrinter(layouter, instantiations, services, - notationInfo.isPrettySyntax(), - notationInfo.isUnicodeEnabled()).print(element); + notationInfo.isPrettySyntax(), + notationInfo.isUnicodeEnabled()).print(element); } /** * Pretty-prints a ProgramElement. * * @param pe You've guessed it, the ProgramElement to be pretty-printedprint(Term t, - * LogicPrinter sp) + * LogicPrinter sp) */ public void printProgramElement(ProgramElement pe) { if (pe instanceof ProgramVariable) { @@ -789,7 +788,7 @@ public void printTerm(Term t) { * * @param t {@link Term} whose visible {@link TermLabel}s will be determined. * @return List of visible {@link TermLabel}s, i.e. labels that are syntactically added to a - * {@link Term} while printing. + * {@link Term} while printing. */ protected ImmutableArray getVisibleTermLabels(Term t) { return t.getLabels(); @@ -1161,8 +1160,8 @@ public void printObserver(Term t, Term tacitHeap) { String p; try { boolean canonical = - obs.isStatic() || ((obs instanceof IProgramMethod) && javaInfo - .isCanonicalProgramMethod((IProgramMethod) obs, keYJavaType)); + obs.isStatic() || ((obs instanceof IProgramMethod) && javaInfo + .isCanonicalProgramMethod((IProgramMethod) obs, keYJavaType)); if (canonical) { p = fieldName; } else { @@ -1308,9 +1307,9 @@ public void printElementOf(Term t, String symbol) { * possible. * * @param name the prefix operator - * @param t whole term - * @param sub the subterm to be printed - * @param ass the associativity for the subterm + * @param t whole term + * @param sub the subterm to be printed + * @param ass the associativity for the subterm */ public void printPrefixTerm(String name, Term t, Term sub, int ass) { layouter.startTerm(1); @@ -1329,8 +1328,8 @@ public void printPrefixTerm(String name, Term t, Term sub, int ass) { * the postfix operator. No line breaks are possible. * * @param name the postfix operator - * @param t the subterm to be printed - * @param ass the associativity for the subterm + * @param t the subterm to be printed + * @param ass the associativity for the subterm */ public void printPostfixTerm(Term t, int ass, String name) { layouter.startTerm(1); @@ -1349,11 +1348,11 @@ public void printPostfixTerm(Term t, int ass, String name) { *

* The subterms are printed using {@link #printTermContinuingBlock(Term)}. * - * @param l the left subterm - * @param assLeft associativity for left subterm - * @param name the infix operator - * @param t whole term - * @param r the right subterm + * @param l the left subterm + * @param assLeft associativity for left subterm + * @param name the infix operator + * @param t whole term + * @param r the right subterm * @param assRight associativity for right subterm */ public void printInfixTerm(Term l, int assLeft, String name, Term t, Term r, int assRight) { @@ -1368,15 +1367,15 @@ public void printInfixTerm(Term l, int assLeft, String name, Term t, Term r, int * {@link #printTermContinuingBlock(Term)} for the idea. Otherwise, like * {@link #printInfixTerm(Term, int, String, Term, Term, int)}. * - * @param l the left subterm - * @param assLeft associativity for left subterm - * @param name the infix operator - * @param t whole term - * @param r the right subterm + * @param l the left subterm + * @param assLeft associativity for left subterm + * @param name the infix operator + * @param t whole term + * @param r the right subterm * @param assRight associativity for right subterm */ public void printInfixTermContinuingBlock(Term l, int assLeft, String name, Term t, Term r, - int assRight) { + int assRight) { boolean isKeyword = false; if (services != null) { LocSetLDT loc = services.getTypeConverter().getLocSetLDT(); @@ -1408,9 +1407,9 @@ public void printInfixTermContinuingBlock(Term l, int assLeft, String name, Term * t * * - * @param l the left brace - * @param r the right brace - * @param t the update term + * @param l the left brace + * @param r the right brace + * @param t the update term * @param ass3 associativity for phi */ public void printUpdateApplicationTerm(String l, String r, Term t, int ass3) { @@ -1484,7 +1483,7 @@ public void printParallelUpdate(String separator, Term t, int ass) { } private void printVariables(ImmutableArray vars, - QuantifiableVariablePrintMode mode) { + QuantifiableVariablePrintMode mode) { int size = vars.size(); for (int j = 0; j != size; j++) { final QuantifiableVariable v = vars.get(j); @@ -1556,16 +1555,16 @@ public void printIfThenElseTerm(Term t, String keyword) { * s * * - * @param l the String used as left brace symbol - * @param v the {@link QuantifiableVariable} to be substituted - * @param t the Term to be used as new value + * @param l the String used as left brace symbol + * @param v the {@link QuantifiableVariable} to be substituted + * @param t the Term to be used as new value * @param ass2 the int defining the associativity for the new value - * @param r the String used as right brace symbol - * @param phi the substituted term/formula + * @param r the String used as right brace symbol + * @param phi the substituted term/formula * @param ass3 the int defining the associativity for phi */ public void printSubstTerm(String l, QuantifiableVariable v, Term t, int ass2, String r, - Term phi, int ass3) { + Term phi, int ass3) { layouter.beginC().print(l); printVariables(new ImmutableArray<>(v), quantifiableVariablePrintMode); layouter.startTerm(2); @@ -1589,11 +1588,11 @@ public void printSubstTerm(String l, QuantifiableVariable v, Term t, int ass2, S * * @param name the name of the quantifier * @param vars the quantified variables (+colon and sort) - * @param phi the quantified formula - * @param ass associativity for phi + * @param phi the quantified formula + * @param ass associativity for phi */ public void printQuantifierTerm(String name, ImmutableArray vars, - Term phi, int ass) { + Term phi, int ass) { layouter.beginC(); layouter.keyWord(name); layouter.print(" "); @@ -1670,9 +1669,9 @@ public void printModalityTerm(String left, JavaBlock jb, String right, Term phi, ta[i] = phi.sub(i); } final Modality m = - Modality.getModality((Modality.JavaModalityKind) o, mod.program()); + Modality.getModality((Modality.JavaModalityKind) o, mod.program()); final Term term = services.getTermFactory().createTerm(m, ta, - phi.boundVars(), null); + phi.boundVars(), null); notationInfo.getNotation(m).print(term, this); return; } @@ -1723,7 +1722,7 @@ public String result() { * {@link #printTermContinuingBlock(Term)}. This currently only makes a difference for infix * operators. * - * @param t the subterm to print + * @param t the subterm to print * @param ass the associativity for this subterm */ protected void maybeParens(Term t, int ass) { @@ -1769,7 +1768,7 @@ public SVInstantiations getInstantiations() { * printInShortForm methods it takes care of meta variable instantiations * * @param attributeProgramName the String of the attribute's program name - * @param t the Term used as reference prefix + * @param t the Term used as reference prefix * @return true if an attribute term shall be printed in short form. */ public boolean printInShortForm(String attributeProgramName, Term t) { @@ -1783,7 +1782,7 @@ public boolean printInShortForm(String attributeProgramName, Term t) { * way * * @param programName the String denoting the program name of the attribute - * @param sort the ObjectSort in whose reachable hierarchy we test for uniqueness + * @param sort the ObjectSort in whose reachable hierarchy we test for uniqueness * @return true if the attribute is uniquely determined */ public boolean printInShortForm(String programName, Sort sort) { @@ -1802,21 +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("<"); - 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); + 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); } } @@ -1828,8 +1827,8 @@ public static String escapeHTML(String text, boolean escapeWhitespace) { * way * * @param programName the String denoting the program name of the attribute - * @param sort the ObjectSort specifying the hierarchy where to test for uniqueness - * @param services the Services class used to access the type hierarchy + * @param sort the ObjectSort specifying the hierarchy where to test for uniqueness + * @param services the Services class used to access the type hierarchy * @return true if the attribute is uniquely determined */ public static boolean printInShortForm(String programName, Sort sort, Services services) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java index 22fb1aba82c..fa6d852b63a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java @@ -47,6 +47,7 @@ import de.uka.ilkd.key.util.KeYConstants; import de.uka.ilkd.key.util.MiscTools; +import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableList; @@ -813,11 +814,11 @@ public static String printProgramElement(ProgramElement pe) { return printer.result(); } - public static String printTerm(Term t, Services serv) { + public static String printTerm(Term t, @Nullable Services serv) { return printTerm(t, serv, false); } - public static String printTerm(Term t, Services serv, boolean shortAttrNotation) { + public static String printTerm(Term t, @Nullable Services serv, boolean shortAttrNotation) { final LogicPrinter logicPrinter = createLogicPrinter(serv, shortAttrNotation); logicPrinter.printTerm(t); return logicPrinter.result(); @@ -854,7 +855,7 @@ private static String printSequent(Sequent val, Services services) { return printer.result(); } - private static LogicPrinter createLogicPrinter(Services serv, boolean shortAttrNotation) { + private static LogicPrinter createLogicPrinter(@Nullable Services serv, boolean shortAttrNotation) { final NotationInfo ni = new NotationInfo(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/MemberPVToField.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/MemberPVToField.java index 38bfb82332d..649f56a7080 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/MemberPVToField.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/MemberPVToField.java @@ -32,8 +32,7 @@ public Term transform(Term term, SVInstantiations svInst, Services services) { } else if (heapLDT.getSortOfSelect(op) != null) { return term.sub(0).sub(2); } else { - assert false; - return null; + throw new RuntimeException("Not Implemented"); } } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java index 08a82f320a3..ef5723e981c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java @@ -8,6 +8,7 @@ import java.util.function.Function; import java.util.stream.Collectors; +import org.checkerframework.checker.initialization.qual.UnknownInitialization; import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; @@ -126,35 +127,40 @@ public void writeSettings(Configuration props) { }); } - protected PropertyEntry createDoubleProperty(String key, double defValue) { + protected PropertyEntry createDoubleProperty(@UnknownInitialization AbstractPropertiesSettings this, + String key, double defValue) { PropertyEntry pe = new DefaultPropertyEntry<>(key, defValue, parseDouble, (it) -> (double) it); propertyEntries.add(pe); return pe; } - protected PropertyEntry createIntegerProperty(String key, int defValue) { + protected PropertyEntry createIntegerProperty(@UnknownInitialization AbstractPropertiesSettings this, + String key, int defValue) { PropertyEntry pe = new DefaultPropertyEntry<>(key, defValue, parseInt, (it) -> Math.toIntExact((Long) it)); propertyEntries.add(pe); return pe; } - protected PropertyEntry createFloatProperty(String key, float defValue) { + protected PropertyEntry createFloatProperty(@UnknownInitialization AbstractPropertiesSettings this, + String key, float defValue) { PropertyEntry pe = new DefaultPropertyEntry<>(key, defValue, parseFloat, (it) -> (float) (double) it); propertyEntries.add(pe); return pe; } - protected PropertyEntry createStringProperty(String key, String defValue) { + protected PropertyEntry createStringProperty(@UnknownInitialization AbstractPropertiesSettings this, + String key, String defValue) { PropertyEntry pe = new DefaultPropertyEntry<>(key, defValue, id -> id, Object::toString); propertyEntries.add(pe); return pe; } - protected PropertyEntry createBooleanProperty(String key, boolean defValue) { + protected PropertyEntry createBooleanProperty(@UnknownInitialization AbstractPropertiesSettings this, + String key, boolean defValue) { PropertyEntry pe = new DefaultPropertyEntry<>(key, defValue, parseBoolean, (it) -> (Boolean) it); propertyEntries.add(pe); diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java index 6ce9497caf5..3a84fdcd874 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java @@ -17,6 +17,7 @@ import de.uka.ilkd.key.logic.Choice; import de.uka.ilkd.key.logic.Namespace; +import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableList; @@ -207,7 +208,7 @@ public ChoiceSettings updateWith(Iterable sc) { } @Override - public boolean equals(Object o) { + public boolean equals(@Nullable Object o) { if (this == o) { return true; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java index 7785598b50a..a68285bc71e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java @@ -3,19 +3,18 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.settings; -import java.io.File; -import java.io.IOException; -import java.io.PrintWriter; -import java.io.Writer; -import java.util.*; - import de.uka.ilkd.key.nparser.ParsingFacade; import de.uka.ilkd.key.util.Position; - import org.antlr.v4.runtime.CharStream; import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; +import java.io.File; +import java.io.IOException; +import java.io.PrintWriter; +import java.io.Writer; +import java.util.*; + /** * A container to hold parsed configurations. Configurations are a mapping between a property name @@ -54,7 +53,7 @@ public static Configuration load(File file) throws IOException { /** * Loads a configuration using the given char stream. * - * @param file existsing file path + * @param input input stream * @return a configuration based on the file contents * @throws IOException i/o error on the steram */ @@ -87,12 +86,11 @@ public boolean exists(String name, Class clazz) { * Returns the stored value for the given name casted to the given clazz if possible. * If no value exists, or value is not compatible to {@code clazz}, {@code null} is returned. * - * @param an arbitrary class, exptected return type - * @param name property name + * @param an arbitrary class, exptected return type + * @param name property name * @param clazz data type because of missing reified generics. */ - @Nullable - public T get(String name, Class clazz) { + public @Nullable T get(String name, Class clazz) { if (exists(name, clazz)) return (T) data.get(name); else @@ -103,12 +101,11 @@ public T get(String name, Class clazz) { * The same as {@link #get(String, Class)} but returns the {@code defaultValue} instead * of a {@code null} reference. * - * @param the expected return type compatible to the {@code defaultValue} - * @param name property name + * @param the expected return type compatible to the {@code defaultValue} + * @param name property name * @param defaultValue the returned instead of {@code null}. */ - @NonNull - public T get(String name, @NonNull T defaultValue) { + public T get(String name, T defaultValue) { if (exists(name, defaultValue.getClass())) return (T) data.get(name); else @@ -129,7 +126,7 @@ public Object get(String name) { * Returns an integer or {@code null} if not such entry exists. * * @param name property name - * @throw ClassCastException if the entry is not an {@link #Long} + * @throw ClassCastException if the entry is not an {@link Long} * @throw NullPointerException if no such value entry exists */ public int getInt(String name) { @@ -141,8 +138,8 @@ public int getInt(String name) { * present. * * @param name property name - * @throw ClassCastException if the entry is not an {@link #Long} - * @throw NullPointerException if no such value entry exists + * @throws ClassCastException if the entry is not an {@link Long} + * @throws NullPointerException if no such value entry exists */ public int getInt(String name, int defaultValue) { return (int) getLong(name, defaultValue); @@ -152,8 +149,8 @@ public int getInt(String name, int defaultValue) { * Returns a long value for the given name. {@code null} if no such value is present. * * @param name property name - * @throw ClassCastException if the entry is not an {@link #Long} - * @throw NullPointerException if no such value entry exists + * @throws ClassCastException if the entry is not an {@link Long} + * @throws NullPointerException if no such value entry exists */ public long getLong(String name) { return get(name, Long.class); @@ -163,8 +160,8 @@ public long getLong(String name) { * Returns a long value for the given name. {@code defaultValue} if no such value is present. * * @param name property name - * @throw ClassCastException if the entry is not an {@link #Long} - * @throw NullPointerException if no such value entry exists + * @throws ClassCastException if the entry is not an {@link Long} + * @throws NullPointerException if no such value entry exists */ public long getLong(String name, long defaultValue) { var value = get(name, Long.class); @@ -175,8 +172,8 @@ public long getLong(String name, long defaultValue) { * Returns a boolean value for the given name. * * @param name property name - * @throw ClassCastException if the entry is not an {@link #Long} - * @throw NullPointerException if no such value entry exists + * @throws ClassCastException if the entry is not an {@link Long} + * @throws NullPointerException if no such value entry exists */ public boolean getBool(String name) { return get(name, Boolean.class); @@ -186,8 +183,8 @@ public boolean getBool(String name) { * Returns a boolean value for the given name. {@code defaultValue} if no such value is present. * * @param name property name - * @throw ClassCastException if the entry is not an {@link #Long} - * @throw NullPointerException if no such value entry exists + * @throws ClassCastException if the entry is not an {@link Long} + * @throws NullPointerException if no such value entry exists */ public boolean getBool(String name, boolean defaultValue) { return get(name, defaultValue); @@ -198,8 +195,8 @@ public boolean getBool(String name, boolean defaultValue) { * present. * * @param name property name - * @throw ClassCastException if the entry is not an {@link #Long} - * @throw NullPointerException if no such value entry exists + * @throws ClassCastException if the entry is not an {@link Long} + * @throws NullPointerException if no such value entry exists */ public double getDouble(String name) { return get(name, Double.class); @@ -264,7 +261,7 @@ public List getStringList(String name) { * Returns string array for the requested entry. {@code defaultValue} is returned if no such * entry exists. * - * @param name a string identifying the entry + * @param name a string identifying the entry * @param defaultValue a default value * @throws ClassCastException if the given entry has non-string elements */ @@ -295,7 +292,7 @@ private ConfigurationMeta getOrCreateMeta(String name) { /** * @see #getTable(String) */ - public Configuration getSection(String name) { + public @Nullable Configuration getSection(String name) { return get(name, Configuration.class); } @@ -307,42 +304,42 @@ public Configuration getSection(String name, boolean createIfNotExists) { if (!exists(name) && createIfNotExists) { set(name, new Configuration()); } - return getSection(name); + return Objects.requireNonNull(getSection(name)); } - public Object set(String name, Object obj) { + public @Nullable Object set(String name, Object obj) { return data.put(name, obj); } - public Object set(String name, Boolean obj) { + public @Nullable Object set(String name, Boolean obj) { return set(name, (Object) obj); } - public Object set(String name, String obj) { + public @Nullable Object set(String name, String obj) { return set(name, (Object) obj); } - public Object set(String name, Long obj) { + public @Nullable Object set(String name, Long obj) { return set(name, (Object) obj); } - public Object set(String name, int obj) { + public @Nullable Object set(String name, int obj) { return set(name, (long) obj); } - public Object set(String name, Double obj) { + public @Nullable Object set(String name, Double obj) { return set(name, (Object) obj); } - public Object set(String name, Configuration obj) { + public @Nullable Object set(String name, Configuration obj) { return set(name, (Object) obj); } - public Object set(String name, List obj) { + public @Nullable Object set(String name, List obj) { return set(name, (Object) obj); } - public Object set(String name, String[] seq) { + public @Nullable Object set(String name, String[] seq) { return set(name, (Object) Arrays.asList(seq)); } @@ -353,23 +350,24 @@ public Set> getEntries() { /** * Interprets the given entry as an enum value. * - * @param the enum - * @param name a name identifying an entry + * @param the enum + * @param name a name identifying an entry * @param defaultValue the default value to be returned */ public > T getEnum(String name, T defaultValue) { var idx = getString(name); try { - return Enum.valueOf((Class) defaultValue.getClass(), idx); - } catch (IllegalArgumentException | NullPointerException e) { - return defaultValue; + if (idx != null) + return Enum.valueOf((Class) defaultValue.getClass(), idx); + } catch (IllegalArgumentException | NullPointerException ignored) { } + return defaultValue; } /** * Serializes this configuration instance into the given writer. * - * @param writer a writer + * @param writer a writer * @param comment a comment */ public void save(Writer writer, String comment) { @@ -380,13 +378,17 @@ public void save(Writer writer, String comment) { * POJO for metadata of configuration entries. */ public static class ConfigurationMeta { - /** Position of declaration within a file */ - private Position position; + /** + * Position of declaration within a file + */ + private @Nullable Position position; - /** documentation given in the file */ - private String documentation; + /** + * documentation given in the file + */ + private @Nullable String documentation; - public Position getPosition() { + public @Nullable Position getPosition() { return position; } @@ -394,7 +396,7 @@ public void setPosition(Position position) { this.position = position; } - public String getDocumentation() { + public @Nullable String getDocumentation() { return documentation; } @@ -468,7 +470,7 @@ private ConfigurationWriter printMap(Map value) { indent += 4; newline().printIndent(); for (Iterator> iterator = - value.entrySet().iterator(); iterator.hasNext();) { + value.entrySet().iterator(); iterator.hasNext(); ) { Map.Entry entry = iterator.next(); String k = entry.getKey(); Object v = entry.getValue(); @@ -495,7 +497,7 @@ private ConfigurationWriter printSeq(Collection value) { indent += 4; newline(); printIndent(); - for (Iterator iterator = value.iterator(); iterator.hasNext();) { + for (Iterator iterator = value.iterator(); iterator.hasNext(); ) { Object o = iterator.next(); printValue(o); if (iterator.hasNext()) { @@ -522,7 +524,7 @@ private ConfigurationWriter printKey(String key) { } @Override - public boolean equals(Object o) { + public boolean equals(@Nullable Object o) { if (this == o) return true; if (!(o instanceof Configuration that)) diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/FeatureSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/FeatureSettings.java index b63849ed328..bf45ced90c5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/FeatureSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/FeatureSettings.java @@ -6,6 +6,7 @@ import java.util.*; import java.util.function.Consumer; +import org.checkerframework.checker.initialization.qual.UnknownInitialization; import org.jspecify.annotations.NonNull; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -73,7 +74,7 @@ public static void onAndActivate(Feature feature, Consumer update) { * Use the system properties ({@code -P FEATURE:XXX=true} to activate a feature from the command * line. */ - private void readFromSystemProperties() { + private void readFromSystemProperties(@UnknownInitialization FeatureSettings this) { var prefix = CATEGORY.toUpperCase() + ":"; for (Map.Entry entries : System.getProperties().entrySet()) { final var s = entries.getKey().toString(); @@ -189,18 +190,19 @@ public static Feature createFeature(String id) { } public static Feature createFeature(String id, String doc) { - return new Feature(id, doc, true); + var f = new Feature(id, doc, true); + FEATURES.add(f); + return f; } public static Feature createFeature(String id, String doc, boolean restartRequired) { - return new Feature(id, doc, restartRequired); + var f = new Feature(id, doc, restartRequired); + FEATURES.add(f); + return f; } - public record Feature(String id, String documentation, boolean restartRequired) { - public static final List FEATURES = new ArrayList<>(); + public static final List FEATURES = new ArrayList<>(); - public Feature { - FEATURES.add(this); - } + public record Feature(String id, String documentation, boolean restartRequired) { } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java index 254e116dfca..f4159c5f561 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java @@ -358,8 +358,7 @@ public boolean toBeSaved() { @Override public String proofToString(Services services) { - assert false; - return null; + throw new RuntimeException("Not Implemented"); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java index 60fdf8e48a5..8d9c2a96603 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java @@ -525,8 +525,7 @@ public String getUniqueName() { @Override public VisibilityModifier getVisibility() { - assert false; - return null; + throw new RuntimeException("Not Implemented"); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java index 63fc487577f..6d04835f95a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java @@ -1120,8 +1120,7 @@ public final String getPlainText(Services services) { @Override public final String proofToString(Services services) { - assert false; - return null; + throw new RuntimeException("Not Implemented"); } @Override 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 aff0835099e..f2aca199e69 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 @@ -1028,8 +1028,7 @@ public SLExpression visitPrimarySuffixAccess(JmlParser.PrimarySuffixAccessContex return new SLExpression(tb.allFields(receiver.getTerm()), javaInfo.getPrimitiveKeYJavaType(PrimitiveType.JAVA_LOCSET)); } - assert false; - return null; + throw new RuntimeException("Not Implemented"); } @Override 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 ed0d6a0e060..2e1303d8e7b 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 @@ -81,7 +81,6 @@ private MiscTools() { * @return The {@link LoopSpecification} for the loop statement in the given term or an empty * optional if there is no specified invariant for the loop. */ - @Nullable public static LoopSpecification getSpecForTermWithLoopStmt(final Term loopTerm, final Services services) { assert loopTerm.op() instanceof Modality; @@ -146,7 +145,7 @@ public static List applicableHeapContexts( } // TODO Is rp always a program variable? - public static ProgramVariable getSelf(MethodFrame mf) { + public static @Nullable ProgramVariable getSelf(MethodFrame mf) { ExecutionContext ec = (ExecutionContext) mf.getExecutionContext(); ReferencePrefix rp = ec.getRuntimeInstance(); if (!(rp instanceof TypeReference) && rp != null) { @@ -165,7 +164,7 @@ public static ProgramVariable getSelf(MethodFrame mf) { * @return the receiver term of the passed method frame, or null if the frame belongs to a * static method. */ - public static Term getSelfTerm(MethodFrame mf, Services services) { + public static @Nullable Term getSelfTerm(MethodFrame mf, Services services) { ExecutionContext ec = (ExecutionContext) mf.getExecutionContext(); ReferencePrefix rp = ec.getRuntimeInstance(); if (!(rp instanceof TypeReference) && rp != null) { @@ -439,7 +438,7 @@ public static boolean isJMLComment(String comment) { * @return The display name of the applied rule in the given {@link Node} or {@code null} if no * one exists. */ - public static String getRuleDisplayName(Node node) { + public static @Nullable String getRuleDisplayName(@Nullable Node node) { String name = null; if (node != null) { name = getRuleDisplayName(node.getAppliedRuleApp()); @@ -459,7 +458,7 @@ public static String getRuleDisplayName(Node node) { * @param ruleApp The given {@link RuleApp}. * @return The display name of the {@link RuleApp} or {@code null} if no one exists. */ - public static String getRuleDisplayName(RuleApp ruleApp) { + public static @Nullable String getRuleDisplayName(@Nullable RuleApp ruleApp) { String name = null; if (ruleApp != null) { Rule rule = ruleApp.rule(); @@ -483,7 +482,7 @@ public static String getRuleDisplayName(RuleApp ruleApp) { * @return The display name of the applied rule in the given {@link Node} or {@code null} if no * one exists. */ - public static String getRuleName(Node node) { + public static @Nullable String getRuleName(@Nullable Node node) { String name = null; if (node != null) { name = getRuleName(node.getAppliedRuleApp()); @@ -503,7 +502,7 @@ public static String getRuleName(Node node) { * @param ruleApp The given {@link RuleApp}. * @return The display name of the {@link RuleApp} or {@code null} if no one exists. */ - public static String getRuleName(RuleApp ruleApp) { + public static @Nullable String getRuleName(@Nullable RuleApp ruleApp) { String name = null; if (ruleApp != null) { Rule rule = ruleApp.rule(); @@ -520,7 +519,7 @@ public static String getRuleName(RuleApp ruleApp) { * @param proof The {@link Proof} to get its used {@link OneStepSimplifier}. * @return The used {@link OneStepSimplifier} or {@code null} if not available. */ - public static OneStepSimplifier findOneStepSimplifier(Proof proof) { + public static @Nullable OneStepSimplifier findOneStepSimplifier(@Nullable Proof proof) { if (proof != null && !proof.isDisposed() && proof.getInitConfig() != null) { Profile profile = proof.getInitConfig().getProfile(); return findOneStepSimplifier(profile); @@ -535,7 +534,7 @@ public static OneStepSimplifier findOneStepSimplifier(Proof proof) { * @param profile The {@link Profile} to get its used {@link OneStepSimplifier}. * @return The used {@link OneStepSimplifier} or {@code null} if not available. */ - public static OneStepSimplifier findOneStepSimplifier(Profile profile) { + public static @Nullable OneStepSimplifier findOneStepSimplifier(Profile profile) { if (profile instanceof JavaProfile) { return ((JavaProfile) profile).getOneStepSimpilifier(); } else { @@ -549,7 +548,7 @@ public static OneStepSimplifier findOneStepSimplifier(Profile profile) { * @param node the Node where to look up the actual variable (result from renaming) * @return The renamed variable */ - public static ProgramVariable findActualVariable(ProgramVariable originalVar, Node node) { + public static ProgramVariable findActualVariable(ProgramVariable originalVar, @Nullable Node node) { if (node != null) { do { if (node.getRenamingTable() != null) { @@ -656,10 +655,8 @@ public ImmutableSet getDeclaredPVs() { public static ImmutableList toTermList(Iterable list, TermBuilder tb) { ImmutableList result = ImmutableSLList.nil(); for (ProgramVariable pv : list) { - if (pv != null) { - Term t = tb.var(pv); - result = result.append(t); - } + Term t = tb.var(pv); + result = result.append(t); } return result; } @@ -725,10 +722,6 @@ public static HashMap getDefaultTacletOptions() { * @return an URI identifying the resource of the DataLocation */ public static Optional extractURI(DataLocation loc) { - if (loc == null) { - throw new IllegalArgumentException("The given DataLocation is null!"); - } - try { return switch (loc.getType()) { case "URL" -> // URLDataLocation @@ -805,13 +798,11 @@ public static URI getZipEntryURI(ZipFile zipFile, String entryName) throws IOExc // } } - @Nullable - public static URI getURIFromTokenSource(TokenSource source) { + public static @Nullable URI getURIFromTokenSource(TokenSource source) { return getURIFromTokenSource(source.getSourceName()); } - @Nullable - public static URI getURIFromTokenSource(String source) { + public static @Nullable URI getURIFromTokenSource(String source) { if (IntStream.UNKNOWN_SOURCE_NAME.equals(source)) { return null; } @@ -858,7 +849,7 @@ public static URI getURIFromTokenSource(String source) { * @throws MalformedURLException if the string can not be converted to URL because of an unknown * protocol or illegal format */ - public static URL parseURL(final String input) throws MalformedURLException { + public static URL parseURL(@Nullable String input) throws MalformedURLException { if (input == null) { throw new NullPointerException("No URL can be created from null!"); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/parsing/BuildingException.java b/key.core/src/main/java/de/uka/ilkd/key/util/parsing/BuildingException.java index ef6cc9d2b2e..af897f77217 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/parsing/BuildingException.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/parsing/BuildingException.java @@ -21,20 +21,20 @@ public class BuildingException extends RuntimeException implements HasLocation { private final @Nullable Token offendingSymbol; - public BuildingException(ParserRuleContext ctx, String format) { + public BuildingException(@Nullable ParserRuleContext ctx, String format) { this(ctx, format, null); } - public BuildingException(Throwable e) { + public BuildingException(@Nullable Throwable e) { super(e); offendingSymbol = null; } - public BuildingException(ParserRuleContext ctx, String message, Throwable e) { + public BuildingException(@Nullable ParserRuleContext ctx, String message, @Nullable Throwable e) { this(ctx == null ? null : ctx.start, message, e); } - public BuildingException(@Nullable Token t, String message, Throwable e) { + public BuildingException(@Nullable Token t, String message, @Nullable Throwable e) { super(message + " at " + getPosition(t), e); offendingSymbol = t; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java b/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java index 2c584aa6fa8..1e29fb86043 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java @@ -3,25 +3,23 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.util.parsing; -import java.net.MalformedURLException; -import java.net.URI; -import java.util.ArrayList; -import java.util.Collections; -import java.util.List; -import java.util.function.Supplier; -import java.util.stream.Collectors; - import de.uka.ilkd.key.java.Position; import de.uka.ilkd.key.parser.Location; import de.uka.ilkd.key.util.MiscTools; - -import org.key_project.util.java.StringUtil; - import org.antlr.v4.runtime.*; import org.jspecify.annotations.Nullable; +import org.key_project.util.java.StringUtil; import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import java.net.MalformedURLException; +import java.net.URI; +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; +import java.util.function.Supplier; +import java.util.stream.Collectors; + /** * An ANTLR4 error listener that stores the errors internally. You can disable the additional * printing of message on the logger {@link #logger} flag. @@ -38,38 +36,39 @@ public class SyntaxErrorReporter extends BaseErrorListener { */ private final boolean throwDirect; + @Nullable private final Logger logger; - public SyntaxErrorReporter(Logger logger, boolean throwDirect) { + public SyntaxErrorReporter(@Nullable Logger logger, boolean throwDirect) { this.logger = logger; this.throwDirect = throwDirect; } - public SyntaxErrorReporter(Class loggerCategory) { + public SyntaxErrorReporter(@Nullable Class loggerCategory) { this(loggerCategory, false); } - public SyntaxErrorReporter(Class loggerCategory, boolean throwDirect) { + public SyntaxErrorReporter(@Nullable Class loggerCategory, boolean throwDirect) { this(loggerCategory != null ? LoggerFactory.getLogger(loggerCategory) : null, throwDirect); } @Override public void syntaxError(Recognizer recognizer, @Nullable Object offendingSymbol, int line, - int charPositionInLine, String msg, RecognitionException e) { + int charPositionInLine, String msg, RecognitionException e) { Parser parser = (Parser) recognizer; String stack = String.join(", ", parser.getRuleInvocationStack()); Token tok = (Token) offendingSymbol; if (tok == null) { throw new IllegalArgumentException( - "offendedSymbol is null. Use SyntaxErrorReporter only in Parsers"); + "offendedSymbol is null. Use SyntaxErrorReporter only in Parsers"); } SyntaxError se = new SyntaxError(recognizer, line, tok, charPositionInLine, msg, - MiscTools.getURIFromTokenSource(tok.getTokenSource()), stack); + MiscTools.getURIFromTokenSource(tok.getTokenSource()), stack); if (logger != null) { logger.warn("[syntax-error] {}:{}:{}: {} {} ({})", se.source, line, charPositionInLine, - msg, tok, stack); + msg, tok, stack); } errors.add(se); @@ -141,7 +140,7 @@ public static class SyntaxError { final String stack; public SyntaxError(Recognizer recognizer, int line, Token offendingSymbol, - int charPositionInLine, String msg, URI source, String stack) { + int charPositionInLine, String msg, URI source, String stack) { this.recognizer = recognizer; this.line = line; this.offendingSymbol = offendingSymbol; @@ -153,13 +152,13 @@ public SyntaxError(Recognizer recognizer, int line, Token offendingSymbol, public String getBeatifulErrorMessage(String[] lines) { return ("syntax-error in " + positionAsUrl() + "\n" + msg + "\n" + showInInput(lines) - + "\n"); + + "\n"); } public String showInInput(String[] lines) { String line = lines[this.line]; return line + "\n" + StringUtil.repeat(" ", (charPositionInLine - 1)) - + StringUtil.repeat("^", (offendingSymbol.getText().length())); + + StringUtil.repeat("^", (offendingSymbol.getText().length())); } public String positionAsUrl() { @@ -197,7 +196,7 @@ public Location getLocation() throws MalformedURLException { SyntaxError e = errors.get(0); // e.charPositionInLine is 0 based! return new Location(e.source, - Position.fromOneZeroBased(e.line, e.charPositionInLine)); + Position.fromOneZeroBased(e.line, e.charPositionInLine)); } return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/parsing/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/util/parsing/package-info.java new file mode 100644 index 00000000000..95c2d8a3589 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/util/parsing/package-info.java @@ -0,0 +1,7 @@ +/** + * @author Alexander Weigl + * @version 1 (03.05.24) + */ +@NullMarked package de.uka.ilkd.key.util.parsing; + +import org.jspecify.annotations.NullMarked; \ No newline at end of file diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/DependencyContractCompletion.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/DependencyContractCompletion.java index 52b5be1005b..75006060c5d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/DependencyContractCompletion.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/DependencyContractCompletion.java @@ -101,8 +101,7 @@ public static PosInOccurrence findCorrespondingStep(List steps, return step; } } - assert false; - return null; + throw new RuntimeException("Not Implemented"); } public static void extractHeaps(List heapContext, List steps, diff --git a/keyext.exploration/build.gradle b/keyext.exploration/build.gradle index 11ae54fd65e..dee17a0bee0 100644 --- a/keyext.exploration/build.gradle +++ b/keyext.exploration/build.gradle @@ -3,4 +3,21 @@ description "Proof exploration capabilities for key.ui" dependencies { implementation project(":key.core") implementation project(":key.ui") -} \ No newline at end of file +} + + +checkerFramework { + if(System.getProperty("ENABLE_NULLNESS")) { + checkers = [ + "org.checkerframework.checker.nullness.NullnessChecker", + ] + extraJavacArgs = [ + "-AonlyDefs=^org\\.key_project\\.logic", + "-Xmaxerrs", "10000", + "-Astubs=$rootDir/key.util/src/main/checkerframework:permit-nullness-assertion-exception.astub", + "-AstubNoWarnIfNotFound", + "-Werror", + "-Aversion", + ] + } +} From c0eafcc9ba600e97d6cf9f7440e3d2f4a26ef120 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Fri, 10 May 2024 00:04:04 +0200 Subject: [PATCH 2/6] Merge branch 'main' into weigl/key-javaparser3 # By Florian Lanzinger (25) and others # Via GitHub (14) and others * main: (69 commits) typo Unify type annotation notation Apply spotless Remove unnecessary warnings and serialization key.ncore done configure key.ncore fix null values eisop in ncore Fix formatting Fix more NoSuchElementExceptions Fix NoSuchElementException in JavaInfo Remove redundant nullness checks and fix test cases Fix proof script #equals must allow null values jspecify was missing in the compile classpath of tests Code style Revert JavaRedux Object Test case Fix merge issues reformat files ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/ParseExceptionInFile.java # key.core/src/main/java/de/uka/ilkd/key/java/PosConvertException.java # key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/Subtype.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java # key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptException.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/AbstractBuilder.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java # key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java # key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java # key.core/src/main/java/de/uka/ilkd/key/proof/SVInstantiationExceptionWithPosition.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java # key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java # key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLTranslationException.java # key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java # key.core/src/main/java/de/uka/ilkd/key/util/RecognitionException.java # key.core/src/main/java/de/uka/ilkd/key/util/parsing/BuildingException.java # key.core/src/main/java/de/uka/ilkd/key/util/parsing/LocatableException.java # key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java # key.util/src/main/java/org/key_project/util/ExtList.java # key.util/src/main/java/org/key_project/util/collection/ImmutableList.java # settings.gradle --- .../key/java/reference/FieldReference.java | 3 +- .../java/de/uka/ilkd/key/ldt/BooleanLDT.java | 3 +- .../java/de/uka/ilkd/key/ldt/CharListLDT.java | 7 +- .../java/de/uka/ilkd/key/ldt/DoubleLDT.java | 3 +- .../java/de/uka/ilkd/key/ldt/FloatLDT.java | 54 +++--- .../java/de/uka/ilkd/key/ldt/HeapLDT.java | 35 ++-- .../java/de/uka/ilkd/key/ldt/IntegerLDT.java | 5 +- .../de/uka/ilkd/key/ldt/JavaDLTheory.java | 1 + .../main/java/de/uka/ilkd/key/ldt/LDT.java | 8 +- .../main/java/de/uka/ilkd/key/ldt/MapLDT.java | 6 +- .../de/uka/ilkd/key/ldt/PermissionLDT.java | 3 +- .../java/de/uka/ilkd/key/ldt/RealLDT.java | 3 +- .../de/uka/ilkd/key/ldt/package-info.java | 5 +- .../uka/ilkd/key/macros/AlternativeMacro.java | 5 +- .../ilkd/key/macros/DoWhileFinallyMacro.java | 7 +- .../de/uka/ilkd/key/macros/ProofMacro.java | 6 +- .../ilkd/key/macros/scripts/EngineState.java | 2 +- .../ilkd/key/macros/scripts/MacroCommand.java | 35 ++-- .../key/macros/scripts/RewriteCommand.java | 3 +- .../ilkd/key/macros/scripts/RuleCommand.java | 54 +++--- .../ilkd/key/macros/scripts/ScriptNode.java | 14 +- .../ilkd/key/macros/scripts/SetCommand.java | 1 + .../key/macros/scripts/meta/package-info.java | 5 +- .../ilkd/key/macros/scripts/package-info.java | 5 +- .../java/de/uka/ilkd/key/pp/LogicPrinter.java | 170 +++++++++--------- .../key/proof/io/OutputStreamProofSaver.java | 5 +- .../settings/AbstractPropertiesSettings.java | 25 +-- .../uka/ilkd/key/settings/ChoiceSettings.java | 2 +- .../uka/ilkd/key/settings/Configuration.java | 68 +++---- .../java/de/uka/ilkd/key/util/MiscTools.java | 3 +- .../key/util/parsing/BuildingException.java | 3 +- .../key/util/parsing/SyntaxErrorReporter.java | 36 ++-- .../ilkd/key/util/parsing/package-info.java | 5 +- .../gui/settings/FeatureSettingsPanel.java | 2 +- 34 files changed, 310 insertions(+), 282 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/reference/FieldReference.java b/key.core/src/main/java/de/uka/ilkd/key/java/reference/FieldReference.java index 9f904b577b7..c5ae3038caf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/reference/FieldReference.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/reference/FieldReference.java @@ -8,9 +8,10 @@ import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.op.ProgramVariable; -import org.jspecify.annotations.Nullable; import org.key_project.util.ExtList; +import org.jspecify.annotations.Nullable; + public class FieldReference extends VariableReference implements MemberReference, ReferenceSuffix, TypeReferenceContainer, ExpressionContainer { diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/BooleanLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/BooleanLDT.java index f1d9169f977..a9b891a4300 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/BooleanLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/BooleanLDT.java @@ -15,10 +15,11 @@ import de.uka.ilkd.key.logic.op.JFunction; import de.uka.ilkd.key.util.Debug; -import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; import org.key_project.util.ExtList; +import org.jspecify.annotations.Nullable; + /** * This class inherits from LDT and implements all method that are necessary to handle the primitive 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 27d5498125b..50972f4468c 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 @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.ldt; +import java.util.Objects; + import de.uka.ilkd.key.java.ConvertException; import de.uka.ilkd.key.java.Expression; import de.uka.ilkd.key.java.Services; @@ -22,8 +24,6 @@ import org.jspecify.annotations.Nullable; -import java.util.Objects; - public final class CharListLDT extends LDT { @@ -58,7 +58,8 @@ public final class CharListLDT extends LDT { // ------------------------------------------------------------------------- public CharListLDT(TermServices services) { - super(NAME, Objects.requireNonNull(services.getNamespaces().sorts().lookup(SeqLDT.NAME)), services); + super(NAME, Objects.requireNonNull(services.getNamespaces().sorts().lookup(SeqLDT.NAME)), + services); clIndexOfChar = addFunction(services, "clIndexOfChar"); clIndexOfCl = addFunction(services, "clIndexOfCl"); clLastIndexOfChar = addFunction(services, "clLastIndexOfChar"); 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 8e50312eb24..02f2168bfa0 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 @@ -14,10 +14,11 @@ import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.JFunction; -import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; import org.key_project.util.ExtList; +import org.jspecify.annotations.Nullable; + public final class DoubleLDT extends LDT implements FloatingPointLDT { public static final Name NAME = new Name("double"); 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 cf38887fc93..1623852f5c7 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 @@ -13,11 +13,13 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.JFunction; -import org.jspecify.annotations.Nullable; + import org.key_project.logic.Name; import org.key_project.logic.op.Function; import org.key_project.util.ExtList; +import org.jspecify.annotations.Nullable; + public final class FloatLDT extends LDT implements FloatingPointLDT { public static final Name NAME = new Name("float"); @@ -96,7 +98,7 @@ public FloatLDT(TermServices services) { @Override public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term[] subs, - Services services, ExecutionContext ec) { + Services services, ExecutionContext ec) { if (subs.length == 1) { return isResponsible(op, subs[0], services, ec); } else if (subs.length == 2) { @@ -107,7 +109,7 @@ public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term[] @Override public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term left, Term right, - Services services, ExecutionContext ec) { + Services services, ExecutionContext ec) { return left != null && left.sort().extendsTrans(targetSort()) && right != null && right.sort().extendsTrans(targetSort()) && getFunctionFor(op, services, ec) != null; @@ -115,7 +117,7 @@ public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term l @Override public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term sub, - TermServices services, ExecutionContext ec) { + TermServices services, ExecutionContext ec) { return sub != null && sub.sort().extendsTrans(targetSort()) && op instanceof Negative; } @@ -129,8 +131,8 @@ public Term translateLiteral(Literal lit, Services services) { @Override public @Nullable JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, - Services services, - ExecutionContext ec) { + Services services, + ExecutionContext ec) { if (op instanceof GreaterThan) { return getGreaterThan(); } else if (op instanceof LessThan) { @@ -159,26 +161,26 @@ public Term translateLiteral(Literal lit, Services services) { @Override public @Nullable JFunction getFunctionFor(String op, Services services) { 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" -> 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; + 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" -> 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; }; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/HeapLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/HeapLDT.java index 6428c3c8f53..b5ad98d1fee 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/HeapLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/HeapLDT.java @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.ldt; +import java.util.Objects; + import de.uka.ilkd.key.java.Expression; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.abstraction.Type; @@ -17,7 +19,7 @@ import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.proof.init.JavaProfile; import de.uka.ilkd.key.proof.io.ProofSaver; -import org.jspecify.annotations.Nullable; + import org.key_project.logic.Name; import org.key_project.logic.Named; import org.key_project.logic.op.Function; @@ -27,7 +29,7 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; -import java.util.Objects; +import org.jspecify.annotations.Nullable; /** @@ -45,7 +47,7 @@ public final class HeapLDT extends LDT { public static final Name SAVED_HEAP_NAME = new Name("savedHeap"); public static final Name PERMISSION_HEAP_NAME = new Name("permissions"); public static final Name[] VALID_HEAP_NAMES = - {BASE_HEAP_NAME, SAVED_HEAP_NAME, PERMISSION_HEAP_NAME}; + { BASE_HEAP_NAME, SAVED_HEAP_NAME, PERMISSION_HEAP_NAME }; // additional sorts @@ -109,7 +111,7 @@ public HeapLDT(TermServices services) { classPrepared = addSortDependingFunction(services, ""); classInitialized = addSortDependingFunction(services, ""); classInitializationInProgress = - addSortDependingFunction(services, ""); + addSortDependingFunction(services, ""); classErroneous = addSortDependingFunction(services, ""); length = addFunction(services, "length"); nullFunc = addFunction(services, "null"); @@ -121,7 +123,8 @@ public HeapLDT(TermServices services) { heaps = ImmutableSLList.nil() .append(heapBase) .append(heapSaved); - if (services instanceof Services s && s.getProfile() instanceof JavaProfile jp && jp.withPermissions()) { + if (services instanceof Services s && s.getProfile() instanceof JavaProfile jp + && jp.withPermissions()) { heapPermission = (LocationVariable) progVars.lookup(PERMISSION_HEAP_NAME); heaps = heaps.append(Objects.requireNonNull(heapPermission)); } else { @@ -153,7 +156,7 @@ private String getFieldSymbolName(LocationVariable fieldPV) { /** * Wrapper class * - * @param className the class name + * @param className the class name * @param attributeName the attribute name */ public record SplitFieldName(String className, String attributeName) { @@ -302,7 +305,7 @@ public JFunction getClassInitialized(Sort instanceSort, TermServices services) { public JFunction getClassInitializationInProgress(Sort instanceSort, - TermServices services) { + TermServices services) { return classInitializationInProgress.getInstanceFor(instanceSort, services); } @@ -385,7 +388,7 @@ public JFunction getFieldSymbolForPV(LocationVariable fieldPV, Services services final Name kind = new Name(name.toString().substring(index + 2)); SortDependingFunction firstInstance = - SortDependingFunction.getFirstInstance(kind, services); + SortDependingFunction.getFirstInstance(kind, services); if (firstInstance != null) { Sort sortDependingOn = fieldPV.getContainerType().getSort(); result = firstInstance.getInstanceFor(sortDependingOn, services); @@ -399,8 +402,8 @@ public JFunction getFieldSymbolForPV(LocationVariable fieldPV, Services services heapCount++; } result = new ObserverFunction(kind.toString(), fieldPV.sort(), - fieldPV.getKeYJavaType(), targetSort(), fieldPV.getContainerType(), - fieldPV.isStatic(), new ImmutableArray<>(), heapCount, 1); + fieldPV.getKeYJavaType(), targetSort(), fieldPV.getContainerType(), + fieldPV.isStatic(), new ImmutableArray<>(), heapCount, 1); } else { result = new JFunction(name, fieldSort, new Sort[0], null, true); } @@ -432,21 +435,21 @@ public boolean containsFunction(Function op) { @Override public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term[] subs, - Services services, ExecutionContext ec) { + Services services, ExecutionContext ec) { return false; } @Override public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term left, Term right, - Services services, ExecutionContext ec) { + Services services, ExecutionContext ec) { return false; } @Override public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term sub, - TermServices services, ExecutionContext ec) { + TermServices services, ExecutionContext ec) { return false; } @@ -459,7 +462,7 @@ public Term translateLiteral(Literal lit, Services services) { @Override public JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Services serv, - ExecutionContext ec) { + ExecutionContext ec) { throw new IllegalStateException("Not implemented"); } @@ -488,10 +491,10 @@ public Expression translateTerm(Term t, ExtList children, Services services) { } else if (t.sort() == getFieldSort() && t.op() instanceof JFunction && ((Function) t.op()).isUnique()) { return services.getJavaInfo().getAttribute(getPrettyFieldName(t.op()), - Objects.requireNonNull(getClassName((Function) t.op()))); + Objects.requireNonNull(getClassName((Function) t.op()))); } throw new IllegalArgumentException( - "Could not translate " + ProofSaver.printTerm(t, null) + " to program."); + "Could not translate " + ProofSaver.printTerm(t, null) + " to program."); } 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 83c5f60d509..3d5c88d339b 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 @@ -19,11 +19,11 @@ import de.uka.ilkd.key.logic.op.Operator; import de.uka.ilkd.key.util.Debug; -import org.checkerframework.checker.initialization.qual.UnknownInitialization; import org.key_project.logic.Name; import org.key_project.logic.op.Function; import org.key_project.util.ExtList; +import org.checkerframework.checker.initialization.qual.UnknownInitialization; import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -170,7 +170,8 @@ public IntegerLDT(Services services) { } neglit = addFunction(services, NEGATIVE_LITERAL_STRING); numbers = addFunction(services, NUMBERS_NAME.toString()); - if (sharp.sort() != numbers.argSort(0)) throw new AssertionError(); + if (sharp.sort() != numbers.argSort(0)) + throw new AssertionError(); charID = addFunction(services, CHAR_ID_NAME.toString()); add = addFunction(services, "add"); neg = addFunction(services, "neg"); diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java index 49e6095c5cd..053fbeaddc0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java @@ -14,6 +14,7 @@ import de.uka.ilkd.key.logic.op.JFunction; import de.uka.ilkd.key.logic.op.SortDependingFunction; import de.uka.ilkd.key.logic.sort.SortImpl; + import org.key_project.logic.Name; import org.key_project.logic.sort.Sort; import org.key_project.util.ExtList; diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java index b2b1321c62d..cc9087b16c3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java @@ -18,14 +18,13 @@ import de.uka.ilkd.key.logic.op.Operator; import de.uka.ilkd.key.logic.op.SortDependingFunction; -import org.checkerframework.checker.initialization.qual.UnderInitialization; -import org.checkerframework.checker.initialization.qual.UnknownInitialization; import org.key_project.logic.Name; import org.key_project.logic.Named; import org.key_project.logic.op.Function; import org.key_project.logic.sort.Sort; import org.key_project.util.ExtList; +import org.checkerframework.checker.initialization.qual.UnknownInitialization; import org.jspecify.annotations.Nullable; /** @@ -84,7 +83,8 @@ protected final JFunction addFunction(@UnknownInitialization LDT this, JFunction * @param funcName the String with the name of the function to look up * @return the added function (for convenience reasons) */ - protected final JFunction addFunction(@UnknownInitialization LDT this, TermServices services, String funcName) { + protected final JFunction addFunction(@UnknownInitialization LDT this, TermServices services, + String funcName) { final Namespace funcNS = services.getNamespaces().functions(); final JFunction f = funcNS.lookup(new Name(funcName)); if (f == null) { @@ -95,7 +95,7 @@ protected final JFunction addFunction(@UnknownInitialization LDT this, TermServi } protected final SortDependingFunction addSortDependingFunction(@UnknownInitialization LDT this, - TermServices services, String kind) { + TermServices services, String kind) { final SortDependingFunction f = SortDependingFunction.getFirstInstance(new Name(kind), services); assert f != null : "LDT: Sort depending function " + kind + " not found"; diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/MapLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/MapLDT.java index 51056a7aced..8d70a2d972a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/MapLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/MapLDT.java @@ -14,11 +14,12 @@ import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.JFunction; -import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; import org.key_project.logic.op.Function; import org.key_project.util.ExtList; +import org.jspecify.annotations.Nullable; + /** * LDT for maps. * @@ -48,7 +49,8 @@ public boolean isResponsible(Operator op, Term left, Term right, Services servic } @Override - public boolean isResponsible(Operator op, @Nullable Term sub, TermServices services, ExecutionContext ec) { + public boolean isResponsible(Operator op, @Nullable Term sub, TermServices services, + ExecutionContext ec) { return false; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/PermissionLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/PermissionLDT.java index 0303223315a..bb3e3df0bfe 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/PermissionLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/PermissionLDT.java @@ -70,6 +70,7 @@ public Expression translateTerm(Term t, ExtList children, Services services) { @Override public Type getType(Term t) { - throw new AssertionError("PermissionLDT: there are no types associated with permissions " + t); + throw new AssertionError( + "PermissionLDT: there are no types associated with permissions " + t); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/RealLDT.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/RealLDT.java index 9346fcaca56..3cd796d97e3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/RealLDT.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/RealLDT.java @@ -13,10 +13,11 @@ import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.JFunction; -import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; import org.key_project.util.ExtList; +import org.jspecify.annotations.Nullable; + /** * Complete this class if you want to add support for the JML \real type. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/package-info.java index dd5425badab..066f75c6ee0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/ldt/package-info.java @@ -4,6 +4,7 @@ * programming interface to access the entities declared in these * rule files. */ -@NullMarked package de.uka.ilkd.key.ldt; +@NullMarked +package de.uka.ilkd.key.ldt; -import org.jspecify.annotations.NullMarked; \ No newline at end of file +import org.jspecify.annotations.NullMarked; diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/AlternativeMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/AlternativeMacro.java index f3cab1b92d7..88e3df26792 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/AlternativeMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/AlternativeMacro.java @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.macros; +import java.util.List; + import de.uka.ilkd.key.control.UserInterfaceControl; import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.proof.Goal; @@ -10,9 +12,8 @@ import de.uka.ilkd.key.prover.ProverTaskListener; import de.uka.ilkd.key.prover.TaskStartedInfo.TaskKind; import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; -import org.key_project.util.collection.ImmutableList; -import java.util.List; +import org.key_project.util.collection.ImmutableList; /** * The abstract class AlternativeMacro can be used to create compound macros which apply the first diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/DoWhileFinallyMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/DoWhileFinallyMacro.java index b6a2af95183..c40ddd93e23 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/DoWhileFinallyMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/DoWhileFinallyMacro.java @@ -11,9 +11,10 @@ import de.uka.ilkd.key.prover.TaskStartedInfo.TaskKind; import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; -import org.jspecify.annotations.Nullable; import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.Nullable; + /** * The abstract class DoWhileFinallyMacro can be used to create compound macros which apply the * macro given by {@link #getProofMacro()} as long the given bound of steps is not reached yet, the @@ -59,8 +60,8 @@ public boolean canApplyTo(Proof proof, ImmutableList goals, PosInOccurrenc @Override public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, - ImmutableList goals, - @Nullable PosInOccurrence posInOcc, ProverTaskListener listener) + ImmutableList goals, + @Nullable PosInOccurrence posInOcc, ProverTaskListener listener) throws Exception { ProofMacroFinishedInfo info = new ProofMacroFinishedInfo(this, goals); int steps = getMaxSteps(proof); diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacro.java index 237f9e73d1d..41205b1804c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacro.java @@ -14,9 +14,10 @@ import de.uka.ilkd.key.prover.TaskStartedInfo.TaskKind; import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; -import org.jspecify.annotations.Nullable; import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.Nullable; + /** * The interface ProofMacro is the entry point to a general strategy extension system. * @@ -92,7 +93,8 @@ public interface ProofMacro { * * @return a constant string, or null */ - @Nullable String getCategory(); + @Nullable + String getCategory(); /** * Gets the description of this macro. 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 4b3c6c5d58a..959b14f8087 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 @@ -22,12 +22,12 @@ import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.settings.ProofSettings; -import org.jspecify.annotations.Nullable; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableList; import org.antlr.v4.runtime.CharStreams; import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; /** * @author Alexander Weigl diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java index 7a696a9d4e1..78781c17618 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java @@ -3,6 +3,10 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.macros.scripts; +import java.util.HashMap; +import java.util.Map; +import java.util.ServiceLoader; + import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.PosInOccurrence; @@ -16,11 +20,8 @@ import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.prover.TaskStartedInfo; import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; -import org.jspecify.annotations.Nullable; -import java.util.HashMap; -import java.util.Map; -import java.util.ServiceLoader; +import org.jspecify.annotations.Nullable; public class MacroCommand extends AbstractCommand { private static final Map macroMap = loadMacroMap(); @@ -73,29 +74,29 @@ public void execute(AbstractUserInterfaceControl uiControl, Parameters args, Eng macro.setParameter(macroParam.getKey(), macroParam.getValue()); } catch (IllegalArgumentException e) { throw new ScriptException(String.format( - "Wrong format for parameter %s of macro %s: %s.\nMessage: %s", - macroParam.getKey(), args.macroName, macroParam.getValue(), - e.getMessage())); + "Wrong format for parameter %s of macro %s: %s.\nMessage: %s", + macroParam.getKey(), args.macroName, macroParam.getValue(), + e.getMessage())); } } else { throw new ScriptException(String.format("Unknown parameter %s for macro %s", - macroParam.getKey(), args.macroName)); + macroParam.getKey(), args.macroName)); } } } Goal g = state.getFirstOpenAutomaticGoal(); ProofMacroFinishedInfo info = - ProofMacroFinishedInfo.getDefaultInfo(macro, state.getProof()); + ProofMacroFinishedInfo.getDefaultInfo(macro, state.getProof()); try { uiControl.taskStarted( - new DefaultTaskStartedInfo(TaskStartedInfo.TaskKind.Macro, macro.getName(), 0)); + new DefaultTaskStartedInfo(TaskStartedInfo.TaskKind.Macro, macro.getName(), 0)); final Sequent sequent = g.node().sequent(); PosInOccurrence pio = null; if (args.occ > -1) { pio = new PosInOccurrence(sequent.getFormulabyNr(args.occ + 1), - PosInTerm.getTopLevel(), args.occ + 1 <= sequent.antecedent().size()); + PosInTerm.getTopLevel(), args.occ + 1 <= sequent.antecedent().size()); } final String matchRegEx = args.matches; @@ -108,7 +109,7 @@ public void execute(AbstractUserInterfaceControl uiControl, Parameters args, Eng } } catch (Exception e) { throw new ScriptException( - "Macro '" + args.macroName + "' raised an exception: " + e.getMessage(), e); + "Macro '" + args.macroName + "' raised an exception: " + e.getMessage(), e); } finally { uiControl.taskFinished(info); macro.resetParams(); @@ -125,27 +126,27 @@ public void execute(AbstractUserInterfaceControl uiControl, Parameters args, Eng * @throws ScriptException */ public static PosInOccurrence extractMatchingPio(final Sequent sequent, final String matchRegEx, - final Services services) throws ScriptException { + final Services services) throws ScriptException { PosInOccurrence pio = null; boolean matched = false; for (int i = 1; i < sequent.size() + 1; i++) { final boolean matchesRegex = formatTermString( - LogicPrinter.quickPrintTerm(sequent.getFormulabyNr(i).formula(), services)) - .matches(".*" + matchRegEx + ".*"); + LogicPrinter.quickPrintTerm(sequent.getFormulabyNr(i).formula(), services)) + .matches(".*" + matchRegEx + ".*"); if (matchesRegex) { if (matched) { throw new ScriptException("More than one occurrence of a matching term."); } matched = true; pio = new PosInOccurrence(sequent.getFormulabyNr(i), PosInTerm.getTopLevel(), - i <= sequent.antecedent().size()); + i <= sequent.antecedent().size()); } } if (!matched) { throw new ScriptException( - String.format("Did not find a formula matching regex %s", matchRegEx)); + String.format("Did not find a formula matching regex %s", matchRegEx)); } return pio; diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RewriteCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RewriteCommand.java index 6b4ee86087f..68f790b14da 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RewriteCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RewriteCommand.java @@ -19,10 +19,11 @@ import de.uka.ilkd.key.rule.RewriteTaclet; import de.uka.ilkd.key.rule.TacletApp; -import org.jspecify.annotations.Nullable; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; +import org.jspecify.annotations.Nullable; + import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY; /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RuleCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RuleCommand.java index 6f2a4582362..098c122f882 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RuleCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RuleCommand.java @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.macros.scripts; +import java.util.*; + import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.PosInOccurrence; @@ -19,12 +21,12 @@ import de.uka.ilkd.key.proof.RuleAppIndex; import de.uka.ilkd.key.proof.rulefilter.TacletFilter; import de.uka.ilkd.key.rule.*; -import org.jspecify.annotations.Nullable; + import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; -import java.util.*; +import org.jspecify.annotations.Nullable; import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY; import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY; @@ -77,21 +79,21 @@ private RuleApp makeRuleApp(Parameters p, EngineState state) throws ScriptExcept final Proof proof = state.getProof(); final Optional maybeBuiltInRule = - proof.getInitConfig().getProfile().getStandardRules().standardBuiltInRules().stream() - .filter(r -> r.name().toString().equals(p.rulename)).findAny(); + proof.getInitConfig().getProfile().getStandardRules().standardBuiltInRules().stream() + .filter(r -> r.name().toString().equals(p.rulename)).findAny(); final Optional maybeTaclet = Optional.ofNullable( - proof.getEnv().getInitConfigForEnvironment().lookupActiveTaclet(new Name(p.rulename))); + proof.getEnv().getInitConfigForEnvironment().lookupActiveTaclet(new Name(p.rulename))); if (!maybeBuiltInRule.isPresent() && !maybeTaclet.isPresent()) { /* * (DS, 2019-01-31): Might be a locally introduced taclet, e.g., by hide_left etc. */ final Optional maybeApp = Optional.ofNullable( - state.getFirstOpenAutomaticGoal().indexOfTaclets().lookup(p.rulename)); + state.getFirstOpenAutomaticGoal().indexOfTaclets().lookup(p.rulename)); TacletApp app = maybeApp.orElseThrow( - () -> new ScriptException("Taclet '" + p.rulename + "' not known.")); + () -> new ScriptException("Taclet '" + p.rulename + "' not known.")); if (app.taclet() instanceof FindTaclet) { app = findTacletApp(p, state); @@ -111,7 +113,7 @@ private RuleApp makeRuleApp(Parameters p, EngineState state) throws ScriptExcept return instantiateTacletApp(p, state, proof, theApp); } else { IBuiltInRuleApp builtInRuleApp = // - builtInRuleApp(p, state, maybeBuiltInRule.get()); + builtInRuleApp(p, state, maybeBuiltInRule.get()); if (builtInRuleApp.isSufficientlyComplete()) { builtInRuleApp = builtInRuleApp.forceInstantiate(state.getFirstOpenAutomaticGoal()); } @@ -120,7 +122,7 @@ private RuleApp makeRuleApp(Parameters p, EngineState state) throws ScriptExcept } private @Nullable TacletApp instantiateTacletApp(final Parameters p, final EngineState state, - final Proof proof, final TacletApp theApp) throws ScriptException { + final Proof proof, final TacletApp theApp) throws ScriptException { TacletApp result; Services services = proof.getServices(); @@ -150,7 +152,7 @@ private RuleApp makeRuleApp(Parameters p, EngineState state) throws ScriptExcept * "\newPV", Skolem terms etc. */ final TacletApp maybeInstApp = result.tryToInstantiateAsMuchAsPossible( - services.getOverlay(state.getFirstOpenAutomaticGoal().getLocalNamespaces())); + services.getOverlay(state.getFirstOpenAutomaticGoal().getLocalNamespaces())); if (maybeInstApp != null) { result = maybeInstApp; @@ -175,7 +177,7 @@ private RuleApp makeRuleApp(Parameters p, EngineState state) throws ScriptExcept // try to instantiate remaining symbols result = result.tryToInstantiate( - services.getOverlay(state.getFirstOpenAutomaticGoal().getLocalNamespaces())); + services.getOverlay(state.getFirstOpenAutomaticGoal().getLocalNamespaces())); if (result == null) { throw new ScriptException("Cannot instantiate this rule"); @@ -183,7 +185,7 @@ private RuleApp makeRuleApp(Parameters p, EngineState state) throws ScriptExcept if (recheckMatchConditions) { final MatchConditions appMC = - result.taclet().getMatcher().checkConditions(result.matchConditions(), services); + result.taclet().getMatcher().checkConditions(result.matchConditions(), services); if (appMC == null) { return null; } else { @@ -201,8 +203,8 @@ private TacletApp makeNoFindTacletApp(Taclet taclet) { private IBuiltInRuleApp builtInRuleApp(Parameters p, EngineState state, BuiltInRule rule) throws ScriptException { final List matchingApps = // - findBuiltInRuleApps(p, state).stream().filter(r -> r.rule().name().equals(rule.name())) - .toList(); + findBuiltInRuleApps(p, state).stream().filter(r -> r.rule().name().equals(rule.name())) + .toList(); if (matchingApps.isEmpty()) { throw new ScriptException("No matching applications."); @@ -217,7 +219,7 @@ private IBuiltInRuleApp builtInRuleApp(Parameters p, EngineState state, BuiltInR } else { if (p.occ >= matchingApps.size()) { throw new ScriptException("Occurence " + p.occ - + " has been specified, but there are only " + matchingApps.size() + " hits."); + + " has been specified, but there are only " + matchingApps.size() + " hits."); } return matchingApps.get(p.occ); @@ -241,7 +243,7 @@ private TacletApp findTacletApp(Parameters p, EngineState state) throws ScriptEx } else { if (p.occ >= matchingApps.size()) { throw new ScriptException("Occurence " + p.occ - + " has been specified, but there are only " + matchingApps.size() + " hits."); + + " has been specified, but there are only " + matchingApps.size() + " hits."); } return matchingApps.get(p.occ); } @@ -260,7 +262,7 @@ private ImmutableList findBuiltInRuleApps(Parameters p, EngineS } allApps = allApps.append( - index.getBuiltInRule(g, new PosInOccurrence(sf, PosInTerm.getTopLevel(), true))); + index.getBuiltInRule(g, new PosInOccurrence(sf, PosInTerm.getTopLevel(), true))); } for (SequentFormula sf : g.node().sequent().succedent()) { @@ -269,7 +271,7 @@ private ImmutableList findBuiltInRuleApps(Parameters p, EngineS } allApps = allApps.append( - index.getBuiltInRule(g, new PosInOccurrence(sf, PosInTerm.getTopLevel(), false))); + index.getBuiltInRule(g, new PosInOccurrence(sf, PosInTerm.getTopLevel(), false))); } return allApps; @@ -290,7 +292,7 @@ private ImmutableList findAllTacletApps(Parameters p, EngineState sta } allApps = allApps.append(index.getTacletAppAtAndBelow(filter, - new PosInOccurrence(sf, PosInTerm.getTopLevel(), true), services)); + new PosInOccurrence(sf, PosInTerm.getTopLevel(), true), services)); } for (SequentFormula sf : g.node().sequent().succedent()) { @@ -299,7 +301,7 @@ private ImmutableList findAllTacletApps(Parameters p, EngineState sta } allApps = allApps.append(index.getTacletAppAtAndBelow(filter, - new PosInOccurrence(sf, PosInTerm.getTopLevel(), false), services)); + new PosInOccurrence(sf, PosInTerm.getTopLevel(), false), services)); } return allApps; @@ -310,17 +312,17 @@ private ImmutableList findAllTacletApps(Parameters p, EngineState sta * {@link Parameters#formula} parameter or its String representation matches the * {@link Parameters#matches} regex. If both parameters are not supplied, always returns true. * - * @param p The {@link Parameters} object. + * @param p The {@link Parameters} object. * @param sf The {@link SequentFormula} to check. * @return true if sf matches. */ private boolean isFormulaSearchedFor(Parameters p, SequentFormula sf, Services services) { final boolean satisfiesFormulaParameter = - p.formula != null && sf.formula().equalsModProperty(p.formula, RENAMING_PROPERTY); + p.formula != null && sf.formula().equalsModProperty(p.formula, RENAMING_PROPERTY); final boolean satisfiesMatchesParameter = p.matches != null && formatTermString(LogicPrinter.quickPrintTerm(sf.formula(), services)) - .matches(".*" + p.matches + ".*"); + .matches(".*" + p.matches + ".*"); return (p.formula == null && p.matches == null) || satisfiesFormulaParameter || satisfiesMatchesParameter; @@ -346,15 +348,15 @@ private List filterList(Parameters p, ImmutableList list) for (TacletApp tacletApp : list) { if (tacletApp instanceof PosTacletApp pta) { boolean add = - p.on == null || pta.posInOccurrence().subTerm() - .equalsModProperty(p.on, RENAMING_PROPERTY); + p.on == null || pta.posInOccurrence().subTerm() + .equalsModProperty(p.on, RENAMING_PROPERTY); Iterator it = pta.instantiations().svIterator(); while (it.hasNext()) { SchemaVariable sv = it.next(); Term userInst = p.instantiations.get(sv.name().toString()); Object ptaInst = - pta.instantiations().getInstantiationEntry(sv).getInstantiation(); + pta.instantiations().getInstantiationEntry(sv).getInstantiation(); add &= userInst == null || userInst.equalsModProperty(ptaInst, IRRELEVANT_TERM_LABELS_PROPERTY); diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptNode.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptNode.java index 0c1501e1dba..63568ad614f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptNode.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptNode.java @@ -3,15 +3,16 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.macros.scripts; +import java.util.LinkedList; +import java.util.List; +import java.util.Map; + import de.uka.ilkd.key.proof.Node; + import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.util.LinkedList; -import java.util.List; -import java.util.Map; - public class ScriptNode { private static final Logger LOGGER = LoggerFactory.getLogger(ScriptNode.class); @@ -23,7 +24,8 @@ public class ScriptNode { private @Nullable Node proofNode; private @Nullable Throwable encounteredException; - public ScriptNode(@Nullable ScriptNode parent, Map command, int fromPos, int toPos) { + public ScriptNode(@Nullable ScriptNode parent, Map command, int fromPos, + int toPos) { this.parent = parent; this.command = command; this.fromPos = fromPos; @@ -36,7 +38,7 @@ public void addNode(ScriptNode node) { public void dump(int indent) { LOGGER.debug("{} {} {}", " ".repeat(indent), - proofNode == null ? "xxx" : proofNode.serialNr(), command); + proofNode == null ? "xxx" : proofNode.serialNr(), command); for (ScriptNode child : children) { child.dump(indent + 1); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetCommand.java index b9b1193c361..a8413690617 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetCommand.java @@ -13,6 +13,7 @@ import de.uka.ilkd.key.strategy.Strategy; import de.uka.ilkd.key.strategy.StrategyFactory; import de.uka.ilkd.key.strategy.StrategyProperties; + import org.jspecify.annotations.Nullable; public class SetCommand extends AbstractCommand { diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/package-info.java index 5c6f5617587..a6cc13e06fa 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/package-info.java @@ -2,6 +2,7 @@ * @author Alexander Weigl * @version 1 (03.05.24) */ -@NullMarked package de.uka.ilkd.key.macros.scripts.meta; +@NullMarked +package de.uka.ilkd.key.macros.scripts.meta; -import org.jspecify.annotations.NullMarked; \ No newline at end of file +import org.jspecify.annotations.NullMarked; diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/package-info.java index 9164279fdfe..c5d5ae32248 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/package-info.java @@ -2,6 +2,7 @@ * @author Alexander Weigl * @version 1 (29.03.17) */ -@NullMarked package de.uka.ilkd.key.macros.scripts; +@NullMarked +package de.uka.ilkd.key.macros.scripts; -import org.jspecify.annotations.NullMarked; \ No newline at end of file +import org.jspecify.annotations.NullMarked; 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 1629b12bb76..c21b9f03c63 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 @@ -3,6 +3,9 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.pp; +import java.util.Iterator; +import java.util.Set; + import de.uka.ilkd.key.control.TermLabelVisibilityManager; import de.uka.ilkd.key.java.JavaInfo; import de.uka.ilkd.key.java.ProgramElement; @@ -23,18 +26,17 @@ import de.uka.ilkd.key.rule.tacletbuilder.TacletGoalTemplate; import de.uka.ilkd.key.util.UnicodeHelper; import de.uka.ilkd.key.util.pp.UnbalancedBlocksException; -import org.jspecify.annotations.Nullable; + import org.key_project.logic.op.Function; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSet; + +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.util.Iterator; -import java.util.Set; - import static de.uka.ilkd.key.pp.PosTableLayouter.DEFAULT_LINE_WIDTH; @@ -76,7 +78,7 @@ public class LogicPrinter { private final StorePrinter storePrinter; private QuantifiableVariablePrintMode quantifiableVariablePrintMode = - QuantifiableVariablePrintMode.NORMAL; + QuantifiableVariablePrintMode.NORMAL; private enum QuantifiableVariablePrintMode { NORMAL, WITH_OUT_DECLARATION @@ -87,8 +89,8 @@ private enum QuantifiableVariablePrintMode { * Java programs and a NotationInfo which determines the concrete syntax. * * @param notationInfo the NotationInfo for the concrete syntax - * @param services services. - * @param layouter the layouter to use + * @param services services. + * @param layouter the layouter to use */ public LogicPrinter(NotationInfo notationInfo, Services services, PosTableLayouter layouter) { this.notationInfo = notationInfo; @@ -105,7 +107,7 @@ public LogicPrinter(NotationInfo notationInfo, Services services, PosTableLayout * Creates a LogicPrinter that does not create a position table. * * @param notationInfo the NotationInfo for the concrete syntax - * @param services The Services object + * @param services The Services object */ public static LogicPrinter purePrinter(NotationInfo notationInfo, @Nullable Services services) { return new LogicPrinter(notationInfo, services, PosTableLayouter.pure()); @@ -119,7 +121,7 @@ public PosTableLayouter layouter() { } public static SequentViewLogicPrinter quickPrinter(Services services, - boolean usePrettyPrinting, boolean useUnicodeSymbols) { + boolean usePrettyPrinting, boolean useUnicodeSymbols) { final NotationInfo ni = new NotationInfo(); if (services != null) { ni.refresh(services, usePrettyPrinting, useUnicodeSymbols); @@ -134,26 +136,26 @@ public static SequentViewLogicPrinter quickPrinter(Services services, /** * Converts a term to a string. * - * @param t a term. + * @param t a term. * @param services services. * @return the printed term. */ public static String quickPrintTerm(Term t, Services services) { return quickPrintTerm(t, services, NotationInfo.DEFAULT_PRETTY_SYNTAX, - NotationInfo.DEFAULT_UNICODE_ENABLED); + NotationInfo.DEFAULT_UNICODE_ENABLED); } /** * Converts a term to a string. * - * @param t a term. - * @param services services. + * @param t a term. + * @param services services. * @param usePrettyPrinting whether to use pretty-printing. * @param useUnicodeSymbols whether to use unicode symbols. * @return the printed term. */ public static String quickPrintTerm(Term t, Services services, boolean usePrettyPrinting, - boolean useUnicodeSymbols) { + boolean useUnicodeSymbols) { var p = quickPrinter(services, usePrettyPrinting, useUnicodeSymbols); p.printTerm(t); return p.result(); @@ -162,13 +164,13 @@ public static String quickPrintTerm(Term t, Services services, boolean usePretty /** * Converts a semisequent to a string. * - * @param s a semisequent. + * @param s a semisequent. * @param services services. * @return the printed semisequent. */ public static String quickPrintSemisequent(Semisequent s, Services services) { var p = quickPrinter(services, NotationInfo.DEFAULT_PRETTY_SYNTAX, - NotationInfo.DEFAULT_UNICODE_ENABLED); + NotationInfo.DEFAULT_UNICODE_ENABLED); p.printSemisequent(s); return p.result(); } @@ -176,13 +178,13 @@ public static String quickPrintSemisequent(Semisequent s, Services services) { /** * Converts a sequent to a string. * - * @param s a sequent. + * @param s a sequent. * @param services services. * @return the printed sequent. */ public static String quickPrintSequent(Sequent s, Services services) { var p = quickPrinter(services, NotationInfo.DEFAULT_PRETTY_SYNTAX, - NotationInfo.DEFAULT_UNICODE_ENABLED); + NotationInfo.DEFAULT_UNICODE_ENABLED); p.printSequent(s); return p.result(); } @@ -216,9 +218,9 @@ public void setLineWidth(int lineWidth) { * Reprints the sequent. This can be useful if settings like PresentationFeatures or * abbreviations have changed. * - * @param filter The SequentPrintFilter for seq + * @param filter The SequentPrintFilter for seq * @param lineWidth the max. number of character to put on one line (the actual taken linewidth - * is the max of {@link PosTableLayouter#DEFAULT_LINE_WIDTH} and the given value + * is the max of {@link PosTableLayouter#DEFAULT_LINE_WIDTH} and the given value */ public void update(SequentPrintFilter filter, int lineWidth) { setLineWidth(lineWidth); @@ -238,14 +240,14 @@ public void setInstantiation(SVInstantiations instantiations) { /** * Pretty-print a taclet. Line-breaks are taken care of. * - * @param taclet The Taclet to be pretty-printed. - * @param sv The instantiations of the SchemaVariables - * @param showWholeTaclet Should the find, varcond and heuristic part be pretty-printed? + * @param taclet The Taclet to be pretty-printed. + * @param sv The instantiations of the SchemaVariables + * @param showWholeTaclet Should the find, varcond and heuristic part be pretty-printed? * @param declareSchemaVars Should declarations for the schema variables used in the taclet be - * pretty-printed? + * pretty-printed? */ public void printTaclet(Taclet taclet, SVInstantiations sv, boolean showWholeTaclet, - boolean declareSchemaVars) { + boolean declareSchemaVars) { instantiations = sv; quantifiableVariablePrintMode = QuantifiableVariablePrintMode.WITH_OUT_DECLARATION; @@ -431,7 +433,7 @@ protected void printHeuristics(Taclet taclet) { return; } layouter.nl().beginRelativeC().print("\\heuristics(").brk(0); - for (Iterator it = taclet.getRuleSets().iterator(); it.hasNext(); ) { + for (Iterator it = taclet.getRuleSets().iterator(); it.hasNext();) { RuleSet tgt = it.next(); printHeuristic(tgt); if (it.hasNext()) { @@ -504,7 +506,7 @@ protected void printGoalTemplates(Taclet taclet) { } for (final Iterator it = taclet.goalTemplates().reverse().iterator(); it - .hasNext(); ) { + .hasNext();) { printGoalTemplate(it.next()); if (it.hasNext()) { layouter.print(";"); @@ -596,15 +598,15 @@ protected void printSchemaVariable(SchemaVariable sv) { private void printSourceElement(SourceElement element) { new PrettyPrinter(layouter, instantiations, services, - notationInfo.isPrettySyntax(), - notationInfo.isUnicodeEnabled()).print(element); + notationInfo.isPrettySyntax(), + notationInfo.isUnicodeEnabled()).print(element); } /** * Pretty-prints a ProgramElement. * * @param pe You've guessed it, the ProgramElement to be pretty-printedprint(Term t, - * LogicPrinter sp) + * LogicPrinter sp) */ public void printProgramElement(ProgramElement pe) { if (pe instanceof ProgramVariable) { @@ -788,7 +790,7 @@ public void printTerm(Term t) { * * @param t {@link Term} whose visible {@link TermLabel}s will be determined. * @return List of visible {@link TermLabel}s, i.e. labels that are syntactically added to a - * {@link Term} while printing. + * {@link Term} while printing. */ protected ImmutableArray getVisibleTermLabels(Term t) { return t.getLabels(); @@ -1160,8 +1162,8 @@ public void printObserver(Term t, Term tacitHeap) { String p; try { boolean canonical = - obs.isStatic() || ((obs instanceof IProgramMethod) && javaInfo - .isCanonicalProgramMethod((IProgramMethod) obs, keYJavaType)); + obs.isStatic() || ((obs instanceof IProgramMethod) && javaInfo + .isCanonicalProgramMethod((IProgramMethod) obs, keYJavaType)); if (canonical) { p = fieldName; } else { @@ -1307,9 +1309,9 @@ public void printElementOf(Term t, String symbol) { * possible. * * @param name the prefix operator - * @param t whole term - * @param sub the subterm to be printed - * @param ass the associativity for the subterm + * @param t whole term + * @param sub the subterm to be printed + * @param ass the associativity for the subterm */ public void printPrefixTerm(String name, Term t, Term sub, int ass) { layouter.startTerm(1); @@ -1328,8 +1330,8 @@ public void printPrefixTerm(String name, Term t, Term sub, int ass) { * the postfix operator. No line breaks are possible. * * @param name the postfix operator - * @param t the subterm to be printed - * @param ass the associativity for the subterm + * @param t the subterm to be printed + * @param ass the associativity for the subterm */ public void printPostfixTerm(Term t, int ass, String name) { layouter.startTerm(1); @@ -1348,11 +1350,11 @@ public void printPostfixTerm(Term t, int ass, String name) { *

* The subterms are printed using {@link #printTermContinuingBlock(Term)}. * - * @param l the left subterm - * @param assLeft associativity for left subterm - * @param name the infix operator - * @param t whole term - * @param r the right subterm + * @param l the left subterm + * @param assLeft associativity for left subterm + * @param name the infix operator + * @param t whole term + * @param r the right subterm * @param assRight associativity for right subterm */ public void printInfixTerm(Term l, int assLeft, String name, Term t, Term r, int assRight) { @@ -1367,15 +1369,15 @@ public void printInfixTerm(Term l, int assLeft, String name, Term t, Term r, int * {@link #printTermContinuingBlock(Term)} for the idea. Otherwise, like * {@link #printInfixTerm(Term, int, String, Term, Term, int)}. * - * @param l the left subterm - * @param assLeft associativity for left subterm - * @param name the infix operator - * @param t whole term - * @param r the right subterm + * @param l the left subterm + * @param assLeft associativity for left subterm + * @param name the infix operator + * @param t whole term + * @param r the right subterm * @param assRight associativity for right subterm */ public void printInfixTermContinuingBlock(Term l, int assLeft, String name, Term t, Term r, - int assRight) { + int assRight) { boolean isKeyword = false; if (services != null) { LocSetLDT loc = services.getTypeConverter().getLocSetLDT(); @@ -1407,9 +1409,9 @@ public void printInfixTermContinuingBlock(Term l, int assLeft, String name, Term * t * * - * @param l the left brace - * @param r the right brace - * @param t the update term + * @param l the left brace + * @param r the right brace + * @param t the update term * @param ass3 associativity for phi */ public void printUpdateApplicationTerm(String l, String r, Term t, int ass3) { @@ -1483,7 +1485,7 @@ public void printParallelUpdate(String separator, Term t, int ass) { } private void printVariables(ImmutableArray vars, - QuantifiableVariablePrintMode mode) { + QuantifiableVariablePrintMode mode) { int size = vars.size(); for (int j = 0; j != size; j++) { final QuantifiableVariable v = vars.get(j); @@ -1555,16 +1557,16 @@ public void printIfThenElseTerm(Term t, String keyword) { * s * * - * @param l the String used as left brace symbol - * @param v the {@link QuantifiableVariable} to be substituted - * @param t the Term to be used as new value + * @param l the String used as left brace symbol + * @param v the {@link QuantifiableVariable} to be substituted + * @param t the Term to be used as new value * @param ass2 the int defining the associativity for the new value - * @param r the String used as right brace symbol - * @param phi the substituted term/formula + * @param r the String used as right brace symbol + * @param phi the substituted term/formula * @param ass3 the int defining the associativity for phi */ public void printSubstTerm(String l, QuantifiableVariable v, Term t, int ass2, String r, - Term phi, int ass3) { + Term phi, int ass3) { layouter.beginC().print(l); printVariables(new ImmutableArray<>(v), quantifiableVariablePrintMode); layouter.startTerm(2); @@ -1588,11 +1590,11 @@ public void printSubstTerm(String l, QuantifiableVariable v, Term t, int ass2, S * * @param name the name of the quantifier * @param vars the quantified variables (+colon and sort) - * @param phi the quantified formula - * @param ass associativity for phi + * @param phi the quantified formula + * @param ass associativity for phi */ public void printQuantifierTerm(String name, ImmutableArray vars, - Term phi, int ass) { + Term phi, int ass) { layouter.beginC(); layouter.keyWord(name); layouter.print(" "); @@ -1669,9 +1671,9 @@ public void printModalityTerm(String left, JavaBlock jb, String right, Term phi, ta[i] = phi.sub(i); } final Modality m = - Modality.getModality((Modality.JavaModalityKind) o, mod.program()); + Modality.getModality((Modality.JavaModalityKind) o, mod.program()); final Term term = services.getTermFactory().createTerm(m, ta, - phi.boundVars(), null); + phi.boundVars(), null); notationInfo.getNotation(m).print(term, this); return; } @@ -1722,7 +1724,7 @@ public String result() { * {@link #printTermContinuingBlock(Term)}. This currently only makes a difference for infix * operators. * - * @param t the subterm to print + * @param t the subterm to print * @param ass the associativity for this subterm */ protected void maybeParens(Term t, int ass) { @@ -1768,7 +1770,7 @@ public SVInstantiations getInstantiations() { * printInShortForm methods it takes care of meta variable instantiations * * @param attributeProgramName the String of the attribute's program name - * @param t the Term used as reference prefix + * @param t the Term used as reference prefix * @return true if an attribute term shall be printed in short form. */ public boolean printInShortForm(String attributeProgramName, Term t) { @@ -1782,7 +1784,7 @@ public boolean printInShortForm(String attributeProgramName, Term t) { * way * * @param programName the String denoting the program name of the attribute - * @param sort the ObjectSort in whose reachable hierarchy we test for uniqueness + * @param sort the ObjectSort in whose reachable hierarchy we test for uniqueness * @return true if the attribute is uniquely determined */ public boolean printInShortForm(String programName, Sort sort) { @@ -1801,21 +1803,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("<"); - 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); + 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); } } @@ -1827,8 +1829,8 @@ public static String escapeHTML(String text, boolean escapeWhitespace) { * way * * @param programName the String denoting the program name of the attribute - * @param sort the ObjectSort specifying the hierarchy where to test for uniqueness - * @param services the Services class used to access the type hierarchy + * @param sort the ObjectSort specifying the hierarchy where to test for uniqueness + * @param services the Services class used to access the type hierarchy * @return true if the attribute is uniquely determined */ public static boolean printInShortForm(String programName, Sort sort, Services services) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java index 7386d12018f..ffd24b4f856 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java @@ -47,12 +47,12 @@ import de.uka.ilkd.key.util.KeYConstants; import de.uka.ilkd.key.util.MiscTools; -import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableMapEntry; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -850,7 +850,8 @@ private static String printSequent(Sequent val, Services services) { return printer.result(); } - private static LogicPrinter createLogicPrinter(@Nullable Services serv, boolean shortAttrNotation) { + private static LogicPrinter createLogicPrinter(@Nullable Services serv, + boolean shortAttrNotation) { final NotationInfo ni = new NotationInfo(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java index ef5723e981c..0a9e0da4bd5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java @@ -127,40 +127,45 @@ public void writeSettings(Configuration props) { }); } - protected PropertyEntry createDoubleProperty(@UnknownInitialization AbstractPropertiesSettings this, - String key, double defValue) { + protected PropertyEntry createDoubleProperty( + @UnknownInitialization AbstractPropertiesSettings this, + String key, double defValue) { PropertyEntry pe = new DefaultPropertyEntry<>(key, defValue, parseDouble, (it) -> (double) it); propertyEntries.add(pe); return pe; } - protected PropertyEntry createIntegerProperty(@UnknownInitialization AbstractPropertiesSettings this, - String key, int defValue) { + protected PropertyEntry createIntegerProperty( + @UnknownInitialization AbstractPropertiesSettings this, + String key, int defValue) { PropertyEntry pe = new DefaultPropertyEntry<>(key, defValue, parseInt, (it) -> Math.toIntExact((Long) it)); propertyEntries.add(pe); return pe; } - protected PropertyEntry createFloatProperty(@UnknownInitialization AbstractPropertiesSettings this, - String key, float defValue) { + protected PropertyEntry createFloatProperty( + @UnknownInitialization AbstractPropertiesSettings this, + String key, float defValue) { PropertyEntry pe = new DefaultPropertyEntry<>(key, defValue, parseFloat, (it) -> (float) (double) it); propertyEntries.add(pe); return pe; } - protected PropertyEntry createStringProperty(@UnknownInitialization AbstractPropertiesSettings this, - String key, String defValue) { + protected PropertyEntry createStringProperty( + @UnknownInitialization AbstractPropertiesSettings this, + String key, String defValue) { PropertyEntry pe = new DefaultPropertyEntry<>(key, defValue, id -> id, Object::toString); propertyEntries.add(pe); return pe; } - protected PropertyEntry createBooleanProperty(@UnknownInitialization AbstractPropertiesSettings this, - String key, boolean defValue) { + protected PropertyEntry createBooleanProperty( + @UnknownInitialization AbstractPropertiesSettings this, + String key, boolean defValue) { PropertyEntry pe = new DefaultPropertyEntry<>(key, defValue, parseBoolean, (it) -> (Boolean) it); propertyEntries.add(pe); diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java index e6f7cd85174..c2b7011eb5a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java @@ -17,7 +17,6 @@ import de.uka.ilkd.key.logic.Choice; import de.uka.ilkd.key.logic.Namespace; -import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableList; @@ -25,6 +24,7 @@ import org.key_project.util.collection.ImmutableSet; import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; /** * diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java index 8c007a93307..b669ed5eb49 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java @@ -3,18 +3,19 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.settings; -import de.uka.ilkd.key.nparser.ParsingFacade; -import de.uka.ilkd.key.util.Position; -import org.antlr.v4.runtime.CharStream; -import org.jspecify.annotations.NonNull; -import org.jspecify.annotations.Nullable; - import java.io.File; import java.io.IOException; import java.io.PrintWriter; import java.io.Writer; import java.util.*; +import de.uka.ilkd.key.nparser.ParsingFacade; +import de.uka.ilkd.key.util.Position; + +import org.antlr.v4.runtime.CharStream; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + /** * A container to hold parsed configurations. Configurations are a mapping between property names @@ -86,8 +87,8 @@ public boolean exists(String name, Class clazz) { * Returns the stored value for the given name casted to the given clazz if possible. * If no value exists, or value is not compatible to {@code clazz}, {@code null} is returned. * - * @param an arbitrary class, exptected return type - * @param name property name + * @param an arbitrary class, exptected return type + * @param name property name * @param clazz data type because of missing reified generics. */ public @Nullable T get(String name, Class clazz) { @@ -101,13 +102,14 @@ public boolean exists(String name, Class clazz) { * The same as {@link #get(String, Class)} but returns the {@code defaultValue} instead * of a {@code null} reference. * - * @param the expected return type compatible to the {@code defaultValue} - * @param name property name + * @param the expected return type compatible to the {@code defaultValue} + * @param name property name * @param defaultValue the returned instead of {@code null}. */ + @SuppressWarnings("unchecked") public T get(String name, T defaultValue) { if (exists(name, defaultValue.getClass())) - return clazz.cast(data.get(name)); + return (T) defaultValue.getClass().cast(data.get(name)); else return defaultValue; } @@ -137,7 +139,7 @@ public int getInt(String name) { * Returns an integer value for the given name. * * @param name property name - * @throws ClassCastException if the entry is not a {@link Long} + * @throws ClassCastException if the entry is not a {@link Long} * @throws NullPointerException if no such value entry exists */ public int getInt(String name, int defaultValue) { @@ -148,7 +150,7 @@ public int getInt(String name, int defaultValue) { * Returns a long value for the given name. * * @param name property name - * @throws ClassCastException if the entry is not a {@link Long} + * @throws ClassCastException if the entry is not a {@link Long} * @throws NullPointerException if no such value entry exists */ public long getLong(String name) { @@ -159,7 +161,7 @@ public long getLong(String name) { * Returns a long value for the given name. {@code defaultValue} if no such value is present. * * @param name property name - * @throws ClassCastException if the entry is not an {@link Long} + * @throws ClassCastException if the entry is not an {@link Long} * @throws NullPointerException if no such value entry exists */ public long getLong(String name, long defaultValue) { @@ -171,7 +173,7 @@ public long getLong(String name, long defaultValue) { * Returns a boolean value for the given name. * * @param name property name - * @throw ClassCastException if the entry is not an {@link #Long} + * @throw ClassCastException if the entry is not an {@link Long} * @throw NullPointerException if no such value entry exists */ public boolean getBool(String name) { @@ -182,11 +184,11 @@ public boolean getBool(String name) { * Returns a boolean value for the given name. {@code defaultValue} if no such value is present. * * @param name property name - * @throws ClassCastException if the entry is not an {@link Long} + * @throws ClassCastException if the entry is not an {@link Long} * @throws NullPointerException if no such value entry exists */ public boolean getBool(String name, boolean defaultValue) { - return get(name, Boolean.class, defaultValue); + return get(name, defaultValue); } /** @@ -194,7 +196,7 @@ public boolean getBool(String name, boolean defaultValue) { * present. * * @param name property name - * @throws ClassCastException if the entry is not an {@link Long} + * @throws ClassCastException if the entry is not an {@link Long} * @throws NullPointerException if no such value entry exists */ public double getDouble(String name) { @@ -219,7 +221,7 @@ public String getString(String name) { * @throws ClassCastException if the entry is not an {@link String} */ public String getString(String name, String defaultValue) { - return get(name, String.class, defaultValue); + return get(name, defaultValue); } /** @@ -268,7 +270,7 @@ public List getList(String name) { /** * Returns a list of strings for the given name. - * + *

* In contrast to the other methods, this method does not throw an exception if the entry does * not * exist in the configuration. Instead, it returns an empty list. @@ -292,7 +294,7 @@ public List getList(String name) { * Returns string array for the requested entry. {@code defaultValue} is returned if no such * entry exists. * - * @param name a string identifying the entry + * @param name a string identifying the entry * @param defaultValue a default value * @throws ClassCastException if the given entry has non-string elements */ @@ -314,7 +316,7 @@ public String[] getStringArray(String name, @NonNull String[] defaultValue) { * @throws IllegalArgumentException if defaultValue does not belong to an enum */ @SuppressWarnings("unchecked") - public > @NonNull T getEnum(String name, @NonNull T defaultValue) { + public > T getEnum(String name, T defaultValue) { Class clazz = (Class) defaultValue.getClass(); if (!clazz.isEnum()) { throw new IllegalArgumentException(clazz + " is not an enum type."); @@ -405,27 +407,10 @@ public Set> getEntries() { return data.entrySet(); } - /** - * Interprets the given entry as an enum value. - * - * @param the enum - * @param name a name identifying an entry - * @param defaultValue the default value to be returned - */ - public > T getEnum(String name, T defaultValue) { - var idx = getString(name); - try { - if (idx != null) - return Enum.valueOf((Class) defaultValue.getClass(), idx); - } catch (IllegalArgumentException | NullPointerException ignored) { - } - return defaultValue; - } - /** * Serializes this configuration instance into the given writer. * - * @param writer a writer + * @param writer a writer * @param comment a comment */ public void save(Writer writer, String comment) { @@ -437,6 +422,7 @@ public void overwriteWith(Configuration other) { } // TODO Add documentation for this. + /** * POJO for metadata of configuration entries. */ @@ -534,7 +520,7 @@ private ConfigurationWriter printMap(Map value) { indent += 4; newline().printIndent(); for (Iterator> iterator = - value.entrySet().iterator(); iterator.hasNext(); ) { + value.entrySet().iterator(); iterator.hasNext();) { Map.Entry entry = iterator.next(); String k = entry.getKey().toString(); Object v = entry.getValue(); 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 2e1303d8e7b..7d43cb130e1 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 @@ -548,7 +548,8 @@ public static boolean isJMLComment(String comment) { * @param node the Node where to look up the actual variable (result from renaming) * @return The renamed variable */ - public static ProgramVariable findActualVariable(ProgramVariable originalVar, @Nullable Node node) { + public static ProgramVariable findActualVariable(ProgramVariable originalVar, + @Nullable Node node) { if (node != null) { do { if (node.getRenamingTable() != null) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/parsing/BuildingException.java b/key.core/src/main/java/de/uka/ilkd/key/util/parsing/BuildingException.java index d832e047e06..06e9b984628 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/parsing/BuildingException.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/parsing/BuildingException.java @@ -30,7 +30,8 @@ public BuildingException(@Nullable Throwable e) { offendingSymbol = null; } - public BuildingException(@Nullable ParserRuleContext ctx, String message, @Nullable Throwable e) { + public BuildingException(@Nullable ParserRuleContext ctx, String message, + @Nullable Throwable e) { this(ctx == null ? null : ctx.start, message, e); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java b/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java index 1e29fb86043..c20e2d5600e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java @@ -3,15 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.util.parsing; -import de.uka.ilkd.key.java.Position; -import de.uka.ilkd.key.parser.Location; -import de.uka.ilkd.key.util.MiscTools; -import org.antlr.v4.runtime.*; -import org.jspecify.annotations.Nullable; -import org.key_project.util.java.StringUtil; -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - import java.net.MalformedURLException; import java.net.URI; import java.util.ArrayList; @@ -20,6 +11,17 @@ import java.util.function.Supplier; import java.util.stream.Collectors; +import de.uka.ilkd.key.java.Position; +import de.uka.ilkd.key.parser.Location; +import de.uka.ilkd.key.util.MiscTools; + +import org.key_project.util.java.StringUtil; + +import org.antlr.v4.runtime.*; +import org.jspecify.annotations.Nullable; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + /** * An ANTLR4 error listener that stores the errors internally. You can disable the additional * printing of message on the logger {@link #logger} flag. @@ -54,21 +56,21 @@ public SyntaxErrorReporter(@Nullable Class loggerCategory, boolean throwDirec @Override public void syntaxError(Recognizer recognizer, @Nullable Object offendingSymbol, int line, - int charPositionInLine, String msg, RecognitionException e) { + int charPositionInLine, String msg, RecognitionException e) { Parser parser = (Parser) recognizer; String stack = String.join(", ", parser.getRuleInvocationStack()); Token tok = (Token) offendingSymbol; if (tok == null) { throw new IllegalArgumentException( - "offendedSymbol is null. Use SyntaxErrorReporter only in Parsers"); + "offendedSymbol is null. Use SyntaxErrorReporter only in Parsers"); } SyntaxError se = new SyntaxError(recognizer, line, tok, charPositionInLine, msg, - MiscTools.getURIFromTokenSource(tok.getTokenSource()), stack); + MiscTools.getURIFromTokenSource(tok.getTokenSource()), stack); if (logger != null) { logger.warn("[syntax-error] {}:{}:{}: {} {} ({})", se.source, line, charPositionInLine, - msg, tok, stack); + msg, tok, stack); } errors.add(se); @@ -140,7 +142,7 @@ public static class SyntaxError { final String stack; public SyntaxError(Recognizer recognizer, int line, Token offendingSymbol, - int charPositionInLine, String msg, URI source, String stack) { + int charPositionInLine, String msg, URI source, String stack) { this.recognizer = recognizer; this.line = line; this.offendingSymbol = offendingSymbol; @@ -152,13 +154,13 @@ public SyntaxError(Recognizer recognizer, int line, Token offendingSymbol, public String getBeatifulErrorMessage(String[] lines) { return ("syntax-error in " + positionAsUrl() + "\n" + msg + "\n" + showInInput(lines) - + "\n"); + + "\n"); } public String showInInput(String[] lines) { String line = lines[this.line]; return line + "\n" + StringUtil.repeat(" ", (charPositionInLine - 1)) - + StringUtil.repeat("^", (offendingSymbol.getText().length())); + + StringUtil.repeat("^", (offendingSymbol.getText().length())); } public String positionAsUrl() { @@ -196,7 +198,7 @@ public Location getLocation() throws MalformedURLException { SyntaxError e = errors.get(0); // e.charPositionInLine is 0 based! return new Location(e.source, - Position.fromOneZeroBased(e.line, e.charPositionInLine)); + Position.fromOneZeroBased(e.line, e.charPositionInLine)); } return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/parsing/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/util/parsing/package-info.java index 95c2d8a3589..9a361feb3fe 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/parsing/package-info.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/parsing/package-info.java @@ -2,6 +2,7 @@ * @author Alexander Weigl * @version 1 (03.05.24) */ -@NullMarked package de.uka.ilkd.key.util.parsing; +@NullMarked +package de.uka.ilkd.key.util.parsing; -import org.jspecify.annotations.NullMarked; \ No newline at end of file +import org.jspecify.annotations.NullMarked; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/FeatureSettingsPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/FeatureSettingsPanel.java index 9cf15adb69d..fac4f4db759 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/FeatureSettingsPanel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/FeatureSettingsPanel.java @@ -33,7 +33,7 @@ public JPanel getPanel(MainWindow window) { pCenter.removeAll(); // start fresh checkboxes.clear(); var fs = ProofIndependentSettings.DEFAULT_INSTANCE.getFeatureSettings(); - for (FeatureSettings.Feature feature : FeatureSettings.Feature.FEATURES) { + for (FeatureSettings.Feature feature : FeatureSettings.FEATURES) { var cb = addCheckBox(feature.id(), feature.documentation(), fs.isActivated(feature), null); checkboxes.put(feature, cb); From c45eb7bd3bd373d77e773ab401f142698e864985 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Fri, 10 May 2024 01:25:07 +0200 Subject: [PATCH 3/6] Merge branch 'main' into weigl/key-javaparser3 # By Florian Lanzinger (25) and others # Via GitHub (14) and others * main: (69 commits) typo Unify type annotation notation Apply spotless Remove unnecessary warnings and serialization key.ncore done configure key.ncore fix null values eisop in ncore Fix formatting Fix more NoSuchElementExceptions Fix NoSuchElementException in JavaInfo Remove redundant nullness checks and fix test cases Fix proof script #equals must allow null values jspecify was missing in the compile classpath of tests Code style Revert JavaRedux Object Test case Fix merge issues reformat files ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/ParseExceptionInFile.java # key.core/src/main/java/de/uka/ilkd/key/java/PosConvertException.java # key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/Subtype.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java # key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptException.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/AbstractBuilder.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java # key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java # key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java # key.core/src/main/java/de/uka/ilkd/key/proof/SVInstantiationExceptionWithPosition.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java # key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java # key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLTranslationException.java # key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java # key.core/src/main/java/de/uka/ilkd/key/util/RecognitionException.java # key.core/src/main/java/de/uka/ilkd/key/util/parsing/BuildingException.java # key.core/src/main/java/de/uka/ilkd/key/util/parsing/LocatableException.java # key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java # key.util/src/main/java/org/key_project/util/ExtList.java # key.util/src/main/java/org/key_project/util/collection/ImmutableList.java # settings.gradle --- .../ilkd/key/macros/AbstractProofMacro.java | 3 +- ...SymbolicExecutionUntilMergePointMacro.java | 16 ++----- .../de/uka/ilkd/key/macros/SkipMacro.java | 3 +- .../de/uka/ilkd/key/macros/TryCloseMacro.java | 3 +- .../key/macros/scripts/AbstractCommand.java | 7 +-- .../key/macros/scripts/AssertCommand.java | 1 + .../key/macros/scripts/AssumeCommand.java | 1 + .../ilkd/key/macros/scripts/AutoCommand.java | 6 ++- .../ilkd/key/macros/scripts/AxiomCommand.java | 1 + .../ilkd/key/macros/scripts/CutCommand.java | 1 + .../ilkd/key/macros/scripts/EchoCommand.java | 1 + .../ilkd/key/macros/scripts/EngineState.java | 23 +++++---- .../ilkd/key/macros/scripts/FocusCommand.java | 1 + .../ilkd/key/macros/scripts/HideCommand.java | 1 + .../key/macros/scripts/JavascriptCommand.java | 1 + .../ilkd/key/macros/scripts/MacroCommand.java | 1 + .../macros/scripts/ProofScriptCommand.java | 2 + .../ilkd/key/macros/scripts/RuleCommand.java | 1 + .../macros/scripts/SaveNewNameCommand.java | 1 + .../key/macros/scripts/SchemaVarCommand.java | 1 + .../key/macros/scripts/ScriptCommand.java | 1 + .../key/macros/scripts/SelectCommand.java | 4 +- .../ilkd/key/macros/scripts/SetCommand.java | 1 + .../key/macros/scripts/SetEchoCommand.java | 1 + .../scripts/SetFailOnClosedCommand.java | 1 + .../key/macros/scripts/TryCloseCommand.java | 1 + .../key/macros/scripts/UnhideCommand.java | 1 + .../scripts/meta/DescriptionFacade.java | 7 +-- .../ilkd/key/settings/FeatureSettings.java | 4 +- .../de/uka/ilkd/key/settings/PathConfig.java | 47 +++++-------------- .../uka/ilkd/key/settings/ProofSettings.java | 5 +- .../util/collection/ImmutableMap.java | 33 +++++++++---- 32 files changed, 96 insertions(+), 85 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/AbstractProofMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/AbstractProofMacro.java index 1465997c934..300ad225fab 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/AbstractProofMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/AbstractProofMacro.java @@ -11,6 +11,7 @@ import de.uka.ilkd.key.prover.ProverTaskListener; import de.uka.ilkd.key.settings.ProofSettings; +import org.jspecify.annotations.Nullable; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -67,7 +68,7 @@ public boolean canApplyTo(Node node, PosInOccurrence posInOcc) { @Override public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Node node, - PosInOccurrence posInOcc, ProverTaskListener listener) + @Nullable PosInOccurrence posInOcc, ProverTaskListener listener) throws Exception { return applyTo(uic, node.proof(), getGoals(node), posInOcc, listener); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/FinishSymbolicExecutionUntilMergePointMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/FinishSymbolicExecutionUntilMergePointMacro.java index 59b6f499d5f..ddf036cd61f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/FinishSymbolicExecutionUntilMergePointMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/FinishSymbolicExecutionUntilMergePointMacro.java @@ -22,6 +22,7 @@ import de.uka.ilkd.key.strategy.Strategy; import de.uka.ilkd.key.util.mergerule.MergeRuleUtils; +import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; @@ -40,18 +41,9 @@ * @see FinishSymbolicExecutionMacro */ public class FinishSymbolicExecutionUntilMergePointMacro extends StrategyProofMacro { - - private HashSet blockElems = new HashSet<>(); + private final HashSet blockElems = new HashSet<>(); private final HashSet alreadySeen = new HashSet<>(); - - private UserInterfaceControl uic = null; - - public FinishSymbolicExecutionUntilMergePointMacro() { - } - - public FinishSymbolicExecutionUntilMergePointMacro(HashSet blockElems) { - this.blockElems = blockElems; - } + private @Nullable UserInterfaceControl uic = null; @Override public String getName() { @@ -73,7 +65,7 @@ public String getDescription() { public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof, ImmutableList goals, PosInOccurrence posInOcc, ProverTaskListener listener) throws InterruptedException { - this.uic = uic; + this.uic = uic; // weigl: It is not appropriate to store uic in a macro. return super.applyTo(uic, proof, goals, posInOcc, listener); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/SkipMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/SkipMacro.java index 5b889cf56fc..307297aed56 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/SkipMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/SkipMacro.java @@ -9,6 +9,7 @@ import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.prover.ProverTaskListener; +import org.jspecify.annotations.Nullable; import org.key_project.util.collection.ImmutableList; /** @@ -25,7 +26,7 @@ public String getName() { } @Override - public String getCategory() { + public @Nullable String getCategory() { return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java index ed2233c62d1..5cafc865cdf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java @@ -14,6 +14,7 @@ import de.uka.ilkd.key.prover.impl.ApplyStrategy; import de.uka.ilkd.key.prover.impl.ApplyStrategyInfo; +import org.jspecify.annotations.Nullable; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -110,7 +111,7 @@ public String getScriptCommandName() { * @see de.uka.ilkd.key.macros.ProofMacro#getCategory() */ @Override - public String getCategory() { + public @Nullable String getCategory() { return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AbstractCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AbstractCommand.java index e81c4416873..ea2c9a896a2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AbstractCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AbstractCommand.java @@ -13,6 +13,7 @@ import de.uka.ilkd.key.macros.scripts.meta.DescriptionFacade; import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument; import de.uka.ilkd.key.proof.Proof; +import org.jspecify.annotations.Nullable; /** *

@@ -36,9 +37,9 @@ public abstract class AbstractCommand implements ProofScriptCommand { /** * ... */ - private final Class parameterClazz; + private final @Nullable Class parameterClazz; - public AbstractCommand(Class clazz) { + public AbstractCommand(@Nullable Class clazz) { this.parameterClazz = clazz; } @@ -51,7 +52,7 @@ public List> getArguments() { @Override - public T evaluateArguments(EngineState state, Map arguments) throws Exception { + public @Nullable T evaluateArguments(EngineState state, Map arguments) throws Exception { if (parameterClazz != null) { T obj = parameterClazz.getDeclaredConstructor().newInstance(); return state.getValueInjector().inject(this, obj, arguments); diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AssertCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AssertCommand.java index 399e77cf310..4963d5f31b8 100755 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AssertCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AssertCommand.java @@ -47,6 +47,7 @@ public String getName() { /** * The Assigned parameters (currently only the passed goals). */ + @SuppressWarnings("initialization") public static class Parameters { /** * The number of open and enabled goals. diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AssumeCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AssumeCommand.java index 56b6561ae68..6704e23a945 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AssumeCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AssumeCommand.java @@ -47,6 +47,7 @@ public void execute(FormulaParameter parameter) throws ScriptException, Interrup state.getFirstOpenAutomaticGoal().apply(app); } + @SuppressWarnings("initialization") public static class FormulaParameter { @Option("#2") public Term formula; diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AutoCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AutoCommand.java index 265f1020ae3..d24d7ececf8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AutoCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AutoCommand.java @@ -19,6 +19,7 @@ import de.uka.ilkd.key.strategy.AutomatedRuleApplicationManager; import de.uka.ilkd.key.strategy.FocussedBreakpointRuleApplicationManager; +import org.jspecify.annotations.Nullable; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -130,6 +131,7 @@ private void setupFocussedBreakpointStrategy(final Optional maybeMatches new AbstractProofControl.FocussedAutoModeTaskListener(services.getProof())); } + @SuppressWarnings("initialization") public static class Parameters { @Option(value = "all", required = false) public boolean onAllOpenGoals = false; @@ -138,11 +140,11 @@ public static class Parameters { public int maxSteps = -1; /** Run on formula matching the given regex */ - @Option(value = "matches", required = false) + @Option(value = "matches", required = false) @Nullable public String matches = null; /** Run on formula matching the given regex */ - @Option(value = "breakpoint", required = false) + @Option(value = "breakpoint", required = false) @Nullable public String breakpoint = null; public boolean isOnAllOpenGoals() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AxiomCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AxiomCommand.java index 1b0a1867e26..37d174a2b08 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AxiomCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AxiomCommand.java @@ -49,6 +49,7 @@ public void execute(FormulaParameter parameter) throws ScriptException, Interrup state.getFirstOpenAutomaticGoal().apply(app); } + @SuppressWarnings("initialization") public static class FormulaParameter { @Option("#2") public Term formula; diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/CutCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/CutCommand.java index 96fa8a12fc3..4eb8341b221 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/CutCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/CutCommand.java @@ -57,6 +57,7 @@ public void execute(AbstractUserInterfaceControl uiControl, Parameters args, Eng state.getFirstOpenAutomaticGoal().apply(app); } + @SuppressWarnings("initialization") public static class Parameters { @Option("#2") public Term formula; diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EchoCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EchoCommand.java index 26943a05988..d169bb73168 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EchoCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EchoCommand.java @@ -36,6 +36,7 @@ public void execute(AbstractUserInterfaceControl uiControl, Parameters args, Eng } } + @SuppressWarnings("initialization") public static class Parameters { /** * The message to show. 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 959b14f8087..fb10aa918fd 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 @@ -61,7 +61,7 @@ public EngineState(Proof proof) { valueInjector.addConverter(Sort.class, this::toSort); } - protected static Goal getGoal(ImmutableList openGoals, Node node) { + protected static @Nullable Goal getGoal(ImmutableList openGoals, Node node) { for (Goal goal : openGoals) { if (goal.node() == node) { return goal; @@ -70,9 +70,9 @@ protected static Goal getGoal(ImmutableList openGoals, Node node) { return null; } - public void setGoal(Goal g) { + public void setGoal(@Nullable Goal g) { goal = g; - lastSetGoalNode = Optional.ofNullable(g).map(Goal::node).orElse(null); + lastSetGoalNode = g != null ? g.node() : null; } public Proof getProof() { @@ -89,7 +89,7 @@ public Proof getProof() { * @throws ScriptException If there is no such {@link Goal}, or something else goes wrong. */ @SuppressWarnings("unused") - public Goal getFirstOpenGoal(boolean checkAutomatic) throws ScriptException { + public @Nullable Goal getFirstOpenGoal(boolean checkAutomatic) throws ScriptException { if (proof.closed()) { throw new ProofAlreadyClosedException("The proof is closed already"); } @@ -125,14 +125,13 @@ public Goal getFirstOpenGoal(boolean checkAutomatic) throws ScriptException { * * @throws ScriptException If there is no such {@link Goal}. */ - public Goal getFirstOpenAutomaticGoal() throws ScriptException { + public @Nullable Goal getFirstOpenAutomaticGoal() throws ScriptException { return getFirstOpenGoal(true); } - private static Node goUpUntilOpen(final Node start) { + private static @Nullable Node goUpUntilOpen(@Nullable Node start) { Node currNode = start; - - while (currNode.isClosed()) { + while (currNode != null && currNode.isClosed()) { /* * There should always be a non-closed parent since we check whether the proof is closed * at the beginning. @@ -143,7 +142,7 @@ private static Node goUpUntilOpen(final Node start) { return currNode; } - private Goal findGoalFromRoot(final Node rootNode, boolean checkAutomatic) { + private @Nullable Goal findGoalFromRoot(@Nullable final Node rootNode, boolean checkAutomatic) { final Deque choices = new LinkedList<>(); Goal result = null; @@ -188,7 +187,7 @@ private Goal findGoalFromRoot(final Node rootNode, boolean checkAutomatic) { } - public Term toTerm(String string, Sort sort) throws ParserException, ScriptException { + public Term toTerm(String string, @Nullable Sort sort) throws ParserException, ScriptException { final var io = getKeyIO(); var term = io.parseExpression(string); if (sort == null || term.sort().equals(sort)) @@ -229,11 +228,11 @@ public void setMaxAutomaticSteps(int steps) { ProofSettings.DEFAULT_SETTINGS.getStrategySettings().setMaxSteps(steps); } - public Consumer getObserver() { + public @Nullable Consumer getObserver() { return observer; } - public void setObserver(Consumer observer) { + public void setObserver(@Nullable Consumer observer) { this.observer = observer; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusCommand.java index 01c41db1bb4..038b0fb469c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusCommand.java @@ -41,6 +41,7 @@ public FocusCommand() { super(Parameters.class); } + @SuppressWarnings("initialization") public static class Parameters { @Option("#2") public Sequent toKeep; diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/HideCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/HideCommand.java index 85edd078c0b..0746a92635f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/HideCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/HideCommand.java @@ -93,6 +93,7 @@ public String getName() { return "hide"; } + @SuppressWarnings("initialization") public static class Parameters { @Option("#2") public Sequent sequent; diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/JavascriptCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/JavascriptCommand.java index 029f735b632..7d7f14ae850 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/JavascriptCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/JavascriptCommand.java @@ -55,6 +55,7 @@ public String getName() { return "javascript"; } + @SuppressWarnings("initialization") public static class Parameters { @Option("#2") public String script; diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java index 78781c17618..222e2b528de 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java @@ -164,6 +164,7 @@ private static String formatTermString(String str) { .replace(" +", " "); } + @SuppressWarnings("initialization") public static class Parameters { /** * Macro name parameter diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ProofScriptCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ProofScriptCommand.java index c6bc38a87cf..9e5cf6e8c9d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ProofScriptCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ProofScriptCommand.java @@ -8,6 +8,7 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument; +import org.jspecify.annotations.Nullable; /** * A {@link ProofScriptCommand} is an executable mutation on the given proof. It abstracts complex @@ -35,6 +36,7 @@ public interface ProofScriptCommand { * @param arguments * @return */ + @Nullable T evaluateArguments(EngineState state, Map arguments) throws Exception; /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RuleCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RuleCommand.java index 098c122f882..bf1d58630fc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RuleCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RuleCommand.java @@ -370,6 +370,7 @@ private List filterList(Parameters p, ImmutableList list) return matchingApps; } + @SuppressWarnings("initialization") public static class Parameters { @Option(value = "#2") public String rulename; diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SaveNewNameCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SaveNewNameCommand.java index b8b4b159e9a..b404af8f3b9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SaveNewNameCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SaveNewNameCommand.java @@ -95,6 +95,7 @@ public void execute(AbstractUserInterfaceControl uiControl, Parameters params, } } + @SuppressWarnings("initialization") public static class Parameters { @Option(value = "#2", required = true) public String abbreviation; diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SchemaVarCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SchemaVarCommand.java index 6e7dacc6d34..f879ff79eba 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SchemaVarCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SchemaVarCommand.java @@ -67,6 +67,7 @@ public String getName() { return "schemaVar"; } + @SuppressWarnings("initialization") public static class Parameters { @Option("#2") public String type; diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptCommand.java index a389c0b0ad3..67c3095f943 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptCommand.java @@ -19,6 +19,7 @@ public ScriptCommand() { super(Parameters.class); } + @SuppressWarnings("initialization") public static class Parameters { @Option("#2") public String filename; 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 f43592bde92..a408d6d784c 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 @@ -18,6 +18,7 @@ import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; +import org.jspecify.annotations.Nullable; import org.key_project.util.collection.ImmutableList; import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY; @@ -62,7 +63,7 @@ private Goal findGoalWith(String branchTitle, Proof proof) throws ScriptExceptio node -> getFirstSubtreeGoal(node, proof), proof); } - private static Goal getFirstSubtreeGoal(Node node, Proof proof) { + private static @Nullable Goal getFirstSubtreeGoal(Node node, Proof proof) { Goal goal; if (node.leaf() && // (goal = EngineState.getGoal(proof.openGoals(), node)) != null) { @@ -147,6 +148,7 @@ public String getName() { return "select"; } + @SuppressWarnings("initialization") public static class Parameters { /** A formula defining the goal to select */ @Option(value = "formula", required = false) diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetCommand.java index a8413690617..4fea676b0fc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetCommand.java @@ -96,6 +96,7 @@ public String getName() { return "set"; } + @SuppressWarnings("initialization") public static class Parameters { /** One Step Simplification parameter */ @Option(value = "oss", required = false) diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetEchoCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetEchoCommand.java index b4a14a5e7b9..139d6451878 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetEchoCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetEchoCommand.java @@ -33,6 +33,7 @@ public void execute(AbstractUserInterfaceControl uiControl, Parameters args, Eng state.setEchoOn("on".equalsIgnoreCase(args.command)); } + @SuppressWarnings("initialization") public static class Parameters { /** * The command: "on" or "off". Anything else defaults to "off". diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetFailOnClosedCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetFailOnClosedCommand.java index f2f9e3840d3..c687807b5f4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetFailOnClosedCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetFailOnClosedCommand.java @@ -38,6 +38,7 @@ public void execute(AbstractUserInterfaceControl uiControl, Parameters args, Eng state.setFailOnClosedOn(!"off".equalsIgnoreCase(args.command)); } + @SuppressWarnings("initialization") public static class Parameters { /** * The command: "on" or "off". Anything else defaults to "on". diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/TryCloseCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/TryCloseCommand.java index 183f12b3e85..4121c42e8a7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/TryCloseCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/TryCloseCommand.java @@ -73,6 +73,7 @@ public String getName() { return "tryclose"; } + @SuppressWarnings("initialization") public static class TryCloseArguments { @Option(value = "steps", required = false) public Integer steps; diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/UnhideCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/UnhideCommand.java index 1a1bfcf4055..e4ba7e34f7c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/UnhideCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/UnhideCommand.java @@ -88,6 +88,7 @@ public String getName() { return "unhide"; } + @SuppressWarnings("initialization") public static class Parameters { @Option("#2") public Sequent sequent; diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/DescriptionFacade.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/DescriptionFacade.java index ddfd0ff19bc..e43a41cc1b8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/DescriptionFacade.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/DescriptionFacade.java @@ -58,7 +58,7 @@ public static Properties getProperties() { /** * Looks up the documentation for the given command in the properties file. If no documentation - * is available an empty string is returned. + * is available, an empty string is returned. * * @param cmd non-null proof script command * @return a non-null string @@ -70,16 +70,13 @@ public static String getDocumentation(ProofScriptCommand cmd) { /** * Looks up the documentation for the given proof script argument. If no documentation is - * available an empty string is returned. + * available, an empty string is returned. * * @param arg non-null proof script argument * @return a string or null, if {@code arg} is null or {@code arg.getCommand} returns null * @see ProofScriptArgument#getDocumentation() */ public static String getDocumentation(ProofScriptArgument arg) { - if (arg == null || arg.getCommand() == null) { - return null; - } String key = arg.getCommand().getName() + "." + arg.getName(); return getString(key); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/FeatureSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/FeatureSettings.java index bf45ced90c5..73269325268 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/FeatureSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/FeatureSettings.java @@ -91,7 +91,7 @@ private void readFromSystemProperties(@UnknownInitialization FeatureSettings thi * * @return true, if {@code value} feels like a feature activation. */ - private boolean isTrue(Object value) { + private boolean isTrue(@UnknownInitialization FeatureSettings this, Object value) { return switch (value.toString().toLowerCase()) { case "true", "yes", "on" -> true; default -> false; @@ -153,7 +153,7 @@ public void activate(Feature f) { /** * Activates the given feature by {@code id}. */ - private void activate(String id) { + private void activate(@UnknownInitialization FeatureSettings this, String id) { if (!isActivated(id)) { activatedFeatures.add(id); firePropertyChange(id, false, isActivated(id)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java b/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java index c75db4e9b53..895895c5fa3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java @@ -3,21 +3,16 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.settings; -import java.io.File; - import org.key_project.util.java.IOUtil; +import java.io.File; + /** - *

* Keeps some central paths to files and directories. - *

*

* By default all KeY configurations are stored in a directory named ".key" inside the user's home * directory. In Microsoft windows operating systems this is directly the hard disc that contains - * the KeY code. But the eclipse integration requires to change the default location. This is - * possible via {@link #setKeyConfigDir(String)} which should be called once before something is - * done with KeY (e.g. before the {@code MainWindow} is opened). - *

+ * the KeY code. But the eclipse integration requires to change the default location. */ public final class PathConfig { @@ -33,35 +28,30 @@ public final class PathConfig { public static final String KEY_DIRECTORY_NAME = ".key"; /** - * In which file to store the recent files. + * directory where to find the KeY configuration files */ - private static String recentFileStorage; + private static String keyConfigDir = IOUtil.getHomeDirectory() + File.separator + KEY_DIRECTORY_NAME; + /** - * In which file to store the proof-independent settings. + * In which file to store the recent files. */ - private static String proofIndependentSettings; + private static String recentFileStorage = getKeyConfigDir() + File.separator + "recentFiles.json"; /** - * directory where to find the KeY configuration files + * In which file to store the proof-independent settings. */ - private static String keyConfigDir; + private static String proofIndependentSettings = getKeyConfigDir() + File.separator + "proofIndependentSettings.props"; + /** * Directory in which the log files are stored. */ - private static File logDirectory; + private static File logDirectory = new File(keyConfigDir, "logs"); private PathConfig() { } - /* - * Initializes the instance variables with the default settings. - */ - static { - setKeyConfigDir(IOUtil.getHomeDirectory() + File.separator + KEY_DIRECTORY_NAME); - } - /** * Returns the path to the directory that contains KeY configuration files. * @@ -71,19 +61,6 @@ public static String getKeyConfigDir() { return keyConfigDir; } - /** - * Sets the path to the directory that contains KeY configuration files. - * - * @param keyConfigDir The new directory to use. - */ - public static void setKeyConfigDir(String keyConfigDir) { - PathConfig.keyConfigDir = keyConfigDir; - PathConfig.recentFileStorage = getKeyConfigDir() + File.separator + "recentFiles.json"; - PathConfig.proofIndependentSettings = - getKeyConfigDir() + File.separator + "proofIndependentSettings.props"; - PathConfig.logDirectory = new File(keyConfigDir, "logs"); - } - /** * Returns the path to the file that is used to store recent files. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java index 319df9a2b2e..c558b07e75e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java @@ -14,6 +14,7 @@ import de.uka.ilkd.key.util.KeYResourceManager; import org.antlr.v4.runtime.CharStreams; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -70,8 +71,8 @@ private static ProofSettings loadedSettings() { private final NewSMTTranslationSettings newSMTSettings = new NewSMTTranslationSettings(); private final TermLabelSettings termLabelSettings = new TermLabelSettings(); - private Properties lastLoadedProperties = null; - private Configuration lastLoadedConfiguration = null; + private @Nullable Properties lastLoadedProperties = null; + private @Nullable Configuration lastLoadedConfiguration = null; /** * create a proof settings object. When you add a new settings object, PLEASE UPDATE THE LIST diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java index 0c13b30233b..efd0333f20a 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java @@ -9,6 +9,7 @@ /** * This interface has to be implemented by a Class providing a persistent Map. */ +@SuppressWarnings({"nullness", "type.argument.type.incompatible"}) public interface ImmutableMap extends Iterable> { @@ -21,19 +22,29 @@ public interface ImmutableMap */ ImmutableMap put(S key, T value); - /** @return value of type that is mapped by key of type */ + /** + * @return value of type that is mapped by key of type + */ T get(S key); - /** @return number of entries as int */ + /** + * @return number of entries as int + */ int size(); - /** @return true iff the map is empty */ + /** + * @return true iff the map is empty + */ boolean isEmpty(); - /** @return true iff the map includes key */ + /** + * @return true iff the map includes key + */ boolean containsKey(S key); - /** @return true iff the map includes value */ + /** + * @return true iff the map includes value + */ boolean containsValue(T value); /** @@ -50,13 +61,19 @@ public interface ImmutableMap */ ImmutableMap removeAll(T value); - /** @return iterator about all keys */ + /** + * @return iterator about all keys + */ Iterator keyIterator(); - /** @return iterator about all values */ + /** + * @return iterator about all values + */ Iterator valueIterator(); - /** @return iterator for entries */ + /** + * @return iterator for entries + */ Iterator> iterator(); From 453d496f9692cf641a5428a43b3b3320b84dc223 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Fri, 10 May 2024 01:25:38 +0200 Subject: [PATCH 4/6] package-infos --- .../uka/ilkd/key/settings/package-info.java | 8 + .../DefinedSymbolsHandler.preamble.xml | 155 ++++++++++++++++++ .../exploration/actions/package-info.java | 7 + .../key_project/exploration/package-info.java | 7 + .../exploration/ui/package-info.java | 7 + 5 files changed, 184 insertions(+) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/settings/package-info.java create mode 100644 key/key.core/src/main/resources/de/uka/ilkd/key/smt/newsmt2/DefinedSymbolsHandler.preamble.xml create mode 100644 keyext.exploration/src/main/java/org/key_project/exploration/actions/package-info.java create mode 100644 keyext.exploration/src/main/java/org/key_project/exploration/package-info.java create mode 100644 keyext.exploration/src/main/java/org/key_project/exploration/ui/package-info.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/settings/package-info.java new file mode 100644 index 00000000000..80eda222bb0 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (10.05.24) + */ +@NullMarked +package de.uka.ilkd.key.settings; + +import org.jspecify.annotations.NullMarked; diff --git a/key/key.core/src/main/resources/de/uka/ilkd/key/smt/newsmt2/DefinedSymbolsHandler.preamble.xml b/key/key.core/src/main/resources/de/uka/ilkd/key/smt/newsmt2/DefinedSymbolsHandler.preamble.xml new file mode 100644 index 00000000000..ce202755c8d --- /dev/null +++ b/key/key.core/src/main/resources/de/uka/ilkd/key/smt/newsmt2/DefinedSymbolsHandler.preamble.xml @@ -0,0 +1,155 @@ + + + += seqLen(s) -> any::seqGet(s, i)<> = seqGetOutside ) +]]> + +> >= 0 +]]> + + + any::seqGet(seqConcat(s1, s2), i) = + \if (i < seqLen(s1)) \then (any::seqGet(s1, i)) \else (any::seqGet(s2, i-seqLen(s1)))) +]]> + + +>) = seqLen(s1) + seqLen(s2) +]]> + + + + + +>, 0) = x +]]> + + +>) = 1 +]]> + + +>, idx) + = \if(0 <= idx & idx < (to - from)) + \then(any::seqGet(seq, idx + from)) + \else(seqGetOutside) +]]> + +>) + = \if(from < to)\then(to - from)\else(0) +]]> +> = + \if(o = o2 & f = f2 & f != java.lang.Object::) + \then(v) + \else(any::select(h, o2, f2)) +]]> + += 0 +]]> + +> = + \if(elementOf(o, f, ls) & f != java.lang.Object:: + | elementOf(o, f, freshLocs(h))) + \then(any::select(h2, o, f)) + \else(any::select(h, o, f)) +]]> + +> = + \if(elementOf(o, f, s) & f != java.lang.Object::) + \then(x) + \else(any::select(h, o, f)) +]]> + +> = + \if(o = o2 & o != null & f = java.lang.Object::) + \then(TRUE) + \else(any::select(h, o2, f)) +]]> + + + boolean::select(h, (java.lang.Object::select(h, o, f))<>, java.lang.Object::) = TRUE + | (java.lang.Object::select(h, o, f)) = null) +]]> + + + + + > = TRUE -> x = null) ]]> + + + + translateJavaMulInt + + + + translateJavaAddInt + + + + + precOfInt + + + \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) + + + + \forall Object o; \forall Field f; \forall LocSet l1; \forall LocSet l2; + ( elementOf(o, f, union(l1, l2))<<Trigger>> <-> elementOf(o,f,l1) | elementOf(o,f,l2) ) + + + + \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) + + + + \forall Heap h; \forall Object o; \forall Field f; + ( elementOf(o,f,freshLocs(h))<<Trigger>> <-> + o != null & !boolean::select(h,o,java.lang.Object::<created>)=TRUE ) + + + + \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; + ( elementOf(o,f, singleton(o2,f2))<<Trigger>> <-> + o = o2 & f = f2 ) + + +> <-> + o = o2 ) +]]> + +> <-> + o = o2 & \exists int iv; (f = arr(iv) & lo <= iv & iv <= hi)) +]]> + + diff --git a/keyext.exploration/src/main/java/org/key_project/exploration/actions/package-info.java b/keyext.exploration/src/main/java/org/key_project/exploration/actions/package-info.java new file mode 100644 index 00000000000..2d2b37e3fd6 --- /dev/null +++ b/keyext.exploration/src/main/java/org/key_project/exploration/actions/package-info.java @@ -0,0 +1,7 @@ +/** + * @author Alexander Weigl + * @version 1 (10.05.24) + */ +@NullMarked package org.key_project.exploration.actions; + +import org.jspecify.annotations.NullMarked; \ No newline at end of file diff --git a/keyext.exploration/src/main/java/org/key_project/exploration/package-info.java b/keyext.exploration/src/main/java/org/key_project/exploration/package-info.java new file mode 100644 index 00000000000..20f24988510 --- /dev/null +++ b/keyext.exploration/src/main/java/org/key_project/exploration/package-info.java @@ -0,0 +1,7 @@ +/** + * @author Alexander Weigl + * @version 1 (10.05.24) + */ +@NullMarked package org.key_project.exploration; + +import org.jspecify.annotations.NullMarked; \ No newline at end of file diff --git a/keyext.exploration/src/main/java/org/key_project/exploration/ui/package-info.java b/keyext.exploration/src/main/java/org/key_project/exploration/ui/package-info.java new file mode 100644 index 00000000000..5480dc06aa7 --- /dev/null +++ b/keyext.exploration/src/main/java/org/key_project/exploration/ui/package-info.java @@ -0,0 +1,7 @@ +/** + * @author Alexander Weigl + * @version 1 (10.05.24) + */ +@NullMarked package org.key_project.exploration.ui; + +import org.jspecify.annotations.NullMarked; \ No newline at end of file From 82ef399b7356017644cf211e9851308cc06ea439 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Fri, 21 Jun 2024 16:07:00 +0200 Subject: [PATCH 5/6] reenable sonarqube, disable the crappy things * also fix some encoding in recorder/src files --- .github/old_workflows/sonarqube.yml | 39 -------- .github/workflows/artiweb.yml | 88 ------------------ .github/workflows/code_quality.yml | 89 +------------------ .github/workflows/codeql.yml | 43 --------- .github/workflows/sonarqube.yml | 49 ++++++++++ build.gradle | 11 +++ gradle.properties | 1 + .../recoder/abstraction/IntersectionType.java | 2 +- .../java5to4/EnhancedFor2For.java | 2 +- 9 files changed, 64 insertions(+), 260 deletions(-) delete mode 100644 .github/old_workflows/sonarqube.yml delete mode 100644 .github/workflows/artiweb.yml delete mode 100644 .github/workflows/codeql.yml create mode 100644 .github/workflows/sonarqube.yml create mode 100644 gradle.properties diff --git a/.github/old_workflows/sonarqube.yml b/.github/old_workflows/sonarqube.yml deleted file mode 100644 index ac751f0d5a8..00000000000 --- a/.github/old_workflows/sonarqube.yml +++ /dev/null @@ -1,39 +0,0 @@ -# This workflow helps you trigger a SonarCloud analysis of your code and populates -# GitHub Code Scanning alerts with the vulnerabilities found. -name: SonarCloud analysis - -on: - push: - branches: [ "main" ] - pull_request: - branches: [ "main" ] - workflow_dispatch: - -permissions: - pull-requests: read # allows SonarCloud to decorate PRs with analysis results - -jobs: - Analysis: - runs-on: ubuntu-latest - steps: - - name: Analyze with SonarCloud - # You can pin the exact commit or the version. - # uses: SonarSource/sonarcloud-github-action@de2e56b42aa84d0b1c5b622644ac17e505c9a049 - uses: SonarSource/sonarcloud-github-action@de2e56b42aa84d0b1c5b622644ac17e505c9a049 - env: - GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} # Needed to get PR information - SONAR_TOKEN: ${{ secrets.SONAR_TOKEN }} # Generate a token on Sonarcloud.io, add it to the secrets of this repo with the name SONAR_TOKEN (Settings > Secrets > Actions > add new repository secret) - with: - args: - # Unique keys of your project and organization. You can find them in SonarCloud > Information (bottom-left menu) - # mandatory - -Dsonar.projectKey=key-main - -Dsonar.organization=keyproject - # Comma-separated paths to directories containing main source files. - #-Dsonar.sources= # optional, default is project base directory - # When you need the analysis to take place in a directory other than the one from which it was launched - #-Dsonar.projectBaseDir= # optional, default is . - # Comma-separated paths to directories containing test source files. - #-Dsonar.tests= # optional. For more info about Code Coverage, please refer to https://docs.sonarcloud.io/enriching/test-coverage/overview/ - # Adds more detail to both client and server-side analysis logs, activating DEBUG mode for the scanner, and adding client-side environment variables and system properties to the server-side log of analysis report processing. - #-Dsonar.verbose= # optional, default is false diff --git a/.github/workflows/artiweb.yml b/.github/workflows/artiweb.yml deleted file mode 100644 index ca963363cf0..00000000000 --- a/.github/workflows/artiweb.yml +++ /dev/null @@ -1,88 +0,0 @@ -name: Artiweb Comment - -on: - workflow_run: - workflows: [Tests] - types: - - completed - -# taken from https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#using-data-from-the-triggering-workflow -jobs: - comment: - runs-on: ubuntu-latest - steps: - - name: 'Download artifact' - id: da - uses: actions/github-script@v7 - with: - script: | - if (context.payload.workflow_run === undefined) { - core.setFailed("No workflow run found"); - } - const allArtifacts = await github.rest.actions.listWorkflowRunArtifacts({ - owner: context.repo.owner, - repo: context.repo.repo, - run_id: context.payload.workflow_run.id, - }); - - const testArtifact = allArtifacts.data.artifacts.find((artifact) => { - return artifact.name == "test-results" - }); - if (testArtifact !== undefined) { - core.info("Found test-results artifact id: " + testArtifact.id); - core.setOutput("test-artifact-id", testArtifact.id); - } else { - core.info("Artifact test-results was not found"); - } - - const numberArtifact = allArtifacts.data.artifacts.find((artifact) => { - return artifact.name == "pr-number" - }); - if (numberArtifact !== undefined) { - core.info("Found pr-number artifact id: " + numberArtifact.id); - let download = await github.rest.actions.downloadArtifact({ - owner: context.repo.owner, - repo: context.repo.repo, - artifact_id: numberArtifact.id, - archive_format: 'zip', - }); - let fs = require('fs'); - fs.writeFileSync(`${process.env.GITHUB_WORKSPACE}/pr_number.zip`, Buffer.from(download.data)); - } else { - core.setFailed("Artifact pr-number was not found"); - } - - - name: 'Unzip artifact' - run: unzip pr_number.zip - - - name: 'Read pr number' - id: rpn - uses: actions/github-script@v7 - with: - github-token: ${{ secrets.GITHUB_TOKEN }} - script: | - let fs = require('fs'); - let issue_number_text = fs.readFileSync('./pr_number', 'utf8'); - core.info("Found pr number \"" + issue_number_text + "\""); - core.setOutput("pr-number", issue_number_text === "" ? "" : Number(issue_number_text)); - - name: Find Comment - if: ${{ steps.rpn.outputs.pr-number != '' }} - uses: peter-evans/find-comment@v3 - id: fc - with: - issue-number: ${{ steps.rpn.outputs.pr-number }} - comment-author: 'github-actions[bot]' - body-includes: Artiweb - - - name: Create or update comment - if: ${{ steps.rpn.outputs.pr-number != '' }} - uses: peter-evans/create-or-update-comment@v4 - with: - comment-id: ${{ steps.fc.outputs.comment-id }} - issue-number: ${{ steps.rpn.outputs.pr-number }} - body: | - Thank you for your contribution. - - The test artifacts are available on [Artiweb](e8e3f762-a110-4e21-bc41-cacb5f3a3a50.ka.bw-cloud-instance.org/${{steps.rpn.outputs.pr-number}}/). - The newest artifact is [here](e8e3f762-a110-4e21-bc41-cacb5f3a3a50.ka.bw-cloud-instance.org/${{steps.rpn.outputs.pr-number}}/${{steps.da.outputs.test-artifact-id}}/). - edit-mode: replace diff --git a/.github/workflows/code_quality.yml b/.github/workflows/code_quality.yml index 5410a014e96..1365c36e398 100644 --- a/.github/workflows/code_quality.yml +++ b/.github/workflows/code_quality.yml @@ -24,21 +24,6 @@ jobs: with: arguments: -DENABLE_NULLNESS=true compileTest - - qodana: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v4 - with: - fetch-depth: 0 - - name: 'Qodana Scan' - uses: JetBrains/qodana-action@v2024.1.5 - - - uses: github/codeql-action/upload-sarif@v3 - if: success() || failure() - with: - sarif_file: ${{ runner.temp }}/qodana/results/qodana.sarif.json - formatting: runs-on: ubuntu-latest steps: @@ -51,76 +36,4 @@ jobs: - name: Build with Gradle uses: gradle/gradle-build-action@v3.3.2 with: - arguments: --continue spotlessCheck - - # checkstyle: - # runs-on: ubuntu-latest - # steps: - # - uses: actions/checkout@v4 - # with: - # fetch-depth: 0 - # - run: scripts/tools/checkstyle/runIncrementalCheckstyle.sh --xml | tee report.xml - # - run: | - # npx violations-command-line -sarif sarif-report.json \ - # -v "CHECKSTYLE" "." ".*/report.xml$" "Checkstyle" \ - # -diff-to $(git merge-base HEAD origin/main) -pv false - - # - uses: github/codeql-action/upload-sarif@v3 - # if: success() || failure() - # with: - # sarif_file: sarif-report.json - - - checkstyle_new: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v4 - - uses: actions/setup-java@v4 - with: - distribution: 'corretto' - java-version: '21' - cache: 'gradle' - - - name: Build with Gradle - uses: gradle/gradle-build-action@v3.3.2 - with: - arguments: --continue checkstyleMainChanged - - run: | - npx violations-command-line -sarif sarif-report.json \ - -v "CHECKSTYLE" "." ".*/build/reports/checkstyle/main_diff.xml$" "Checkstyle" - - #-diff-from $(git merge-base HEAD origin/main) - # - run: python3 ./.github/printcs.py */build/reports/checkstyle/main_diff.xml - - # $(git merge-base HEAD origin/main) - - - uses: github/codeql-action/upload-sarif@v3 - if: success() || failure() - with: - sarif_file: sarif-report.json - - pmd: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v4 - - uses: actions/setup-java@v4 - with: - distribution: 'corretto' - java-version: '21' - cache: 'gradle' - - name: Build with Gradle - uses: gradle/gradle-build-action@v3.3.2 - with: - arguments: --continue pmdMainChanged - - # - run: python3 ./.github/printAnnotations.py */build/reports/pmd/main.xml - - - run: | - npx violations-command-line -sarif pmd-report.json \ - -v "PMD" "." ".*/build/reports/pmd/main_diff.xml$" "PMD" - - # -diff-from $(git merge-base HEAD origin/main) - - name: Upload SARIF file - uses: github/codeql-action/upload-sarif@v3 - with: - sarif_file: pmd-report.json + arguments: --continue spotlessCheck \ No newline at end of file diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml deleted file mode 100644 index efdedd8caf2..00000000000 --- a/.github/workflows/codeql.yml +++ /dev/null @@ -1,43 +0,0 @@ -name: "CodeQL" - -on: - push: - branches: [ "main" ] - pull_request: - branches: - - "main" - - "KeY-*" - schedule: - - cron: '21 21 * * 4' - merge_group: - -jobs: - analyze: - name: Analyze - runs-on: ubuntu-latest - permissions: - actions: read - contents: read - security-events: write - - strategy: - fail-fast: false - matrix: - language: [ 'java' ] - - steps: - - name: Checkout repository - uses: actions/checkout@v4 - - - name: Initialize CodeQL - uses: github/codeql-action/init@v3 - with: - languages: ${{ matrix.language }} - - - name: Autobuild - uses: github/codeql-action/autobuild@v3 - - - name: Perform CodeQL Analysis - uses: github/codeql-action/analyze@v3 - with: - category: "/language:${{matrix.language}}" diff --git a/.github/workflows/sonarqube.yml b/.github/workflows/sonarqube.yml new file mode 100644 index 00000000000..5749981d98f --- /dev/null +++ b/.github/workflows/sonarqube.yml @@ -0,0 +1,49 @@ +## Copied from SonarCloud + +name: SonarCloud +on: + push: + branches: + - main + pull_request: + types: [opened, synchronize, reopened] + +jobs: + build: + name: Build and analyze + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v3 + with: + fetch-depth: 0 # Shallow clones should be disabled for a better relevancy of analysis + - name: Set up JDK 21 + uses: actions/setup-java@v3 + with: + java-version: 21 + distribution: 'zulu' + - name: Cache SonarCloud packages + uses: actions/cache@v3 + with: + path: ~/.sonar/cache + key: ${{ runner.os }}-sonar + restore-keys: ${{ runner.os }}-sonar + - name: Cache Gradle packages + uses: actions/cache@v3 + with: + path: ~/.gradle/caches + key: ${{ runner.os }}-gradle-${{ hashFiles('**/*.gradle') }} + restore-keys: ${{ runner.os }}-gradle + + - name: Generate and submit dependency graph + uses: gradle/actions/dependency-submission@v3 + with: + build-scan-publish: true + build-scan-terms-of-use-url: "https://gradle.com/terms-of-service" + build-scan-terms-of-use-agree: "yes" + + - name: Build and analyze + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} # Needed to get PR information, if any + SONAR_TOKEN: ${{ secrets.SONAR_TOKEN }} + GRADLE_OPTS: "-Xmx6g -XX:MaxMetaspaceSize=512m -Dfile.encoding=UTF-8" + run: ./gradlew --parallel --continue -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test classes testClasses :key.util:test jacocoTestReport sonar \ No newline at end of file diff --git a/build.gradle b/build.gradle index 935addaa9a8..487eb193e5c 100644 --- a/build.gradle +++ b/build.gradle @@ -25,8 +25,19 @@ plugins { // EISOP Checker Framework id "org.checkerframework" version "0.6.39" + + id("org.sonarqube") version "5.0.0.4638" +} + +sonar { + properties { + property "sonar.projectKey", "KeYProject_key" + property "sonar.organization", "keyproject" + property "sonar.host.url", "https://sonarcloud.io" + } } + // Configure this project for use inside IntelliJ: idea { module { diff --git a/gradle.properties b/gradle.properties new file mode 100644 index 00000000000..7937f1c737f --- /dev/null +++ b/gradle.properties @@ -0,0 +1 @@ +org.gradle.jvmargs=-Xmx2g -XX:MaxMetaspaceSize=512m -Dfile.encoding=UTF-8 \ No newline at end of file diff --git a/recoder/src/main/java/recoder/abstraction/IntersectionType.java b/recoder/src/main/java/recoder/abstraction/IntersectionType.java index 49186270c8c..c3e5cc0b836 100644 --- a/recoder/src/main/java/recoder/abstraction/IntersectionType.java +++ b/recoder/src/main/java/recoder/abstraction/IntersectionType.java @@ -11,7 +11,7 @@ import recoder.service.ProgramModelInfo; /** - * Represents an intersection type, which was introduced in java 5. See JLS, 3rd edition, �4.9 for + * Represents an intersection type, which was introduced in java 5. See JLS, 3rd edition, §4.9 for * details. * * @author Tobias Gutzmann diff --git a/recoder/src/main/java/recoder/kit/transformation/java5to4/EnhancedFor2For.java b/recoder/src/main/java/recoder/kit/transformation/java5to4/EnhancedFor2For.java index 52e98bccb81..17e4f816382 100644 --- a/recoder/src/main/java/recoder/kit/transformation/java5to4/EnhancedFor2For.java +++ b/recoder/src/main/java/recoder/kit/transformation/java5to4/EnhancedFor2For.java @@ -25,7 +25,7 @@ import recoder.list.generic.ASTList; /** - * converts an enhanced for loop to an "old style" for loop. This follows JLS 3rd edition, �14.14.2. + * converts an enhanced for loop to an "old style" for loop. This follows JLS 3rd edition, §14.14.2. *

* Currently, if given enhanced for iterates over an array, this will replace the enhanced for with * a statement block and not inline it into a possibly given statement block, yielding possibly not From 6c4a4bac296a371ce78cc9dd59a8240b0577def6 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Fri, 5 Jul 2024 16:06:02 +0200 Subject: [PATCH 6/6] spotless --- .../de/uka/ilkd/key/macros/AbstractProofMacro.java | 5 +++-- ...FinishSymbolicExecutionUntilMergePointMacro.java | 3 ++- .../main/java/de/uka/ilkd/key/macros/SkipMacro.java | 3 ++- .../java/de/uka/ilkd/key/macros/TryCloseMacro.java | 3 ++- .../ilkd/key/macros/scripts/AbstractCommand.java | 4 +++- .../de/uka/ilkd/key/macros/scripts/AutoCommand.java | 9 ++++++--- .../de/uka/ilkd/key/macros/scripts/EngineState.java | 1 - .../ilkd/key/macros/scripts/ProofScriptCommand.java | 1 + .../uka/ilkd/key/macros/scripts/SelectCommand.java | 3 ++- .../java/de/uka/ilkd/key/settings/PathConfig.java | 13 ++++++++----- .../key_project/util/collection/ImmutableMap.java | 2 +- .../exploration/actions/package-info.java | 5 +++-- .../org/key_project/exploration/package-info.java | 5 +++-- .../key_project/exploration/ui/package-info.java | 5 +++-- 14 files changed, 39 insertions(+), 23 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/AbstractProofMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/AbstractProofMacro.java index 300ad225fab..8b267c1fdea 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/AbstractProofMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/AbstractProofMacro.java @@ -11,10 +11,11 @@ import de.uka.ilkd.key.prover.ProverTaskListener; import de.uka.ilkd.key.settings.ProofSettings; -import org.jspecify.annotations.Nullable; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; +import org.jspecify.annotations.Nullable; + /** * Takes care of providing the whole ProofMacro interface by only making it necessary to implement * to most general application methods for a given list of goals and translating the less general @@ -68,7 +69,7 @@ public boolean canApplyTo(Node node, PosInOccurrence posInOcc) { @Override public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Node node, - @Nullable PosInOccurrence posInOcc, ProverTaskListener listener) + @Nullable PosInOccurrence posInOcc, ProverTaskListener listener) throws Exception { return applyTo(uic, node.proof(), getGoals(node), posInOcc, listener); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/FinishSymbolicExecutionUntilMergePointMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/FinishSymbolicExecutionUntilMergePointMacro.java index ddf036cd61f..5d1bd6611ad 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/FinishSymbolicExecutionUntilMergePointMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/FinishSymbolicExecutionUntilMergePointMacro.java @@ -22,11 +22,12 @@ import de.uka.ilkd.key.strategy.Strategy; import de.uka.ilkd.key.util.mergerule.MergeRuleUtils; -import org.jspecify.annotations.Nullable; import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.Nullable; + /** * The macro FinishSymbolicExecutionUntilJionPointMacro continues automatic rule application until a * merge point is reached (i.e. a point where a {@link MergeRule} can be applied) or there is no diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/SkipMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/SkipMacro.java index 307297aed56..6d5233871f3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/SkipMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/SkipMacro.java @@ -9,9 +9,10 @@ import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.prover.ProverTaskListener; -import org.jspecify.annotations.Nullable; import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.Nullable; + /** * This macro does nothing and is not applicable. It can be used to create compound macros, e.g. as * an alternative macro for {@link DoWhileFinallyMacro}. diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java index 5cafc865cdf..9a26c7b0fb0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java @@ -14,10 +14,11 @@ import de.uka.ilkd.key.prover.impl.ApplyStrategy; import de.uka.ilkd.key.prover.impl.ApplyStrategyInfo; -import org.jspecify.annotations.Nullable; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; +import org.jspecify.annotations.Nullable; + /** * The Class TryCloseMacro tries to close goals. Goals are either closed or left untouched. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AbstractCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AbstractCommand.java index ea2c9a896a2..a8f312350be 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AbstractCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AbstractCommand.java @@ -13,6 +13,7 @@ import de.uka.ilkd.key.macros.scripts.meta.DescriptionFacade; import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument; import de.uka.ilkd.key.proof.Proof; + import org.jspecify.annotations.Nullable; /** @@ -52,7 +53,8 @@ public List> getArguments() { @Override - public @Nullable T evaluateArguments(EngineState state, Map arguments) throws Exception { + public @Nullable T evaluateArguments(EngineState state, Map arguments) + throws Exception { if (parameterClazz != null) { T obj = parameterClazz.getDeclaredConstructor().newInstance(); return state.getValueInjector().inject(this, obj, arguments); diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AutoCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AutoCommand.java index d24d7ececf8..b7256161caa 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AutoCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AutoCommand.java @@ -19,10 +19,11 @@ import de.uka.ilkd.key.strategy.AutomatedRuleApplicationManager; import de.uka.ilkd.key.strategy.FocussedBreakpointRuleApplicationManager; -import org.jspecify.annotations.Nullable; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; +import org.jspecify.annotations.Nullable; + /** * The AutoCommand invokes the automatic strategy "Auto". * @@ -140,11 +141,13 @@ public static class Parameters { public int maxSteps = -1; /** Run on formula matching the given regex */ - @Option(value = "matches", required = false) @Nullable + @Option(value = "matches", required = false) + @Nullable public String matches = null; /** Run on formula matching the given regex */ - @Option(value = "breakpoint", required = false) @Nullable + @Option(value = "breakpoint", required = false) + @Nullable public String breakpoint = null; public boolean isOnAllOpenGoals() { 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 fb10aa918fd..330aa063516 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 @@ -7,7 +7,6 @@ import java.util.Deque; import java.util.LinkedList; import java.util.Objects; -import java.util.Optional; import java.util.function.Consumer; import de.uka.ilkd.key.java.Services; diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ProofScriptCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ProofScriptCommand.java index 9e5cf6e8c9d..7370928763c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ProofScriptCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ProofScriptCommand.java @@ -8,6 +8,7 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument; + import org.jspecify.annotations.Nullable; /** 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 a408d6d784c..bc2af71b461 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 @@ -18,9 +18,10 @@ import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; -import org.jspecify.annotations.Nullable; import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.Nullable; + import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY; public class SelectCommand extends AbstractCommand { diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java b/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java index 895895c5fa3..8bbe6242c29 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java @@ -3,10 +3,10 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.settings; -import org.key_project.util.java.IOUtil; - import java.io.File; +import org.key_project.util.java.IOUtil; + /** * Keeps some central paths to files and directories. *

@@ -30,18 +30,21 @@ public final class PathConfig { /** * directory where to find the KeY configuration files */ - private static String keyConfigDir = IOUtil.getHomeDirectory() + File.separator + KEY_DIRECTORY_NAME; + private static String keyConfigDir = + IOUtil.getHomeDirectory() + File.separator + KEY_DIRECTORY_NAME; /** * In which file to store the recent files. */ - private static String recentFileStorage = getKeyConfigDir() + File.separator + "recentFiles.json"; + private static String recentFileStorage = + getKeyConfigDir() + File.separator + "recentFiles.json"; /** * In which file to store the proof-independent settings. */ - private static String proofIndependentSettings = getKeyConfigDir() + File.separator + "proofIndependentSettings.props"; + private static String proofIndependentSettings = + getKeyConfigDir() + File.separator + "proofIndependentSettings.props"; /** diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java index efd0333f20a..00f0ca2cd84 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java @@ -9,7 +9,7 @@ /** * This interface has to be implemented by a Class providing a persistent Map. */ -@SuppressWarnings({"nullness", "type.argument.type.incompatible"}) +@SuppressWarnings({ "nullness", "type.argument.type.incompatible" }) public interface ImmutableMap extends Iterable> { diff --git a/keyext.exploration/src/main/java/org/key_project/exploration/actions/package-info.java b/keyext.exploration/src/main/java/org/key_project/exploration/actions/package-info.java index 2d2b37e3fd6..a9fb5af0e04 100644 --- a/keyext.exploration/src/main/java/org/key_project/exploration/actions/package-info.java +++ b/keyext.exploration/src/main/java/org/key_project/exploration/actions/package-info.java @@ -2,6 +2,7 @@ * @author Alexander Weigl * @version 1 (10.05.24) */ -@NullMarked package org.key_project.exploration.actions; +@NullMarked +package org.key_project.exploration.actions; -import org.jspecify.annotations.NullMarked; \ No newline at end of file +import org.jspecify.annotations.NullMarked; diff --git a/keyext.exploration/src/main/java/org/key_project/exploration/package-info.java b/keyext.exploration/src/main/java/org/key_project/exploration/package-info.java index 20f24988510..d54dd05f951 100644 --- a/keyext.exploration/src/main/java/org/key_project/exploration/package-info.java +++ b/keyext.exploration/src/main/java/org/key_project/exploration/package-info.java @@ -2,6 +2,7 @@ * @author Alexander Weigl * @version 1 (10.05.24) */ -@NullMarked package org.key_project.exploration; +@NullMarked +package org.key_project.exploration; -import org.jspecify.annotations.NullMarked; \ No newline at end of file +import org.jspecify.annotations.NullMarked; diff --git a/keyext.exploration/src/main/java/org/key_project/exploration/ui/package-info.java b/keyext.exploration/src/main/java/org/key_project/exploration/ui/package-info.java index 5480dc06aa7..8d5c4c96a28 100644 --- a/keyext.exploration/src/main/java/org/key_project/exploration/ui/package-info.java +++ b/keyext.exploration/src/main/java/org/key_project/exploration/ui/package-info.java @@ -2,6 +2,7 @@ * @author Alexander Weigl * @version 1 (10.05.24) */ -@NullMarked package org.key_project.exploration.ui; +@NullMarked +package org.key_project.exploration.ui; -import org.jspecify.annotations.NullMarked; \ No newline at end of file +import org.jspecify.annotations.NullMarked;