isofs: Assist proofs
diff --git a/src/filo-fs-iso9660.ads b/src/filo-fs-iso9660.ads
index dd82d74..0a28cc2 100644
--- a/src/filo-fs-iso9660.ads
+++ b/src/filo-fs-iso9660.ads
@@ -31,14 +31,19 @@
Pre => Is_Open (State),
Post => Is_Mounted (State);
+ pragma Warnings
+ (GNATprove, Off, """State"" is not modified*",
+ Reason => "It's `in out' to fulfill common interface.");
procedure Read
(State : in out T;
File_Pos : in out File_Offset;
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;
+ pragma Warnings (GNATprove, On, """State"" is not modified*");
private
type State is (Unmounted, Mounted, File_Opened);
@@ -52,11 +57,13 @@
subtype Directory_Record_Range is Index_Type range 0 .. 32;
subtype Directory_Record is Buffer_Type (Directory_Record_Range);
+ subtype Directory_Record_Offset is FSBlock_Index
+ range 0 .. FSBlock_Size - Directory_Record'Length;
-- We'll use the absolute position of the dir record
type Inode_Index is record
Block : FSBlock := 0;
- Offset : FSBlock_Index := 0;
+ Offset : Directory_Record_Offset := 0;
end record;
type Inode_Length is range 0 .. FSBlock_Count'Last * FSBlock_Size;