1------------------------------------------------------------------------------ 2-- -- 3-- GNAT COMPILER COMPONENTS -- 4-- -- 5-- S Y S T E M . V A L _ U T I L -- 6-- -- 7-- S p e c -- 8-- -- 9-- Copyright (C) 1992-2021, 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 provides some common utilities used by the s-valxxx files 33 34-- Preconditions in this unit are meant for analysis only, not for run-time 35-- checking, so that the expected exceptions are raised. This is enforced by 36-- setting the corresponding assertion policy to Ignore. Postconditions and 37-- contract cases should not be executed at runtime as well, in order not to 38-- slow down the execution of these functions. 39 40pragma Assertion_Policy (Pre => Ignore, 41 Post => Ignore, 42 Contract_Cases => Ignore, 43 Ghost => Ignore); 44 45with System.Case_Util; 46 47package System.Val_Util 48 with SPARK_Mode, Pure 49is 50 pragma Unevaluated_Use_Of_Old (Allow); 51 52 procedure Bad_Value (S : String) 53 with 54 Depends => (null => S); 55 pragma No_Return (Bad_Value); 56 -- Raises constraint error with message: bad input for 'Value: "xxx" 57 58 function Only_Space_Ghost (S : String; From, To : Integer) return Boolean is 59 (for all J in From .. To => S (J) = ' ') 60 with 61 Ghost, 62 Pre => From > To or else (From >= S'First and then To <= S'Last); 63 -- Ghost function that returns True if S has only space characters from 64 -- index From to index To. 65 66 function First_Non_Space_Ghost (S : String) return Positive 67 with 68 Ghost, 69 Pre => not Only_Space_Ghost (S, S'First, S'Last), 70 Post => First_Non_Space_Ghost'Result in S'Range 71 and then S (First_Non_Space_Ghost'Result) /= ' ' 72 and then Only_Space_Ghost 73 (S, S'First, First_Non_Space_Ghost'Result - 1); 74 -- Ghost function that returns the index of the first non-space character 75 -- in S, which necessarily exists given the precondition on S. 76 77 procedure Normalize_String 78 (S : in out String; 79 F, L : out Integer) 80 with 81 Post => (if Only_Space_Ghost (S'Old, S'First, S'Last) then 82 F > L 83 else 84 F >= S'First 85 and then L <= S'Last 86 and then F <= L 87 and then Only_Space_Ghost (S'Old, S'First, F - 1) 88 and then S'Old (F) /= ' ' 89 and then S'Old (L) /= ' ' 90 and then 91 (if L < S'Last then 92 Only_Space_Ghost (S'Old, L + 1, S'Last)) 93 and then 94 (if S'Old (F) /= ''' then 95 (for all J in S'Range => 96 (if J in F .. L then 97 S (J) = System.Case_Util.To_Upper (S'Old (J)) 98 else 99 S (J) = S'Old (J))))); 100 -- This procedure scans the string S setting F to be the index of the first 101 -- non-blank character of S and L to be the index of the last non-blank 102 -- character of S. Any lower case characters present in S will be folded to 103 -- their upper case equivalent except for character literals. If S consists 104 -- of entirely blanks (including when S = "") then we return with F > L. 105 106 procedure Scan_Sign 107 (Str : String; 108 Ptr : not null access Integer; 109 Max : Integer; 110 Minus : out Boolean; 111 Start : out Positive) 112 with 113 Pre => 114 -- Ptr.all .. Max is either an empty range, or a valid range in Str 115 (Ptr.all > Max or else (Ptr.all >= Str'First and then Max <= Str'Last)) 116 and then not Only_Space_Ghost (Str, Ptr.all, Max) 117 and then 118 (declare 119 F : constant Positive := 120 First_Non_Space_Ghost (Str (Ptr.all .. Max)); 121 begin 122 (if Str (F) in '+' | '-' then 123 F <= Max - 1 and then Str (F + 1) /= ' ')), 124 Post => 125 (declare 126 F : constant Positive := 127 First_Non_Space_Ghost (Str (Ptr.all'Old .. Max)); 128 begin 129 Minus = (Str (F) = '-') 130 and then Ptr.all = (if Str (F) in '+' | '-' then F + 1 else F) 131 and then Start = F); 132 -- The Str, Ptr, Max parameters are as for the scan routines (Str is the 133 -- string to be scanned starting at Ptr.all, and Max is the index of the 134 -- last character in the string). Scan_Sign first scans out any initial 135 -- blanks, raising Constraint_Error if the field is all blank. It then 136 -- checks for and skips an initial plus or minus, requiring a non-blank 137 -- character to follow (Constraint_Error is raised if plus or minus appears 138 -- at the end of the string or with a following blank). Minus is set True 139 -- if a minus sign was skipped, and False otherwise. On exit Ptr.all points 140 -- to the character after the sign, or to the first non-blank character 141 -- if no sign is present. Start is set to the point to the first non-blank 142 -- character (sign or digit after it). 143 -- 144 -- Note: if Str is null, i.e. if Max is less than Ptr, then this is a 145 -- special case of an all-blank string, and Ptr is unchanged, and hence 146 -- is greater than Max as required in this case. Constraint_Error is also 147 -- raised in this case. 148 -- 149 -- This routine must not be called with Str'Last = Positive'Last. There is 150 -- no check for this case, the caller must ensure this condition is met. 151 152 procedure Scan_Plus_Sign 153 (Str : String; 154 Ptr : not null access Integer; 155 Max : Integer; 156 Start : out Positive) 157 with 158 Pre => 159 -- Ptr.all .. Max is either an empty range, or a valid range in Str 160 (Ptr.all > Max or else (Ptr.all >= Str'First and then Max <= Str'Last)) 161 and then not Only_Space_Ghost (Str, Ptr.all, Max) 162 and then 163 (declare 164 F : constant Positive := 165 First_Non_Space_Ghost (Str (Ptr.all .. Max)); 166 begin 167 (if Str (F) = '+' then 168 F <= Max - 1 and then Str (F + 1) /= ' ')), 169 Post => 170 (declare 171 F : constant Positive := 172 First_Non_Space_Ghost (Str (Ptr.all'Old .. Max)); 173 begin 174 Ptr.all = (if Str (F) = '+' then F + 1 else F) 175 and then Start = F); 176 -- Same as Scan_Sign, but allows only plus, not minus. This is used for 177 -- modular types. 178 179 function Only_Number_Ghost (Str : String; From, To : Integer) return Boolean 180 is 181 (for all J in From .. To => Str (J) in '0' .. '9' | '_') 182 with 183 Ghost, 184 Pre => From > To or else (From >= Str'First and then To <= Str'Last); 185 -- Ghost function that returns True if S has only number characters from 186 -- index From to index To. 187 188 function Last_Number_Ghost (Str : String) return Positive 189 with 190 Ghost, 191 Pre => Str /= "" and then Str (Str'First) in '0' .. '9', 192 Post => Last_Number_Ghost'Result in Str'Range 193 and then (if Last_Number_Ghost'Result < Str'Last then 194 Str (Last_Number_Ghost'Result + 1) not in '0' .. '9' | '_') 195 and then Only_Number_Ghost (Str, Str'First, Last_Number_Ghost'Result); 196 -- Ghost function that returns the index of the last character in S that 197 -- is either a figure or underscore, which necessarily exists given the 198 -- precondition on S. 199 200 function Is_Natural_Format_Ghost (Str : String) return Boolean is 201 (Str /= "" 202 and then Str (Str'First) in '0' .. '9' 203 and then 204 (declare 205 L : constant Positive := Last_Number_Ghost (Str); 206 begin 207 Str (L) in '0' .. '9' 208 and then (for all J in Str'First .. L => 209 (if Str (J) = '_' then Str (J + 1) /= '_')))) 210 with 211 Ghost; 212 -- Ghost function that determines if Str has the correct format for a 213 -- natural number, consisting in a sequence of figures possibly separated 214 -- by single underscores. It may be followed by other characters. 215 216 function Scan_Natural_Ghost 217 (Str : String; 218 P : Natural; 219 Acc : Natural) 220 return Natural 221 with 222 Ghost, 223 Subprogram_Variant => (Increases => P), 224 Pre => Is_Natural_Format_Ghost (Str) 225 and then P in Str'First .. Last_Number_Ghost (Str) 226 and then Acc < Integer'Last / 10; 227 -- Ghost function that recursively computes the natural number in Str, up 228 -- to the first number greater or equal to Natural'Last / 10, assuming Acc 229 -- has been scanned already and scanning continues at index P. 230 231 procedure Scan_Exponent 232 (Str : String; 233 Ptr : not null access Integer; 234 Max : Integer; 235 Exp : out Integer; 236 Real : Boolean := False) 237 with 238 Pre => 239 -- Ptr.all .. Max is either an empty range, or a valid range in Str 240 (Ptr.all > Max or else (Ptr.all >= Str'First and then Max <= Str'Last)) 241 and then 242 Max < Natural'Last 243 and then 244 (if Ptr.all < Max and then Str (Ptr.all) in 'E' | 'e' then 245 (declare 246 Plus_Sign : constant Boolean := Str (Ptr.all + 1) = '+'; 247 Minus_Sign : constant Boolean := Str (Ptr.all + 1) = '-'; 248 Sign : constant Boolean := Plus_Sign or Minus_Sign; 249 begin 250 (if Minus_Sign and not Real then True 251 elsif Sign 252 and then (Ptr.all > Max - 2 253 or else Str (Ptr.all + 2) not in '0' .. '9') 254 then True 255 else 256 (declare 257 Start : constant Natural := 258 (if Sign then Ptr.all + 2 else Ptr.all + 1); 259 begin 260 Is_Natural_Format_Ghost (Str (Start .. Max)))))), 261 Post => 262 (if Ptr.all'Old < Max and then Str (Ptr.all'Old) in 'E' | 'e' then 263 (declare 264 Plus_Sign : constant Boolean := Str (Ptr.all'Old + 1) = '+'; 265 Minus_Sign : constant Boolean := Str (Ptr.all'Old + 1) = '-'; 266 Sign : constant Boolean := Plus_Sign or Minus_Sign; 267 Unchanged : constant Boolean := 268 Exp = 0 and Ptr.all = Ptr.all'Old; 269 begin 270 (if Minus_Sign and not Real then Unchanged 271 elsif Sign 272 and then (Ptr.all'Old > Max - 2 273 or else Str (Ptr.all'Old + 2) not in '0' .. '9') 274 then Unchanged 275 else 276 (declare 277 Start : constant Natural := 278 (if Sign then Ptr.all'Old + 2 else Ptr.all'Old + 1); 279 Value : constant Natural := 280 Scan_Natural_Ghost (Str (Start .. Max), Start, 0); 281 begin 282 Exp = (if Minus_Sign then -Value else Value)))) 283 else 284 Exp = 0 and Ptr.all = Ptr.all'Old); 285 -- Called to scan a possible exponent. Str, Ptr, Max are as described above 286 -- for Scan_Sign. If Ptr.all < Max and Str (Ptr.all) = 'E' or 'e', then an 287 -- exponent is scanned out, with the exponent value returned in Exp, and 288 -- Ptr.all updated to point past the exponent. If the exponent field is 289 -- incorrectly formed or not present, then Ptr.all is unchanged, and the 290 -- returned exponent value is zero. Real indicates whether a minus sign 291 -- is permitted (True = permitted). Very large exponents are handled by 292 -- returning a suitable large value. If the base is zero, then any value 293 -- is allowed, and otherwise the large value will either cause underflow 294 -- or overflow during the scaling process which is fine. 295 -- 296 -- This routine must not be called with Str'Last = Positive'Last. There is 297 -- no check for this case, the caller must ensure this condition is met. 298 299 procedure Scan_Trailing_Blanks (Str : String; P : Positive) 300 with 301 Pre => P >= Str'First 302 and then Only_Space_Ghost (Str, P, Str'Last); 303 -- Checks that the remainder of the field Str (P .. Str'Last) is all 304 -- blanks. Raises Constraint_Error if a non-blank character is found. 305 306 pragma Warnings 307 (GNATprove, Off, """Ptr"" is not modified", 308 Reason => "Ptr is actually modified when raising an exception"); 309 procedure Scan_Underscore 310 (Str : String; 311 P : in out Natural; 312 Ptr : not null access Integer; 313 Max : Integer; 314 Ext : Boolean) 315 with 316 Pre => P in Str'Range 317 and then Str (P) = '_' 318 and then Max in Str'Range 319 and then P < Max 320 and then 321 (if Ext then 322 Str (P + 1) in '0' .. '9' | 'A' .. 'F' | 'a' .. 'f' 323 else 324 Str (P + 1) in '0' .. '9'), 325 Post => 326 P = P'Old + 1 327 and then Ptr.all = Ptr.all; 328 -- Called if an underscore is encountered while scanning digits. Str (P) 329 -- contains the underscore. Ptr is the pointer to be returned to the 330 -- ultimate caller of the scan routine, Max is the maximum subscript in 331 -- Str, and Ext indicates if extended digits are allowed. In the case 332 -- where the underscore is invalid, Constraint_Error is raised with Ptr 333 -- set appropriately, otherwise control returns with P incremented past 334 -- the underscore. 335 -- 336 -- This routine must not be called with Str'Last = Positive'Last. There is 337 -- no check for this case, the caller must ensure this condition is met. 338 pragma Warnings (GNATprove, On, """Ptr"" is not modified"); 339 340private 341 342 ------------------------ 343 -- Scan_Natural_Ghost -- 344 ------------------------ 345 346 function Scan_Natural_Ghost 347 (Str : String; 348 P : Natural; 349 Acc : Natural) 350 return Natural 351 is 352 (if Str (P) = '_' then 353 Scan_Natural_Ghost (Str, P + 1, Acc) 354 else 355 (declare 356 Shift_Acc : constant Natural := 357 Acc * 10 + (Character'Pos (Str (P)) - Character'Pos ('0')); 358 begin 359 (if P = Str'Last 360 or else Str (P + 1) not in '0' .. '9' | '_' 361 or else Shift_Acc >= Integer'Last / 10 362 then 363 Shift_Acc 364 else 365 Scan_Natural_Ghost (Str, P + 1, Shift_Acc)))); 366 367end System.Val_Util; 368