nullness-specifying class Filenames

KeYProject · Jun 26, 2023 · 8637aa7 · 8637aa7
1 parent 08673f9
commit 8637aa7
Showing 1 changed file with 7 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
@@ -1,5 +1,8 @@
 package org.key_project.util;
 
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
+
 import java.io.File;
 import java.util.ArrayList;
 import java.util.Arrays;
@@ -9,7 +12,7 @@
  * @author Alexander Weigl
  * @version 1 (29.03.19)
  */
-@SuppressWarnings("nullness")
+@NullMarked
 public class Filenames {
     // =======================================================
     // Methods operating on Strings
@@ -154,7 +157,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) {