FS: Add pre-conditions for deserialization functions
diff --git a/src/fs.ads b/src/fs.ads
index 2085490..600dc53 100644
--- a/src/fs.ads
+++ b/src/fs.ads
@@ -12,13 +12,17 @@
function Read_LE16 (Buf : Buffer_Type; Off : Index_Type16) return Unsigned_16
is
- (Shift_Left (Unsigned_16 (Buf (Off + 1)), 8) or Unsigned_16 (Buf (Off)));
+ (Shift_Left (Unsigned_16 (Buf (Off + 1)), 8) or Unsigned_16 (Buf (Off)))
+ with
+ Pre => Buf'First <= Off and Off + 1 <= Buf'Last;
function Read_LE32 (Buf : Buffer_Type; Off : Index_Type32) return Unsigned_32
is
(Shift_Left (Unsigned_32 (Buf (Off + 3)), 24) or
Shift_Left (Unsigned_32 (Buf (Off + 2)), 16) or
Shift_Left (Unsigned_32 (Buf (Off + 1)), 8) or
- Unsigned_32 (Buf (Off)));
+ Unsigned_32 (Buf (Off)))
+ with
+ Pre => Buf'First <= Off and Off + 3 <= Buf'Last;
end FS;