diff --git a/src/filo-fs-ext2.adb b/src/filo-fs-ext2.adb
index d7bd018..3276cdd 100644
--- a/src/filo-fs-ext2.adb
+++ b/src/filo-fs-ext2.adb
@@ -691,7 +691,7 @@
       Inode    : in     Inode_Index;
       Success  : out Boolean)
    with
-      Pre => Is_Mounted (State) and not Is_Open (State),
+      Pre => Is_Mounted (State),
       Post => Success = Is_Open (State)
    is
       Static : Mount_State renames State.Static;
@@ -706,6 +706,8 @@
       Cache_Start, Cache_End : Max_Block_Index;
       First_Table_Block : FSBlock_Offset;
    begin
+      State.S := Mounted;
+
       Cache_FSBlock
         (Static      => Static,
          Cache       => State.Cache,
@@ -788,7 +790,10 @@
       File_Name_Max : constant := 255;
       Root_Inode : constant := 2;
 
-      function Str_Buf_Equal (Str : String; Buf : Buffer_Type) return Boolean is
+      function Str_Buf_Equal (Str : String; Buf : Buffer_Type) return Boolean
+      with
+         Pre => Str'Length <= Buf'Length
+      is
       begin
          for I in Str'Range loop
             if Character'Pos (Str (I)) /= Buf (Buf'First + (I - Str'First)) then
@@ -830,58 +835,72 @@
       --
       File_Pos := 0;
       Success := False;
-      while Unsigned_64 (File_Pos) < Unsigned_64 (State.Inode.Size) loop
+      loop
+         pragma Loop_Invariant (Is_Open (State) and not Success);
          declare
             Dir_Entry_Header_Length : constant := 4 + 2 + 1 + 1;
-            subtype Dir_Entry_Index is Natural
-               range 0 .. Dir_Entry_Header_Length + File_Name_Max - 1;
-            Dir_Entry : Buffer_Type (Dir_Entry_Index);
+            Dir_Entry_Header : Buffer_Type (0 .. Dir_Entry_Header_Length - 1);
+            Dir_Entry_Name : Buffer_Type (0 .. File_Name_Max - 1);
             Entry_File_Pos : File_Offset := File_Pos;
+            Dir_Entry_Length : File_Length;
+            Inode : Inode_0_Index;
             Len : Natural;
          begin
             Read
               (State    => State,
                File_Pos => Entry_File_Pos,
-               Buf      => Dir_Entry (0 .. 7),
+               Buf      => Dir_Entry_Header,
                Len      => Len);
             if Len < Dir_Entry_Header_Length then
                return;
             end if;
 
             -- Only check filenames of exact same length
-            if Read_LE32 (Dir_Entry, 0) > Root_Inode and then
-               File_Name'Length = Natural (Dir_Entry (6))
+            Inode := Inode_0_Index (Read_LE32 (Dir_Entry_Header, 0));
+            if Inode > Root_Inode and then
+               File_Name'Length = Natural (Dir_Entry_Header (6))
             then
+               pragma Warnings
+                 (GNATprove, Off, """Entry_File_Pos"" is set*but not used",
+                  Reason => "We only care about intermedidate values.");
                Read
                  (State    => State,
                   File_Pos => Entry_File_Pos,
-                  Buf      => Dir_Entry (8 .. 8 + File_Name'Length - 1),
+                  Buf      => Dir_Entry_Name,
                   Len      => Len);
+               pragma Warnings (GNATprove, On, """Entry_File_Pos"" is set*but not used");
                if Len < File_Name'Length then
                   return;
                end if;
 
-               File_Inode := Inode_Index (Read_LE32 (Dir_Entry, 0));
-               Success := Str_Buf_Equal (File_Name, Dir_Entry (8 .. 8 + File_Name'Length - 1));
-               exit when Success;
+               Success := Str_Buf_Equal (File_Name, Dir_Entry_Name);
+               if Success then
+                  File_Inode := Inode;
+                  exit;
+               end if;
             end if;
 
-            File_Pos := File_Pos + File_Length (Read_LE16 (Dir_Entry, 4));
+            Dir_Entry_Length := File_Length (Read_LE16 (Dir_Entry_Header, 4));
+            if File_Pos > File_Length'Last - Dir_Entry_Length or
+               Unsigned_64 (File_Pos) >= Unsigned_64 (State.Inode.Size) - Unsigned_64 (Dir_Entry_Length)
+            then
+               return;
+            end if;
+            File_Pos := File_Pos + Dir_Entry_Length;
          end;
       end loop;
+      pragma Assert_And_Cut (Success and Is_Mounted (State));
 
-      if Success then
-         Open (State, File_Inode, Success);
-         if not Success then
-            return;
-         end if;
-
-         if State.Inode.Mode = Dir then
-            State.Cur_Dir := File_Inode;
-         end if;
+      Open (State, File_Inode, Success);
+      if not Success then
+         return;
       end if;
 
-      Success := Unsigned_64 (State.Inode.Size) <= Unsigned_64 (File_Length'Last);
+      if State.Inode.Mode = Dir then
+         State.Cur_Dir := File_Inode;
+      end if;
+
+      Success := State.Inode.Size <= Inode_Length (File_Length'Last);
       if Success then
          File_Len := File_Length (State.Inode.Size);
          File_Type := (case State.Inode.Mode is