Nullness Type System activated for key.ncore (KeYProject#3468)

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java

@@ -128,9 +128,8 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) {
     /**
      * {@inheritDoc}
      */
-    @NonNull
     @Override
-    public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
+    public @NonNull ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
             throws RuleAbortException {
         try {
             // Extract required Terms from goal

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java

@@ -189,9 +189,8 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) {
     /**
      * {@inheritDoc}
      */
-    @NonNull
     @Override
-    public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
+    public @NonNull ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
             throws RuleAbortException {
         try {
             // Extract required Terms from goal

key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java

@@ -296,8 +296,7 @@ public void set(TestGenerationSettings settings) {
     }
 
 
-    @Nullable
-    private static TestGenerationSettings instance;
+    private static @Nullable TestGenerationSettings instance;
 
     public static @NonNull TestGenerationSettings getInstance() {
         if (instance == null) {

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

@@ -38,18 +38,17 @@ public String getFilename() {
         return filename;
     }
 
-    @Nullable
     @Override
-    public Location getLocation() throws MalformedURLException {
+    public @Nullable Location getLocation() throws MalformedURLException {
         // This kind of exception has a filename but no line/col information
         // Retrieve the latter from the cause. location remains null if
         // no line/col is available in cause.
         if (getCause() != null) {
             var location = ExceptionTools.getLocation(getCause());
-            if (location.isEmpty()) {
+            if (location == null) {
                 return null;
             }
-            return Location.fromFileName(getFilename(), location.get().getPosition());
+            return Location.fromFileName(getFilename(), location.getPosition());
         }
         return null;
     }

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

@@ -67,9 +67,8 @@ public Position getPosition() {
         return position;
     }
 
-    @Nullable
     @Override
-    public Location getLocation() throws MalformedURLException {
+    public @Nullable Location getLocation() throws MalformedURLException {
         Throwable cause = getCause();
         if (this.file == null) {
             if (cause instanceof UnresolvedReferenceException ure) {

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

@@ -35,15 +35,13 @@ public class PositionInfo {
     /**
      * The URI of the resource this location refers to. Either a meaningful value or null.
      */
-    @Nullable
-    private final URI fileURI;
+    private final @Nullable URI fileURI;
 
     /**
      * The URI of the parent class of this location (the class the statement originates from). May
      * be null.
      */
-    @Nullable
-    private URI parentClassURI;
+    private @Nullable URI parentClassURI;
 
     private PositionInfo() {
         this.relPos = SourceElement.Position.UNDEFINED;
@@ -111,8 +109,7 @@ public String getFileName() {
         return null;
     }
 
-    @Nullable
-    public URI getParentClassURI() {
+    public @Nullable URI getParentClassURI() {
         return parentClassURI;
     }
 

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

@@ -1206,8 +1206,7 @@ private static String trim(String s, int length) {
     /**
      * tries to parse recoders exception position information
      */
-    @Nullable
-    private static Pair<String, Position> extractPositionInfo(String errorMessage) {
+    private static @Nullable Pair<String, Position> extractPositionInfo(String errorMessage) {
         if (errorMessage == null || errorMessage.indexOf('@') == -1) {
             return null;
         }

key.core/src/main/java/de/uka/ilkd/key/ldt/CharListLDT.java

@@ -248,9 +248,8 @@ public Type getType(Term t) {
         return null;
     }
 
-    @Nullable
     @Override
-    public JFunction getFunctionFor(String operationName, Services services) {
+    public @Nullable JFunction getFunctionFor(String operationName, Services services) {
         // This is not very elegant; but seqConcat is actually in the SeqLDT.
         if (operationName.equals("add")) {
             return services.getNamespaces().functions().lookup("seqConcat");

key.core/src/main/java/de/uka/ilkd/key/ldt/IntegerLDT.java

@@ -715,9 +715,8 @@ public JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Ser
         return null;
     }
 
-    @Nullable
     @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();

key.core/src/main/java/de/uka/ilkd/key/ldt/LocSetLDT.java

@@ -210,9 +210,8 @@ public Type getType(Term t) {
         return null;
     }
 
-    @Nullable
     @Override
-    public JFunction getFunctionFor(String operationName, Services services) {
+    public @Nullable JFunction getFunctionFor(String operationName, Services services) {
         return switch (operationName) {
         case "add" -> getUnion();
         case "sub" -> getSetMinus();

key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java

@@ -170,9 +170,8 @@ public JFunction getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Ser
         return null;
     }
 
-    @Nullable
     @Override
-    public JFunction getFunctionFor(String operationName, Services services) {
+    public @Nullable JFunction getFunctionFor(String operationName, Services services) {
         if (operationName.equals("add")) {
             return getSeqConcat();
         }

key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java

@@ -692,8 +692,7 @@ public static final class FileOrigin extends Origin {
         /**
          * The file the term originates from.
          */
-        @Nullable
-        private final URI fileName;
+        private final @Nullable URI fileName;
 
         /**
          * The line in the file the term originates from.

key.core/src/main/java/de/uka/ilkd/key/logic/op/AbstractSV.java

@@ -30,7 +30,7 @@ protected AbstractSV(Name name, Sort[] argSorts, Sort sort, boolean isRigid, boo
 
 
     protected AbstractSV(Name name, Sort sort, boolean isRigid, boolean isStrict) {
-        this(name, (ImmutableArray<Sort>) null, sort, isRigid, isStrict);
+        this(name, new ImmutableArray<>(), sort, isRigid, isStrict);
     }
 
 

key.core/src/main/java/de/uka/ilkd/key/logic/op/AbstractSortedOperator.java

@@ -46,7 +46,7 @@ protected AbstractSortedOperator(Name name, Sort[] argSorts, Sort sort, boolean
     }
 
     protected AbstractSortedOperator(Name name, Sort sort, boolean isRigid) {
-        this(name, (ImmutableArray<Sort>) null, sort, null, isRigid);
+        this(name, new ImmutableArray<>(), sort, null, isRigid);
     }
 
     /**

key.core/src/main/java/de/uka/ilkd/key/logic/sort/SortImpl.java

@@ -87,15 +87,13 @@ public String declarationString() {
         return name().toString();
     }
 
-    @Nullable
     @Override
-    public String getDocumentation() {
+    public @Nullable String getDocumentation() {
         return documentation;
     }
 
-    @Nullable
     @Override
-    public String getOrigin() {
+    public @Nullable String getOrigin() {
         return origin;
     }
 

key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EngineState.java

@@ -200,8 +200,7 @@ public Term toTerm(String string, Sort sort) throws ParserException, ScriptExcep
                 "Unexpected sort for term: " + term + ". Expected: " + sort);
     }
 
-    @NonNull
-    private KeyIO getKeyIO() throws ScriptException {
+    private @NonNull KeyIO getKeyIO() throws ScriptException {
         Services services = proof.getServices();
         KeyIO io = new KeyIO(services, getFirstOpenAutomaticGoal().getLocalNamespaces());
         io.setAbbrevMap(abbrevMap);

key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptException.java

@@ -45,9 +45,8 @@ public ScriptException(String message, Throwable cause) {
         this.location = null;
     }
 
-    @Nullable
     @Override
-    public Location getLocation() {
+    public @Nullable Location getLocation() {
         return location;
     }
 

key.core/src/main/java/de/uka/ilkd/key/nparser/ConfigurationBuilder.java

@@ -44,8 +44,7 @@ public String visitCstring(KeYParser.CstringContext ctx) {
         return sanitizeStringLiteral(text);
     }
 
-    @NonNull
-    private static String sanitizeStringLiteral(String text) {
+    private static @NonNull String sanitizeStringLiteral(String text) {
         return text.substring(1, text.length() - 1)
                 .replace("\\\"", "\"")
                 .replace("\\\\", "\\");

key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java

@@ -39,8 +39,8 @@
  * @version 1 (5.12.19)
  */
 public abstract class KeyAst<T extends ParserRuleContext> {
-    @NonNull
-    final T ctx;
+
+    final @NonNull T ctx;
 
     protected KeyAst(@NonNull T ctx) {
         this.ctx = ctx;

key.core/src/main/java/de/uka/ilkd/key/nparser/KeyIO.java

@@ -49,8 +49,7 @@ public class KeyIO {
 
     private final Services services;
     private final NamespaceSet nss;
-    @Nullable
-    private Namespace<SchemaVariable> schemaNamespace;
+    private @Nullable Namespace<SchemaVariable> schemaNamespace;
     private List<BuildingIssue> warnings = new LinkedList<>();
     private AbbrevMap abbrevMap;
 
@@ -207,8 +206,7 @@ public List<BuildingIssue> getWarnings() {
         return warnings;
     }
 
-    @Nullable
-    public List<BuildingIssue> resetWarnings() {
+    public @Nullable List<BuildingIssue> resetWarnings() {
         var w = warnings;
         warnings = new LinkedList<>();
         return w;

key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java

@@ -54,8 +54,8 @@ private ParsingFacade() {
      * @param <T> parse tree type
      * @return the {@link ParserRuleContext} inside the given ast object.
      */
-    @NonNull
-    public static <T extends ParserRuleContext> T getParseRuleContext(@NonNull KeyAst<T> ast) {
+    public static <T extends ParserRuleContext> @NonNull T getParseRuleContext(
+            @NonNull KeyAst<T> ast) {
         return ast.ctx;
     }
 
@@ -192,8 +192,7 @@ public static KeYParser.Id_declarationContext parseIdDeclaration(CharStream stre
         return p.id_declaration();
     }
 
-    @Nullable
-    public static String getValueDocumentation(@Nullable TerminalNode docComment) {
+    public static @Nullable String getValueDocumentation(@Nullable TerminalNode docComment) {
         if (docComment == null) {
             return null;
         }

key.core/src/main/java/de/uka/ilkd/key/nparser/ProblemInformation.java

@@ -70,62 +70,55 @@ public ProblemInformation() {
         classpath = new LinkedList<>();
     }
 
-    @Nullable
-    public String getChooseContract() {
+    public @Nullable String getChooseContract() {
         return chooseContract;
     }
 
     public void setChooseContract(@Nullable String chooseContract) {
         this.chooseContract = chooseContract;
     }
 
-    @Nullable
-    public String getProofObligation() {
+    public @Nullable String getProofObligation() {
         return proofObligation;
     }
 
     public void setProofObligation(@Nullable String proofObligation) {
         this.proofObligation = proofObligation;
     }
 
-    @Nullable
-    public String getProfile() {
+    public @Nullable String getProfile() {
         return profile;
     }
 
     public void setProfile(@Nullable String profile) {
         this.profile = profile;
     }
 
-    @Nullable
-    public String getPreferences() {
+    public @Nullable String getPreferences() {
         return preferences;
     }
 
     public void setPreferences(@Nullable String preferences) {
         this.preferences = preferences;
     }
 
-    @Nullable
-    public String getBootClassPath() {
+    public @Nullable String getBootClassPath() {
         return bootClassPath;
     }
 
     public void setBootClassPath(@Nullable String bootClassPath) {
         this.bootClassPath = bootClassPath;
     }
 
-    @Nullable
-    public String getJavaSource() {
+    public @Nullable String getJavaSource() {
         return javaSource;
     }
 
     public void setJavaSource(@Nullable String javaSource) {
         this.javaSource = javaSource;
     }
 
-    @NonNull
-    public List<String> getClasspath() {
+    public @NonNull List<String> getClasspath() {
         return classpath;
     }
 

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/AbstractBuilder.java

@@ -29,10 +29,9 @@
  */
 @SuppressWarnings("unchecked")
 abstract class AbstractBuilder<T> extends KeYParserBaseVisitor<T> {
-    @Nullable
-    private List<BuildingIssue> buildingIssues = null;
-    @Nullable
-    private Stack<Object> parameters = null;
+
+    private @Nullable List<BuildingIssue> buildingIssues = null;
+    private @Nullable Stack<Object> parameters = null;
 
     /**
      * Helper function for avoiding cast.

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ChoiceFinder.java

@@ -23,8 +23,8 @@
  * @see ChoiceInformation
  */
 public class ChoiceFinder extends AbstractBuilder<Object> {
-    @NonNull
-    private final ChoiceInformation choiceInformation;
+
+    private final @NonNull ChoiceInformation choiceInformation;
 
     public ChoiceFinder() {
         choiceInformation = new ChoiceInformation();
@@ -82,8 +82,7 @@ public Choice visitActivated_choice(KeYParser.Activated_choiceContext ctx) {
         return c;
     }
 
-    @NonNull
-    public ChoiceInformation getChoiceInformation() {
+    public @NonNull ChoiceInformation getChoiceInformation() {
         return choiceInformation;
     }
 

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java

@@ -1247,8 +1247,7 @@ private Term visitAccesstermAsJava(KeYParser.AccesstermContext ctx) {
                 if (a.heap != null) {
                     break; // No heap on java package allowed
                 }
-                @Nullable
-                Object cur = accept(a.id);
+                @Nullable Object cur = accept(a.id);
                 if (isPackage(javaPackage + "." + cur)) {
                     javaPackage += "." + cur;
                     currentSuffix++;