Skip to content

Commit

Permalink
Fix SPARK mode violations detected by GCC 14
Browse files Browse the repository at this point in the history
  • Loading branch information
@onox
onox committed Jul 28, 2024
1 parent fda3e8b commit 9d32469
Show file tree
Hide file tree
Showing 5 changed files with 56 additions and 67 deletions.
59 changes: 26 additions & 33 deletions json/src/json-parsers.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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;
Expand Down
22 changes: 8 additions & 14 deletions json/src/json-parsers.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand All @@ -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;
Expand Down
17 changes: 9 additions & 8 deletions json/src/json-streams.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
7 changes: 4 additions & 3 deletions json/src/json-streams.ads
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
18 changes: 9 additions & 9 deletions json/src/json-tokenizers.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 = '"';
Expand Down Expand Up @@ -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;
Expand All @@ -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;
Expand All @@ -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;
Expand All @@ -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
Expand All @@ -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;
Expand All @@ -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;
Expand Down Expand Up @@ -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;
Expand All @@ -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;
Expand Down

0 comments on commit 9d32469

Please sign in to comment.