diff --git a/src/filo-fs-ext2.adb b/src/filo-fs-ext2.adb
index 3dbbb2b..3cdeca5 100644
--- a/src/filo-fs-ext2.adb
+++ b/src/filo-fs-ext2.adb
@@ -433,12 +433,15 @@
 
       function Bin_Search (Buf : Buffer_Type; Refs : Extent_Idx) return Extent_Idx
       with
-         Pre => Refs in 1 .. Extent_Idx (Buf'Length / Extent_Header_Size - 1) and
-                  Extent_Logical (Buf, 1) <= Logical,
-         Post => Bin_Search'Result in 1 .. Refs and
-                  Extent_Logical (Buf, Bin_Search'Result) <= Logical
+         Pre =>
+            Buf'Length in 2 * Extent_Header_Size .. Max_Block_Index'Last and then
+            Refs in 1 .. Extent_Idx (Buf'Length / Extent_Header_Size - 1) and then
+            Extent_Logical (Buf, 1) <= Logical,
+         Post =>
+            Bin_Search'Result in 1 .. Refs and
+            Extent_Logical (Buf, Bin_Search'Result) <= Logical
       is
-         Left : Extent_Idx := 1;
+         Left : Positive := 2;
          Right : Extent_Idx := Refs;
       begin
          while Left <= Right loop
@@ -451,6 +454,10 @@
                else
                   Left := Mid + 1;
                end if;
+               pragma Loop_Invariant
+                 (Right <= Refs and then
+                  Left in 2 .. Refs + 1 and then
+                  Extent_Logical (Buf, Left - 1) <= Logical);
             end;
          end loop;
          return Left - 1;