diff --git a/src/filo-fs-vfs.adb b/src/filo-fs-vfs.adb
index a43edf6..02e4c52 100644
--- a/src/filo-fs-vfs.adb
+++ b/src/filo-fs-vfs.adb
@@ -107,7 +107,7 @@
         (Path        : in out Path_String;
          Rest_First  : in     Path_Index_Plus;
          Rest_Last   : in     Path_Index;
-         Link_Len    : in     Natural;
+         Link_Len    : in     Positive;
          Success     :    out Boolean)
       with
          Pre =>
@@ -127,11 +127,15 @@
             return;
          end if;
 
+         pragma Warnings
+           (GNATprove, Off, """File_Pos"" is set*but not used",
+            Reason => "We only read the link at once, during path walks.");
          Read
            (State    => State,
             File_Pos => File_Pos,
             Buf      => Path_Buf (1 .. Link_Len),
             Len      => Read_Len);
+         pragma Warnings (GNATprove, On, """File_Pos"" is set*but not used");
          Success := Read_Len = Link_Len;
 
          if Success then
@@ -209,14 +213,14 @@
                            return;
                         end if;
                      when Link =>
-                        if File_Len > Path_Max then
+                        if File_Len = 0 or File_Len > Path_Max then
                            Success := False;
                         else
                            Read_Link
                              (Path        => Path,
                               Rest_First  => Comp_Last + 1,
                               Rest_Last   => Path_Last,
-                              Link_Len    => Natural (File_Len),
+                              Link_Len    => Positive (File_Len),
                               Success     => Success);
                         end if;
                         Close (State);