ext2: Relax initialization in Read()
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);