diff --git a/src/filo-fs-iso9660.adb b/src/filo-fs-iso9660.adb
index 8c1b441..03f1abb 100644
--- a/src/filo-fs-iso9660.adb
+++ b/src/filo-fs-iso9660.adb
@@ -22,7 +22,7 @@
    --------------------------------------------------------------------------
 
    procedure Read
-     (Buf      : in out Buffer_Type;
+     (Buf      :    out Buffer_Type;
       Block    : in     FSBlock;
       Offset   : in     FSBlock_Index;
       FS_Len   : in     Partition_Length;
@@ -35,6 +35,7 @@
       Max_Block_Offset : constant Integer_64 := Integer_64 (FS_Len) / FSBlock_Size - 1;
    begin
       if Block_64 > Max_Block_Offset then
+         Buf := (others => 16#00#);
          Success := False;
          return;
       end if;
@@ -59,18 +60,19 @@
 
       Static : Mount_State renames State.Static;
 
-      Volume_Descriptor : Buffer_Type (0 .. 190 - 1);
+      Volume_Descriptor : Buffer_Type (0 .. D_Ver);
       Block : FSBlock := 32;
    begin
       loop
          pragma Loop_Invariant (Block < 1024);
+         pragma Loop_Invariant (not Is_Mounted (State));
 
          if Part_Len < Partition_Length (Block + 1) * FSBlock_Size then
             Success := False;
             return;
          end if;
 
-         Read (Volume_Descriptor (0 .. D_Ver), Block, 0, Part_Len, Success);
+         Read (Volume_Descriptor, Block, 0, Part_Len, Success);
          if not Success then
             return;
          end if;
@@ -79,6 +81,7 @@
             Volume_Descriptor (D_Id .. D_Ver - 1) /= CD001 or
             Volume_Descriptor (D_Type) = D_Type_Terminator
          then
+            Success := False;
             return;
          end if;
 
@@ -86,6 +89,7 @@
 
          Block := Block + 1;
          if Block >= 1024 then
+            Success := False;
             return;
          end if;
       end loop;
@@ -109,6 +113,8 @@
 
       Dir_Rec : Directory_Record;
    begin
+      State.S := Mounted;
+
       Inode := (I, others => <>);
 
       Read (Dir_Rec, I.Block, I.Offset, Static.Part_Len, Success);
@@ -120,11 +126,17 @@
          D_Flag_Dir  : constant := 16#02#;
          D_Flag_Cont : constant := 16#80#;
          D_Flags : constant Unsigned_8 := Dir_Rec (25);
+         D_Extent : constant Unsigned_32 := Read_LE32 (Dir_Rec, 2);
       begin
+         if D_Extent > Unsigned_32 (FSBlock'Last) then
+            Success := False;
+            return;
+         end if;
          if (D_Flags and D_Flag_Cont) /= 0 then
             Success := False;
             return;
          end if;
+
          if (D_Flags and D_Flag_Dir) /= 0 then
             Inode.Mode := Dir;
          else
@@ -132,7 +144,7 @@
          end if;
          Inode.Size := Inode_Length (Read_LE32 (Dir_Rec, 10));
          Inode.Extents (0) :=
-           (Start => FSBlock (Read_LE32 (Dir_Rec, 2)),
+           (Start => FSBlock (D_Extent),
             Count => FSBlock_Count (Inode.Size / Inode_Length (FSBlock_Size)));
          State.S := File_Opened;
       end;
@@ -199,6 +211,9 @@
       Success := False;
       loop
          pragma Loop_Invariant (Is_Open (State) and not Success);
+         pragma Loop_Invariant
+           (FSBlock_Index (Dir_Pos mod FSBlock_Size) <= Directory_Record_Offset'Last);
+
          declare
             Dir_Rec : Directory_Record;
             Dir_Rec_Name : Buffer_Type (0 .. File_Name_Max - 1);
@@ -241,8 +256,10 @@
             end if;
 
             Dir_Rec_Length := File_Length (Dir_Rec (0));
-            if Dir_Rec_Length = 0 or
-               Dir_Pos > File_Length'Last - Dir_Rec_Length or
+            if Dir_Rec_Length = 0 or else
+               Dir_Pos > File_Length'Last - Dir_Rec_Length or else
+               (Dir_Pos + Dir_Rec_Length) mod FSBlock_Size
+                  > File_Length (Directory_Record_Offset'Last) or else
                Unsigned_64 (Dir_Pos) >= Unsigned_64 (State.Inode.Size) - Unsigned_64 (Dir_Rec_Length)
             then
                return;
@@ -261,7 +278,7 @@
          State.Cur_Dir := Found_Inode;
       end if;
 
-      --Success := State.Inode.Size <= Inode_Length (File_Length'Last);
+      Success := State.Inode.Size <= Inode_Length (File_Length'Last);
       if Success then
          File_Len := File_Length (State.Inode.Size);
          File_Type := State.Inode.Mode;
@@ -291,6 +308,7 @@
             File_Pos < File_Offset'Last and
             Inode_Length (File_Pos) < State.Inode.Size
       loop
+         pragma Loop_Invariant (for all I in Buf'First .. Pos - 1 => Buf (I)'Initialized);
          pragma Loop_Invariant (Is_Open (State));
          declare
             In_Block : constant FSBlock_Index := Natural (File_Pos mod FSBlock_Size);