gcc/ada/libgnat/s-vauspe.adb

   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 --                                 B o d y                                  --
   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 pragma Assertion_Policy (Pre                => Ignore,
  33                          Post               => Ignore,
  34                          Contract_Cases     => Ignore,
  35                          Ghost              => Ignore,
  36                          Subprogram_Variant => Ignore);
  37
  38 package body System.Value_U_Spec with SPARK_Mode is
  39
  40    -----------------------------
  41    -- Exponent_Unsigned_Ghost --
  42    -----------------------------
  43
  44    function Exponent_Unsigned_Ghost
  45      (Value : Uns;
  46       Exp   : Natural;
  47       Base  : Uns := 10) return Uns_Option
  48    is
  49       (if Exp = 0 or Value = 0 then (Overflow => False, Value => Value)
  50        elsif Scan_Overflows_Ghost (0, Base, Value) then (Overflow => True)
  51        else Exponent_Unsigned_Ghost (Value * Base, Exp - 1, Base));
  52
  53    ---------------------
  54    -- Last_Hexa_Ghost --
  55    ---------------------
  56
  57    function Last_Hexa_Ghost (Str : String) return Positive is
  58    begin
  59       for J in Str'Range loop
  60          if Str (J) not in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_' then
  61             return J - 1;
  62          end if;
  63
  64          pragma Loop_Invariant
  65            (for all K in Str'First .. J =>
  66               Str (K) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_');
  67       end loop;
  68
  69       return Str'Last;
  70    end Last_Hexa_Ghost;
  71
  72    -----------------------------
  73    -- Lemmas with null bodies --
  74    -----------------------------
  75
  76    procedure Lemma_Scan_Based_Number_Ghost_Base
  77      (Str      : String;
  78       From, To : Integer;
  79       Base     : Uns := 10;
  80       Acc      : Uns := 0)
  81    is null;
  82
  83    procedure Lemma_Scan_Based_Number_Ghost_Underscore
  84      (Str      : String;
  85       From, To : Integer;
  86       Base     : Uns := 10;
  87       Acc      : Uns := 0)
  88    is null;
  89
  90    procedure Lemma_Scan_Based_Number_Ghost_Overflow
  91      (Str      : String;
  92       From, To : Integer;
  93       Base     : Uns := 10;
  94       Acc      : Uns := 0)
  95    is null;
  96
  97    procedure Lemma_Scan_Based_Number_Ghost_Step
  98      (Str      : String;
  99       From, To : Integer;
 100       Base     : Uns := 10;
 101       Acc      : Uns := 0)
 102    is null;
 103
 104    procedure Lemma_Exponent_Unsigned_Ghost_Base
 105      (Value : Uns;
 106       Exp   : Natural;
 107       Base  : Uns := 10)
 108    is null;
 109
 110    procedure Lemma_Exponent_Unsigned_Ghost_Overflow
 111      (Value : Uns;
 112       Exp   : Natural;
 113       Base  : Uns := 10)
 114    is null;
 115
 116    procedure Lemma_Exponent_Unsigned_Ghost_Step
 117      (Value : Uns;
 118       Exp   : Natural;
 119       Base  : Uns := 10)
 120    is null;
 121
 122    --------------------------------------
 123    -- Prove_Scan_Based_Number_Ghost_Eq --
 124    --------------------------------------
 125
 126    procedure Prove_Scan_Based_Number_Ghost_Eq
 127      (Str1, Str2 : String;
 128       From, To : Integer;
 129       Base     : Uns := 10;
 130       Acc      : Uns := 0)
 131    is
 132    begin
 133       if From > To then
 134          null;
 135       elsif Str1 (From) = '_' then
 136          Prove_Scan_Based_Number_Ghost_Eq
 137            (Str1, Str2, From + 1, To, Base, Acc);
 138       elsif Scan_Overflows_Ghost
 139         (Hexa_To_Unsigned_Ghost (Str1 (From)), Base, Acc)
 140       then
 141          null;
 142       else
 143          Prove_Scan_Based_Number_Ghost_Eq
 144            (Str1, Str2, From + 1, To, Base,
 145             Base * Acc + Hexa_To_Unsigned_Ghost (Str1 (From)));
 146       end if;
 147    end Prove_Scan_Based_Number_Ghost_Eq;
 148
 149    -----------------------------------
 150    -- Prove_Scan_Only_Decimal_Ghost --
 151    -----------------------------------
 152
 153    procedure Prove_Scan_Only_Decimal_Ghost
 154      (Str : String;
 155       Val : Uns)
 156    is
 157       pragma Assert (Str (Str'First + 1) /= ' ');
 158       Non_Blank : constant Positive := First_Non_Space_Ghost
 159         (Str, Str'First, Str'Last);
 160       pragma Assert (Non_Blank = Str'First + 1);
 161       Fst_Num   : constant Positive :=
 162         (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
 163       pragma Assert (Fst_Num = Str'First + 1);
 164    begin
 165       pragma Assert
 166         (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
 167       pragma Assert
 168         (Scan_Split_No_Overflow_Ghost (Str, Str'First + 1, Str'Last));
 169       pragma Assert
 170         ((Val, 10, 0) = Scan_Split_Value_Ghost (Str, Str'First + 1, Str'Last));
 171       pragma Assert
 172         (Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last));
 173       pragma Assert (Val = Exponent_Unsigned_Ghost (Val, 0, 10).Value);
 174       pragma Assert (Is_Unsigned_Ghost (Str));
 175       pragma Assert (Is_Value_Unsigned_Ghost (Str, Val));
 176    end Prove_Scan_Only_Decimal_Ghost;
 177
 178    -----------------------------
 179    -- Scan_Based_Number_Ghost --
 180    -----------------------------
 181
 182    function Scan_Based_Number_Ghost
 183      (Str      : String;
 184       From, To : Integer;
 185       Base     : Uns := 10;
 186       Acc      : Uns := 0) return Uns_Option
 187    is
 188       (if From > To then (Overflow => False, Value => Acc)
 189        elsif Str (From) = '_'
 190        then Scan_Based_Number_Ghost (Str, From + 1, To, Base, Acc)
 191        elsif Scan_Overflows_Ghost
 192          (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc)
 193        then (Overflow => True)
 194        else Scan_Based_Number_Ghost
 195          (Str, From + 1, To, Base,
 196           Base * Acc + Hexa_To_Unsigned_Ghost (Str (From))));
 197
 198 end System.Value_U_Spec;