nullness-specifying class Filenames

KeYProject · Jun 26, 2023 · de7cdae · de7cdae
1 parent 08673f9
commit de7cdae
Showing 1 changed file with 6 additions and 2 deletions.
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
@@ -5,11 +5,13 @@
 import java.util.Arrays;
 import java.util.List;
 
+import org.jspecify.annotations.NullMarked;
+
 /**
  * @author Alexander Weigl
  * @version 1 (29.03.19)
  */
-@SuppressWarnings("nullness")
+@NullMarked
 public class Filenames {
     // =======================================================
     // Methods operating on Strings
@@ -154,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) {