Fix SPARK mode violations detected by GCC 14

onox · onox · commit 9d324693de04 · 2024-07-28T16:05:00.000+02:00
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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;
