diff --git a/src/filo-fs-iso9660.adb b/src/filo-fs-iso9660.adb
index c542ee0..a4af392 100644
--- a/src/filo-fs-iso9660.adb
+++ b/src/filo-fs-iso9660.adb
@@ -109,7 +109,9 @@
       Dir_Rec_Len    : in     FSBlock_Length;
       Searched_Sig   : in     SUSP_Signature)
    with
-      Pre => FSBlock_Index (Dir_Rec_Pos mod FSBlock_Size) <= FSBlock_Size - Dir_Rec_Len
+      Pre =>
+         Dir_Rec_Pos mod FSBlock_Size <= File_Offset (FSBlock_Size - Dir_Rec_Len) and
+         FSBlock_Count (Dir_Rec_Pos / FSBlock_Size) < State.Inode.Extents (0).Count
    is
       subtype Signature_Buf is Buffer_Type (0 .. 1);
       function Signature (Str : SUSP_Signature) return Signature_Buf
@@ -121,7 +123,7 @@
          Offset => FSBlock_Index (Dir_Rec_Pos mod FSBlock_Size),
          Size   => Dir_Rec_Len);
 
-      Continuation : FS_Record := (others => <>);
+      Continuation : FS_Record := (Size => 0, others => <>);
 
       SUSP_Head : Buffer_Type (0 .. 3);
 
@@ -138,7 +140,7 @@
 
       for I in 1 .. 2**16 loop -- arbitrary limit to avoid endless loop
          if Cur.Size < SUSP_Head'Length then
-            if Continuation.Size = 0 then
+            if Continuation.Size < SUSP_Head'Length then
                return;
             else
                Cur := Continuation;
@@ -175,14 +177,15 @@
                   CE_Offset : constant Unsigned_32 := Read_LE32 (SUSP_CE, 12);
                   CE_Size   : constant Unsigned_32 := Read_LE32 (SUSP_CE, 20);
                begin
-                  if (CE_Offset > FSBlock_Size or CE_Size > FSBlock_Size) or else
-                     CE_Offset > FSBlock_Size - CE_Size
+                  if CE_Extent > Unsigned_32 (FSBlock'Last) or else
+                     (CE_Offset > FSBlock_Size or CE_Size > FSBlock_Size) or else
+                     FSBlock_Length (CE_Size) > FSBlock_Size - FSBlock_Length (CE_Offset)
                   then
                      return;
                   end if;
                   Continuation :=
                     (Block  => FSBlock (CE_Extent),
-                     Offset => FSBlock_Index (CE_Offset),
+                     Offset => FSBlock_Length (CE_Offset),
                      Size   => FSBlock_Length (CE_Size));
                end;
             end if;
@@ -233,10 +236,17 @@
          else
             Inode.Mode := Regular;
          end if;
+
          Inode.Size := Inode_Length (Read_LE32 (Dir_Rec, 10));
+         if FSBlock (D_Extent) > FSBlock_Count'Last - FSBlock_Count (Inode.Size / FSBlock_Size)
+         then
+            Success := False;
+            return;
+         end if;
+
          Inode.Extents (0) :=
            (Start => FSBlock (D_Extent),
-            Count => FSBlock_Count (Inode.Size / Inode_Length (FSBlock_Size)));
+            Count => FSBlock_Count (Inode.Size / FSBlock_Size));
          State.S := File_Opened;
       end;
    end Open;
@@ -252,11 +262,12 @@
       File_Name_Max : constant := 255;
 
       procedure Match_ISO_Name
-        (ISO_Name_Length   : in     Natural;
+        (ISO_Name_Length   : in     Positive;
          Record_Dir_Pos    : in     File_Offset;
          Success           : in out Boolean)
       with
-         Post => State.Static = State.Static'Old
+         Pre => Is_Open (State) and File_Name'Length <= Natural'Last - 3,
+         Post => Is_Open (State)
       is
          function Upper_Case_Equal (Str : String; Buf : Buffer_Type) return Boolean
          with
@@ -304,23 +315,23 @@
          end if;
          pragma Warnings (GNATprove, On, """Dir_Pos"" is set*but not used");
 
-         if (Name_Len = 1 and ISO_Name (0) = 16#00# and File_Name = ".") or
-            (Name_Len = 1 and ISO_Name (0) = 16#01# and File_Name = "..")
+         if (Name_Len = 1 and then (ISO_Name (0) = 16#00# and File_Name = ".")) or
+            (Name_Len = 1 and then (ISO_Name (0) = 16#01# and File_Name = ".."))
          then
             Success := True;
             return;
          end if;
 
          -- Ignore file version `;1'
-         if Name_Len >= File_Name'Length + 2 and
-            ISO_Name (Name_Len - 2) = Character'Pos (';') and
-            ISO_Name (Name_Len - 1) = Character'Pos ('1')
+         if Name_Len >= File_Name'Length + 2 and then
+            (ISO_Name (Name_Len - 2) = Character'Pos (';') and
+             ISO_Name (Name_Len - 1) = Character'Pos ('1'))
          then
             Name_Len := Name_Len - 2;
          end if;
 
          -- Ignore trailing `.'
-         if Name_Len >= File_Name'Length + 1 and
+         if Name_Len >= File_Name'Length + 1 and then
             ISO_Name (Name_Len - 1) = Character'Pos ('.')
          then
             Name_Len := Name_Len - 1;
@@ -332,15 +343,18 @@
 
       procedure Match_Rock_Ridge_Name
         (Pos      : in     File_Offset;
-         Len      : in     Natural;
-         Success  : in out Boolean)
+         Len      : in     FSBlock_Length;
+         Success  :    out Boolean)
       with
+         Pre =>
+            Pos mod FSBlock_Size <= File_Offset (FSBlock_Size - Len) and
+            FSBlock_Count (Pos / FSBlock_Size) < State.Inode.Extents (0).Count,
          Post => State = State'Old
       is
          Name_Rec : FS_Record;
       begin
          Find_SUSP_Record (State, Name_Rec, Pos, Len, "NM");
-         if Name_Rec.Size /= File_Name'Length + 5 then
+         if Name_Rec.Size - 5 /= File_Name'Length then
             Success := False;
             return;
          end if;
@@ -415,7 +429,7 @@
                if Dir_Rec_Length /= 0 then
 
                   if Unsigned_64 (Dir_Pos) > Unsigned_64 (State.Inode.Size) - Unsigned_64 (Dir_Rec_Length) or
-                     Dir_Rec_Name_Length > Dir_Rec_Length - Dir_Rec_Head'Length
+                     Dir_Rec_Name_Length not in 1 .. Dir_Rec_Length - Dir_Rec_Head'Length
                   then
                      return;
                   end if;
diff --git a/src/filo-fs-iso9660.ads b/src/filo-fs-iso9660.ads
index 480ce39..20d2989 100644
--- a/src/filo-fs-iso9660.ads
+++ b/src/filo-fs-iso9660.ads
@@ -23,7 +23,7 @@
       In_Root     : in     Boolean;
       Success     : out    Boolean)
    with
-      Pre => Is_Mounted (State),
+      Pre => Is_Mounted (State) and File_Name'Length <= Natural'Last - 3,
       Post => (if Success then Is_Open (State) else Is_Mounted (State));
 
    procedure Close (State : in out T)
@@ -73,24 +73,28 @@
    -- We'll use the absolute position of the dir record
    subtype Inode_Index is FS_Record
    with
-      Dynamic_Predicate => Inode_Index.Offset <= Directory_Record_Offset'Last;
+      Dynamic_Predicate =>
+         Inode_Index.Size >= Directory_Record'Length;
    type Inode_Length is range 0 .. FSBlock_Count'Last * FSBlock_Size;
 
    type Mount_State is record
       Part_Len    : Partition_Length := 0;
-      Root_Inode  : Inode_Index := (others => <>);
+      Root_Inode  : Inode_Index := (Size => Directory_Record'Length, others => <>);
    end record;
 
    type Extent is record
       Start : FSBlock := 0;
       Count : FSBlock_Count := 0;
-   end record;
+   end record
+   with
+      Dynamic_Predicate =>
+         Start <= FSBlock_Count'Last - Count;
 
    type Extent_Range is range 0 .. 0; -- Linux allows 100 "file sections"
    type Extents is array (Extent_Range) of Extent;
 
    type Inode_Info is record
-      I        : Inode_Index := (others => <>);
+      I        : Inode_Index := (Size => Directory_Record'Length, others => <>);
       Mode     : File_Type := File_Type'First;
       Size     : Inode_Length := 0;
       Extents  : ISO9660.Extents := (Extent_Range => (others => <>));
@@ -100,7 +104,7 @@
       Static   : Mount_State  := (others => <>);
       S        : State;
       Inode    : Inode_Info := (others => <>);
-      Cur_Dir  : Inode_Index := (others => <>);
+      Cur_Dir  : Inode_Index := (Size => Directory_Record'Length, others => <>);
    end record;
 
 end FILO.FS.ISO9660;