------------------------------------------------------------------------------ -- -- -- GNAT COMPILER COMPONENTS -- -- -- -- S Y S T E M . V A L U E _ U -- -- -- -- S p e c -- -- -- -- Copyright (C) 1992-2022, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- -- ware Foundation; either version 3, or (at your option) any later ver- -- -- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- -- or FITNESS FOR A PARTICULAR PURPOSE. -- -- -- -- As a special exception under Section 7 of GPL version 3, you are granted -- -- additional permissions described in the GCC Runtime Library Exception, -- -- version 3.1, as published by the Free Software Foundation. -- -- -- -- You should have received a copy of the GNU General Public License and -- -- a copy of the GCC Runtime Library Exception along with this program; -- -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- -- . -- -- -- -- GNAT was originally developed by the GNAT team at New York University. -- -- Extensive contributions were provided by Ada Core Technologies Inc. -- -- -- ------------------------------------------------------------------------------ -- This package contains routines for scanning modular Unsigned -- values for use in Text_IO.Modular_IO, and the Value attribute. -- Preconditions in this unit are meant for analysis only, not for run-time -- checking, so that the expected exceptions are raised. This is enforced by -- setting the corresponding assertion policy to Ignore. Postconditions and -- contract cases should not be executed at runtime as well, in order not to -- slow down the execution of these functions. pragma Assertion_Policy (Pre => Ignore, Post => Ignore, Contract_Cases => Ignore, Ghost => Ignore, Subprogram_Variant => Ignore); pragma Warnings (Off, "postcondition does not mention function result"); -- True postconditions are used to avoid inlining for GNATprove with System.Val_Util; use System.Val_Util; generic type Uns is mod <>; package System.Value_U is pragma Preelaborate; type Uns_Option (Overflow : Boolean := False) is record case Overflow is when True => null; when False => Value : Uns := 0; end case; end record with Ghost; function Only_Hexa_Ghost (Str : String; From, To : Integer) return Boolean is (for all J in From .. To => Str (J) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_') with Ghost, Pre => From > To or else (From >= Str'First and then To <= Str'Last); -- Ghost function that returns True if S has only hexadecimal characters -- from index From to index To. function Last_Hexa_Ghost (Str : String) return Positive with Ghost, Pre => Str /= "" and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F', Post => Last_Hexa_Ghost'Result in Str'Range and then (if Last_Hexa_Ghost'Result < Str'Last then Str (Last_Hexa_Ghost'Result + 1) not in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_') and then Only_Hexa_Ghost (Str, Str'First, Last_Hexa_Ghost'Result); -- Ghost function that returns the index of the last character in S that -- is either an hexadecimal digit or an underscore, which necessarily -- exists given the precondition on Str. function Is_Based_Format_Ghost (Str : String) return Boolean is (Str /= "" and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' and then (declare L : constant Positive := Last_Hexa_Ghost (Str); begin Str (L) /= '_' and then (for all J in Str'First .. L => (if Str (J) = '_' then Str (J + 1) /= '_')))) with Ghost; -- Ghost function that determines if Str has the correct format for a -- based number, consisting in a sequence of hexadecimal digits possibly -- separated by single underscores. It may be followed by other characters. function Hexa_To_Unsigned_Ghost (X : Character) return Uns is (case X is when '0' .. '9' => Character'Pos (X) - Character'Pos ('0'), when 'a' .. 'f' => Character'Pos (X) - Character'Pos ('a') + 10, when 'A' .. 'F' => Character'Pos (X) - Character'Pos ('A') + 10, when others => raise Program_Error) with Ghost, Pre => X in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; -- Ghost function that computes the value corresponding to an hexadecimal -- digit. function Scan_Overflows_Ghost (Digit : Uns; Base : Uns; Acc : Uns) return Boolean is (Digit >= Base or else Acc > Uns'Last / Base or else Uns'Last - Digit < Base * Acc) with Ghost; -- Ghost function which returns True if Digit + Base * Acc overflows or -- Digit is greater than Base, as this is used by the algorithm for the -- test of overflow. function Scan_Based_Number_Ghost (Str : String; From, To : Integer; Base : Uns := 10; Acc : Uns := 0) return Uns_Option with Ghost, Subprogram_Variant => (Increases => From), Pre => Str'Last /= Positive'Last and then (From > To or else (From >= Str'First and then To <= Str'Last)) and then Only_Hexa_Ghost (Str, From, To); -- Ghost function that recursively computes the based number in Str, -- assuming Acc has been scanned already and scanning continues at index -- From. function Exponent_Unsigned_Ghost (Value : Uns; Exp : Natural; Base : Uns := 10) return Uns_Option with Ghost, Subprogram_Variant => (Decreases => Exp); -- Ghost function that recursively computes Value * Base ** Exp function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean is (Is_Natural_Format_Ghost (Str) and then (declare Last_Num_Init : constant Integer := Last_Number_Ghost (Str); Starts_As_Based : constant Boolean := Last_Num_Init < Str'Last - 1 and then Str (Last_Num_Init + 1) in '#' | ':' and then Str (Last_Num_Init + 2) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; Last_Num_Based : constant Integer := (if Starts_As_Based then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Str'Last)) else Last_Num_Init); Is_Based : constant Boolean := Starts_As_Based and then Last_Num_Based < Str'Last and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1); First_Exp : constant Integer := (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1); begin (if Starts_As_Based then Is_Based_Format_Ghost (Str (Last_Num_Init + 2 .. Str'Last)) and then Last_Num_Based < Str'Last) and then Is_Opt_Exponent_Format_Ghost (Str (First_Exp .. Str'Last)))) with Ghost, Pre => Str'Last /= Positive'Last, Post => True; -- Ghost function that determines if Str has the correct format for an -- unsigned number without a sign character. -- It is a natural number in base 10, optionally followed by a based -- number surrounded by delimiters # or :, optionally followed by an -- exponent part. function Raw_Unsigned_Overflows_Ghost (Str : String; From, To : Integer) return Boolean is (declare Last_Num_Init : constant Integer := Last_Number_Ghost (Str (From .. To)); Init_Val : constant Uns_Option := Scan_Based_Number_Ghost (Str, From, Last_Num_Init); Starts_As_Based : constant Boolean := Last_Num_Init < To - 1 and then Str (Last_Num_Init + 1) in '#' | ':' and then Str (Last_Num_Init + 2) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; Last_Num_Based : constant Integer := (if Starts_As_Based then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To)) else Last_Num_Init); Is_Based : constant Boolean := Starts_As_Based and then Last_Num_Based < To and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1); Based_Val : constant Uns_Option := (if Starts_As_Based and then not Init_Val.Overflow then Scan_Based_Number_Ghost (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value) else Init_Val); First_Exp : constant Integer := (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1); Expon : constant Natural := (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To)) then Scan_Exponent_Ghost (Str (First_Exp .. To)) else 0); begin Init_Val.Overflow or else (Last_Num_Init < To - 1 and then Str (Last_Num_Init + 1) in '#' | ':' and then Init_Val.Value not in 2 .. 16) or else (Starts_As_Based and then Based_Val.Overflow) or else (Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To)) and then (declare Base : constant Uns := (if Is_Based then Init_Val.Value else 10); Value : constant Uns := (if Is_Based then Based_Val.Value else Init_Val.Value); begin Exponent_Unsigned_Ghost (Value, Expon, Base).Overflow))) with Ghost, Pre => Str'Last /= Positive'Last and then From in Str'Range and then To in From .. Str'Last and then Str (From) in '0' .. '9', Post => True; -- Ghost function that determines if the computation of the unsigned number -- represented by Str will overflow. The computation overflows if either: -- * The computation of the decimal part overflows, -- * The decimal part is followed by a valid delimiter for a based -- part, and the number corresponding to the base is not a valid base, -- * The computation of the based part overflows, or -- * There is an exponent and the computation of the exponentiation -- overflows. function Scan_Raw_Unsigned_Ghost (Str : String; From, To : Integer) return Uns is (declare Last_Num_Init : constant Integer := Last_Number_Ghost (Str (From .. To)); Init_Val : constant Uns_Option := Scan_Based_Number_Ghost (Str, From, Last_Num_Init); Starts_As_Based : constant Boolean := Last_Num_Init < To - 1 and then Str (Last_Num_Init + 1) in '#' | ':' and then Str (Last_Num_Init + 2) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; Last_Num_Based : constant Integer := (if Starts_As_Based then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To)) else Last_Num_Init); Is_Based : constant Boolean := Starts_As_Based and then Last_Num_Based < To and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1); Based_Val : constant Uns_Option := (if Starts_As_Based and then not Init_Val.Overflow then Scan_Based_Number_Ghost (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value) else Init_Val); First_Exp : constant Integer := (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1); Expon : constant Natural := (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To)) then Scan_Exponent_Ghost (Str (First_Exp .. To)) else 0); Base : constant Uns := (if Is_Based then Init_Val.Value else 10); Value : constant Uns := (if Is_Based then Based_Val.Value else Init_Val.Value); begin Exponent_Unsigned_Ghost (Value, Expon, Base).Value) with Ghost, Pre => Str'Last /= Positive'Last and then From in Str'Range and then To in From .. Str'Last and then Str (From) in '0' .. '9' and then not Raw_Unsigned_Overflows_Ghost (Str, From, To), Post => True; -- Ghost function that scans an unsigned number without a sign character function Raw_Unsigned_Last_Ghost (Str : String; From, To : Integer) return Positive is (declare Last_Num_Init : constant Integer := Last_Number_Ghost (Str (From .. To)); Starts_As_Based : constant Boolean := Last_Num_Init < To - 1 and then Str (Last_Num_Init + 1) in '#' | ':' and then Str (Last_Num_Init + 2) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; Last_Num_Based : constant Integer := (if Starts_As_Based then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To)) else Last_Num_Init); Is_Based : constant Boolean := Starts_As_Based and then Last_Num_Based < To and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1); First_Exp : constant Integer := (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1); begin (if not Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To)) then First_Exp elsif Str (First_Exp + 1) in '-' | '+' then Last_Number_Ghost (Str (First_Exp + 2 .. To)) + 1 else Last_Number_Ghost (Str (First_Exp + 1 .. To)) + 1)) with Ghost, Pre => Str'Last /= Positive'Last and then From in Str'Range and then To in From .. Str'Last and then Str (From) in '0' .. '9', Post => Raw_Unsigned_Last_Ghost'Result in From .. To + 1; -- Ghost function that returns the position of the cursor once an unsigned -- number has been seen. procedure Scan_Raw_Unsigned (Str : String; Ptr : not null access Integer; Max : Integer; Res : out Uns) with Pre => Str'Last /= Positive'Last and then Ptr.all in Str'Range and then Max in Ptr.all .. Str'Last and then Is_Raw_Unsigned_Format_Ghost (Str (Ptr.all .. Max)), Post => not Raw_Unsigned_Overflows_Ghost (Str, Ptr.all'Old, Max) and Res = Scan_Raw_Unsigned_Ghost (Str, Ptr.all'Old, Max) and Ptr.all = Raw_Unsigned_Last_Ghost (Str, Ptr.all'Old, Max); -- This function scans the string starting at Str (Ptr.all) for a valid -- integer according to the syntax described in (RM 3.5(43)). The substring -- scanned extends no further than Str (Max). Note: this does not scan -- leading or trailing blanks, nor leading sign. -- -- There are three cases for the return: -- -- If a valid integer is found, then Ptr.all is updated past the last -- character of the integer. -- -- If no valid integer is found, then Ptr.all points either to an initial -- non-digit character, or to Max + 1 if the field is all spaces and the -- exception Constraint_Error is raised. -- -- If a syntactically valid integer is scanned, but the value is out of -- range, or, in the based case, the base value is out of range or there -- is an out of range digit, then Ptr.all points past the integer, and -- Constraint_Error is raised. -- -- Note: these rules correspond to the requirements for leaving the pointer -- positioned in Text_IO.Get. Note that the rules as stated in the RM would -- seem to imply that for a case like: -- -- 8#12345670009# -- -- the pointer should be left at the first # having scanned out the longest -- valid integer literal (8), but in fact in this case the pointer points -- past the final # and Constraint_Error is raised. This is the behavior -- expected for Text_IO and enforced by the ACATS tests. -- -- If a based literal is malformed in that a character other than a valid -- hexadecimal digit is encountered during scanning out the digits after -- the # (this includes the case of using the wrong terminator, : instead -- of # or vice versa) there are two cases. If all the digits before the -- non-digit are in range of the base, as in -- -- 8#100x00# -- 8#100: -- -- then in this case, the "base" value before the initial # is returned as -- the result, and the pointer points to the initial # character on return. -- -- If an out of range digit has been detected before the invalid character, -- as in: -- -- 8#900x00# -- 8#900: -- -- then the pointer is also left at the initial # character, but constraint -- error is raised reflecting the encounter of an out of range digit. -- -- Finally if we have an unterminated fixed-point constant where the final -- # or : character is missing, Constraint_Error is raised and the pointer -- is left pointing past the last digit, as in: -- -- 8#22 -- -- This string results in a Constraint_Error with the pointer pointing -- past the second 2. -- -- Note: if Str is empty, i.e. if Max is less than Ptr, then this is a -- special case of an all-blank string, and Ptr is unchanged, and hence -- is greater than Max as required in this case. -- ??? This is not the case. We will read Str (Ptr.all) without checking -- and increase Ptr.all by one. -- -- Note: this routine should not be called with Str'Last = Positive'Last. -- If this occurs Program_Error is raised with a message noting that this -- case is not supported. Most such cases are eliminated by the caller. procedure Scan_Unsigned (Str : String; Ptr : not null access Integer; Max : Integer; Res : out Uns) with Pre => Str'Last /= Positive'Last and then Ptr.all in Str'Range and then Max in Ptr.all .. Str'Last and then not Only_Space_Ghost (Str, Ptr.all, Max) and then (declare Non_Blank : constant Positive := First_Non_Space_Ghost (Str, Ptr.all, Max); Fst_Num : constant Positive := (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank); begin Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max))), Post => (declare Non_Blank : constant Positive := First_Non_Space_Ghost (Str, Ptr.all'Old, Max); Fst_Num : constant Positive := (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank); begin not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Max) and then Res = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max) and then Ptr.all = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Max)); -- Same as Scan_Raw_Unsigned, except scans optional leading -- blanks, and an optional leading plus sign. -- -- Note: if a minus sign is present, Constraint_Error will be raised. -- Note: trailing blanks are not scanned. function Slide_To_1 (Str : String) return String with Ghost, Post => Only_Space_Ghost (Str, Str'First, Str'Last) = (for all J in Str'First .. Str'Last => Slide_To_1'Result (J - Str'First + 1) = ' '); -- Slides Str so that it starts at 1 function Slide_If_Necessary (Str : String) return String is (if Str'Last = Positive'Last then Slide_To_1 (Str) else Str) with Ghost, Post => Only_Space_Ghost (Str, Str'First, Str'Last) = Only_Space_Ghost (Slide_If_Necessary'Result, Slide_If_Necessary'Result'First, Slide_If_Necessary'Result'Last); -- If Str'Last = Positive'Last then slides Str so that it starts at 1 function Is_Unsigned_Ghost (Str : String) return Boolean is (declare Non_Blank : constant Positive := First_Non_Space_Ghost (Str, Str'First, Str'Last); Fst_Num : constant Positive := (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank); begin Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)) and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Str'Last) and then Only_Space_Ghost (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last)) with Ghost, Pre => not Only_Space_Ghost (Str, Str'First, Str'Last) and then Str'Last /= Positive'Last, Post => True; -- Ghost function that determines if Str has the correct format for an -- unsigned number, consisting in some blank characters, an optional -- + sign, a raw unsigned number which does not overflow and then some -- more blank characters. function Is_Value_Unsigned_Ghost (Str : String; Val : Uns) return Boolean is (declare Non_Blank : constant Positive := First_Non_Space_Ghost (Str, Str'First, Str'Last); Fst_Num : constant Positive := (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank); begin Val = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last)) with Ghost, Pre => not Only_Space_Ghost (Str, Str'First, Str'Last) and then Str'Last /= Positive'Last and then Is_Unsigned_Ghost (Str), Post => True; -- Ghost function that returns True if Val is the value corresponding to -- the unsigned number represented by Str. function Value_Unsigned (Str : String) return Uns with Pre => not Only_Space_Ghost (Str, Str'First, Str'Last) and then Str'Length /= Positive'Last and then Is_Unsigned_Ghost (Slide_If_Necessary (Str)), Post => Is_Value_Unsigned_Ghost (Slide_If_Necessary (Str), Value_Unsigned'Result), Subprogram_Variant => (Decreases => Str'First); -- Used in computing X'Value (Str) where X is a modular integer type whose -- modulus does not exceed the range of System.Unsigned_Types.Unsigned. Str -- is the string argument of the attribute. Constraint_Error is raised if -- the string is malformed, or if the value is out of range. private ----------------------------- -- Exponent_Unsigned_Ghost -- ----------------------------- function Exponent_Unsigned_Ghost (Value : Uns; Exp : Natural; Base : Uns := 10) return Uns_Option is (if Exp = 0 or Value = 0 then (Overflow => False, Value => Value) elsif Scan_Overflows_Ghost (0, Base, Value) then (Overflow => True) else Exponent_Unsigned_Ghost (Value * Base, Exp - 1, Base)); ----------------------------- -- Scan_Based_Number_Ghost -- ----------------------------- function Scan_Based_Number_Ghost (Str : String; From, To : Integer; Base : Uns := 10; Acc : Uns := 0) return Uns_Option is (if From > To then (Overflow => False, Value => Acc) elsif Str (From) = '_' then Scan_Based_Number_Ghost (Str, From + 1, To, Base, Acc) elsif Scan_Overflows_Ghost (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc) then (Overflow => True) else Scan_Based_Number_Ghost (Str, From + 1, To, Base, Base * Acc + Hexa_To_Unsigned_Ghost (Str (From)))); ---------------- -- Slide_To_1 -- ---------------- function Slide_To_1 (Str : String) return String is (declare Res : constant String (1 .. Str'Length) := Str; begin Res); end System.Value_U;