gcc/ada/libgnat/s-vauspe.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT COMPILER COMPONENTS                         --
   4 --                                                                          --
   5 --                   S Y S T E M . V A L U E _ U _ S P E C                  --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 --          Copyright (C) 2022-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 --  This package contains the specification entities using for the formal
  33 --  verification of the routines for scanning modular Unsigned values.
  34
  35 --  Preconditions in this unit are meant for analysis only, not for run-time
  36 --  checking, so that the expected exceptions are raised. This is enforced by
  37 --  setting the corresponding assertion policy to Ignore. Postconditions and
  38 --  contract cases should not be executed at runtime as well, in order not to
  39 --  slow down the execution of these functions.
  40
  41 pragma Assertion_Policy (Pre                => Ignore,
  42                          Post               => Ignore,
  43                          Contract_Cases     => Ignore,
  44                          Ghost              => Ignore,
  45                          Subprogram_Variant => Ignore);
  46
  47 with System.Val_Util; use System.Val_Util;
  48
  49 generic
  50
  51    type Uns is mod <>;
  52
  53 package System.Value_U_Spec with
  54    Ghost,
  55    SPARK_Mode,
  56    Annotate => (GNATprove, Always_Return)
  57 is
  58    pragma Preelaborate;
  59
  60    type Uns_Option (Overflow : Boolean := False) is record
  61       case Overflow is
  62          when True =>
  63             null;
  64          when False =>
  65             Value : Uns := 0;
  66       end case;
  67    end record;
  68
  69    function Wrap_Option (Value : Uns) return Uns_Option is
  70      (Overflow => False, Value => Value);
  71
  72    function Only_Decimal_Ghost
  73      (Str      : String;
  74       From, To : Integer)
  75       return Boolean
  76    is
  77       (for all J in From .. To => Str (J) in '0' .. '9')
  78    with
  79      Pre => From > To or else (From >= Str'First and then To <= Str'Last);
  80    --  Ghost function that returns True if S has only decimal characters
  81    --  from index From to index To.
  82
  83    function Only_Hexa_Ghost (Str : String; From, To : Integer) return Boolean
  84    is
  85       (for all J in From .. To =>
  86           Str (J) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_')
  87    with
  88      Pre => From > To or else (From >= Str'First and then To <= Str'Last);
  89    --  Ghost function that returns True if S has only hexadecimal characters
  90    --  from index From to index To.
  91
  92    function Last_Hexa_Ghost (Str : String) return Positive
  93    with
  94      Pre  => Str /= ""
  95        and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F',
  96      Post => Last_Hexa_Ghost'Result in Str'Range
  97        and then (if Last_Hexa_Ghost'Result < Str'Last then
  98                    Str (Last_Hexa_Ghost'Result + 1) not in
  99                      '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_')
 100        and then Only_Hexa_Ghost (Str, Str'First, Last_Hexa_Ghost'Result);
 101    --  Ghost function that returns the index of the last character in S that
 102    --  is either an hexadecimal digit or an underscore, which necessarily
 103    --  exists given the precondition on Str.
 104
 105    function Is_Based_Format_Ghost (Str : String) return Boolean
 106    is
 107      (Str /= ""
 108         and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
 109         and then
 110         (declare
 111            L : constant Positive := Last_Hexa_Ghost (Str);
 112          begin
 113            Str (L) /= '_'
 114              and then (for all J in Str'First .. L =>
 115                          (if Str (J) = '_' then Str (J + 1) /= '_'))));
 116    --  Ghost function that determines if Str has the correct format for a
 117    --  based number, consisting in a sequence of hexadecimal digits possibly
 118    --  separated by single underscores. It may be followed by other characters.
 119
 120    function Hexa_To_Unsigned_Ghost (X : Character) return Uns is
 121      (case X is
 122          when '0' .. '9' => Character'Pos (X) - Character'Pos ('0'),
 123          when 'a' .. 'f' => Character'Pos (X) - Character'Pos ('a') + 10,
 124          when 'A' .. 'F' => Character'Pos (X) - Character'Pos ('A') + 10,
 125          when others     => raise Program_Error)
 126    with
 127      Pre => X in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
 128    --  Ghost function that computes the value corresponding to an hexadecimal
 129    --  digit.
 130
 131    function Scan_Overflows_Ghost
 132      (Digit : Uns;
 133       Base  : Uns;
 134       Acc   : Uns) return Boolean
 135    is
 136      (Digit >= Base
 137       or else Acc > Uns'Last / Base
 138       or else Uns'Last - Digit < Base * Acc);
 139    --  Ghost function which returns True if Digit + Base * Acc overflows or
 140    --  Digit is greater than Base, as this is used by the algorithm for the
 141    --  test of overflow.
 142
 143    function Scan_Based_Number_Ghost
 144      (Str      : String;
 145       From, To : Integer;
 146       Base     : Uns := 10;
 147       Acc      : Uns := 0) return Uns_Option
 148    with
 149      Subprogram_Variant => (Increases => From),
 150      Pre  => Str'Last /= Positive'Last
 151          and then
 152            (From > To or else (From >= Str'First and then To <= Str'Last))
 153          and then Only_Hexa_Ghost (Str, From, To);
 154    --  Ghost function that recursively computes the based number in Str,
 155    --  assuming Acc has been scanned already and scanning continues at index
 156    --  From.
 157
 158    --  Lemmas unfolding the recursive definition of Scan_Based_Number_Ghost
 159
 160    procedure Lemma_Scan_Based_Number_Ghost_Base
 161      (Str      : String;
 162       From, To : Integer;
 163       Base     : Uns := 10;
 164       Acc      : Uns := 0)
 165    with
 166      Global => null,
 167      Pre  => Str'Last /= Positive'Last
 168          and then
 169            (From > To or else (From >= Str'First and then To <= Str'Last))
 170          and then Only_Hexa_Ghost (Str, From, To),
 171      Post =>
 172       (if From > To
 173        then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) =
 174          (Overflow => False, Value => Acc));
 175    --  Base case: Scan_Based_Number_Ghost returns Acc if From is bigger than To
 176
 177    procedure Lemma_Scan_Based_Number_Ghost_Underscore
 178      (Str      : String;
 179       From, To : Integer;
 180       Base     : Uns := 10;
 181       Acc      : Uns := 0)
 182    with
 183      Global => null,
 184      Pre  => Str'Last /= Positive'Last
 185          and then
 186            (From > To or else (From >= Str'First and then To <= Str'Last))
 187          and then Only_Hexa_Ghost (Str, From, To),
 188      Post =>
 189       (if From <= To and then Str (From) = '_'
 190        then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) =
 191            Scan_Based_Number_Ghost (Str, From + 1, To, Base, Acc));
 192    --  Underscore case: underscores are ignored while scanning
 193
 194    procedure Lemma_Scan_Based_Number_Ghost_Overflow
 195      (Str      : String;
 196       From, To : Integer;
 197       Base     : Uns := 10;
 198       Acc      : Uns := 0)
 199    with
 200      Global => null,
 201      Pre  => Str'Last /= Positive'Last
 202          and then
 203            (From > To or else (From >= Str'First and then To <= Str'Last))
 204          and then Only_Hexa_Ghost (Str, From, To),
 205      Post =>
 206       (if From <= To
 207          and then Str (From) /= '_'
 208          and then Scan_Overflows_Ghost
 209            (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc)
 210        then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) =
 211            (Overflow => True));
 212    --  Overflow case: scanning a digit which causes an overflow
 213
 214    procedure Lemma_Scan_Based_Number_Ghost_Step
 215      (Str      : String;
 216       From, To : Integer;
 217       Base     : Uns := 10;
 218       Acc      : Uns := 0)
 219    with
 220      Global => null,
 221      Pre  => Str'Last /= Positive'Last
 222          and then
 223            (From > To or else (From >= Str'First and then To <= Str'Last))
 224          and then Only_Hexa_Ghost (Str, From, To),
 225      Post =>
 226       (if From <= To
 227          and then Str (From) /= '_'
 228          and then not Scan_Overflows_Ghost
 229            (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc)
 230        then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) =
 231          Scan_Based_Number_Ghost
 232            (Str, From + 1, To, Base,
 233             Base * Acc + Hexa_To_Unsigned_Ghost (Str (From))));
 234    --  Normal case: scanning a digit without overflows
 235
 236    function Exponent_Unsigned_Ghost
 237      (Value : Uns;
 238       Exp   : Natural;
 239       Base  : Uns := 10) return Uns_Option
 240    with
 241      Subprogram_Variant => (Decreases => Exp);
 242    --  Ghost function that recursively computes Value * Base ** Exp
 243
 244    --  Lemmas unfolding the recursive definition of Exponent_Unsigned_Ghost
 245
 246    procedure Lemma_Exponent_Unsigned_Ghost_Base
 247      (Value : Uns;
 248       Exp   : Natural;
 249       Base  : Uns := 10)
 250    with
 251      Post =>
 252        (if Exp = 0 or Value = 0
 253         then Exponent_Unsigned_Ghost (Value, Exp, Base) =
 254           (Overflow => False, Value => Value));
 255    --  Base case: Exponent_Unsigned_Ghost returns 0 if Value or Exp is 0
 256
 257    procedure Lemma_Exponent_Unsigned_Ghost_Overflow
 258      (Value : Uns;
 259       Exp   : Natural;
 260       Base  : Uns := 10)
 261    with
 262      Post =>
 263        (if Exp /= 0
 264           and then Value /= 0
 265           and then Scan_Overflows_Ghost (0, Base, Value)
 266         then Exponent_Unsigned_Ghost (Value, Exp, Base) = (Overflow => True));
 267    --  Overflow case: the next multiplication overflows
 268
 269    procedure Lemma_Exponent_Unsigned_Ghost_Step
 270      (Value : Uns;
 271       Exp   : Natural;
 272       Base  : Uns := 10)
 273    with
 274      Post =>
 275        (if Exp /= 0
 276           and then Value /= 0
 277           and then not Scan_Overflows_Ghost (0, Base, Value)
 278         then Exponent_Unsigned_Ghost (Value, Exp, Base) =
 279             Exponent_Unsigned_Ghost (Value * Base, Exp - 1, Base));
 280    --  Normal case: exponentiation without overflows
 281
 282    function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean is
 283      (Is_Natural_Format_Ghost (Str)
 284       and then
 285         (declare
 286            Last_Num_Init   : constant Integer := Last_Number_Ghost (Str);
 287            Starts_As_Based : constant Boolean :=
 288              Last_Num_Init < Str'Last - 1
 289              and then Str (Last_Num_Init + 1) in '#' | ':'
 290              and then Str (Last_Num_Init + 2) in
 291                '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
 292            Last_Num_Based  : constant Integer :=
 293              (if Starts_As_Based
 294               then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Str'Last))
 295               else Last_Num_Init);
 296            Is_Based        : constant Boolean :=
 297              Starts_As_Based
 298              and then Last_Num_Based < Str'Last
 299              and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
 300            First_Exp       : constant Integer :=
 301              (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
 302          begin
 303            (if Starts_As_Based then
 304               Is_Based_Format_Ghost (Str (Last_Num_Init + 2 .. Str'Last))
 305               and then Last_Num_Based < Str'Last)
 306             and then Is_Opt_Exponent_Format_Ghost
 307               (Str (First_Exp .. Str'Last))))
 308    with
 309      Pre  => Str'Last /= Positive'Last;
 310    --  Ghost function that determines if Str has the correct format for an
 311    --  unsigned number without a sign character.
 312    --  It is a natural number in base 10, optionally followed by a based
 313    --  number surrounded by delimiters # or :, optionally followed by an
 314    --  exponent part.
 315
 316    type Split_Value_Ghost is record
 317       Value : Uns;
 318       Base  : Uns;
 319       Expon : Natural;
 320    end record;
 321
 322    function Scan_Split_No_Overflow_Ghost
 323      (Str      : String;
 324       From, To : Integer)
 325       return Boolean
 326    is
 327      (declare
 328         Last_Num_Init   : constant Integer :=
 329           Last_Number_Ghost (Str (From .. To));
 330         Init_Val        : constant Uns_Option :=
 331           Scan_Based_Number_Ghost (Str, From, Last_Num_Init);
 332         Starts_As_Based : constant Boolean :=
 333           Last_Num_Init < To - 1
 334           and then Str (Last_Num_Init + 1) in '#' | ':'
 335           and then Str (Last_Num_Init + 2) in
 336           '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
 337         Last_Num_Based  : constant Integer :=
 338           (if Starts_As_Based
 339            then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
 340            else Last_Num_Init);
 341         Based_Val       : constant Uns_Option :=
 342           (if Starts_As_Based and then not Init_Val.Overflow
 343            then Scan_Based_Number_Ghost
 344              (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
 345            else Init_Val);
 346       begin
 347         not Init_Val.Overflow
 348         and then
 349           (Last_Num_Init >= To - 1
 350            or else Str (Last_Num_Init + 1) not in '#' | ':'
 351            or else Init_Val.Value in 2 .. 16)
 352         and then
 353           (not Starts_As_Based
 354            or else not Based_Val.Overflow))
 355    with
 356      Pre  => Str'Last /= Positive'Last
 357        and then From in Str'Range
 358        and then To in From .. Str'Last
 359        and then Str (From) in '0' .. '9';
 360    --  Ghost function that determines if an overflow might occur while scanning
 361    --  the representation of an unsigned number. The computation overflows if
 362    --  either:
 363    --    * The computation of the decimal part overflows,
 364    --    * The decimal part is followed by a valid delimiter for a based
 365    --      part, and the number corresponding to the base is not a valid base,
 366    --      or
 367    --    * The computation of the based part overflows.
 368
 369    pragma Warnings (Off, "constant * is not referenced");
 370    function Scan_Split_Value_Ghost
 371      (Str      : String;
 372       From, To : Integer)
 373       return Split_Value_Ghost
 374    is
 375      (declare
 376         Last_Num_Init   : constant Integer :=
 377           Last_Number_Ghost (Str (From .. To));
 378         Init_Val        : constant Uns_Option :=
 379           Scan_Based_Number_Ghost (Str, From, Last_Num_Init);
 380         Starts_As_Based : constant Boolean :=
 381           Last_Num_Init < To - 1
 382           and then Str (Last_Num_Init + 1) in '#' | ':'
 383           and then Str (Last_Num_Init + 2) in
 384           '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
 385         Last_Num_Based  : constant Integer :=
 386           (if Starts_As_Based
 387            then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
 388            else Last_Num_Init);
 389         Is_Based        : constant Boolean :=
 390           Starts_As_Based
 391           and then Last_Num_Based < To
 392           and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
 393         Based_Val       : constant Uns_Option :=
 394           (if Starts_As_Based and then not Init_Val.Overflow
 395            then Scan_Based_Number_Ghost
 396              (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
 397            else Init_Val);
 398         First_Exp       : constant Integer :=
 399           (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
 400         Expon           : constant Natural :=
 401           (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
 402            then Scan_Exponent_Ghost (Str (First_Exp .. To))
 403            else 0);
 404         Base            : constant Uns :=
 405           (if Is_Based then Init_Val.Value else 10);
 406         Value           : constant Uns :=
 407           (if Is_Based then Based_Val.Value else Init_Val.Value);
 408       begin
 409         (Value => Value, Base => Base, Expon => Expon))
 410    with
 411      Pre => Str'Last /= Positive'Last
 412        and then From in Str'Range
 413        and then To in From .. Str'Last
 414        and then Str (From) in '0' .. '9'
 415        and then Scan_Split_No_Overflow_Ghost (Str, From, To);
 416    --  Ghost function that scans an unsigned number without a sign character
 417    --  and return a record containing the values scanned for its value, its
 418    --  base, and its exponent.
 419    pragma Warnings (On, "constant * is not referenced");
 420
 421    function Raw_Unsigned_No_Overflow_Ghost
 422      (Str      : String;
 423       From, To : Integer)
 424       return Boolean
 425    is
 426      (Scan_Split_No_Overflow_Ghost (Str, From, To)
 427       and then
 428         (declare
 429            Val : constant Split_Value_Ghost := Scan_Split_Value_Ghost
 430              (Str, From, To);
 431          begin
 432            not Exponent_Unsigned_Ghost
 433              (Val.Value, Val.Expon, Val.Base).Overflow))
 434    with
 435      Pre => Str'Last /= Positive'Last
 436        and then From in Str'Range
 437        and then To in From .. Str'Last
 438        and then Str (From) in '0' .. '9';
 439    --  Ghost function that determines if the computation of the unsigned number
 440    --  represented by Str will overflow. The computation overflows if either:
 441    --    * The scan of the string overflows, or
 442    --    * The computation of the exponentiation overflows.
 443
 444    function Scan_Raw_Unsigned_Ghost
 445      (Str      : String;
 446       From, To : Integer)
 447       return Uns
 448    is
 449      (declare
 450         Val : constant Split_Value_Ghost := Scan_Split_Value_Ghost
 451           (Str, From, To);
 452       begin
 453         Exponent_Unsigned_Ghost (Val.Value, Val.Expon, Val.Base).Value)
 454    with
 455      Pre  => Str'Last /= Positive'Last
 456        and then From in Str'Range
 457        and then To in From .. Str'Last
 458        and then Str (From) in '0' .. '9'
 459        and then Raw_Unsigned_No_Overflow_Ghost (Str, From, To);
 460    --  Ghost function that scans an unsigned number without a sign character
 461
 462    function Raw_Unsigned_Last_Ghost
 463      (Str      : String;
 464       From, To : Integer)
 465       return Positive
 466    is
 467      (declare
 468         Last_Num_Init   : constant Integer :=
 469           Last_Number_Ghost (Str (From .. To));
 470         Starts_As_Based : constant Boolean :=
 471           Last_Num_Init < To - 1
 472           and then Str (Last_Num_Init + 1) in '#' | ':'
 473           and then Str (Last_Num_Init + 2) in
 474           '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
 475         Last_Num_Based  : constant Integer :=
 476           (if Starts_As_Based
 477            then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
 478            else Last_Num_Init);
 479         Is_Based        : constant Boolean :=
 480           Starts_As_Based
 481           and then Last_Num_Based < To
 482           and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
 483         First_Exp       : constant Integer :=
 484           (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
 485       begin
 486         (if not Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
 487          then First_Exp
 488          elsif Str (First_Exp + 1) in '-' | '+' then
 489            Last_Number_Ghost (Str (First_Exp + 2 .. To)) + 1
 490          else Last_Number_Ghost (Str (First_Exp + 1 .. To)) + 1))
 491    with
 492      Pre  => Str'Last /= Positive'Last
 493        and then From in Str'Range
 494        and then To in From .. Str'Last
 495        and then Str (From) in '0' .. '9';
 496    --  Ghost function that returns the position of the cursor once an unsigned
 497    --  number has been seen.
 498
 499    function Slide_To_1 (Str : String) return String
 500    with
 501      Post =>
 502        Only_Space_Ghost (Str, Str'First, Str'Last) =
 503        (for all J in Str'First .. Str'Last =>
 504           Slide_To_1'Result (J - Str'First + 1) = ' ');
 505    --  Slides Str so that it starts at 1
 506
 507    function Slide_If_Necessary (Str : String) return String is
 508      (if Str'Last = Positive'Last then Slide_To_1 (Str) else Str);
 509    --  If Str'Last = Positive'Last then slides Str so that it starts at 1
 510
 511    function Is_Unsigned_Ghost (Str : String) return Boolean is
 512      (declare
 513         Non_Blank : constant Positive := First_Non_Space_Ghost
 514           (Str, Str'First, Str'Last);
 515         Fst_Num   : constant Positive :=
 516           (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
 517       begin
 518         Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))
 519           and then Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last)
 520           and then Only_Space_Ghost
 521              (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last))
 522    with
 523        Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
 524        and then Str'Last /= Positive'Last;
 525    --  Ghost function that determines if Str has the correct format for an
 526    --  unsigned number, consisting in some blank characters, an optional
 527    --  + sign, a raw unsigned number which does not overflow and then some
 528    --  more blank characters.
 529
 530    function Is_Value_Unsigned_Ghost (Str : String; Val : Uns) return Boolean is
 531      (declare
 532         Non_Blank : constant Positive := First_Non_Space_Ghost
 533           (Str, Str'First, Str'Last);
 534         Fst_Num   : constant Positive :=
 535           (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
 536       begin
 537         Val = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last))
 538    with
 539        Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
 540        and then Str'Last /= Positive'Last
 541        and then Is_Unsigned_Ghost (Str);
 542    --  Ghost function that returns True if Val is the value corresponding to
 543    --  the unsigned number represented by Str.
 544
 545    procedure Prove_Scan_Based_Number_Ghost_Eq
 546      (Str1, Str2 : String;
 547       From, To : Integer;
 548       Base     : Uns := 10;
 549       Acc      : Uns := 0)
 550    with
 551      Subprogram_Variant => (Increases => From),
 552      Pre  => Str1'Last /= Positive'Last
 553        and then Str2'Last /= Positive'Last
 554        and then
 555          (From > To or else (From >= Str1'First and then To <= Str1'Last))
 556        and then
 557          (From > To or else (From >= Str2'First and then To <= Str2'Last))
 558        and then Only_Hexa_Ghost (Str1, From, To)
 559        and then (for all J in From .. To => Str1 (J) = Str2 (J)),
 560      Post =>
 561        Scan_Based_Number_Ghost (Str1, From, To, Base, Acc)
 562          = Scan_Based_Number_Ghost (Str2, From, To, Base, Acc);
 563    --  Scan_Based_Number_Ghost returns the same value on two slices which are
 564    --  equal.
 565
 566    procedure Prove_Scan_Only_Decimal_Ghost
 567      (Str : String;
 568       Val : Uns)
 569    with
 570      Pre  => Str'Last /= Positive'Last
 571        and then Str'Length >= 2
 572        and then Str (Str'First) = ' '
 573        and then Only_Decimal_Ghost (Str, Str'First + 1, Str'Last)
 574        and then Scan_Based_Number_Ghost (Str, Str'First + 1, Str'Last)
 575          = Wrap_Option (Val),
 576      Post => Is_Unsigned_Ghost (Slide_If_Necessary (Str))
 577        and then
 578          Is_Value_Unsigned_Ghost (Slide_If_Necessary (Str), Val);
 579    --  Ghost lemma used in the proof of 'Image implementation, to prove that
 580    --  the result of Value_Unsigned on a decimal string is the same as the
 581    --  result of Scan_Based_Number_Ghost.
 582
 583    --  Bundle Uns type with other types, constants and subprograms used in
 584    --  ghost code, so that this package can be instantiated once and used
 585    --  multiple times as generic formal for a given Int type.
 586
 587    package Uns_Params is new System.Val_Util.Uns_Params
 588      (Uns                                        => Uns,
 589       P_Uns_Option                               => Uns_Option,
 590       P_Wrap_Option                              => Wrap_Option,
 591       P_Hexa_To_Unsigned_Ghost                   => Hexa_To_Unsigned_Ghost,
 592       P_Scan_Overflows_Ghost                     => Scan_Overflows_Ghost,
 593       P_Is_Raw_Unsigned_Format_Ghost             =>
 594          Is_Raw_Unsigned_Format_Ghost,
 595       P_Scan_Split_No_Overflow_Ghost             =>
 596          Scan_Split_No_Overflow_Ghost,
 597       P_Raw_Unsigned_No_Overflow_Ghost           =>
 598          Raw_Unsigned_No_Overflow_Ghost,
 599       P_Exponent_Unsigned_Ghost                  => Exponent_Unsigned_Ghost,
 600       P_Lemma_Exponent_Unsigned_Ghost_Base       =>
 601          Lemma_Exponent_Unsigned_Ghost_Base,
 602       P_Lemma_Exponent_Unsigned_Ghost_Overflow   =>
 603          Lemma_Exponent_Unsigned_Ghost_Overflow,
 604       P_Lemma_Exponent_Unsigned_Ghost_Step       =>
 605          Lemma_Exponent_Unsigned_Ghost_Step,
 606       P_Scan_Raw_Unsigned_Ghost                  => Scan_Raw_Unsigned_Ghost,
 607       P_Lemma_Scan_Based_Number_Ghost_Base       =>
 608          Lemma_Scan_Based_Number_Ghost_Base,
 609       P_Lemma_Scan_Based_Number_Ghost_Underscore =>
 610          Lemma_Scan_Based_Number_Ghost_Underscore,
 611       P_Lemma_Scan_Based_Number_Ghost_Overflow   =>
 612          Lemma_Scan_Based_Number_Ghost_Overflow,
 613       P_Lemma_Scan_Based_Number_Ghost_Step       =>
 614          Lemma_Scan_Based_Number_Ghost_Step,
 615       P_Raw_Unsigned_Last_Ghost                  => Raw_Unsigned_Last_Ghost,
 616       P_Only_Decimal_Ghost                       => Only_Decimal_Ghost,
 617       P_Scan_Based_Number_Ghost                  => Scan_Based_Number_Ghost,
 618       P_Is_Unsigned_Ghost                        =>
 619          Is_Unsigned_Ghost,
 620       P_Is_Value_Unsigned_Ghost                  =>
 621          Is_Value_Unsigned_Ghost,
 622       P_Prove_Scan_Only_Decimal_Ghost            =>
 623          Prove_Scan_Only_Decimal_Ghost,
 624       P_Prove_Scan_Based_Number_Ghost_Eq         =>
 625          Prove_Scan_Based_Number_Ghost_Eq);
 626
 627 private
 628
 629    ----------------
 630    -- Slide_To_1 --
 631    ----------------
 632
 633    function Slide_To_1 (Str : String) return String is
 634       (declare
 635          Res : constant String (1 .. Str'Length) := Str;
 636        begin
 637          Res);
 638
 639 end System.Value_U_Spec;