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-2023, 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    -- First_Non_Space_Ghost --
  67    ---------------------------
  68
  69    function First_Non_Space_Ghost
  70      (S        : String;
  71       From, To : Integer) return Positive
  72    is
  73    begin
  74       for J in From .. To loop
  75          if S (J) /= ' ' then
  76             return J;
  77          end if;
  78
  79          pragma Loop_Invariant (for all K in From .. J => S (K) = ' ');
  80       end loop;
  81
  82       raise Program_Error;
  83    end First_Non_Space_Ghost;
  84
  85    -----------------------
  86    -- Last_Number_Ghost --
  87    -----------------------
  88
  89    function Last_Number_Ghost (Str : String) return Positive is
  90    begin
  91       for J in Str'Range loop
  92          if Str (J) not in '0' .. '9' | '_' then
  93             return J - 1;
  94          end if;
  95
  96          pragma Loop_Invariant
  97            (for all K in Str'First .. J => Str (K) in '0' .. '9' | '_');
  98       end loop;
  99
 100       return Str'Last;
 101    end Last_Number_Ghost;
 102
 103    ----------------------
 104    -- Normalize_String --
 105    ----------------------
 106
 107    procedure Normalize_String
 108      (S    : in out String;
 109       F, L : out Integer)
 110    is
 111    begin
 112       F := S'First;
 113       L := S'Last;
 114
 115       --  Case of empty string
 116
 117       if F > L then
 118          return;
 119       end if;
 120
 121       --  Scan for leading spaces
 122
 123       while F < L and then S (F) = ' ' loop
 124          pragma Loop_Invariant (F in S'First .. L - 1);
 125          pragma Loop_Invariant (for all J in S'First .. F => S (J) = ' ');
 126          pragma Loop_Variant (Increases => F);
 127          F := F + 1;
 128       end loop;
 129
 130       --  Case of no nonspace characters found. Decrease L to ensure L < F
 131       --  without risking an overflow if F is Integer'Last.
 132
 133       if S (F) = ' ' then
 134          L := L - 1;
 135          return;
 136       end if;
 137
 138       --  Scan for trailing spaces
 139
 140       while S (L) = ' ' loop
 141          pragma Loop_Invariant (L in F + 1 .. S'Last);
 142          pragma Loop_Invariant (for all J in L .. S'Last => S (J) = ' ');
 143          pragma Loop_Variant (Decreases => L);
 144          L := L - 1;
 145       end loop;
 146
 147       --  Except in the case of a character literal, convert to upper case
 148
 149       if S (F) /= ''' then
 150          for J in F .. L loop
 151             S (J) := To_Upper (S (J));
 152             pragma Loop_Invariant
 153               (for all K in F .. J => S (K) = To_Upper (S'Loop_Entry (K)));
 154          end loop;
 155       end if;
 156    end Normalize_String;
 157
 158    -------------------
 159    -- Scan_Exponent --
 160    -------------------
 161
 162    procedure Scan_Exponent
 163      (Str  : String;
 164       Ptr  : not null access Integer;
 165       Max  : Integer;
 166       Exp  : out Integer;
 167       Real : Boolean := False)
 168    is
 169       P : Integer := Ptr.all;
 170       M : Boolean;
 171       X : Integer;
 172
 173    begin
 174       if P >= Max
 175         or else (Str (P) /= 'E' and then Str (P) /= 'e')
 176       then
 177          Exp := 0;
 178          return;
 179       end if;
 180       pragma Annotate
 181         (CodePeer, False_Positive, "test always false",
 182          "the slice might be empty or not start with an 'e'");
 183
 184       --  We have an E/e, see if sign follows
 185
 186       P := P + 1;
 187
 188       if Str (P) = '+' then
 189          P := P + 1;
 190
 191          if P > Max then
 192             Exp := 0;
 193             return;
 194          else
 195             M := False;
 196          end if;
 197
 198       elsif Str (P) = '-' then
 199          P := P + 1;
 200
 201          if P > Max or else not Real then
 202             Exp := 0;
 203             return;
 204          else
 205             M := True;
 206          end if;
 207
 208       else
 209          M := False;
 210       end if;
 211
 212       if Str (P) not in '0' .. '9' then
 213          Exp := 0;
 214          return;
 215       end if;
 216
 217       --  Scan out the exponent value as an unsigned integer. Values larger
 218       --  than (Integer'Last / 10) are simply considered large enough here.
 219       --  This assumption is correct for all machines we know of (e.g. in the
 220       --  case of 16 bit integers it allows exponents up to 3276, which is
 221       --  large enough for the largest floating types in base 2.)
 222
 223       X := 0;
 224
 225       declare
 226          Rest : constant String := Str (P .. Max) with Ghost;
 227          Last : constant Natural := Last_Number_Ghost (Rest) with Ghost;
 228
 229       begin
 230          pragma Assert (Is_Natural_Format_Ghost (Rest));
 231
 232          loop
 233             pragma Assert (Str (P) in '0' .. '9');
 234
 235             if X < (Integer'Last / 10) then
 236                X := X * 10 + (Character'Pos (Str (P)) - Character'Pos ('0'));
 237             end if;
 238
 239             pragma Loop_Invariant (X >= 0);
 240             pragma Loop_Invariant (P in Rest'First .. Last);
 241             pragma Loop_Invariant (Str (P) in '0' .. '9');
 242             pragma Loop_Invariant
 243               (Scan_Natural_Ghost (Rest, Rest'First, 0)
 244                = Scan_Natural_Ghost (Rest, P + 1, X));
 245
 246             P := P + 1;
 247
 248             exit when P > Max;
 249
 250             if Str (P) = '_' then
 251                Scan_Underscore (Str, P, Ptr, Max, False);
 252             else
 253                exit when Str (P) not in '0' .. '9';
 254             end if;
 255          end loop;
 256
 257          pragma Assert (P = Last + 1);
 258       end;
 259
 260       if M then
 261          X := -X;
 262       end if;
 263
 264       Ptr.all := P;
 265       Exp := X;
 266    end Scan_Exponent;
 267
 268    --------------------
 269    -- Scan_Plus_Sign --
 270    --------------------
 271
 272    procedure Scan_Plus_Sign
 273      (Str   : String;
 274       Ptr   : not null access Integer;
 275       Max   : Integer;
 276       Start : out Positive)
 277    is
 278       P : Integer := Ptr.all;
 279
 280    begin
 281       if P > Max then
 282          Bad_Value (Str);
 283       end if;
 284
 285       --  Scan past initial blanks
 286
 287       while Str (P) = ' ' loop
 288          P := P + 1;
 289
 290          pragma Loop_Invariant (Ptr.all = Ptr.all'Loop_Entry);
 291          pragma Loop_Invariant (P in Ptr.all .. Max);
 292          pragma Loop_Invariant (for some J in P .. Max => Str (J) /= ' ');
 293          pragma Loop_Invariant
 294            (for all J in Ptr.all .. P - 1 => Str (J) = ' ');
 295
 296          if P > Max then
 297             Ptr.all := P;
 298             Bad_Value (Str);
 299          end if;
 300       end loop;
 301
 302       Start := P;
 303
 304       pragma Assert (Start = First_Non_Space_Ghost (Str, Ptr.all, Max));
 305
 306       --  Skip past an initial plus sign
 307
 308       if Str (P) = '+' then
 309          P := P + 1;
 310
 311          if P > Max then
 312             Ptr.all := Start;
 313             Bad_Value (Str);
 314          end if;
 315       end if;
 316
 317       Ptr.all := P;
 318    end Scan_Plus_Sign;
 319
 320    ---------------
 321    -- Scan_Sign --
 322    ---------------
 323
 324    procedure Scan_Sign
 325      (Str   : String;
 326       Ptr   : not null access Integer;
 327       Max   : Integer;
 328       Minus : out Boolean;
 329       Start : out Positive)
 330    is
 331       P : Integer := Ptr.all;
 332
 333    begin
 334       --  Deal with case of null string (all blanks). As per spec, we raise
 335       --  constraint error, with Ptr unchanged, and thus > Max.
 336
 337       if P > Max then
 338          Bad_Value (Str);
 339       end if;
 340
 341       --  Scan past initial blanks
 342
 343       while Str (P) = ' ' loop
 344          P := P + 1;
 345
 346          pragma Loop_Invariant (Ptr.all = Ptr.all'Loop_Entry);
 347          pragma Loop_Invariant (P in Ptr.all .. Max);
 348          pragma Loop_Invariant (for some J in P .. Max => Str (J) /= ' ');
 349          pragma Loop_Invariant
 350            (for all J in Ptr.all .. P - 1 => Str (J) = ' ');
 351
 352          if P > Max then
 353             Ptr.all := P;
 354             Bad_Value (Str);
 355          end if;
 356       end loop;
 357
 358       Start := P;
 359
 360       pragma Assert (Start = First_Non_Space_Ghost (Str, Ptr.all, Max));
 361
 362       --  Remember an initial minus sign
 363
 364       if Str (P) = '-' then
 365          Minus := True;
 366          P := P + 1;
 367
 368          if P > Max then
 369             Ptr.all := Start;
 370             Bad_Value (Str);
 371          end if;
 372
 373       --  Skip past an initial plus sign
 374
 375       elsif Str (P) = '+' then
 376          Minus := False;
 377          P := P + 1;
 378
 379          if P > Max then
 380             Ptr.all := Start;
 381             Bad_Value (Str);
 382          end if;
 383
 384       else
 385          Minus := False;
 386       end if;
 387
 388       Ptr.all := P;
 389    end Scan_Sign;
 390
 391    --------------------------
 392    -- Scan_Trailing_Blanks --
 393    --------------------------
 394
 395    procedure Scan_Trailing_Blanks (Str : String; P : Positive) is
 396    begin
 397       for J in P .. Str'Last loop
 398          if Str (J) /= ' ' then
 399             Bad_Value (Str);
 400          end if;
 401
 402          pragma Loop_Invariant (for all K in P .. J => Str (K) = ' ');
 403       end loop;
 404    end Scan_Trailing_Blanks;
 405
 406    ---------------------
 407    -- Scan_Underscore --
 408    ---------------------
 409
 410    procedure Scan_Underscore
 411      (Str : String;
 412       P   : in out Natural;
 413       Ptr : not null access Integer;
 414       Max : Integer;
 415       Ext : Boolean)
 416    is
 417       C : Character;
 418
 419    begin
 420       P := P + 1;
 421
 422       --  If underscore is at the end of string, then this is an error and we
 423       --  raise Constraint_Error, leaving the pointer past the underscore. This
 424       --  seems a bit strange. It means e.g. that if the field is:
 425
 426       --    345_
 427
 428       --  that Constraint_Error is raised. You might think that the RM in this
 429       --  case would scan out the 345 as a valid integer, leaving the pointer
 430       --  at the underscore, but the ACVC suite clearly requires an error in
 431       --  this situation (see for example CE3704M).
 432
 433       if P > Max then
 434          Ptr.all := P;
 435          Bad_Value (Str);
 436       end if;
 437
 438       --  Similarly, if no digit follows the underscore raise an error. This
 439       --  also catches the case of double underscore which is also an error.
 440
 441       C := Str (P);
 442
 443       if C in '0' .. '9'
 444         or else (Ext and then (C in 'A' .. 'F' or else C in 'a' .. 'f'))
 445       then
 446          return;
 447       else
 448          Ptr.all := P;
 449          Bad_Value (Str);
 450       end if;
 451    end Scan_Underscore;
 452
 453 end System.Val_Util;