diff --git a/build.gradle b/build.gradle index fa473fe1ce4..bcaf5563441 100644 --- a/build.gradle +++ b/build.gradle @@ -419,7 +419,7 @@ subprojects { "org.checkerframework.checker.nullness.NullnessChecker", ] extraJavacArgs = [ - "-AonlyDefs=^org\\.key_project\\.util\\.lookup", + "-AonlyDefs=^org\\.key_project\\.util", "-Xmaxerrs", "10000", "-Werror", "-Aversion", diff --git a/key.util/src/main/java/org/key_project/util/EqualsModProofIrrelevancyUtil.java b/key.util/src/main/java/org/key_project/util/EqualsModProofIrrelevancyUtil.java index 9e6e1e7d965..6e8dc28668b 100644 --- a/key.util/src/main/java/org/key_project/util/EqualsModProofIrrelevancyUtil.java +++ b/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() { diff --git a/key.util/src/main/java/org/key_project/util/EqualsModProofIrrelevancyWrapper.java b/key.util/src/main/java/org/key_project/util/EqualsModProofIrrelevancyWrapper.java index c80c3a8fdfa..92f40585468 100644 --- a/key.util/src/main/java/org/key_project/util/EqualsModProofIrrelevancyWrapper.java +++ b/key.util/src/main/java/org/key_project/util/EqualsModProofIrrelevancyWrapper.java @@ -9,6 +9,7 @@ * @param type to wrap * @author Arne Keller */ +@SuppressWarnings("nullness") public class EqualsModProofIrrelevancyWrapper { /** * The wrapped object. diff --git a/key.util/src/main/java/org/key_project/util/ExtList.java b/key.util/src/main/java/org/key_project/util/ExtList.java index 8d5bf780754..460a4770592 100644 --- a/key.util/src/main/java/org/key_project/util/ExtList.java +++ b/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 { private static final long serialVersionUID = 9182017368310263908L; diff --git a/key.util/src/main/java/org/key_project/util/Filenames.java b/key.util/src/main/java/org/key_project/util/Filenames.java index b7122a98e48..05fcbb78483 100644 --- a/key.util/src/main/java/org/key_project/util/Filenames.java +++ b/key.util/src/main/java/org/key_project/util/Filenames.java @@ -9,6 +9,7 @@ * @author Alexander Weigl * @version 1 (29.03.19) */ +@SuppressWarnings("nullness") public class Filenames { // ======================================================= // Methods operating on Strings diff --git a/key.util/src/main/java/org/key_project/util/LRUCache.java b/key.util/src/main/java/org/key_project/util/LRUCache.java index 7690a5975b3..3488b9d6db4 100644 --- a/key.util/src/main/java/org/key_project/util/LRUCache.java +++ b/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 extends LinkedHashMap { /** diff --git a/key.util/src/main/java/org/key_project/util/RandomName.java b/key.util/src/main/java/org/key_project/util/RandomName.java index 976e13d7b71..a62cc7c8358 100644 --- a/key.util/src/main/java/org/key_project/util/RandomName.java +++ b/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(); diff --git a/key.util/src/main/java/org/key_project/util/Streams.java b/key.util/src/main/java/org/key_project/util/Streams.java index 6cc8b817209..b10f298b2b2 100644 --- a/key.util/src/main/java/org/key_project/util/Streams.java +++ b/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() { diff --git a/key.util/src/main/java/org/key_project/util/Strings.java b/key.util/src/main/java/org/key_project/util/Strings.java index 55e292a1257..1bfa338ea74 100644 --- a/key.util/src/main/java/org/key_project/util/Strings.java +++ b/key.util/src/main/java/org/key_project/util/Strings.java @@ -1,5 +1,6 @@ package org.key_project.util; +import org.jspecify.annotations.NullMarked; import org.key_project.util.java.StringUtil; /** @@ -8,6 +9,7 @@ * @author Alexander Weigl * @version 1 (29.03.19) */ +@NullMarked public class Strings { /** * @deprecated This class has been merged with {@link org.key_project.util.java.StringUtil}. diff --git a/key.util/src/main/java/org/key_project/util/bean/Bean.java b/key.util/src/main/java/org/key_project/util/bean/Bean.java index d9d8a085c16..04c5899a2ca 100644 --- a/key.util/src/main/java/org/key_project/util/bean/Bean.java +++ b/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}. diff --git a/key.util/src/main/java/org/key_project/util/bitops/ImmutableFixedLengthBitSet.java b/key.util/src/main/java/org/key_project/util/bitops/ImmutableFixedLengthBitSet.java index b8f6c19ecc8..4e1fafae447 100644 --- a/key.util/src/main/java/org/key_project/util/bitops/ImmutableFixedLengthBitSet.java +++ b/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; diff --git a/key.util/src/main/java/org/key_project/util/collection/DefaultEdge.java b/key.util/src/main/java/org/key_project/util/collection/DefaultEdge.java index a2b422b1ca6..3562fa26b76 100644 --- a/key.util/src/main/java/org/key_project/util/collection/DefaultEdge.java +++ b/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. diff --git a/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java b/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java index c903a8a3c90..b81a4d7327d 100644 --- a/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java +++ b/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java @@ -6,6 +6,7 @@ * This class implements ImmMap and provides a persistent Map. It is a simple implementation * like lists */ +@SuppressWarnings("nullness") public class DefaultImmutableMap implements ImmutableMap { /** diff --git a/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableSet.java b/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableSet.java index 37b5d60c728..486f3988989 100644 --- a/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableSet.java +++ b/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableSet.java @@ -15,6 +15,7 @@ * * @param type of object to store */ +@SuppressWarnings("nullness") public class DefaultImmutableSet implements ImmutableSet { /** diff --git a/key.util/src/main/java/org/key_project/util/collection/DirectedGraph.java b/key.util/src/main/java/org/key_project/util/collection/DirectedGraph.java index dfc67953ff1..1bd08b623c5 100644 --- a/key.util/src/main/java/org/key_project/util/collection/DirectedGraph.java +++ b/key.util/src/main/java/org/key_project/util/collection/DirectedGraph.java @@ -14,6 +14,7 @@ * @param edge type * @author Arne Keller */ +@SuppressWarnings("nullness") public class DirectedGraph implements Graph { /** * Set of vertices in this graph. diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java index 3723550909d..29619b553cd 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java +++ b/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 implements java.lang.Iterable, java.io.Serializable { /** diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableLeftistHeap.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableLeftistHeap.java index 7fd38d909f2..baa197a1f45 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableLeftistHeap.java +++ b/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> implements ImmutableHeap { /** diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java index 2ac3f8c1fd7..c189524f6fd 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java +++ b/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 implements ImmutableList { /** diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java index b1c1655c51a..6264ae12d9d 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableSet.java @@ -12,6 +12,7 @@ * offer a public static final variable .nil() */ +@SuppressWarnings("nullness") public interface ImmutableSet extends Iterable, java.io.Serializable { /** diff --git a/key.util/src/main/java/org/key_project/util/collection/Immutables.java b/key.util/src/main/java/org/key_project/util/collection/Immutables.java index 7401b27e682..b37b1c36729 100644 --- a/key.util/src/main/java/org/key_project/util/collection/Immutables.java +++ b/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() { diff --git a/key.util/src/main/java/org/key_project/util/collection/KeYCollections.java b/key.util/src/main/java/org/key_project/util/collection/KeYCollections.java index 00acea0741a..11d479a6f91 100644 --- a/key.util/src/main/java/org/key_project/util/collection/KeYCollections.java +++ b/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 diff --git a/key.util/src/main/java/org/key_project/util/collection/NotUniqueException.java b/key.util/src/main/java/org/key_project/util/collection/NotUniqueException.java index 340a04eda06..360179ba951 100644 --- a/key.util/src/main/java/org/key_project/util/collection/NotUniqueException.java +++ b/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; diff --git a/key.util/src/main/java/org/key_project/util/collection/PropertiesUtil.java b/key.util/src/main/java/org/key_project/util/collection/PropertiesUtil.java index b193a693911..d2884d43f9f 100644 --- a/key.util/src/main/java/org/key_project/util/collection/PropertiesUtil.java +++ b/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() { diff --git a/key.util/src/main/java/org/key_project/util/helper/FindResources.java b/key.util/src/main/java/org/key_project/util/helper/FindResources.java index 0ee3215b281..a2365f38712 100644 --- a/key.util/src/main/java/org/key_project/util/helper/FindResources.java +++ b/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 diff --git a/key.util/src/main/java/org/key_project/util/helper/HelperClassForUtilityTests.java b/key.util/src/main/java/org/key_project/util/helper/HelperClassForUtilityTests.java index bf55ef35fcb..d4a855147fc 100644 --- a/key.util/src/main/java/org/key_project/util/helper/HelperClassForUtilityTests.java +++ b/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(); diff --git a/key.util/src/main/java/org/key_project/util/java/ArrayUtil.java b/key.util/src/main/java/org/key_project/util/java/ArrayUtil.java index e19552eb30b..03e635d16df 100644 --- a/key.util/src/main/java/org/key_project/util/java/ArrayUtil.java +++ b/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. diff --git a/key.util/src/main/java/org/key_project/util/java/CollectionUtil.java b/key.util/src/main/java/org/key_project/util/java/CollectionUtil.java index 3ce65775909..82a97084db8 100644 --- a/key.util/src/main/java/org/key_project/util/java/CollectionUtil.java +++ b/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. diff --git a/key.util/src/main/java/org/key_project/util/java/IOUtil.java b/key.util/src/main/java/org/key_project/util/java/IOUtil.java index 91a1e6a6c97..37b60c4fa67 100644 --- a/key.util/src/main/java/org/key_project/util/java/IOUtil.java +++ b/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. diff --git a/key.util/src/main/java/org/key_project/util/java/IntegerUtil.java b/key.util/src/main/java/org/key_project/util/java/IntegerUtil.java index 495fd5ae775..1dd354bf163 100644 --- a/key.util/src/main/java/org/key_project/util/java/IntegerUtil.java +++ b/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. diff --git a/key.util/src/main/java/org/key_project/util/java/MapUtil.java b/key.util/src/main/java/org/key_project/util/java/MapUtil.java index d6d441fb87a..37712c59b15 100644 --- a/key.util/src/main/java/org/key_project/util/java/MapUtil.java +++ b/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() {} diff --git a/key.util/src/main/java/org/key_project/util/java/NumberUtil.java b/key.util/src/main/java/org/key_project/util/java/NumberUtil.java index 2c77796e405..76c34dac6f5 100644 --- a/key.util/src/main/java/org/key_project/util/java/NumberUtil.java +++ b/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. diff --git a/key.util/src/main/java/org/key_project/util/java/WrapUtils.java b/key.util/src/main/java/org/key_project/util/java/WrapUtils.java index 2c6cdfc4657..09f264ef2f0 100644 --- a/key.util/src/main/java/org/key_project/util/java/WrapUtils.java +++ b/key.util/src/main/java/org/key_project/util/java/WrapUtils.java @@ -13,6 +13,7 @@ * * @author Mattias Ulbrich, Mar 2021 */ +@SuppressWarnings("nullness") public class WrapUtils { /* diff --git a/key.util/src/main/java/org/key_project/util/java/XMLUtil.java b/key.util/src/main/java/org/key_project/util/java/XMLUtil.java index 508ad47f6ad..f57110156c7 100644 --- a/key.util/src/main/java/org/key_project/util/java/XMLUtil.java +++ b/key.util/src/main/java/org/key_project/util/java/XMLUtil.java @@ -8,6 +8,7 @@ * * @author Martin Hentschel */ +@SuppressWarnings("nullness") public final class XMLUtil { /** * Attribute name to store encodings. diff --git a/key.util/src/main/java/org/key_project/util/java/thread/AbstractRunnableWithException.java b/key.util/src/main/java/org/key_project/util/java/thread/AbstractRunnableWithException.java index c9d889e5e71..adb9aa9ca68 100644 --- a/key.util/src/main/java/org/key_project/util/java/thread/AbstractRunnableWithException.java +++ b/key.util/src/main/java/org/key_project/util/java/thread/AbstractRunnableWithException.java @@ -12,6 +12,7 @@ * @author Martin Hentschel * @see IRunnableWithResult */ +@SuppressWarnings("nullness") public abstract class AbstractRunnableWithException implements IRunnableWithException { /** * An occurred exception. diff --git a/key.util/src/main/java/org/key_project/util/java/thread/AbstractRunnableWithResult.java b/key.util/src/main/java/org/key_project/util/java/thread/AbstractRunnableWithResult.java index 91ddb7aad27..a05c67b1696 100644 --- a/key.util/src/main/java/org/key_project/util/java/thread/AbstractRunnableWithResult.java +++ b/key.util/src/main/java/org/key_project/util/java/thread/AbstractRunnableWithResult.java @@ -12,6 +12,7 @@ * @author Martin Hentschel * @see IRunnableWithResult */ +@SuppressWarnings("nullness") public abstract class AbstractRunnableWithResult extends AbstractRunnableWithException implements IRunnableWithResult { /** diff --git a/key.util/src/main/java/org/key_project/util/lookup/InjectionException.java b/key.util/src/main/java/org/key_project/util/lookup/InjectionException.java index 863f301d044..2b61eb564c2 100644 --- a/key.util/src/main/java/org/key_project/util/lookup/InjectionException.java +++ b/key.util/src/main/java/org/key_project/util/lookup/InjectionException.java @@ -4,6 +4,7 @@ * @author Alexander Weigl * @version 1 (13.01.19) */ +@SuppressWarnings("nullness") public class InjectionException extends RuntimeException { private static final long serialVersionUID = 119998955722036861L; diff --git a/key.util/src/main/java/org/key_project/util/lookup/Lookup.java b/key.util/src/main/java/org/key_project/util/lookup/Lookup.java index 441e91b69fa..254a6e3cd81 100644 --- a/key.util/src/main/java/org/key_project/util/lookup/Lookup.java +++ b/key.util/src/main/java/org/key_project/util/lookup/Lookup.java @@ -24,6 +24,7 @@ * @version 1 (15.03.19) */ @NullMarked +@SuppressWarnings("nullness") public class Lookup { public static final Lookup DEFAULT = new Lookup(); diff --git a/key.util/src/main/java/org/key_project/util/reflection/ClassLoaderUtil.java b/key.util/src/main/java/org/key_project/util/reflection/ClassLoaderUtil.java index 1601f192add..b58cab00727 100644 --- a/key.util/src/main/java/org/key_project/util/reflection/ClassLoaderUtil.java +++ b/key.util/src/main/java/org/key_project/util/reflection/ClassLoaderUtil.java @@ -35,6 +35,7 @@ * @see IClassLoader * @see JavaApplicationClassLoader */ +@SuppressWarnings("nullness") public class ClassLoaderUtil { /** * The {@link IClassLoader} instance to use. diff --git a/key.util/src/main/java/org/key_project/util/reflection/JavaApplicationClassLoader.java b/key.util/src/main/java/org/key_project/util/reflection/JavaApplicationClassLoader.java index b7f07142c5e..38feed62992 100644 --- a/key.util/src/main/java/org/key_project/util/reflection/JavaApplicationClassLoader.java +++ b/key.util/src/main/java/org/key_project/util/reflection/JavaApplicationClassLoader.java @@ -10,6 +10,7 @@ * * @author Martin Hentschel */ +@SuppressWarnings("nullness") public class JavaApplicationClassLoader implements IClassLoader { /** * {@inheritDoc}