Basic Nullness Checker configuration

build.gradle

@@ -22,6 +22,9 @@ plugins {
 
     // Code formatting
     id "com.diffplug.spotless" version "6.16.0"
+
+    // EISOP Checker Framework
+    id "org.checkerframework" version "0.6.28"
 }
 
 // Configure this project for use inside IntelliJ:
@@ -62,6 +65,7 @@ subprojects {
     apply plugin: "com.diffplug.spotless"
     apply plugin: "checkstyle"
     apply plugin: "pmd"
+    apply plugin: "org.checkerframework"
 
     group = rootProject.group
     version = rootProject.version
@@ -84,6 +88,11 @@ subprojects {
         //compile group: 'org.apache.logging.log4j', name: 'log4j-core', version: '2.12.0'
         implementation 'com.google.code.findbugs:jsr305:3.0.2'
 
+        compileOnly 'org.jspecify:jspecify:0.3.0'
+        compileOnly 'io.github.eisop:checker-qual:3.34.0-eisop1'
+        testCompileOnly 'io.github.eisop:checker-qual:3.34.0-eisop1'
+        checkerFramework 'io.github.eisop:checker:3.34.0-eisop1'
+
         testImplementation 'org.junit.jupiter:junit-jupiter-api:5.9.3'
         testImplementation 'org.junit.jupiter:junit-jupiter-params:5.9.3'
         testCompileOnly 'junit:junit:4.13.2'
@@ -405,6 +414,17 @@ subprojects {
         }
     }
 
+    checkerFramework {
+        checkers = [
+            "org.checkerframework.checker.nullness.NullnessChecker",
+        ]
+        extraJavacArgs = [
+            "-AonlyDefs=^org\\.key_project\\.util",
+            "-Xmaxerrs", "10000",
+            "-Werror",
+            "-Aversion",
+        ]
+    }
 }
 
 task start {

key.util/src/main/java/org/key_project/util/EqualsModProofIrrelevancyUtil.java

@@ -10,6 +10,7 @@
  *
  * @author Arne Keller
  */
+@SuppressWarnings("nullness")
 public final class EqualsModProofIrrelevancyUtil {
     private EqualsModProofIrrelevancyUtil() {
 

key.util/src/main/java/org/key_project/util/EqualsModProofIrrelevancyWrapper.java

@@ -9,6 +9,7 @@
  * @param <T> type to wrap
  * @author Arne Keller
  */
+@SuppressWarnings("nullness")
 public class EqualsModProofIrrelevancyWrapper<T extends EqualsModProofIrrelevancy> {
     /**
      * The wrapped object.

key.util/src/main/java/org/key_project/util/ExtList.java

@@ -10,6 +10,7 @@
  * Extends java.util.LinkedList in order to collect elements according to their type.
  * Has facilities to get elements of a certain type ({@link #get(Class)}, {@link #collect(Class)}).
  */
+@SuppressWarnings("nullness")
 public class ExtList extends LinkedList<Object> {
 
     private static final long serialVersionUID = 9182017368310263908L;

key.util/src/main/java/org/key_project/util/Filenames.java

@@ -5,10 +5,13 @@
 import java.util.Arrays;
 import java.util.List;
 
+import org.jspecify.annotations.NullMarked;
+
 /**
  * @author Alexander Weigl
  * @version 1 (29.03.19)
  */
+@NullMarked
 public class Filenames {
     // =======================================================
     // Methods operating on Strings
@@ -153,7 +156,9 @@ private static String[] removeDotDot(String[] a) {
         if (!a[a.length - 1].equals("..")) {
             newa[k++] = a[a.length - 1];
         }
-        return Arrays.copyOf(newa, k);
+        // @ assert (\forall int i; 0 <= i < k; newa[i] != null);
+        // TODO: nullness. This cast cannot be checked, can it? But there is no error message
+        return (String[]) Arrays.copyOf(newa, k);
     }
 
     public static String toValidFileName(String s) {

key.util/src/main/java/org/key_project/util/LRUCache.java

@@ -6,6 +6,7 @@
 /**
  * Simple realisation of an LRU cache.
  */
+@SuppressWarnings("nullness")
 public class LRUCache<K, V> extends LinkedHashMap<K, V> {
 
     /**

key.util/src/main/java/org/key_project/util/RandomName.java

@@ -6,6 +6,7 @@
  * @author Alexander Weigl
  * @version 1 (06.12.18)
  */
+@SuppressWarnings("nullness")
 public class RandomName {
     private static final Random random = new Random();
 

key.util/src/main/java/org/key_project/util/Streams.java

@@ -4,6 +4,7 @@
 import java.io.IOException;
 import java.io.InputStream;
 
+@SuppressWarnings("nullness")
 public class Streams {
 
     private Streams() {

key.util/src/main/java/org/key_project/util/Strings.java

@@ -1,53 +1,33 @@
 package org.key_project.util;
 
-import java.util.regex.Matcher;
-import java.util.regex.Pattern;
+import org.key_project.util.java.StringUtil;
+
+import org.jspecify.annotations.NullMarked;
 
 /**
  * Helper functions for {@link String}s
  *
  * @author Alexander Weigl
  * @version 1 (29.03.19)
  */
+@NullMarked
 public class Strings {
     /**
-     * Checks whether a string contains another one as a whole word (i.e., separated by whitespaces
-     * or a semicolon at the end).
-     *
-     * @param s string to search in
-     * @param word string to be searched for
+     * @deprecated This class has been merged with {@link org.key_project.util.java.StringUtil}.
+     *             Call
+     *             {@link org.key_project.util.java.StringUtil#containsWholeWord(String, String)}
      */
+    @Deprecated
     public static boolean containsWholeWord(String s, String word) {
-        Pattern p = Pattern.compile("\\b" + word + "\\b");
-        Matcher m = p.matcher(s);
-        return m.find();
-        /*
-         * if (s == null || word == null) { return false; } int i = -1; final int wl =
-         * word.length(); while (true) { i = s.indexOf(word, i + 1); if (i < 0 || i >= s.length())
-         * break; if (i == 0 || Character.isWhitespace(s.charAt(i - 1))) { if (i + wl == s.length()
-         * || Character.isWhitespace(s.charAt(i + wl)) || s.charAt(i + wl) == ';') { return true; }
-         * } } return false;
-         */
+        return StringUtil.containsWholeWord(s, word);
     }
 
-
     /**
-     * There are different kinds of JML markers. See Section 4.4 "Annotation markers" of the JML
-     * reference manual.
-     *
-     * @param comment
-     * @return
+     * @deprecated This class has been merged with {@link org.key_project.util.java.StringUtil}.
+     *             Call {@link org.key_project.util.java.StringUtil#isJMLComment(String)}
      */
+    @Deprecated
     public static boolean isJMLComment(String comment) {
-        try {
-            return (comment.startsWith("/*@") || comment.startsWith("//@")
-                    || comment.startsWith("/*+KeY@") || comment.startsWith("//+KeY@")
-                    || (comment.startsWith("/*-") && !comment.startsWith("KeY", 3)
-                            && comment.contains("@"))
-                    || (comment.startsWith("//-") && !comment.startsWith("KeY", 3)
-                            && comment.contains("@")));
-        } catch (IndexOutOfBoundsException e) {
-            return false;
-        }
+        return StringUtil.isJMLComment(comment);
     }
 }

key.util/src/main/java/org/key_project/util/bean/Bean.java

@@ -13,6 +13,7 @@
  * @author Martin Hentschel
  * @see IBean
  */
+@SuppressWarnings("nullness")
 public class Bean implements IBean {
     /**
      * The used {@link PropertyChangeSupport}.

key.util/src/main/java/org/key_project/util/bitops/ImmutableFixedLengthBitSet.java

@@ -9,6 +9,7 @@
  *
  * @author Dominic Scheurer
  */
+@SuppressWarnings("nullness")
 public class ImmutableFixedLengthBitSet {
 
     private boolean[] bitSet = null;

key.util/src/main/java/org/key_project/util/collection/DefaultEdge.java

@@ -6,6 +6,7 @@
  *
  * @author Arne Keller
  */
+@SuppressWarnings("nullness")
 public class DefaultEdge implements GraphEdge {
     /**
      * Source node of this edge.

key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java

@@ -6,6 +6,7 @@
  * This class implements ImmMap<S,T> and provides a persistent Map. It is a simple implementation
  * like lists
  */
+@SuppressWarnings("nullness")
 public class DefaultImmutableMap<S, T> implements ImmutableMap<S, T> {
 
     /**

key.util/src/main/java/org/key_project/util/collection/DefaultImmutableSet.java

@@ -15,6 +15,7 @@
  *
  * @param <T> type of object to store
  */
+@SuppressWarnings("nullness")
 public class DefaultImmutableSet<T> implements ImmutableSet<T> {
 
     /**

key.util/src/main/java/org/key_project/util/collection/DirectedGraph.java

@@ -14,6 +14,7 @@
  * @param <E> edge type
  * @author Arne Keller
  */
+@SuppressWarnings("nullness")
 public class DirectedGraph<V, E extends GraphEdge> implements Graph<V, E> {
     /**
      * Set of vertices in this graph.

key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java

@@ -10,6 +10,7 @@
 import java.util.stream.StreamSupport;
 import javax.annotation.Nonnull;
 
+@SuppressWarnings("nullness")
 public class ImmutableArray<S> implements java.lang.Iterable<S>, java.io.Serializable {
 
     /**

key.util/src/main/java/org/key_project/util/collection/ImmutableLeftistHeap.java

@@ -7,6 +7,7 @@
  * This class implements the leftist heap, see "Functional Data Structures" by Chris
  * Okasaki
  */
+@SuppressWarnings("nullness")
 public abstract class ImmutableLeftistHeap<T extends Comparable<T>> implements ImmutableHeap<T> {
 
     /**

key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java

@@ -20,7 +20,7 @@
  * and head with amortized O(1). This will be done later (if necessary).
  */
 
-@SuppressWarnings("unchecked")
+@SuppressWarnings({ "unchecked", "nullness" })
 public abstract class ImmutableSLList<T> implements ImmutableList<T> {
 
     /**

key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java

@@ -12,6 +12,7 @@
  * offer a public static final variable .<called>nil()
  */
 
+@SuppressWarnings("nullness")
 public interface ImmutableSet<T> extends Iterable<T>, java.io.Serializable {
 
     /**

key.util/src/main/java/org/key_project/util/collection/Immutables.java

@@ -13,6 +13,7 @@
  *
  * @author Mattias Ulbrich
  */
+@SuppressWarnings("nullness")
 public final class Immutables {
 
     private Immutables() {

key.util/src/main/java/org/key_project/util/collection/KeYCollections.java

@@ -14,6 +14,7 @@
  * @author Alexander Weigl
  * @version 1 (29.03.19)
  */
+@SuppressWarnings("nullness")
 public class KeYCollections {
     // =======================================================
     // Methods operating on Arrays

key.util/src/main/java/org/key_project/util/collection/NotUniqueException.java

@@ -3,6 +3,7 @@
 
 
 /** thrown if a duplicate is being added via addUnique() */
+@SuppressWarnings("nullness")
 public class NotUniqueException extends Exception {
 
     private static final long serialVersionUID = 6565515240836947955L;

key.util/src/main/java/org/key_project/util/collection/PropertiesUtil.java

@@ -7,6 +7,7 @@
 import java.nio.charset.StandardCharsets;
 import java.util.Properties;
 
+@SuppressWarnings("nullness")
 public class PropertiesUtil {
 
     private PropertiesUtil() {

key.util/src/main/java/org/key_project/util/helper/FindResources.java

@@ -14,6 +14,7 @@
  * @author Alexander Weigl
  * @version 1 (13.02.19)
  */
+@SuppressWarnings("nullness")
 public final class FindResources {
     /**
      * List directory contents for a resource folder. Not recursive. This is basically a brute-force

key.util/src/main/java/org/key_project/util/helper/HelperClassForUtilityTests.java

@@ -5,6 +5,7 @@
 import java.io.IOException;
 import java.nio.charset.StandardCharsets;
 
+@SuppressWarnings("nullness")
 public class HelperClassForUtilityTests {
     public static final File RESOURCE_DIRECTORY = FindResources.getTestResourcesDirectory();
 

key.util/src/main/java/org/key_project/util/java/ArrayUtil.java

@@ -10,6 +10,7 @@
  *
  * @author Martin Hentschel
  */
+@SuppressWarnings("nullness")
 public final class ArrayUtil {
     /**
      * Forbid instances by this private constructor.

key.util/src/main/java/org/key_project/util/java/CollectionUtil.java

@@ -8,6 +8,7 @@
  *
  * @author Martin Hentschel
  */
+@SuppressWarnings("nullness")
 public class CollectionUtil {
     /**
      * The default separator.

key.util/src/main/java/org/key_project/util/java/IOUtil.java

@@ -18,6 +18,7 @@
  *
  * @author Martin Hentschel
  */
+@SuppressWarnings("nullness")
 public final class IOUtil {
     /**
      * The size of used buffers.

key.util/src/main/java/org/key_project/util/java/IntegerUtil.java

@@ -1,5 +1,6 @@
 package org.key_project.util.java;
 
+@SuppressWarnings("nullness")
 public final class IntegerUtil {
     /**
      * Forbid instances.

key.util/src/main/java/org/key_project/util/java/MapUtil.java

@@ -12,6 +12,7 @@
  *
  * @author lanzinger
  */
+@SuppressWarnings("nullness")
 public final class MapUtil {
 
     private MapUtil() {}

key.util/src/main/java/org/key_project/util/java/NumberUtil.java

@@ -5,6 +5,7 @@
  *
  * @author Martin Hentschel
  */
+@SuppressWarnings("nullness")
 public class NumberUtil {
     /**
      * The maximal number of digits of an integer value.