From 1f66c1e4cae616787bd70f84df2bf05fe3451e19 Mon Sep 17 00:00:00 2001 From: Johannes Kliemann Date: Tue, 7 Apr 2020 18:34:03 +0200 Subject: [PATCH] prove broker with only low checks missing ref #161 --- init/gneiss-broker-lookup.adb | 4 + init/gneiss-broker-lookup.ads | 7 ++ init/gneiss-broker-main.adb | 9 +- init/gneiss-broker-main.ads | 3 +- init/gneiss-broker-message.adb | 135 ++++++++++++++++--------- init/gneiss-broker-message.ads | 84 ++++++++++++--- init/gneiss-broker-startup.adb | 4 + init/gneiss-broker-startup.ads | 16 +-- init/gneiss-command_line.adb | 5 +- init/gneiss-config.adb | 9 +- src/platform/linux/gneiss_internal.ads | 3 +- 11 files changed, 199 insertions(+), 80 deletions(-) diff --git a/init/gneiss-broker-lookup.adb b/init/gneiss-broker-lookup.adb index bd30c13..2b2c3c4 100644 --- a/init/gneiss-broker-lookup.adb +++ b/init/gneiss-broker-lookup.adb @@ -19,6 +19,9 @@ is pragma Loop_Invariant (SXML.Query.Is_Valid (Query_State, Document)); pragma Loop_Invariant (SXML.Query.Is_Open (Query_State, Document) or else SXML.Query.Is_Content (Query_State, Document)); + pragma Loop_Invariant (Default_State = SXML.Query.Invalid_State + or else (SXML.Query.State_Result (Default_State) = SXML.Result_OK + and then SXML.Query.Is_Valid (Default_State, Document))); Query_State := SXML.Query.Find_Sibling (Query_State, Document, "service", "name", Kind); exit when SXML.Query.State_Result (Query_State) /= SXML.Result_OK; SXML.Query.Attribute (Query_State, Document, "label", Result, Buffer, Last); @@ -50,6 +53,7 @@ is return; end if; for I in State.Components'Range loop + pragma Loop_Invariant (not Valid); if State.Components (I).Fd > -1 then SXML.Query.Attribute (State.Components (I).Node, State.Xml, "name", Result, XML_Buf, Last); Valid := Result = SXML.Result_OK and then Compare (XML_Buf, Last, Name); diff --git a/init/gneiss-broker-lookup.ads b/init/gneiss-broker-lookup.ads index 90f3a27..0a42beb 100644 --- a/init/gneiss-broker-lookup.ads +++ b/init/gneiss-broker-lookup.ads @@ -6,6 +6,7 @@ with Gneiss_Protocol.Session; package Gneiss.Broker.Lookup with SPARK_Mode is + use type SXML.Query.State_Type; procedure Match_Service (Document : SXML.Document_Type; Comp : SXML.Query.State_Type; @@ -14,6 +15,9 @@ is Dest : out SXML.Query.State_Type) with Pre => SXML.Query.Is_Valid (Comp, Document) and then SXML.Query.State_Result (Comp) = SXML.Result_OK, + Post => Dest = SXML.Query.Invalid_State + or else (SXML.Query.State_Result (Dest) = SXML.Result_OK + and then SXML.Query.Is_Valid (Dest, Document)), Global => null; procedure Lookup_Request (State : Broker_State; @@ -32,6 +36,8 @@ is Index : out Positive; Valid : out Boolean) with Pre => Is_Valid (State.Xml, State.Components), + Post => (if Valid then (Index in State.Components'Range + and then State.Components (Index).Fd > -1)), Global => null; procedure Find_Resource_By_Name (State : Broker_State; @@ -52,6 +58,7 @@ is and then SXML.Query.Is_Open (Serv, State.Xml) and then Location'Length > 0 and then Location'Last <= Natural'Last - SXML.Chunk_Length, + Post => (if Valid then Last in Location'Range), Global => null; private diff --git a/init/gneiss-broker-main.adb b/init/gneiss-broker-main.adb index d219683..250c121 100644 --- a/init/gneiss-broker-main.adb +++ b/init/gneiss-broker-main.adb @@ -55,6 +55,8 @@ is Status := 1; return; end if; + State.Resources := (others => (Fd => -1, + Node => SXML.Query.Invalid_State)); Startup.Parse_Resources (State.Resources, State.Xml, Query); State.Components := (others => (Fd => -1, Node => SXML.Query.Initial_State, @@ -80,12 +82,13 @@ is Status := 1; loop pragma Loop_Invariant (Is_Valid (B_State.Xml, B_State.Components)); + pragma Loop_Invariant (Is_Valid (B_State.Xml, B_State.Resources)); pragma Loop_Invariant (Gneiss_Epoll.Valid_Fd (B_State.Epoll_Fd)); Gneiss_Epoll.Wait (B_State.Epoll_Fd, Ev, Fd); Index := Get_Dest (B_State, Fd); if Index in B_State.Components'Range and then B_State.Components (Index).Fd > -1 then SXML.Query.Attribute (B_State.Components (Index).Node, B_State.Xml, "name", Result, XML_Buf, Last); - if Ev.Epoll_In then + if Ev.Epoll_In and then Fd > -1 then Message.Read_Message (B_State, Index, Fd); end if; if Ev.Epoll_Hup or else Ev.Epoll_Rdhup then @@ -101,7 +104,9 @@ is & " exited with status " & Basalt.Strings.Image (Success)); end if; - Gneiss_Epoll.Remove (B_State.Epoll_Fd, B_State.Components (Index).Fd, Success); + if B_State.Components (Index).Fd > -1 then + Gneiss_Epoll.Remove (B_State.Epoll_Fd, B_State.Components (Index).Fd, Success); + end if; Gneiss_Syscall.Close (B_State.Components (Index).Fd); B_State.Components (Index).Node := SXML.Query.Init (B_State.Xml); B_State.Components (Index).Pid := -1; diff --git a/init/gneiss-broker-main.ads b/init/gneiss-broker-main.ads index 800996d..da5f02e 100644 --- a/init/gneiss-broker-main.ads +++ b/init/gneiss-broker-main.ads @@ -15,6 +15,7 @@ private procedure Event_Loop (B_State : in out Broker_State; Status : out Return_Code) with Pre => Gneiss_Epoll.Valid_Fd (B_State.Epoll_Fd) - and then Is_Valid (B_State.Xml, B_State.Components); + and then Is_Valid (B_State.Xml, B_State.Components) + and then Is_Valid (B_State.Xml, B_State.Resources); end Gneiss.Broker.Main; diff --git a/init/gneiss-broker-message.adb b/init/gneiss-broker-message.adb index ef0059c..30523fc 100644 --- a/init/gneiss-broker-message.adb +++ b/init/gneiss-broker-message.adb @@ -16,41 +16,45 @@ is when Gneiss_Protocol.Session.Rom => "Rom", when Gneiss_Protocol.Session.Timer => "Timer"); - procedure Setup_Service (State : in out Broker_State; + procedure Setup_Service (State : in out Service_List; Kind : Gneiss_Protocol.Session.Kind_Type; - Index : Positive); + Efd : Gneiss_Epoll.Epoll_Fd; + Valid : out Boolean) with + Pre => Gneiss_Epoll.Valid_Fd (Efd), + Post => (if Valid then (State (Kind).Broker > -1 and then State (Kind).Disp > -1)); - procedure Setup_Service (State : in out Broker_State; + procedure Setup_Service (State : in out Service_List; Kind : Gneiss_Protocol.Session.Kind_Type; - Index : Positive) + Efd : Gneiss_Epoll.Epoll_Fd; + Valid : out Boolean) is - Ignore_Success : Integer; + Success : Integer; begin - if - State.Components (Index).Serv (Kind).Broker > -1 - and then State.Components (Index).Serv (Kind).Disp > -1 - then + Valid := False; + if State (Kind).Broker > -1 and then State (Kind).Disp > -1 then + Valid := True; return; end if; - Gneiss_Syscall.Socketpair (State.Components (Index).Serv (Kind).Broker, - State.Components (Index).Serv (Kind).Disp); - if - State.Components (Index).Serv (Kind).Broker < 0 - or else State.Components (Index).Serv (Kind).Disp < 0 - then + Gneiss_Syscall.Socketpair (State (Kind).Broker, State (Kind).Disp); + if State (Kind).Broker < 0 or else State (Kind).Disp < 0 then Gneiss_Log.Error ("Failed to create service fds"); - Gneiss_Syscall.Close (State.Components (Index).Serv (Kind).Broker); - Gneiss_Syscall.Close (State.Components (Index).Serv (Kind).Disp); + Gneiss_Syscall.Close (State (Kind).Broker); + Gneiss_Syscall.Close (State (Kind).Disp); + return; + end if; + Gneiss_Epoll.Add (Efd, State (Kind).Broker, State (Kind).Broker, Success); + if Success /= 0 then + Gneiss_Log.Error ("Failed to register broker callback"); + Gneiss_Syscall.Close (State (Kind).Broker); + Gneiss_Syscall.Close (State (Kind).Disp); return; end if; - Gneiss_Epoll.Add (State.Epoll_Fd, State.Components (Index).Serv (Kind).Broker, - State.Components (Index).Serv (Kind).Broker, Ignore_Success); + Valid := True; end Setup_Service; function Convert_Message (S : String) return Gneiss_Protocol_String is - use type Gneiss_Protocol.Session.Length_Type; - R : Gneiss_Protocol_String (1 .. Gneiss_Protocol.Session.Length_Type (S'Length)); + R : Gneiss_Protocol_String (1 .. RFLX.Session.Length_Type (S'Length)); begin for I in R'Range loop R (I) := S (S'First + Natural (I - R'First)); @@ -129,14 +133,14 @@ is Source_Name : String (1 .. 255); Last : Natural; Result : SXML.Result_Type; - Fds_Out : Gneiss_Syscall.Fd_Array (1 .. 4) := (others => -1); + Fds_Out : Gneiss_Syscall.Fd_Array (1 .. 4); begin if State.Components (Source).Fd < 0 then Gneiss_Log.Warning ("Cannot process invalid source"); return; end if; Lookup.Match_Service (State.Xml, State.Components (Source).Node, Image (Kind), Label, Serv_State); - if Serv_State = SXML.Query.Invalid_State then + if Serv_State = SXML.Query.Invalid_State or else not SXML.Query.Is_Open (Serv_State, State.Xml) then Gneiss_Log.Error ("No service found"); Send_Reject (State.Components (Source).Fd, Kind, Label); return; @@ -155,17 +159,28 @@ is end if; case Kind is when Gneiss_Protocol.Session.Message | Gneiss_Protocol.Session.Log => + if Destination not in State.Components'Range then + Send_Reject (State.Components (Source).Fd, Kind, Label); + return; + end if; Process_Message_Request (Fds_Out, Valid); - if Valid and then Destination in State.Components'Range then - Setup_Service (State, Kind, Destination); - Send_Request (State.Components (Destination).Serv (Kind).Broker, - Kind, - Source_Name (Source_Name'First .. Last), - Label, - Fds_Out (Fds_Out'First .. Fds_Out'First + 1)); - else + if not Valid then Send_Reject (State.Components (Source).Fd, Kind, Label); + return; + end if; + Setup_Service (State.Components (Destination).Serv, Kind, State.Epoll_Fd, Valid); + if not Valid then + for Fd of Fds_Out loop + Gneiss_Syscall.Close (Fd); + end loop; + Send_Reject (State.Components (Source).Fd, Kind, Label); + return; end if; + Send_Request (State.Components (Destination).Serv (Kind).Broker, + Kind, + Source_Name (Source_Name'First .. Last), + Label, + Fds_Out (Fds_Out'First .. Fds_Out'First + 1)); when Gneiss_Protocol.Session.Rom => if Destination in State.Components'Range then Gneiss_Log.Warning ("Rom server currently not supported"); @@ -178,17 +193,28 @@ is end if; end if; when Gneiss_Protocol.Session.Memory => + if Destination not in State.Components'Range or else Fds'Length < 1 then + Send_Reject (State.Components (Source).Fd, Kind, Label); + return; + end if; Process_Memory_Request (Fds, Fds_Out, Valid); - if Valid and then Destination in State.Components'Range then - Setup_Service (State, Kind, Destination); - Send_Request (State.Components (Destination).Serv (Kind).Broker, - Kind, - Source_Name (Source_Name'First .. Last), - Label, - Fds_Out (Fds_Out'First .. Fds_Out'First + 2)); - else + if not Valid then + Send_Reject (State.Components (Source).Fd, Kind, Label); + return; + end if; + Setup_Service (State.Components (Destination).Serv, Kind, State.Epoll_Fd, Valid); + if not Valid then + for Fd of Fds_Out loop + Gneiss_Syscall.Close (Fd); + end loop; Send_Reject (State.Components (Source).Fd, Kind, Label); + return; end if; + Send_Request (State.Components (Destination).Serv (Kind).Broker, + Kind, + Source_Name (Source_Name'First .. Last), + Label, + Fds_Out (Fds_Out'First .. Fds_Out'First + 2)); when Gneiss_Protocol.Session.Timer => Process_Timer_Request (Fds_Out, Valid); if Valid then @@ -202,14 +228,17 @@ is procedure Process_Message_Request (Fds : out Gneiss_Syscall.Fd_Array; Valid : out Boolean) is + Fd1 : Integer; + Fd2 : Integer; begin Fds := (others => -1); - Gneiss_Syscall.Socketpair (Fds (Fds'First), Fds (Fds'First + 1)); - Valid := Fds (Fds'First) > -1 and then Fds (Fds'First + 1) > -1; + Gneiss_Syscall.Socketpair (Fd1, Fd2); + Valid := Fd1 > -1 and then Fd2 > -1; if not Valid then - Gneiss_Syscall.Close (Fds (Fds'First)); - Gneiss_Syscall.Close (Fds (Fds'First + 1)); + Gneiss_Syscall.Close (Fd1); + Gneiss_Syscall.Close (Fd2); end if; + Fds (Fds'First .. Fds'First + 1) := (Fd1, Fd2); end Process_Message_Request; procedure Process_Memory_Request (Fds_In : Gneiss_Syscall.Fd_Array; @@ -217,6 +246,8 @@ is Valid : out Boolean) is Success : Integer; + Fd1 : Integer; + Fd2 : Integer; begin Valid := False; Fds_Out := (others => -1); @@ -229,7 +260,8 @@ is Gneiss_Syscall.Close (Fds_Out (Fds_Out'First + 2)); return; end if; - Gneiss_Syscall.Socketpair (Fds_Out (Fds_Out'First), Fds_Out (Fds_Out'First + 1)); + Gneiss_Syscall.Socketpair (Fd1, Fd2); + Fds_Out (Fds_Out'First .. Fds_Out'First + 1) := (Fd1, Fd2); Valid := Fds_Out (Fds_Out'First) > -1 and then Fds_Out (Fds_Out'First + 1) > -1; if not Valid then Gneiss_Syscall.Close (Fds_Out (Fds_Out'First)); @@ -258,6 +290,7 @@ is Valid : out Boolean) is begin + Fds := (others => -1); Gneiss_Syscall.Timerfd_Create (Fds (Fds'First)); Valid := Fds (Fds'First) > -1; end Process_Timer_Request; @@ -275,7 +308,7 @@ is if Valid then case Kind is when Gneiss_Protocol.Session.Message | Gneiss_Protocol.Session.Log | Gneiss_Protocol.Session.Memory => - if Fds (Fds'First) >= 0 then + if Fds'Length > 0 and then Fds (Fds'First) >= 0 then Send_Confirm (State.Components (Destination).Fd, Kind, Label, Fds (Fds'First .. Fds'First)); else Gneiss_Log.Warning ("Invalid Fd, rejecting"); @@ -309,11 +342,17 @@ is Source : Positive; Kind : Gneiss_Protocol.Session.Kind_Type) is - Fds : Gneiss_Syscall.Fd_Array (1 .. 1); + Fds : Gneiss_Syscall.Fd_Array (1 .. 1); + Valid : Boolean; begin - Setup_Service (State, Kind, Source); + pragma Assert (if State.Components (Source).Fd > -1 + then SXML.Query.State_Result (State.Components (Source).Node) = SXML.Result_OK + and then SXML.Query.Is_Valid (State.Components (Source).Node, State.Xml) + and then SXML.Query.Is_Open (State.Components (Source).Node, State.Xml)); + Setup_Service (State.Components (Source).Serv, Kind, State.Epoll_Fd, Valid); + pragma Assert (Is_Valid (State.Xml, State.Components)); Fds := (1 => State.Components (Source).Serv (Kind).Disp); - if Fds (Fds'First) > -1 then + if Valid then Send_Confirm (State.Components (Source).Fd, Kind, "", Fds); else Send_Reject (State.Components (Source).Fd, Kind, ""); diff --git a/init/gneiss-broker-message.ads b/init/gneiss-broker-message.ads index c1e2958..95a4ff5 100644 --- a/init/gneiss-broker-message.ads +++ b/init/gneiss-broker-message.ads @@ -10,15 +10,23 @@ is Index : Positive; Filedesc : Integer) with Pre => Gneiss_Epoll.Valid_Fd (State.Epoll_Fd) - and then Is_Valid (State.Xml, State.Components), + and then Is_Valid (State.Xml, State.Components) + and then Is_Valid (State.Xml, State.Resources) + and then Filedesc > -1 + and then Index in State.Components'Range + and then State.Components (Index).Fd > -1, Post => Gneiss_Epoll.Valid_Fd (State.Epoll_Fd) - and then Is_Valid (State.Xml, State.Components); + and then Is_Valid (State.Xml, State.Components) + and then Is_Valid (State.Xml, State.Resources); private + use type Gneiss_Protocol.Session.Length_Type; + type Gneiss_Protocol_String is array (Gneiss_Protocol.Session.Length_Type range <>) of Character; - function Convert_Message (S : String) return Gneiss_Protocol_String; + function Convert_Message (S : String) return Gneiss_Protocol_String with + Pre => S'Length < Natural (Gneiss_Protocol.Session.Length_Type'Last); procedure Handle_Message (State : in out Broker_State; Source : Positive; @@ -26,56 +34,102 @@ private Kind : Gneiss_Protocol.Session.Kind_Type; Name : String; Label : String; - Fds : Gneiss_Syscall.Fd_Array); + Fds : Gneiss_Syscall.Fd_Array) with + Pre => Source in State.Components'Range + and then State.Components (Source).Fd > -1 + and then Gneiss_Epoll.Valid_Fd (State.Epoll_Fd) + and then Is_Valid (State.Xml, State.Components) + and then Is_Valid (State.Xml, State.Resources), + Post => Is_Valid (State.Xml, State.Components) + and then Is_Valid (State.Xml, State.Resources) + and then Gneiss_Epoll.Valid_Fd (State.Epoll_Fd); procedure Process_Request (State : in out Broker_State; Source : Positive; Kind : Gneiss_Protocol.Session.Kind_Type; Label : String; - Fds : Gneiss_Syscall.Fd_Array); + Fds : Gneiss_Syscall.Fd_Array) with + Pre => Source in State.Components'Range + and then Is_Valid (State.Xml, State.Components) + and then Is_Valid (State.Xml, State.Resources) + and then State.Components (Source).Fd > -1 + and then Gneiss_Epoll.Valid_Fd (State.Epoll_Fd) + and then Label'Length < 256, + Post => Is_Valid (State.Xml, State.Components) + and then Is_Valid (State.Xml, State.Resources) + and then Gneiss_Epoll.Valid_Fd (State.Epoll_Fd); procedure Process_Message_Request (Fds : out Gneiss_Syscall.Fd_Array; - Valid : out Boolean); + Valid : out Boolean) with + Pre => Fds'Length > 1; procedure Process_Rom_Request (State : Broker_State; Serv_State : SXML.Query.State_Type; Fds : out Gneiss_Syscall.Fd_Array; - Valid : out Boolean); + Valid : out Boolean) with + Pre => SXML.Query.Is_Valid (Serv_State, State.Xml) + and then SXML.Query.State_Result (Serv_State) = SXML.Result_OK + and then SXML.Query.Is_Open (Serv_State, State.Xml) + and then Is_Valid (State.Xml, State.Resources) + and then Fds'Length > 0; procedure Process_Memory_Request (Fds_In : Gneiss_Syscall.Fd_Array; Fds_Out : out Gneiss_Syscall.Fd_Array; - Valid : out Boolean); + Valid : out Boolean) with + Pre => Fds_In'Length > 0 and then Fds_Out'Length > 2; procedure Process_Timer_Request (Fds : out Gneiss_Syscall.Fd_Array; - Valid : out Boolean); + Valid : out Boolean) with + Pre => Fds'Length > 0; procedure Process_Confirm (State : Broker_State; Kind : Gneiss_Protocol.Session.Kind_Type; Name : String; Label : String; - Fds : Gneiss_Syscall.Fd_Array); + Fds : Gneiss_Syscall.Fd_Array) with + Pre => Is_Valid (State.Xml, State.Components) + and then Name'Length < 256 + and then Label'Length < 256; procedure Process_Reject (State : Broker_State; Kind : Gneiss_Protocol.Session.Kind_Type; Name : String; - Label : String); + Label : String) with + Pre => Is_Valid (State.Xml, State.Components) + and then Label'Length < 256; procedure Process_Register (State : in out Broker_State; Source : Positive; - Kind : Gneiss_Protocol.Session.Kind_Type); + Kind : Gneiss_Protocol.Session.Kind_Type) with + Pre => Gneiss_Epoll.Valid_Fd (State.Epoll_Fd) + and then Is_Valid (State.Xml, State.Components) + and then Is_Valid (State.Xml, State.Resources) + and then Source in State.Components'Range + and then State.Components (Source).Fd > -1, + Post => Gneiss_Epoll.Valid_Fd (State.Epoll_Fd) + and then Is_Valid (State.Xml, State.Components) + and then Is_Valid (State.Xml, State.Resources); procedure Send_Request (Destination : Integer; Kind : Gneiss_Protocol.Session.Kind_Type; Name : String; Label : String; - Fds : Gneiss_Syscall.Fd_Array); + Fds : Gneiss_Syscall.Fd_Array) with + Pre => Name'Length < 256 + and then Label'Length < 256 + and then Destination > -1; procedure Send_Confirm (Destination : Integer; Kind : Gneiss_Protocol.Session.Kind_Type; Label : String; - Fds : Gneiss_Syscall.Fd_Array); + Fds : Gneiss_Syscall.Fd_Array) with + Pre => Label'Length < 256 + and then Destination > -1; procedure Send_Reject (Destination : Integer; Kind : Gneiss_Protocol.Session.Kind_Type; - Label : String); + Label : String) with + Pre => Label'Length < 256 + and then Destination > -1; + end Gneiss.Broker.Message; diff --git a/init/gneiss-broker-startup.adb b/init/gneiss-broker-startup.adb index a6cb7b7..948b6f3 100644 --- a/init/gneiss-broker-startup.adb +++ b/init/gneiss-broker-startup.adb @@ -33,6 +33,9 @@ is pragma Loop_Invariant (SXML.Query.Is_Valid (Query, State.Xml)); pragma Loop_Invariant (Index in State.Components'Range); pragma Loop_Invariant (Gneiss_Epoll.Valid_Fd (State.Epoll_Fd)); + pragma Loop_Invariant (Is_Valid (State.Xml, State.Components)); + pragma Loop_Invariant (Is_Valid (State.Xml, State.Resources)); + pragma Loop_Invariant (Parent); Query := SXML.Query.Find_Sibling (Query, State.Xml, "component"); exit when SXML.Query.State_Result (Query) /= SXML.Result_OK; SXML.Query.Attribute (Query, State.Xml, "name", Result, XML_Buf, Last); @@ -85,6 +88,7 @@ is pragma Loop_Invariant (SXML.Query.State_Result (State) = SXML.Result_OK); pragma Loop_Invariant (SXML.Query.Is_Valid (State, Document)); pragma Loop_Invariant (Index in Resources'Range); + pragma Loop_Invariant (Is_Valid (Document, Resources)); State := SXML.Query.Find_Sibling (State, Document, "resource"); exit when SXML.Query.State_Result (State) /= SXML.Result_OK; Resources (Index).Node := State; diff --git a/init/gneiss-broker-startup.ads b/init/gneiss-broker-startup.ads index 7e56c5c..cf42d4d 100644 --- a/init/gneiss-broker-startup.ads +++ b/init/gneiss-broker-startup.ads @@ -14,9 +14,11 @@ is Pre => Gneiss_Epoll.Valid_Fd (State.Epoll_Fd) and then SXML.Query.State_Result (Root) = SXML.Result_OK and then SXML.Query.Is_Valid (Root, State.Xml) - and then Is_Valid (State.Xml, State.Components), + and then Is_Valid (State.Xml, State.Components) + and then Is_Valid (State.Xml, State.Resources), Post => (if Parent then Gneiss_Epoll.Valid_Fd (State.Epoll_Fd) - and then Is_Valid (State.Xml, State.Components)); + and then Is_Valid (State.Xml, State.Components) + and then Is_Valid (State.Xml, State.Resources)); procedure Parse (Data : String; Document : in out SXML.Document_Type); @@ -24,10 +26,12 @@ is procedure Parse_Resources (Resources : in out Resource_List; Document : SXML.Document_Type; Root : SXML.Query.State_Type) with - Pre => SXML.Query.State_Result (Root) = SXML.Result_OK - and then SXML.Query.Is_Valid (Root, Document) - and then SXML.Query.Is_Open (Root, Document) - and then Resources'Length > 0; + Pre => SXML.Query.State_Result (Root) = SXML.Result_OK + and then SXML.Query.Is_Valid (Root, Document) + and then SXML.Query.Is_Open (Root, Document) + and then Resources'Length > 0 + and then Is_Valid (Document, Resources), + Post => Is_Valid (Document, Resources); private diff --git a/init/gneiss-command_line.adb b/init/gneiss-command_line.adb index 679ac86..0e9667e 100644 --- a/init/gneiss-command_line.adb +++ b/init/gneiss-command_line.adb @@ -3,7 +3,7 @@ with System; with Gneiss.Libc; package body Gneiss.Command_Line with - SPARK_Mode + SPARK_Mode => Off is type Ptr_List is array (Natural range <>) of System.Address; @@ -25,8 +25,7 @@ is function Argument_Count return Natural is (Argc); - function Argument (Number : Natural) return String with - SPARK_Mode => Off + function Argument (Number : Natural) return String is Arg : String (1 .. Libc.Strlen (Argvl (Number))) with Import, diff --git a/init/gneiss-config.adb b/init/gneiss-config.adb index 5d0ee48..7c16643 100644 --- a/init/gneiss-config.adb +++ b/init/gneiss-config.adb @@ -3,16 +3,16 @@ with System; with Gneiss_Syscall; package body Gneiss.Config with - SPARK_Mode => Off + SPARK_Mode is procedure Load (Location : String) is use type System.Address; - Fd : Integer; + Fd : Integer; Addr : System.Address; begin - Gneiss_Syscall.Open (Location, Fd, 0); + Gneiss_Syscall.Open (Location & ASCII.NUL, Fd, 0); if Fd < 0 then return; end if; @@ -22,7 +22,8 @@ is return; end if; declare - Data : String (1 .. Gneiss_Syscall.Stat_Size (Fd)) with + Size : constant Integer := Gneiss_Syscall.Stat_Size (Fd); + Data : String (1 .. Size) with Import, Address => Addr; begin diff --git a/src/platform/linux/gneiss_internal.ads b/src/platform/linux/gneiss_internal.ads index 4ca5389..f27b9ac 100644 --- a/src/platform/linux/gneiss_internal.ads +++ b/src/platform/linux/gneiss_internal.ads @@ -6,7 +6,8 @@ package Gneiss_Internal is type Session_Label is record Last : Natural := 0; Value : String (1 .. 255) := (others => Character'First); - end record; + end record with + Dynamic_Predicate => Last <= Value'Last; type Capability is record Broker_Fd : Integer;