| commit | b735a1d246336674d5c7c1bd213593ad9ae42113 | [log] [tgz] |
|---|---|---|
| author | Nico Huber <nico.huber@secunet.com> | Mon Feb 05 11:43:12 2024 +0100 |
| committer | Nico Huber <nico.huber@secunet.com> | Mon Feb 05 11:43:12 2024 +0100 |
| tree | 284c337f1ba2a3341f1109364dedb864107ba056 | |
| parent | 4210fccae3dc0d63de7da6105dfb9a8317d1a9fa [diff] [blame] |
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;