gcc/ada/libgnat/s-valueu.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT COMPILER COMPONENTS                         --
   4 --                                                                          --
   5 --                       S Y S T E M . V A L U E _ U                        --
   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 package body System.Value_U is
  33
  34    --  Ghost code, loop invariants and assertions in this unit are meant for
  35    --  analysis only, not for run-time checking, as it would be too costly
  36    --  otherwise. This is enforced by setting the assertion policy to Ignore.
  37
  38    pragma Assertion_Policy (Ghost              => Ignore,
  39                             Loop_Invariant     => Ignore,
  40                             Assert             => Ignore,
  41                             Assert_And_Cut     => Ignore,
  42                             Subprogram_Variant => Ignore);
  43
  44    use type Spec.Uns_Option;
  45    use type Spec.Split_Value_Ghost;
  46
  47    --  Local lemmas
  48
  49    procedure Lemma_Digit_Not_Last
  50      (Str  : String;
  51       P    : Integer;
  52       From : Integer;
  53       To   : Integer)
  54    with Ghost,
  55      Pre  => Str'Last /= Positive'Last
  56        and then From in Str'Range
  57        and then To in From .. Str'Last
  58        and then Str (From) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
  59        and then P in From .. To
  60        and then P <= Spec.Last_Hexa_Ghost (Str (From .. To)) + 1
  61        and then Spec.Is_Based_Format_Ghost (Str (From .. To)),
  62      Post =>
  63        (if Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
  64         then P <= Spec.Last_Hexa_Ghost (Str (From .. To)));
  65
  66    procedure Lemma_Underscore_Not_Last
  67      (Str  : String;
  68       P    : Integer;
  69       From : Integer;
  70       To   : Integer)
  71    with Ghost,
  72      Pre  => Str'Last /= Positive'Last
  73        and then From in Str'Range
  74        and then To in From .. Str'Last
  75        and then Str (From) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
  76        and then P in From .. To
  77        and then Str (P) = '_'
  78        and then P <= Spec.Last_Hexa_Ghost (Str (From .. To)) + 1
  79        and then Spec.Is_Based_Format_Ghost (Str (From .. To)),
  80      Post => P + 1 <= Spec.Last_Hexa_Ghost (Str (From .. To))
  81        and then Str (P + 1) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
  82
  83    -----------------------------
  84    -- Local lemma null bodies --
  85    -----------------------------
  86
  87    procedure Lemma_Digit_Not_Last
  88      (Str  : String;
  89       P    : Integer;
  90       From : Integer;
  91       To   : Integer)
  92    is null;
  93
  94    procedure Lemma_Underscore_Not_Last
  95      (Str  : String;
  96       P    : Integer;
  97       From : Integer;
  98       To   : Integer)
  99    is null;
 100
 101    -----------------------
 102    -- Scan_Raw_Unsigned --
 103    -----------------------
 104
 105    procedure Scan_Raw_Unsigned
 106      (Str : String;
 107       Ptr : not null access Integer;
 108       Max : Integer;
 109       Res : out Uns)
 110    is
 111       P : Integer;
 112       --  Local copy of the pointer
 113
 114       Uval : Uns;
 115       --  Accumulated unsigned integer result
 116
 117       Expon : Integer;
 118       --  Exponent value
 119
 120       Overflow : Boolean := False;
 121       --  Set True if overflow is detected at any point
 122
 123       Base_Char : Character;
 124       --  Base character (# or :) in based case
 125
 126       Base : Uns := 10;
 127       --  Base value (reset in based case)
 128
 129       Digit : Uns;
 130       --  Digit value
 131
 132       Ptr_Old       : constant Integer := Ptr.all
 133       with Ghost;
 134       Last_Num_Init : constant Integer :=
 135         Last_Number_Ghost (Str (Ptr.all .. Max))
 136       with Ghost;
 137       Init_Val      : constant Spec.Uns_Option :=
 138         Spec.Scan_Based_Number_Ghost (Str, Ptr.all, Last_Num_Init)
 139       with Ghost;
 140       Starts_As_Based : constant Boolean :=
 141         Last_Num_Init < Max - 1
 142         and then Str (Last_Num_Init + 1) in '#' | ':'
 143         and then Str (Last_Num_Init + 2) in
 144         '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
 145       with Ghost;
 146       Last_Num_Based  : constant Integer :=
 147         (if Starts_As_Based
 148          then Spec.Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Max))
 149          else Last_Num_Init)
 150       with Ghost;
 151       Is_Based        : constant Boolean :=
 152         Starts_As_Based
 153         and then Last_Num_Based < Max
 154         and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1)
 155       with Ghost;
 156       Based_Val       : constant Spec.Uns_Option :=
 157         (if Starts_As_Based and then not Init_Val.Overflow
 158          then Spec.Scan_Based_Number_Ghost
 159            (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
 160          else Init_Val)
 161       with Ghost;
 162       First_Exp       : constant Integer :=
 163         (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1)
 164       with Ghost;
 165
 166    begin
 167       --  We do not tolerate strings with Str'Last = Positive'Last
 168
 169       if Str'Last = Positive'Last then
 170          raise Program_Error with
 171            "string upper bound is Positive'Last, not supported";
 172       end if;
 173
 174       P := Ptr.all;
 175       Spec.Lemma_Scan_Based_Number_Ghost_Step (Str, P, Last_Num_Init);
 176       Uval := Character'Pos (Str (P)) - Character'Pos ('0');
 177       P := P + 1;
 178
 179       --  Scan out digits of what is either the number or the base.
 180       --  In either case, we are definitely scanning out in base 10.
 181
 182       declare
 183          Umax : constant Uns := (Uns'Last - 9) / 10;
 184          --  Max value which cannot overflow on accumulating next digit
 185
 186          Umax10 : constant Uns := Uns'Last / 10;
 187          --  Numbers bigger than Umax10 overflow if multiplied by 10
 188
 189       begin
 190          --  Loop through decimal digits
 191          loop
 192             pragma Loop_Invariant (P in P'Loop_Entry .. Last_Num_Init + 1);
 193             pragma Loop_Invariant
 194               (if Overflow then Init_Val.Overflow);
 195             pragma Loop_Invariant
 196               (if not Overflow
 197                then Init_Val = Spec.Scan_Based_Number_Ghost
 198                  (Str, P, Last_Num_Init, Acc => Uval));
 199
 200             exit when P > Max;
 201
 202             Digit := Character'Pos (Str (P)) - Character'Pos ('0');
 203
 204             --  Non-digit encountered
 205
 206             if Digit > 9 then
 207                if Str (P) = '_' then
 208                   Spec.Lemma_Scan_Based_Number_Ghost_Underscore
 209                     (Str, P, Last_Num_Init, Acc => Uval);
 210                   Scan_Underscore (Str, P, Ptr, Max, False);
 211                else
 212                   exit;
 213                end if;
 214
 215             --  Accumulate result, checking for overflow
 216
 217             else
 218                Spec.Lemma_Scan_Based_Number_Ghost_Step
 219                  (Str, P, Last_Num_Init, Acc => Uval);
 220                Spec.Lemma_Scan_Based_Number_Ghost_Overflow
 221                  (Str, P, Last_Num_Init, Acc => Uval);
 222
 223                if Uval <= Umax then
 224                   pragma Assert
 225                     (Spec.Hexa_To_Unsigned_Ghost (Str (P)) = Digit);
 226                   Uval := 10 * Uval + Digit;
 227                   pragma Assert
 228                     (if not Overflow
 229                      then Init_Val = Spec.Scan_Based_Number_Ghost
 230                        (Str, P + 1, Last_Num_Init, Acc => Uval));
 231
 232                elsif Uval > Umax10 then
 233                   Overflow := True;
 234
 235                else
 236                   Uval := 10 * Uval + Digit;
 237
 238                   if Uval < Umax10 then
 239                      Overflow := True;
 240                   end if;
 241                   pragma Assert
 242                     (if not Overflow
 243                      then Init_Val = Spec.Scan_Based_Number_Ghost
 244                        (Str, P + 1, Last_Num_Init, Acc => Uval));
 245                end if;
 246
 247                P := P + 1;
 248             end if;
 249          end loop;
 250          Spec.Lemma_Scan_Based_Number_Ghost_Base
 251             (Str, P, Last_Num_Init, Acc => Uval);
 252       end;
 253
 254       pragma Assert_And_Cut
 255         (P = Last_Num_Init + 1
 256          and then Overflow = Init_Val.Overflow
 257          and then (if not Overflow then Init_Val.Value = Uval));
 258
 259       Ptr.all := P;
 260
 261       --  Deal with based case. We recognize either the standard '#' or the
 262       --  allowed alternative replacement ':' (see RM J.2(3)).
 263
 264       if P < Max and then (Str (P) = '#' or else Str (P) = ':') then
 265          Base_Char := Str (P);
 266          P := P + 1;
 267          Base := Uval;
 268          Uval := 0;
 269
 270          --  Check base value. Overflow is set True if we find a bad base, or
 271          --  a digit that is out of range of the base. That way, we scan out
 272          --  the numeral that is still syntactically correct, though illegal.
 273          --  We use a safe base of 16 for this scan, to avoid zero divide.
 274
 275          if Base not in 2 .. 16 then
 276             Overflow := True;
 277             Base := 16;
 278          end if;
 279
 280          --  Scan out based integer
 281
 282          declare
 283             Umax : constant Uns := (Uns'Last - Base + 1) / Base;
 284             --  Max value which cannot overflow on accumulating next digit
 285
 286             UmaxB : constant Uns := Uns'Last / Base;
 287             --  Numbers bigger than UmaxB overflow if multiplied by base
 288
 289          begin
 290             pragma Assert
 291               (if Str (P) in '0' .. '9' | 'A' .. 'F' | 'a' .. 'f'
 292                then Spec.Is_Based_Format_Ghost (Str (P .. Max)));
 293
 294             --  Loop to scan out based integer value
 295
 296             loop
 297                --  We require a digit at this stage
 298
 299                if Str (P) in '0' .. '9' then
 300                   Digit := Character'Pos (Str (P)) - Character'Pos ('0');
 301
 302                elsif Str (P) in 'A' .. 'F' then
 303                   Digit :=
 304                     Character'Pos (Str (P)) - (Character'Pos ('A') - 10);
 305
 306                elsif Str (P) in 'a' .. 'f' then
 307                   Digit :=
 308                     Character'Pos (Str (P)) - (Character'Pos ('a') - 10);
 309
 310                --  If we don't have a digit, then this is not a based number
 311                --  after all, so we use the value we scanned out as the base
 312                --  (now in Base), and the pointer to the base character was
 313                --  already stored in Ptr.all.
 314
 315                else
 316                   Spec.Lemma_Scan_Based_Number_Ghost_Base
 317                     (Str, P, Last_Num_Based, Base, Uval);
 318                   Uval := Base;
 319                   Base := 10;
 320                   pragma Assert (Ptr.all = Last_Num_Init + 1);
 321                   pragma Assert
 322                     (if Starts_As_Based then P = Last_Num_Based + 1);
 323                   pragma Assert (not Is_Based);
 324                   pragma Assert (if not Overflow then Uval = Init_Val.Value);
 325                   exit;
 326                end if;
 327
 328                pragma Loop_Invariant (P in P'Loop_Entry .. Last_Num_Based);
 329                pragma Loop_Invariant
 330                  (Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
 331                   and then Digit = Spec.Hexa_To_Unsigned_Ghost (Str (P)));
 332                pragma Loop_Invariant
 333                  (if Overflow'Loop_Entry then Overflow);
 334                pragma Loop_Invariant
 335                  (if Overflow then
 336                     (Overflow'Loop_Entry or else Based_Val.Overflow));
 337                pragma Loop_Invariant
 338                  (if not Overflow
 339                   then Based_Val = Spec.Scan_Based_Number_Ghost
 340                     (Str, P, Last_Num_Based, Base, Uval));
 341                pragma Loop_Invariant (Ptr.all = Last_Num_Init + 1);
 342
 343                Spec.Lemma_Scan_Based_Number_Ghost_Step
 344                  (Str, P, Last_Num_Based, Base, Uval);
 345                Spec.Lemma_Scan_Based_Number_Ghost_Overflow
 346                  (Str, P, Last_Num_Based, Base, Uval);
 347
 348                --  If digit is too large, just signal overflow and continue.
 349                --  The idea here is to keep scanning as long as the input is
 350                --  syntactically valid, even if we have detected overflow
 351
 352                if Digit >= Base then
 353                   Overflow := True;
 354
 355                --  Here we accumulate the value, checking overflow
 356
 357                elsif Uval <= Umax then
 358                   Uval := Base * Uval + Digit;
 359                   pragma Assert
 360                     (if not Overflow
 361                      then Based_Val = Spec.Scan_Based_Number_Ghost
 362                        (Str, P + 1, Last_Num_Based, Base, Uval));
 363
 364                elsif Uval > UmaxB then
 365                   Overflow := True;
 366
 367                else
 368                   Uval := Base * Uval + Digit;
 369
 370                   if Uval < UmaxB then
 371                      Overflow := True;
 372                   end if;
 373                   pragma Assert
 374                     (if not Overflow
 375                      then Based_Val = Spec.Scan_Based_Number_Ghost
 376                        (Str, P + 1, Last_Num_Based, Base, Uval));
 377                end if;
 378
 379                --  If at end of string with no base char, not a based number
 380                --  but we signal Constraint_Error and set the pointer past
 381                --  the end of the field, since this is what the ACVC tests
 382                --  seem to require, see CE3704N, line 204.
 383
 384                P := P + 1;
 385
 386                if P > Max then
 387                   Ptr.all := P;
 388                   Bad_Value (Str);
 389                end if;
 390
 391                --  If terminating base character, we are done with loop
 392
 393                if Str (P) = Base_Char then
 394                   Ptr.all := P + 1;
 395                   pragma Assert (P = Last_Num_Based + 1);
 396                   pragma Assert (Ptr.all = Last_Num_Based + 2);
 397                   pragma Assert (Starts_As_Based);
 398                   pragma Assert (Last_Num_Based < Max);
 399                   pragma Assert (Str (Last_Num_Based + 1) = Base_Char);
 400                   pragma Assert (Base_Char = Str (Last_Num_Init + 1));
 401                   pragma Assert (Is_Based);
 402                   Spec.Lemma_Scan_Based_Number_Ghost_Base
 403                     (Str, P, Last_Num_Based, Base, Uval);
 404                   exit;
 405
 406                --  Deal with underscore
 407
 408                elsif Str (P) = '_' then
 409                   Lemma_Underscore_Not_Last (Str, P, Last_Num_Init + 2, Max);
 410                   Spec.Lemma_Scan_Based_Number_Ghost_Underscore
 411                     (Str, P, Last_Num_Based, Base, Uval);
 412                   Scan_Underscore (Str, P, Ptr, Max, True);
 413                   pragma Assert
 414                     (if not Overflow
 415                      then Based_Val = Spec.Scan_Based_Number_Ghost
 416                        (Str, P, Last_Num_Based, Base, Uval));
 417                   pragma Assert (Str (P) /= '_');
 418                   pragma Assert (Str (P) /= Base_Char);
 419                end if;
 420
 421                Lemma_Digit_Not_Last (Str, P, Last_Num_Init + 2, Max);
 422                pragma Assert (Str (P) /= '_');
 423                pragma Assert (Str (P) /= Base_Char);
 424             end loop;
 425          end;
 426          pragma Assert
 427            (if Starts_As_Based then P = Last_Num_Based + 1
 428             else P = Last_Num_Init + 2);
 429          pragma Assert
 430            (Last_Num_Init < Max - 1
 431             and then Str (Last_Num_Init + 1) in '#' | ':');
 432          pragma Assert
 433            (Overflow =
 434               (Init_Val.Overflow
 435                or else Init_Val.Value not in 2 .. 16
 436                or else (Starts_As_Based and then Based_Val.Overflow)));
 437          pragma Assert
 438            (Overflow /= Spec.Scan_Split_No_Overflow_Ghost (Str, Ptr_Old, Max));
 439       end if;
 440
 441       pragma Assert_And_Cut
 442         (Overflow /= Spec.Scan_Split_No_Overflow_Ghost (Str, Ptr_Old, Max)
 443          and then
 444            (if not Overflow then
 445                 (if Is_Based then Uval = Based_Val.Value
 446                  else Uval = Init_Val.Value))
 447          and then Ptr.all = First_Exp
 448          and then Base in 2 .. 16
 449          and then
 450            (if not Overflow then
 451                 (if Is_Based then Base = Init_Val.Value else Base = 10)));
 452
 453       --  Come here with scanned unsigned value in Uval. The only remaining
 454       --  required step is to deal with exponent if one is present.
 455
 456       Scan_Exponent (Str, Ptr, Max, Expon);
 457
 458       pragma Assert
 459         (Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Ptr_Old, Max));
 460       pragma Assert
 461         (if not Overflow
 462          then Spec.Scan_Split_Value_Ghost (Str, Ptr_Old, Max) =
 463            (Uval, Base, Expon));
 464
 465       if Expon /= 0 and then Uval /= 0 then
 466
 467          --  For non-zero value, scale by exponent value. No need to do this
 468          --  efficiently, since use of exponent in integer literals is rare,
 469          --  and in any case the exponent cannot be very large.
 470
 471          declare
 472             UmaxB : constant Uns := Uns'Last / Base;
 473             --  Numbers bigger than UmaxB overflow if multiplied by base
 474
 475             Res_Val : constant Spec.Uns_Option :=
 476               Spec.Exponent_Unsigned_Ghost (Uval, Expon, Base)
 477             with Ghost;
 478          begin
 479             for J in 1 .. Expon loop
 480                pragma Loop_Invariant
 481                  (if Overflow'Loop_Entry then Overflow);
 482                pragma Loop_Invariant
 483                  (if Overflow
 484                   then Overflow'Loop_Entry or else Res_Val.Overflow);
 485                pragma Loop_Invariant (Uval /= 0);
 486                pragma Loop_Invariant
 487                  (if not Overflow
 488                   then Res_Val = Spec.Exponent_Unsigned_Ghost
 489                     (Uval, Expon - J + 1, Base));
 490
 491                pragma Assert
 492                  ((Uval > UmaxB) = Spec.Scan_Overflows_Ghost (0, Base, Uval));
 493
 494                if Uval > UmaxB then
 495                   Spec.Lemma_Exponent_Unsigned_Ghost_Overflow
 496                      (Uval, Expon - J + 1, Base);
 497                   Overflow := True;
 498                   exit;
 499                end if;
 500
 501                Spec.Lemma_Exponent_Unsigned_Ghost_Step
 502                   (Uval, Expon - J + 1, Base);
 503
 504                Uval := Uval * Base;
 505             end loop;
 506             Spec.Lemma_Exponent_Unsigned_Ghost_Base (Uval, 0, Base);
 507
 508             pragma Assert
 509               (Overflow /=
 510                  Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Ptr_Old, Max));
 511             pragma Assert (if not Overflow then Res_Val = (False, Uval));
 512          end;
 513       end if;
 514       Spec.Lemma_Exponent_Unsigned_Ghost_Base (Uval, Expon, Base);
 515       pragma Assert
 516         (if Expon = 0 or else Uval = 0 then
 517             Spec.Exponent_Unsigned_Ghost (Uval, Expon, Base) = (False, Uval));
 518       pragma Assert
 519         (Overflow /=
 520            Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Ptr_Old, Max));
 521       pragma Assert
 522         (if not Overflow then
 523             Uval = Spec.Scan_Raw_Unsigned_Ghost (Str, Ptr_Old, Max));
 524
 525       --  Return result, dealing with overflow
 526
 527       if Overflow then
 528          Bad_Value (Str);
 529          pragma Annotate
 530            (GNATprove, Intentional,
 531             "call to nonreturning subprogram might be executed",
 532             "it is expected that Constraint_Error is raised in case of"
 533             & " overflow");
 534       else
 535          Res := Uval;
 536       end if;
 537    end Scan_Raw_Unsigned;
 538
 539    -------------------
 540    -- Scan_Unsigned --
 541    -------------------
 542
 543    procedure Scan_Unsigned
 544      (Str : String;
 545       Ptr : not null access Integer;
 546       Max : Integer;
 547       Res : out Uns)
 548    is
 549       Start : Positive;
 550       --  Save location of first non-blank character
 551
 552    begin
 553       pragma Warnings
 554         (Off,
 555          """Start"" is set by ""Scan_Plus_Sign"" but not used after the call");
 556       Scan_Plus_Sign (Str, Ptr, Max, Start);
 557       pragma Warnings
 558         (On,
 559          """Start"" is set by ""Scan_Plus_Sign"" but not used after the call");
 560
 561       if Str (Ptr.all) not in '0' .. '9' then
 562          Ptr.all := Start;
 563          Bad_Value (Str);
 564       end if;
 565
 566       Scan_Raw_Unsigned (Str, Ptr, Max, Res);
 567    end Scan_Unsigned;
 568
 569    --------------------
 570    -- Value_Unsigned --
 571    --------------------
 572
 573    function Value_Unsigned (Str : String) return Uns is
 574    begin
 575       --  We have to special case Str'Last = Positive'Last because the normal
 576       --  circuit ends up setting P to Str'Last + 1 which is out of bounds. We
 577       --  deal with this by converting to a subtype which fixes the bounds.
 578
 579       if Str'Last = Positive'Last then
 580          declare
 581             subtype NT is String (1 .. Str'Length);
 582             procedure Prove_Is_Unsigned_Ghost with
 583               Ghost,
 584               Pre  => Str'Length < Natural'Last
 585               and then not Only_Space_Ghost (Str, Str'First, Str'Last)
 586               and then Spec.Is_Unsigned_Ghost (Spec.Slide_To_1 (Str)),
 587               Post => Spec.Is_Unsigned_Ghost (NT (Str));
 588             procedure Prove_Is_Unsigned_Ghost is null;
 589          begin
 590             Prove_Is_Unsigned_Ghost;
 591             return Value_Unsigned (NT (Str));
 592          end;
 593
 594       --  Normal case where Str'Last < Positive'Last
 595
 596       else
 597          declare
 598             V : Uns;
 599             P : aliased Integer := Str'First;
 600             Non_Blank : constant Positive := First_Non_Space_Ghost
 601               (Str, Str'First, Str'Last)
 602             with Ghost;
 603             Fst_Num   : constant Positive :=
 604               (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank)
 605             with Ghost;
 606          begin
 607             declare
 608                P_Acc : constant not null access Integer := P'Access;
 609             begin
 610                Scan_Unsigned (Str, P_Acc, Str'Last, V);
 611             end;
 612
 613             pragma Assert
 614               (P = Spec.Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last));
 615             pragma Assert
 616               (V = Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last));
 617
 618             Scan_Trailing_Blanks (Str, P);
 619
 620             pragma Assert
 621               (Spec.Is_Value_Unsigned_Ghost
 622                  (Spec.Slide_If_Necessary (Str), V));
 623             return V;
 624          end;
 625       end if;
 626    end Value_Unsigned;
 627
 628 end System.Value_U;