| 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.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);