replace JSR305 annotations with JSpecify (#3290)

This PR replaces the JSR305 annotations with the JSpecify annotations.

In preparation to #3183.

Author: wadoon

build.gradle

@@ -71,20 +71,17 @@ subprojects {
 
     dependencies {
         implementation("org.slf4j:slf4j-api:2.0.9")
-        testImplementation("ch.qos.logback:logback-classic:1.4.11")
-
-        //compile group: 'org.apache.logging.log4j', name: 'log4j-api', version: '2.12.0'
-        //compile group: 'org.apache.logging.log4j', name: 'log4j-core', version: '2.12.0'
-        implementation 'com.google.code.findbugs:jsr305:3.0.2'
 
+        testImplementation("ch.qos.logback:logback-classic:1.4.11")
         testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.0'
         testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.0'
+        testImplementation project(':key.util')
+
         testCompileOnly 'junit:junit:4.13.2'
         testRuntimeOnly 'org.junit.vintage:junit-vintage-engine:5.10.0'
         testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.0'
 
-
-        testImplementation project(':key.util')
+        implementation("org.jspecify:jspecify:0.3.0")
     }
 
     tasks.withType(JavaCompile) {

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

@@ -38,6 +38,8 @@
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
 
+import org.jspecify.annotations.NonNull;
+
 /**
  * <p>
  * A {@link BuiltInRule} which evaluates a modality in a side proof.
@@ -132,6 +134,7 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) {
     /**
      * {@inheritDoc}
      */
+    @NonNull
     @Override
     public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
             throws RuleAbortException {

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

@@ -5,8 +5,9 @@
 
 import java.io.File;
 import java.util.Properties;
-import javax.annotation.Nonnull;
-import javax.annotation.Nullable;
+
+import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.Nullable;
 
 public class TestGenerationSettings extends AbstractSettings {
     // region Default Values for option fields
@@ -279,7 +280,7 @@ public void set(TestGenerationSettings settings) {
     @Nullable
     private static TestGenerationSettings instance;
 
-    public static @Nonnull TestGenerationSettings getInstance() {
+    public static @NonNull TestGenerationSettings getInstance() {
         if (instance == null) {
             instance = new TestGenerationSettings();
             ProofIndependentSettings.DEFAULT_INSTANCE.addSettings(instance);

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

@@ -4,12 +4,12 @@
 package de.uka.ilkd.key.java;
 
 import java.net.MalformedURLException;
-import javax.annotation.Nullable;
 
 import de.uka.ilkd.key.parser.Location;
 import de.uka.ilkd.key.util.ExceptionTools;
 import de.uka.ilkd.key.util.parsing.HasLocation;
 
+import org.jspecify.annotations.Nullable;
 import recoder.parser.ParseException;
 
 /**

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

@@ -5,11 +5,11 @@
 
 
 import java.net.MalformedURLException;
-import javax.annotation.Nullable;
 
 import de.uka.ilkd.key.parser.Location;
 import de.uka.ilkd.key.util.parsing.HasLocation;
 
+import org.jspecify.annotations.Nullable;
 import recoder.java.CompilationUnit;
 import recoder.kit.UnitKit;
 import recoder.service.UnresolvedReferenceException;

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

@@ -8,8 +8,8 @@
 import java.net.URL;
 import java.nio.file.Paths;
 import java.util.Optional;
-import javax.annotation.Nullable;
 
+import org.jspecify.annotations.Nullable;
 import recoder.java.SourceElement;
 
 /**

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

@@ -8,7 +8,6 @@
 import java.nio.charset.StandardCharsets;
 import java.nio.file.Paths;
 import java.util.*;
-import javax.annotation.Nullable;
 
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
 import de.uka.ilkd.key.java.abstraction.NullType;
@@ -29,6 +28,7 @@
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 
+import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 import recoder.ModelException;

key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java

@@ -5,7 +5,6 @@
 
 import java.net.URI;
 import java.util.*;
-import javax.annotation.Nonnull;
 
 import de.uka.ilkd.key.parser.Location;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
@@ -22,6 +21,7 @@
 
 import org.antlr.v4.runtime.ParserRuleContext;
 import org.antlr.v4.runtime.misc.Interval;
+import org.jspecify.annotations.NonNull;
 import recoder.CrossReferenceServiceConfiguration;
 import recoder.abstraction.Constructor;
 import recoder.abstraction.Method;
@@ -732,7 +732,7 @@ private static class TypeDeclarationCollector extends SourceVisitor {
 
         final HashSet<TypeDeclaration> result = new LinkedHashSet<>();
 
-        public void walk(@Nonnull SourceElement s) {
+        public void walk(@NonNull SourceElement s) {
             s.accept(this);
             if (s instanceof NonTerminalProgramElement pe) {
                 for (int i = 0; i < pe.getChildCount(); i++) {

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

@@ -3,8 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.ldt;
 
-import javax.annotation.Nullable;
-
 import de.uka.ilkd.key.java.ConvertException;
 import de.uka.ilkd.key.java.Expression;
 import de.uka.ilkd.key.java.Services;
@@ -21,6 +19,8 @@
 
 import org.key_project.util.ExtList;
 
+import org.jspecify.annotations.Nullable;
+
 
 public final class CharListLDT extends LDT {
 

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

@@ -3,8 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.ldt;
 
-import javax.annotation.Nullable;
-
 import de.uka.ilkd.key.java.Expression;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.abstraction.PrimitiveType;
@@ -24,6 +22,7 @@
 
 import org.key_project.util.ExtList;
 
+import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;