diff --git a/json/src/json-parsers.adb b/json/src/json-parsers.adb index 5f6dd75..320b581 100644 --- a/json/src/json-parsers.adb +++ b/json/src/json-parsers.adb @@ -144,7 +144,7 @@ package body JSON.Parsers is function Parse (Stream : Streams.Stream_Ptr; - Allocator : Types.Memory_Allocator_Ptr) return Types.JSON_Value + Allocator : Types.Memory_Allocator_Ptr) return Types.JSON_Value with SPARK_Mode => On is Token : Tokenizers.Token; begin @@ -161,55 +161,51 @@ package body JSON.Parsers is function Create (Pointer : not null JSON.Streams.Stream_Element_Array_Access; - Maximum_Depth : Positive := Default_Maximum_Depth) return Parser - is - Allocator : Types.Memory_Allocator (Maximum_Depth); + Maximum_Depth : Positive := Default_Maximum_Depth) return Parser is begin return - (AF.Limited_Controlled with - Pointer => Pointer, - Own_Pointer => False, - Stream => Stream_Holders.To_Holder (Streams.Create_Stream (Pointer)), - Allocator => Memory_Holders.To_Holder (Allocator)); + (Ada.Finalization.Limited_Controlled with + Maximum_Depth => Maximum_Depth, + Pointer => Pointer, + Own_Pointer => False, + Stream => Streams.Create_Stream (Pointer), + Allocator => <>); end Create; function Create (Text : String; Maximum_Depth : Positive := Default_Maximum_Depth) return Parser is - Allocator : Types.Memory_Allocator (Maximum_Depth); + Pointer : constant not null Streams.Stream_Element_Array_Access := Streams.From_Text (Text); begin - return Result : Parser := - (AF.Limited_Controlled with - Pointer => Streams.From_Text (Text), - Own_Pointer => True, - Allocator => Memory_Holders.To_Holder (Allocator), - others => <>) - do - Result.Stream := Stream_Holders.To_Holder (Streams.Create_Stream (Result.Pointer)); - end return; + return + (Ada.Finalization.Limited_Controlled with + Maximum_Depth => Maximum_Depth, + Pointer => Pointer, + Own_Pointer => True, + Stream => Streams.Create_Stream (Pointer), + Allocator => <>); end Create; function Create_From_File (File_Name : String; Maximum_Depth : Positive := Default_Maximum_Depth) return Parser is - Allocator : Types.Memory_Allocator (Maximum_Depth); + Pointer : constant not null Streams.Stream_Element_Array_Access := + Streams.From_File (File_Name); begin - return Result : Parser := - (AF.Limited_Controlled with - Pointer => Streams.From_File (File_Name), - Own_Pointer => True, - Allocator => Memory_Holders.To_Holder (Allocator), - others => <>) - do - Result.Stream := Stream_Holders.To_Holder (Streams.Create_Stream (Result.Pointer)); - end return; + return + (Ada.Finalization.Limited_Controlled with + Maximum_Depth => Maximum_Depth, + Pointer => Pointer, + Own_Pointer => True, + Stream => Streams.Create_Stream (Pointer), + Allocator => <>); end Create_From_File; function Parse (Object : in out Parser) return Types.JSON_Value is begin - return Parse (Object.Stream.Reference.Element, Object.Allocator.Reference.Element); + return Parse (Object.Stream'Unchecked_Access, Object.Allocator'Unchecked_Access); end Parse; overriding @@ -221,9 +217,6 @@ package body JSON.Parsers is use type Streams.Stream_Element_Array_Access; begin if Object.Pointer /= null then - Object.Stream.Clear; - Object.Allocator.Clear; - if Object.Own_Pointer then Free (Object.Pointer); end if; diff --git a/json/src/json-parsers.ads b/json/src/json-parsers.ads index 3133798..b17dffb 100644 --- a/json/src/json-parsers.ads +++ b/json/src/json-parsers.ads @@ -14,7 +14,6 @@ -- See the License for the specific language governing permissions and -- limitations under the License. -private with Ada.Containers.Indefinite_Holders; private with Ada.Finalization; with JSON.Types; @@ -31,7 +30,7 @@ generic package JSON.Parsers with SPARK_Mode => On is pragma Preelaborate; - type Parser is tagged limited private; + type Parser (<>) is tagged limited private; function Create (Pointer : not null JSON.Streams.Stream_Element_Array_Access; @@ -45,23 +44,18 @@ package JSON.Parsers with SPARK_Mode => On is (File_Name : String; Maximum_Depth : Positive := Default_Maximum_Depth) return Parser; - function Parse (Object : in out Parser) return Types.JSON_Value; + function Parse (Object : in out Parser) return Types.JSON_Value + with SPARK_Mode => Off; Parse_Error : exception; private - package Stream_Holders is new Ada.Containers.Indefinite_Holders - (Element_Type => Streams.Stream, "=" => Streams."="); - - package Memory_Holders is new Ada.Containers.Indefinite_Holders - (Element_Type => Types.Memory_Allocator, "=" => Types."="); - - package AF renames Ada.Finalization; - - type Parser is limited new AF.Limited_Controlled with record - Stream : Stream_Holders.Holder; - Allocator : Memory_Holders.Holder; + type Parser (Maximum_Depth : Positive) + is limited new Ada.Finalization.Limited_Controlled with + record + Stream : aliased Streams.Stream; + Allocator : aliased Types.Memory_Allocator (Maximum_Depth); Pointer : Streams.Stream_Element_Array_Access; Own_Pointer : Boolean; end record; diff --git a/json/src/json-streams.adb b/json/src/json-streams.adb index 46020b3..46f7ed7 100644 --- a/json/src/json-streams.adb +++ b/json/src/json-streams.adb @@ -23,7 +23,7 @@ package body JSON.Streams is use type AS.Stream_Element_Offset; - procedure Read_Character (Object : in out Stream; Item : out Character) is + procedure Read_Character_From_Stream (Object : in out Stream; Item : out Character) is function Convert is new Ada.Unchecked_Conversion (Source => AS.Stream_Element, Target => Character); begin @@ -33,31 +33,32 @@ package body JSON.Streams is Item := Convert (Object.Bytes (Object.Index)); Object.Index := Object.Index + 1; - end Read_Character; + end Read_Character_From_Stream; function Has_Buffered_Character (Object : Stream) return Boolean is (Object.Next_Character /= Ada.Characters.Latin_1.NUL); - function Read_Character (Object : in out Stream) return Character is + procedure Read_Character (Object : in out Stream; Result : out Character) is Index : AS.Stream_Element_Offset; begin - return Object.Read_Character (Index); + Object.Read_Character (Index, Result); end Read_Character; - function Read_Character + procedure Read_Character (Object : in out Stream; - Index : out AS.Stream_Element_Offset) return Character + Index : out AS.Stream_Element_Offset; + Result : out Character) is C : Character; begin Index := Object.Index; if Object.Next_Character = Ada.Characters.Latin_1.NUL then - Object.Read_Character (C); + Object.Read_Character_From_Stream (C); else C := Object.Next_Character; Object.Next_Character := Ada.Characters.Latin_1.NUL; end if; - return C; + Result := C; end Read_Character; procedure Write_Character (Object : in out Stream; Next : Character) is diff --git a/json/src/json-streams.ads b/json/src/json-streams.ads index f99a127..48fd30f 100644 --- a/json/src/json-streams.ads +++ b/json/src/json-streams.ads @@ -29,12 +29,13 @@ package JSON.Streams with SPARK_Mode => On is function Has_Buffered_Character (Object : Stream) return Boolean; - function Read_Character (Object : in out Stream) return Character + procedure Read_Character (Object : in out Stream; Result : out Character) with Post => not Object.Has_Buffered_Character; - function Read_Character + procedure Read_Character (Object : in out Stream; - Index : out AS.Stream_Element_Offset) return Character + Index : out AS.Stream_Element_Offset; + Result : out Character) with Post => not Object.Has_Buffered_Character; -- Writes the offset of the read character to Index. This is needed -- for string tokens. diff --git a/json/src/json-tokenizers.adb b/json/src/json-tokenizers.adb index 15ee442..9071391 100644 --- a/json/src/json-tokenizers.adb +++ b/json/src/json-tokenizers.adb @@ -32,7 +32,7 @@ package body JSON.Tokenizers is use Ada.Characters.Latin_1; begin loop - C := Stream.Read_Character (Index); + Stream.Read_Character (Index, C); -- An unescaped '"' character denotes the end of the string exit when not Escaped and C = '"'; @@ -118,7 +118,7 @@ package body JSON.Tokenizers is -- Accept sequence of digits, including leading zeroes loop - C := Stream.Read_Character; + Stream.Read_Character (C); exit when C not in '0' .. '9'; SB.Append (Value, C); end loop; @@ -136,7 +136,7 @@ package body JSON.Tokenizers is -- Require at least one digit after decimal point begin - C := Stream.Read_Character; + Stream.Read_Character (C); if C not in '0' .. '9' then raise Tokenizer_Error with Error_Dot_Message; end if; @@ -148,7 +148,7 @@ package body JSON.Tokenizers is -- Accept sequence of digits loop - C := Stream.Read_Character; + Stream.Read_Character (C); exit when C not in '0' .. '9'; SB.Append (Value, C); end loop; @@ -160,7 +160,7 @@ package body JSON.Tokenizers is SB.Append (Value, C); begin - C := Stream.Read_Character; + Stream.Read_Character (C); -- Append optional '+' or '-' character if C in '+' | '-' then -- If exponent is negative, number will be a float @@ -171,7 +171,7 @@ package body JSON.Tokenizers is SB.Append (Value, C); -- Require at least one digit after +/- sign - C := Stream.Read_Character; + Stream.Read_Character (C); if C not in '0' .. '9' then raise Tokenizer_Error with Error_One_Digit_Message; end if; @@ -188,7 +188,7 @@ package body JSON.Tokenizers is -- Accept sequence of digits loop - C := Stream.Read_Character; + Stream.Read_Character (C); exit when C not in '0' .. '9'; SB.Append (Value, C); end loop; @@ -238,7 +238,7 @@ package body JSON.Tokenizers is begin SB.Append (Value, First); loop - C := Stream.Read_Character; + Stream.Read_Character (C); exit when C not in 'a' .. 'z' or else SB.Length (Value) = SB.Max_Length; SB.Append (Value, C); end loop; @@ -264,7 +264,7 @@ package body JSON.Tokenizers is begin loop -- Read the first next character and decide which token it could be part of - C := Stream.Read_Character; + Stream.Read_Character (C); -- Skip whitespace exit when C not in Space | HT | LF | CR;