ext2: Somewhat finish proofs
diff --git a/src/filo-fs-vfs.adb b/src/filo-fs-vfs.adb
index a43edf6..02e4c52 100644
--- a/src/filo-fs-vfs.adb
+++ b/src/filo-fs-vfs.adb
@@ -107,7 +107,7 @@
(Path : in out Path_String;
Rest_First : in Path_Index_Plus;
Rest_Last : in Path_Index;
- Link_Len : in Natural;
+ Link_Len : in Positive;
Success : out Boolean)
with
Pre =>
@@ -127,11 +127,15 @@
return;
end if;
+ pragma Warnings
+ (GNATprove, Off, """File_Pos"" is set*but not used",
+ Reason => "We only read the link at once, during path walks.");
Read
(State => State,
File_Pos => File_Pos,
Buf => Path_Buf (1 .. Link_Len),
Len => Read_Len);
+ pragma Warnings (GNATprove, On, """File_Pos"" is set*but not used");
Success := Read_Len = Link_Len;
if Success then
@@ -209,14 +213,14 @@
return;
end if;
when Link =>
- if File_Len > Path_Max then
+ if File_Len = 0 or File_Len > Path_Max then
Success := False;
else
Read_Link
(Path => Path,
Rest_First => Comp_Last + 1,
Rest_Last => Path_Last,
- Link_Len => Natural (File_Len),
+ Link_Len => Positive (File_Len),
Success => Success);
end if;
Close (State);