diff --git a/src/filo-fs-iso9660.ads b/src/filo-fs-iso9660.ads
index dd82d74..0a28cc2 100644
--- a/src/filo-fs-iso9660.ads
+++ b/src/filo-fs-iso9660.ads
@@ -31,14 +31,19 @@
       Pre => Is_Open (State),
       Post => Is_Mounted (State);
 
+   pragma Warnings
+     (GNATprove, Off, """State"" is not modified*",
+      Reason => "It's `in out' to fulfill common interface.");
    procedure Read
      (State    : in out T;
       File_Pos : in out File_Offset;
       Buf      :    out Buffer_Type;
       Len      :    out Natural)
    with
+      Relaxed_Initialization => Buf,
       Pre => Is_Open (State) and Buf'Length > 0,
-      Post => Is_Open (State);
+      Post => Is_Open (State) and Buf'Initialized;
+   pragma Warnings (GNATprove, On, """State"" is not modified*");
 
 private
    type State is (Unmounted, Mounted, File_Opened);
@@ -52,11 +57,13 @@
 
    subtype Directory_Record_Range is Index_Type range 0 .. 32;
    subtype Directory_Record is Buffer_Type (Directory_Record_Range);
+   subtype Directory_Record_Offset is FSBlock_Index
+      range 0 .. FSBlock_Size - Directory_Record'Length;
 
    -- We'll use the absolute position of the dir record
    type Inode_Index is record
       Block : FSBlock := 0;
-      Offset : FSBlock_Index := 0;
+      Offset : Directory_Record_Offset := 0;
    end record;
    type Inode_Length is range 0 .. FSBlock_Count'Last * FSBlock_Size;