gcc/ada/libgnat/s-valuei.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT COMPILER COMPONENTS                         --
   4 --                                                                          --
   5 --                       S Y S T E M . V A L U E _ I                        --
   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 with System.Val_Util; use System.Val_Util;
  33
  34 package body System.Value_I is
  35
  36    --  Ghost code, loop invariants and assertions in this unit are meant for
  37    --  analysis only, not for run-time checking, as it would be too costly
  38    --  otherwise. This is enforced by setting the assertion policy to Ignore.
  39
  40    pragma Assertion_Policy (Ghost              => Ignore,
  41                             Loop_Invariant     => Ignore,
  42                             Assert             => Ignore,
  43                             Assert_And_Cut     => Ignore,
  44                             Subprogram_Variant => Ignore);
  45
  46    ------------------
  47    -- Scan_Integer --
  48    ------------------
  49
  50    procedure Scan_Integer
  51      (Str : String;
  52       Ptr : not null access Integer;
  53       Max : Integer;
  54       Res : out Int)
  55    is
  56       procedure Prove_Is_Int_Of_Uns
  57         (Minus : Boolean;
  58          Uval  : Uns;
  59          Val   : Int)
  60       with Ghost,
  61         Pre => Spec.Uns_Is_Valid_Int (Minus, Uval)
  62           and then
  63             (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First
  64              elsif Minus then Val = -(Int (Uval))
  65              else Val = Int (Uval)),
  66         Post => Spec.Is_Int_Of_Uns (Minus, Uval, Val);
  67       --  Unfold the definition of Is_Int_Of_Uns
  68
  69       procedure Prove_Is_Int_Of_Uns
  70         (Minus : Boolean;
  71          Uval  : Uns;
  72          Val   : Int)
  73       is null;
  74
  75       Uval : Uns;
  76       --  Unsigned result
  77
  78       Minus : Boolean;
  79       --  Set to True if minus sign is present, otherwise to False
  80
  81       Unused_Start : Positive;
  82       --  Saves location of first non-blank (not used in this case)
  83
  84       Non_Blank : constant Positive :=
  85         First_Non_Space_Ghost (Str, Ptr.all, Max)
  86       with Ghost;
  87
  88       Fst_Num   : constant Positive :=
  89         (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
  90          else Non_Blank)
  91       with Ghost;
  92
  93    begin
  94       Scan_Sign (Str, Ptr, Max, Minus, Unused_Start);
  95
  96       if Str (Ptr.all) not in '0' .. '9' then
  97          Ptr.all := Unused_Start;
  98          Bad_Value (Str);
  99       end if;
 100
 101       Scan_Raw_Unsigned (Str, Ptr, Max, Uval);
 102       pragma Assert
 103         (Uval = U_Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max));
 104
 105       --  Deal with overflow cases, and also with largest negative number
 106
 107       if Uval > Uns (Int'Last) then
 108          if Minus and then Uval = Uns (Int'Last) + 1 then
 109             Res := Int'First;
 110          else
 111             Bad_Value (Str);
 112          end if;
 113
 114       --  Negative values
 115
 116       elsif Minus then
 117          Res := -(Int (Uval));
 118
 119       --  Positive values
 120
 121       else
 122          Res := Int (Uval);
 123       end if;
 124
 125       Prove_Is_Int_Of_Uns
 126         (Minus => Str (Non_Blank) = '-',
 127          Uval  => Uval,
 128          Val   => Res);
 129    end Scan_Integer;
 130
 131    -------------------
 132    -- Value_Integer --
 133    -------------------
 134
 135    function Value_Integer (Str : String) return Int is
 136    begin
 137       --  We have to special case Str'Last = Positive'Last because the normal
 138       --  circuit ends up setting P to Str'Last + 1 which is out of bounds. We
 139       --  deal with this by converting to a subtype which fixes the bounds.
 140
 141       if Str'Last = Positive'Last then
 142          declare
 143             subtype NT is String (1 .. Str'Length);
 144             procedure Prove_Is_Integer_Ghost with
 145               Ghost,
 146               Pre  => Str'Length < Natural'Last
 147               and then not Only_Space_Ghost (Str, Str'First, Str'Last)
 148               and then Spec.Is_Integer_Ghost (Spec.Slide_To_1 (Str)),
 149               Post => Spec.Is_Integer_Ghost (NT (Str));
 150             procedure Prove_Is_Integer_Ghost is null;
 151          begin
 152             Prove_Is_Integer_Ghost;
 153             return Value_Integer (NT (Str));
 154          end;
 155
 156       --  Normal case where Str'Last < Positive'Last
 157
 158       else
 159          declare
 160             V : Int;
 161             P : aliased Integer := Str'First;
 162
 163             Non_Blank : constant Positive := First_Non_Space_Ghost
 164               (Str, Str'First, Str'Last)
 165             with Ghost;
 166
 167             Fst_Num   : constant Positive :=
 168               (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
 169                else Non_Blank)
 170             with Ghost;
 171          begin
 172
 173             declare
 174                P_Acc : constant not null access Integer := P'Access;
 175             begin
 176                Scan_Integer (Str, P_Acc, Str'Last, V);
 177             end;
 178
 179             pragma Assert
 180               (P = U_Spec.Raw_Unsigned_Last_Ghost
 181                  (Str, Fst_Num, Str'Last));
 182
 183             Scan_Trailing_Blanks (Str, P);
 184
 185             pragma Assert
 186               (Spec.Is_Value_Integer_Ghost (Spec.Slide_If_Necessary (Str), V));
 187             return V;
 188          end;
 189       end if;
 190    end Value_Integer;
 191
 192 end System.Value_I;