diff --git a/src/filo-fs-ext2.adb b/src/filo-fs-ext2.adb
index 5e34e51..47244bc 100644
--- a/src/filo-fs-ext2.adb
+++ b/src/filo-fs-ext2.adb
@@ -936,6 +936,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 Max_Block_Index := Natural (File_Pos) mod Static.Block_Size;
diff --git a/src/filo-fs-ext2.ads b/src/filo-fs-ext2.ads
index 96c3597..31a679e 100644
--- a/src/filo-fs-ext2.ads
+++ b/src/filo-fs-ext2.ads
@@ -37,8 +37,9 @@
       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;
 
 private
    type State is (Unmounted, Mounted, File_Opened);