iso9660: Fix small bugs and proofs
diff --git a/src/filo-fs-iso9660.ads b/src/filo-fs-iso9660.ads
index 480ce39..20d2989 100644
--- a/src/filo-fs-iso9660.ads
+++ b/src/filo-fs-iso9660.ads
@@ -23,7 +23,7 @@
In_Root : in Boolean;
Success : out Boolean)
with
- Pre => Is_Mounted (State),
+ Pre => Is_Mounted (State) and File_Name'Length <= Natural'Last - 3,
Post => (if Success then Is_Open (State) else Is_Mounted (State));
procedure Close (State : in out T)
@@ -73,24 +73,28 @@
-- We'll use the absolute position of the dir record
subtype Inode_Index is FS_Record
with
- Dynamic_Predicate => Inode_Index.Offset <= Directory_Record_Offset'Last;
+ Dynamic_Predicate =>
+ Inode_Index.Size >= Directory_Record'Length;
type Inode_Length is range 0 .. FSBlock_Count'Last * FSBlock_Size;
type Mount_State is record
Part_Len : Partition_Length := 0;
- Root_Inode : Inode_Index := (others => <>);
+ Root_Inode : Inode_Index := (Size => Directory_Record'Length, others => <>);
end record;
type Extent is record
Start : FSBlock := 0;
Count : FSBlock_Count := 0;
- end record;
+ end record
+ with
+ Dynamic_Predicate =>
+ Start <= FSBlock_Count'Last - Count;
type Extent_Range is range 0 .. 0; -- Linux allows 100 "file sections"
type Extents is array (Extent_Range) of Extent;
type Inode_Info is record
- I : Inode_Index := (others => <>);
+ I : Inode_Index := (Size => Directory_Record'Length, others => <>);
Mode : File_Type := File_Type'First;
Size : Inode_Length := 0;
Extents : ISO9660.Extents := (Extent_Range => (others => <>));
@@ -100,7 +104,7 @@
Static : Mount_State := (others => <>);
S : State;
Inode : Inode_Info := (others => <>);
- Cur_Dir : Inode_Index := (others => <>);
+ Cur_Dir : Inode_Index := (Size => Directory_Record'Length, others => <>);
end record;
end FILO.FS.ISO9660;