gcc/ada/libgnat/s-valuti.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT COMPILER COMPONENTS                         --
   4 --                                                                          --
   5 --                      S Y S T E M . V A L _ U T I L                       --
   6 --                                                                          --
   7 --                                 B o d y                                  --
   8 --                                                                          --
   9 --          Copyright (C) 1992-2024, Free Software Foundation, Inc.         --
  10 --                                                                          --
  11 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
  12 -- terms of the  GNU General Public License as published  by the Free Soft- --
  13 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
  14 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
  15 -- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
  16 -- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
  17 --                                                                          --
  18 -- As a special exception under Section 7 of GPL version 3, you are granted --
  19 -- additional permissions described in the GCC Runtime Library Exception,   --
  20 -- version 3.1, as published by the Free Software Foundation.               --
  21 --                                                                          --
  22 -- You should have received a copy of the GNU General Public License and    --
  23 -- a copy of the GCC Runtime Library Exception along with this program;     --
  24 -- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
  25 -- <http://www.gnu.org/licenses/>.                                          --
  26 --                                                                          --
  27 -- GNAT was originally developed  by the GNAT team at  New York University. --
  28 -- Extensive contributions were provided by Ada Core Technologies Inc.      --
  29 --                                                                          --
  30 ------------------------------------------------------------------------------
  31
  32 --  Ghost code, loop invariants and assertions in this unit are meant for
  33 --  analysis only, not for run-time checking, as it would be too costly
  34 --  otherwise. This is enforced by setting the assertion policy to Ignore.
  35
  36 pragma Assertion_Policy (Ghost          => Ignore,
  37                          Loop_Invariant => Ignore,
  38                          Assert         => Ignore);
  39
  40 with System.Case_Util; use System.Case_Util;
  41
  42 package body System.Val_Util
  43   with SPARK_Mode
  44 is
  45
  46    ---------------
  47    -- Bad_Value --
  48    ---------------
  49
  50    procedure Bad_Value (S : String) is
  51       pragma Annotate (GNATprove, Intentional, "exception might be raised",
  52                        "Intentional exception from Bad_Value");
  53    begin
  54       --  Bad_Value might be called with very long strings allocated on the
  55       --  heap. Limit the size of the message so that we avoid creating a
  56       --  Storage_Error during error handling.
  57       if S'Length > 127 then
  58          raise Constraint_Error with "bad input for 'Value: """
  59          & S (S'First .. S'First + 127) & "...""";
  60       else
  61          raise Constraint_Error with "bad input for 'Value: """ & S & '"';
  62       end if;
  63    end Bad_Value;
  64
  65    ----------------------
  66    -- Normalize_String --
  67    ----------------------
  68
  69    procedure Normalize_String
  70      (S    : in out String;
  71       F, L : out Integer)
  72    is
  73    begin
  74       F := S'First;
  75       L := S'Last;
  76
  77       --  Case of empty string
  78
  79       if F > L then
  80          return;
  81       end if;
  82
  83       --  Scan for leading spaces
  84
  85       while F < L and then S (F) = ' ' loop
  86          pragma Loop_Invariant (F in S'First .. L - 1);
  87          pragma Loop_Invariant (for all J in S'First .. F => S (J) = ' ');
  88          pragma Loop_Variant (Increases => F);
  89          F := F + 1;
  90       end loop;
  91
  92       --  Case of no nonspace characters found. Decrease L to ensure L < F
  93       --  without risking an overflow if F is Integer'Last.
  94
  95       if S (F) = ' ' then
  96          L := L - 1;
  97          return;
  98       end if;
  99
 100       --  Scan for trailing spaces
 101
 102       while S (L) = ' ' loop
 103          pragma Loop_Invariant (L in F + 1 .. S'Last);
 104          pragma Loop_Invariant (for all J in L .. S'Last => S (J) = ' ');
 105          pragma Loop_Variant (Decreases => L);
 106          L := L - 1;
 107       end loop;
 108
 109       --  Except in the case of a character literal, convert to upper case
 110
 111       if S (F) /= ''' then
 112          for J in F .. L loop
 113             S (J) := To_Upper (S (J));
 114             pragma Loop_Invariant
 115               (for all K in F .. J => S (K) = To_Upper (S'Loop_Entry (K)));
 116          end loop;
 117       end if;
 118    end Normalize_String;
 119
 120    -------------------
 121    -- Scan_Exponent --
 122    -------------------
 123
 124    procedure Scan_Exponent
 125      (Str  : String;
 126       Ptr  : not null access Integer;
 127       Max  : Integer;
 128       Exp  : out Integer;
 129       Real : Boolean := False)
 130    is
 131       P : Integer := Ptr.all;
 132       M : Boolean;
 133       X : Integer;
 134
 135    begin
 136       if P >= Max
 137         or else (Str (P) /= 'E' and then Str (P) /= 'e')
 138       then
 139          Exp := 0;
 140          return;
 141       end if;
 142       pragma Annotate
 143         (CodePeer, False_Positive, "test always false",
 144          "the slice might be empty or not start with an 'e'");
 145
 146       --  We have an E/e, see if sign follows
 147
 148       P := P + 1;
 149
 150       if Str (P) = '+' then
 151          P := P + 1;
 152
 153          if P > Max then
 154             Exp := 0;
 155             return;
 156          else
 157             M := False;
 158          end if;
 159
 160       elsif Str (P) = '-' then
 161          P := P + 1;
 162
 163          if P > Max or else not Real then
 164             Exp := 0;
 165             return;
 166          else
 167             M := True;
 168          end if;
 169
 170       else
 171          M := False;
 172       end if;
 173
 174       if Str (P) not in '0' .. '9' then
 175          Exp := 0;
 176          return;
 177       end if;
 178
 179       --  Scan out the exponent value as an unsigned integer. Values larger
 180       --  than (Integer'Last / 10) are simply considered large enough here.
 181       --  This assumption is correct for all machines we know of (e.g. in the
 182       --  case of 16 bit integers it allows exponents up to 3276, which is
 183       --  large enough for the largest floating types in base 2.)
 184
 185       X := 0;
 186
 187       declare
 188          Rest : constant String := Str (P .. Max) with Ghost;
 189          Last : constant Natural := Sp.Last_Number_Ghost (Rest) with Ghost;
 190
 191       begin
 192          pragma Assert (Sp.Is_Natural_Format_Ghost (Rest));
 193
 194          loop
 195             pragma Assert (Str (P) in '0' .. '9');
 196
 197             if X < (Integer'Last / 10) then
 198                X := X * 10 + (Character'Pos (Str (P)) - Character'Pos ('0'));
 199             end if;
 200
 201             pragma Loop_Invariant (X >= 0);
 202             pragma Loop_Invariant (P in Rest'First .. Last);
 203             pragma Loop_Invariant (Str (P) in '0' .. '9');
 204             pragma Loop_Invariant
 205               (Sp.Scan_Natural_Ghost (Rest, Rest'First, 0)
 206                = Sp.Scan_Natural_Ghost (Rest, P + 1, X));
 207
 208             P := P + 1;
 209
 210             exit when P > Max;
 211
 212             if Str (P) = '_' then
 213                Scan_Underscore (Str, P, Ptr, Max, False);
 214             else
 215                exit when Str (P) not in '0' .. '9';
 216             end if;
 217          end loop;
 218
 219          pragma Assert (P = Last + 1);
 220       end;
 221
 222       if M then
 223          X := -X;
 224       end if;
 225
 226       Ptr.all := P;
 227       Exp := X;
 228    end Scan_Exponent;
 229
 230    --------------------
 231    -- Scan_Plus_Sign --
 232    --------------------
 233
 234    procedure Scan_Plus_Sign
 235      (Str   : String;
 236       Ptr   : not null access Integer;
 237       Max   : Integer;
 238       Start : out Positive)
 239    is
 240       P : Integer := Ptr.all;
 241
 242    begin
 243       if P > Max then
 244          Bad_Value (Str);
 245       end if;
 246
 247       --  Scan past initial blanks
 248
 249       while Str (P) = ' ' loop
 250          P := P + 1;
 251
 252          pragma Loop_Invariant (Ptr.all = Ptr.all'Loop_Entry);
 253          pragma Loop_Invariant (P in Ptr.all .. Max);
 254          pragma Loop_Invariant (for some J in P .. Max => Str (J) /= ' ');
 255          pragma Loop_Invariant
 256            (for all J in Ptr.all .. P - 1 => Str (J) = ' ');
 257
 258          if P > Max then
 259             Ptr.all := P;
 260             Bad_Value (Str);
 261          end if;
 262       end loop;
 263
 264       Start := P;
 265
 266       pragma Assert (Start = Sp.First_Non_Space_Ghost (Str, Ptr.all, Max));
 267
 268       --  Skip past an initial plus sign
 269
 270       if Str (P) = '+' then
 271          P := P + 1;
 272
 273          if P > Max then
 274             Ptr.all := Start;
 275             Bad_Value (Str);
 276          end if;
 277       end if;
 278
 279       Ptr.all := P;
 280    end Scan_Plus_Sign;
 281
 282    ---------------
 283    -- Scan_Sign --
 284    ---------------
 285
 286    procedure Scan_Sign
 287      (Str   : String;
 288       Ptr   : not null access Integer;
 289       Max   : Integer;
 290       Minus : out Boolean;
 291       Start : out Positive)
 292    is
 293       P : Integer := Ptr.all;
 294
 295    begin
 296       --  Deal with case of null string (all blanks). As per spec, we raise
 297       --  constraint error, with Ptr unchanged, and thus > Max.
 298
 299       if P > Max then
 300          Bad_Value (Str);
 301       end if;
 302
 303       --  Scan past initial blanks
 304
 305       while Str (P) = ' ' loop
 306          P := P + 1;
 307
 308          pragma Loop_Invariant (Ptr.all = Ptr.all'Loop_Entry);
 309          pragma Loop_Invariant (P in Ptr.all .. Max);
 310          pragma Loop_Invariant (for some J in P .. Max => Str (J) /= ' ');
 311          pragma Loop_Invariant
 312            (for all J in Ptr.all .. P - 1 => Str (J) = ' ');
 313
 314          if P > Max then
 315             Ptr.all := P;
 316             Bad_Value (Str);
 317          end if;
 318       end loop;
 319
 320       Start := P;
 321
 322       pragma Assert (Start = Sp.First_Non_Space_Ghost (Str, Ptr.all, Max));
 323
 324       --  Remember an initial minus sign
 325
 326       if Str (P) = '-' then
 327          Minus := True;
 328          P := P + 1;
 329
 330          if P > Max then
 331             Ptr.all := Start;
 332             Bad_Value (Str);
 333          end if;
 334
 335       --  Skip past an initial plus sign
 336
 337       elsif Str (P) = '+' then
 338          Minus := False;
 339          P := P + 1;
 340
 341          if P > Max then
 342             Ptr.all := Start;
 343             Bad_Value (Str);
 344          end if;
 345
 346       else
 347          Minus := False;
 348       end if;
 349
 350       Ptr.all := P;
 351    end Scan_Sign;
 352
 353    --------------------------
 354    -- Scan_Trailing_Blanks --
 355    --------------------------
 356
 357    procedure Scan_Trailing_Blanks (Str : String; P : Positive) is
 358    begin
 359       for J in P .. Str'Last loop
 360          if Str (J) /= ' ' then
 361             Bad_Value (Str);
 362          end if;
 363
 364          pragma Loop_Invariant (for all K in P .. J => Str (K) = ' ');
 365       end loop;
 366    end Scan_Trailing_Blanks;
 367
 368    ---------------------
 369    -- Scan_Underscore --
 370    ---------------------
 371
 372    procedure Scan_Underscore
 373      (Str : String;
 374       P   : in out Natural;
 375       Ptr : not null access Integer;
 376       Max : Integer;
 377       Ext : Boolean)
 378    is
 379       C : Character;
 380
 381    begin
 382       P := P + 1;
 383
 384       --  If underscore is at the end of string, then this is an error and we
 385       --  raise Constraint_Error, leaving the pointer past the underscore. This
 386       --  seems a bit strange. It means e.g. that if the field is:
 387
 388       --    345_
 389
 390       --  that Constraint_Error is raised. You might think that the RM in this
 391       --  case would scan out the 345 as a valid integer, leaving the pointer
 392       --  at the underscore, but the ACVC suite clearly requires an error in
 393       --  this situation (see for example CE3704M).
 394
 395       if P > Max then
 396          Ptr.all := P;
 397          Bad_Value (Str);
 398       end if;
 399
 400       --  Similarly, if no digit follows the underscore raise an error. This
 401       --  also catches the case of double underscore which is also an error.
 402
 403       C := Str (P);
 404
 405       if C in '0' .. '9'
 406         or else (Ext and then (C in 'A' .. 'F' or else C in 'a' .. 'f'))
 407       then
 408          return;
 409       else
 410          Ptr.all := P;
 411          Bad_Value (Str);
 412       end if;
 413    end Scan_Underscore;
 414
 415 end System.Val_Util;