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;