VFS: Satisfy GNATprove and No_Secondary_Stack
diff --git a/default.adc b/default.adc
index c4a1e03..a1cf743 100644
--- a/default.adc
+++ b/default.adc
@@ -1 +1,2 @@
+pragma Restrictions (No_Secondary_Stack);
pragma SPARK_Mode (On);
diff --git a/src/filo-fs-ext2.adb b/src/filo-fs-ext2.adb
index 9cd9c7a..ccc8b31 100644
--- a/src/filo-fs-ext2.adb
+++ b/src/filo-fs-ext2.adb
@@ -11,7 +11,6 @@
with System;
with Interfaces;
with Interfaces.C;
-with Interfaces.C.Strings;
with FILO.Blockdev;
with FILO.FS.VFS;
@@ -947,12 +946,12 @@
return C.C_Mount;
end C_Mount;
- function C_Open (File_Path : Strings.chars_ptr) return int
+ function C_Open (File_Path : System.Address) return int
with
Export,
Convention => C,
External_Name => "ext2fs_dir";
- function C_Open (File_Path : Strings.chars_ptr) return int
+ function C_Open (File_Path : System.Address) return int
with
SPARK_Mode => Off
is
diff --git a/src/filo-fs-vfs.adb b/src/filo-fs-vfs.adb
index 388f2cb..a43edf6 100644
--- a/src/filo-fs-vfs.adb
+++ b/src/filo-fs-vfs.adb
@@ -1,26 +1,32 @@
with Ada.Unchecked_Conversion;
with Interfaces.C;
-with Interfaces.C.Strings;
use Interfaces.C;
-package body FILO.FS.VFS
-with
- SPARK_Mode => Off
-is
+package body FILO.FS.VFS is
State : T := Initial;
Path_Max : constant := 4096;
Max_Link_Depth : constant := 32;
- subtype Path_Buffer is Buffer_Type (1 .. Path_Max);
+ subtype Path_Length is Natural range 0 .. Path_Max;
+ subtype Path_Index_Plus is Positive range 1 .. Path_Max + 1;
+ subtype Path_Index is Path_Index_Plus range 1 .. Path_Max;
+
+ subtype Path_Buffer is Buffer_Type (Path_Index)
+ with
+ Object_Size => Path_Max * 8;
Path_Buf : Path_Buffer;
- subtype Path_String is String (1 .. Path_Max);
+ subtype Path_String is String (Path_Index)
+ with
+ Object_Size => Path_Max * 8;
Path : Path_String;
function C_Mount return int
+ with
+ SPARK_Mode => Off
is
Success : Boolean;
begin
@@ -31,9 +37,40 @@
return (if Success then 1 else 0);
end C_Mount;
- function C_Open (File_Path : Strings.chars_ptr) return int
+ procedure Open (File_Path : System.Address; Ret : out int)
is
- function Component_Start (Path : String; Pos : Positive) return Positive is
+ function Str_Len (S : System.Address) return Natural;
+ function Str_Len (S : System.Address) return Natural
+ with
+ SPARK_Mode => Off
+ is
+ Buf : Buffer_Type (1 .. Path_Max + 1)
+ with
+ Convention => C,
+ Address => S;
+ begin
+ for I in Buf'Range loop
+ if Buf (I) = 16#00# then
+ return I - 1;
+ end if;
+ end loop;
+ return Path_Max + 1;
+ end Str_Len;
+
+ procedure Str_Cpy (Dst : out String; Src : in System.Address);
+ procedure Str_Cpy (Dst : out String; Src : in System.Address)
+ with
+ SPARK_Mode => Off
+ is
+ Src_String : String (Dst'Range)
+ with
+ Convention => C,
+ Address => Src;
+ begin
+ Dst := Src_String;
+ end Str_Cpy;
+
+ function Component_Start (Path : Path_String; Pos : Positive) return Path_Index_Plus is
begin
for I in Pos .. Path'Last loop
if Path (I) /= '/' then
@@ -43,17 +80,20 @@
return Path'Last + 1;
end Component_Start;
- function Component_End (Path : String; Start : Positive) return Positive is
+ function Component_End (Path : Path_String; Start : Path_Index_Plus; Limit : Path_Index) return Path_Length
+ with
+ Post => Component_End'Result <= Limit
+ is
begin
- for I in Start .. Path'Last loop
+ for I in Start .. Limit loop
if Path (I) = '/' or Is_Space (Path (I)) then
return I - 1;
end if;
end loop;
- return Path'Last;
+ return Limit;
end Component_End;
- function Path_End (Path : String; Start : Positive) return Positive is
+ function Path_End (Path : Path_String; Start : Path_Index) return Path_Length is
begin
for I in Start .. Path'Last loop
if Is_Space (Path (I)) then
@@ -65,10 +105,16 @@
procedure Read_Link
(Path : in out Path_String;
- Rest_First : in Positive;
- Rest_Last : in Positive;
+ Rest_First : in Path_Index_Plus;
+ Rest_Last : in Path_Index;
Link_Len : in Natural;
Success : out Boolean)
+ with
+ Pre =>
+ Is_Open (State) and
+ Rest_First - 1 <= Rest_Last,
+ Post =>
+ Is_Open (State)
is
function As_String is new Ada.Unchecked_Conversion (Path_Buffer, Path_String);
@@ -95,33 +141,43 @@
end if;
end Read_Link;
- Path_Len : constant size_t := Strings.Strlen (File_Path);
+ Path_Len : constant Natural := Str_Len (File_Path);
Root_Dir : Boolean := True;
begin
+ Ret := 0;
+
if not Is_Mounted (State) or Path_Len > Path_Max then
- return 0;
+ return;
end if;
- Path (1 .. Natural (Path_Len)) := Strings.Value (File_Path);
- Path (Natural (Path_Len + 1) .. Path'Last) := (others => ' ');
+ Str_Cpy (Path (1 .. Path_Len), File_Path);
+ Path (Path_Len + 1 .. Path'Last) := (others => ' ');
Link_Loop :
for I in 1 .. Max_Link_Depth loop
+ pragma Loop_Invariant (Is_Mounted (State));
declare
- Path_Pos : Positive := Path'First;
- Path_Last : constant Positive := Path_End (Path, Path_Pos);
+ Path_Pos : Path_Index_Plus := Path'First;
+ Path_Last : constant Path_Length := Path_End (Path, Path_Pos);
begin
+ if Path_Last < Path'First then
+ return;
+ end if;
+
Path_Loop :
loop
+ pragma Loop_Invariant
+ (Is_Mounted (State) and
+ Path_Last in Path'Range);
declare
- Comp_First : constant Positive := Component_Start (Path, Path_Pos);
- Comp_Last : constant Positive := Component_End (Path, Comp_First);
+ Comp_First : constant Path_Index_Plus := Component_Start (Path, Path_Pos);
+ Comp_Last : constant Path_Length := Component_End (Path, Comp_First, Path_Last);
File_Type : FS.File_Type;
File_Len : File_Length;
Success : Boolean;
begin
if Comp_First > Comp_Last then
- return 0;
+ return;
end if;
Open
@@ -132,7 +188,7 @@
In_Root => Root_Dir,
Success => Success);
if not Success then
- return 0;
+ return;
end if;
Root_Dir := False;
@@ -140,16 +196,17 @@
when Dir =>
if Comp_Last = Path_Last then
Close (State);
- return 0;
+ return;
end if;
Path_Pos := Comp_Last + 1;
when Regular =>
if Comp_Last = Path_Last then
Set_File_Max (File_Len);
- return 1;
+ Ret := 1;
+ return;
else
Close (State);
- return 0;
+ return;
end if;
when Link =>
if File_Len > Path_Max then
@@ -164,7 +221,7 @@
end if;
Close (State);
if not Success then
- return 0;
+ return;
end if;
Root_Dir := Path (1) = '/';
exit Path_Loop; -- continue in Link_Loop
@@ -173,8 +230,20 @@
end loop Path_Loop;
end;
end loop Link_Loop;
+ end Open;
- return 0;
+ function C_Open (File_Path : System.Address) return int
+ with
+ SPARK_Mode => Off
+ is
+ Ret : int;
+ begin
+ if Is_Mounted (State) then
+ Open (File_Path, Ret);
+ else
+ Ret := 0;
+ end if;
+ return Ret;
end C_Open;
procedure C_Close is
@@ -185,6 +254,8 @@
end C_Close;
function C_Read (Buf : System.Address; Len : int) return int
+ with
+ SPARK_Mode => Off
is
subtype Buffer_Range is Natural range 0 .. Integer (Len) - 1;
Buffer : Buffer_Type (Buffer_Range)
diff --git a/src/filo-fs-vfs.ads b/src/filo-fs-vfs.ads
index 5ae086c..55c309a 100644
--- a/src/filo-fs-vfs.ads
+++ b/src/filo-fs-vfs.ads
@@ -59,7 +59,7 @@
function C_Mount return int;
- function C_Open (File_Path : Strings.chars_ptr) return int;
+ function C_Open (File_Path : System.Address) return int;
procedure C_Close;
function C_Read (Buf : System.Address; Len : int) return int;