From patchwork Thu Dec 2 16:28:35 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 48397 Return-Path: X-Original-To: patchwork@sourceware.org Delivered-To: patchwork@sourceware.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 31D6D3857816 for ; Thu, 2 Dec 2021 16:32:14 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 31D6D3857816 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1638462734; bh=OsU/LW4WhUTsJD3GYXJbRwhSKmY8YplclBD8dncK2k4=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=NoCGR8TBeAvfP448s3Fc7drHUp/aBqC3+FZb4inJ49TGzxqacp+1qEEyUDTws5OCA zTJTY0qmbospefwy50fM2zpYzF7IQ5eUMEUAT6T6EQXyS4gfW2wxVF/DabsWwjNMTD AvEmwoJ+MGvLQd0cWElZR0ylo8aRnn/o8MxvmBeg= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wr1-x431.google.com (mail-wr1-x431.google.com [IPv6:2a00:1450:4864:20::431]) by sourceware.org (Postfix) with ESMTPS id 783423858001 for ; Thu, 2 Dec 2021 16:28:38 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 783423858001 Received: by mail-wr1-x431.google.com with SMTP id j3so60840409wrp.1 for ; Thu, 02 Dec 2021 08:28:38 -0800 (PST) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=OsU/LW4WhUTsJD3GYXJbRwhSKmY8YplclBD8dncK2k4=; b=dl9V7fRGu2hwlHoH3uGiZVrAam3ItS5FZQyGD8HIQ0DJZicr3wVG9GTWAHP4tG8yvJ WwZM6jjLDxdTdoCsXhziOp6n/56cGI8I/6AckEh1teoAomXK949BIVfccp5V9iizNTS+ 3Q6WK+8wM1qAe8y1LqAZS45dhi2Gl3bXCiw/aDSjbK2bvxf1TEGT2LdzuYvhW1xzyeKX ysfv4yGiXZxR0z1jpz3h784fthUzkQluernJ/lgcQwXu8OYvS3g4jETC6e2JhEp5N3A/ vAeTfwawJfDLSzwmI5b2TNQj2DF8YQQda5xLxXekF9a6GygaUR1E1p8HaTGm4ENqPaxC 1OKw== X-Gm-Message-State: AOAM533coCjHGNW4KAIFoUaHivBVFQouw6WvyyyWqFqxFfHb94CfGCKR 29MFeV10voKK55Q1R+MMzsF3z1ajEoekGg== X-Google-Smtp-Source: ABdhPJxM89MZB3LHo7hYjrl+WxoT9j008ZslIMzll2RhVEvq+cmWpUFK04PC79HOCDt3KDkS1/RMng== X-Received: by 2002:adf:ce8b:: with SMTP id r11mr15602976wrn.294.1638462516445; Thu, 02 Dec 2021 08:28:36 -0800 (PST) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id o4sm295986wry.80.2021.12.02.08.28.35 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 02 Dec 2021 08:28:35 -0800 (PST) Date: Thu, 2 Dec 2021 16:28:35 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] Proof of System.Val_Util utilities for 'Value support Message-ID: <20211202162835.GA2156201@adacore.com> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-12.2 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SCC_5_SHORT_WORD_LINES, SPF_HELO_NONE, SPF_PASS, TXREP, WEIRD_QUOTING autolearn=ham autolearn_force=no version=3.4.4 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-Patchwork-Original-From: Pierre-Marie de Rodat via Gcc-patches From: Pierre-Marie de Rodat Reply-To: Pierre-Marie de Rodat Cc: Yannick Moy Errors-To: gcc-patches-bounces+patchwork=sourceware.org@gcc.gnu.org Sender: "Gcc-patches" This proves the functionality of the utility procedures supporting the implementation of 'Value attributes. As a side-effect of this proof, fix possible range check failures. GNATprove is run with switch --level=3. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-valboo.adb (First_Non_Space_Ghost): Move to utilities. (Value_Boolean): Prefix call to First_Non_Space_Ghost. * libgnat/s-valboo.ads (First_Non_Space_Ghost): Move to utilities. (Is_Boolean_Image_Ghost, Value_Boolean): Prefix call to First_Non_Space_Ghost. * libgnat/s-valuer.adb (Scan_Raw_Real): Adapt to change of function Scan_Exponent to procedure. * libgnat/s-valueu.adb (Scan_Raw_Unsigned): Adapt to change of function Scan_Exponent to procedure. * libgnat/s-valuti.adb (First_Non_Space_Ghost): Function moved here. (Last_Number_Ghost): New ghost query function. (Scan_Exponent): Change function with side-effects into procedure, to mark in SPARK. Prove procedure wrt contract. Change type of local P to avoid possible range check failure (it is not known whether this can be activated by callers). (Scan_Plus_Sign, Scan_Sign): Change type of local P to avoid possible range check failure. Add loop invariants and assertions for proof. (Scan_Trailing_Blanks): Add loop invariant. (Scan_Underscore): Remove SPARK_Mode Off. * libgnat/s-valuti.ads (First_Non_Space_Ghost): Function moved here. (Last_Number_Ghost, Only_Number_Ghost, Is_Natural_Format_Ghost, Scan_Natural_Ghost): New ghost query functions. (Scan_Plus_Sign, Scan_Sign, Scan_Exponent, Scan_Trailing_Blanks, Scan_Underscore): Add functional contracts. diff --git a/gcc/ada/libgnat/s-valboo.adb b/gcc/ada/libgnat/s-valboo.adb --- a/gcc/ada/libgnat/s-valboo.adb +++ b/gcc/ada/libgnat/s-valboo.adb @@ -43,19 +43,6 @@ package body System.Val_Bool with SPARK_Mode is - function First_Non_Space_Ghost (S : String) return Positive is - begin - for J in S'Range loop - if S (J) /= ' ' then - return J; - end if; - - pragma Loop_Invariant (for all K in S'First .. J => S (K) = ' '); - end loop; - - raise Program_Error; - end First_Non_Space_Ghost; - ------------------- -- Value_Boolean -- ------------------- @@ -68,7 +55,7 @@ is begin Normalize_String (S, F, L); - pragma Assert (F = First_Non_Space_Ghost (S)); + pragma Assert (F = System.Val_Util.First_Non_Space_Ghost (S)); if S (F .. L) = "TRUE" then return True; diff --git a/gcc/ada/libgnat/s-valboo.ads b/gcc/ada/libgnat/s-valboo.ads --- a/gcc/ada/libgnat/s-valboo.ads +++ b/gcc/ada/libgnat/s-valboo.ads @@ -47,22 +47,11 @@ package System.Val_Bool is pragma Preelaborate; - function First_Non_Space_Ghost (S : String) return Positive - with - Ghost, - Pre => not System.Val_Util.Only_Space_Ghost (S, S'First, S'Last), - Post => First_Non_Space_Ghost'Result in S'Range - and then S (First_Non_Space_Ghost'Result) /= ' ' - and then System.Val_Util.Only_Space_Ghost - (S, S'First, First_Non_Space_Ghost'Result - 1); - -- Ghost function that returns the index of the first non-space character - -- in S, which necessarily exists given the precondition on S. - function Is_Boolean_Image_Ghost (Str : String) return Boolean is (not System.Val_Util.Only_Space_Ghost (Str, Str'First, Str'Last) and then (declare - F : constant Positive := First_Non_Space_Ghost (Str); + F : constant Positive := System.Val_Util.First_Non_Space_Ghost (Str); begin (F <= Str'Last - 3 and then Str (F) in 't' | 'T' @@ -92,7 +81,8 @@ is with Pre => Is_Boolean_Image_Ghost (Str), Post => - Value_Boolean'Result = (Str (First_Non_Space_Ghost (Str)) in 't' | 'T'); + Value_Boolean'Result = + (Str (System.Val_Util.First_Non_Space_Ghost (Str)) in 't' | 'T'); -- Computes Boolean'Value (Str) end System.Val_Bool; diff --git a/gcc/ada/libgnat/s-valuer.adb b/gcc/ada/libgnat/s-valuer.adb --- a/gcc/ada/libgnat/s-valuer.adb +++ b/gcc/ada/libgnat/s-valuer.adb @@ -511,6 +511,8 @@ package body System.Value_R is Value : Uns; -- Mantissa as an Integer + Expon : Integer; + begin -- The default base is 10 @@ -643,7 +645,8 @@ package body System.Value_R is -- Update pointer and scan exponent Ptr.all := Index; - Scale := Scale + Scan_Exponent (Str, Ptr, Max, Real => True); + Scan_Exponent (Str, Ptr, Max, Expon, Real => True); + Scale := Scale + Expon; -- Here is where we check for a bad based number diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb --- a/gcc/ada/libgnat/s-valueu.adb +++ b/gcc/ada/libgnat/s-valueu.adb @@ -234,7 +234,7 @@ package body System.Value_U is -- Come here with scanned unsigned value in Uval. The only remaining -- required step is to deal with exponent if one is present. - Expon := Scan_Exponent (Str, Ptr, Max); + Scan_Exponent (Str, Ptr, Max, Expon); if Expon /= 0 and then Uval /= 0 then diff --git a/gcc/ada/libgnat/s-valuti.adb b/gcc/ada/libgnat/s-valuti.adb --- a/gcc/ada/libgnat/s-valuti.adb +++ b/gcc/ada/libgnat/s-valuti.adb @@ -62,6 +62,41 @@ is end if; end Bad_Value; + --------------------------- + -- First_Non_Space_Ghost -- + --------------------------- + + function First_Non_Space_Ghost (S : String) return Positive is + begin + for J in S'Range loop + if S (J) /= ' ' then + return J; + end if; + + pragma Loop_Invariant (for all K in S'First .. J => S (K) = ' '); + end loop; + + raise Program_Error; + end First_Non_Space_Ghost; + + ----------------------- + -- Last_Number_Ghost -- + ----------------------- + + function Last_Number_Ghost (Str : String) return Positive is + begin + for J in Str'Range loop + if Str (J) not in '0' .. '9' | '_' then + return J - 1; + end if; + + pragma Loop_Invariant + (for all K in Str'First .. J => Str (K) in '0' .. '9' | '_'); + end loop; + + return Str'Last; + end Last_Number_Ghost; + ---------------------- -- Normalize_String -- ---------------------- @@ -119,15 +154,14 @@ is -- Scan_Exponent -- ------------------- - function Scan_Exponent + procedure Scan_Exponent (Str : String; Ptr : not null access Integer; Max : Integer; - Real : Boolean := False) return Integer - with - SPARK_Mode => Off -- Function with side-effect through Ptr + Exp : out Integer; + Real : Boolean := False) is - P : Natural := Ptr.all; + P : Integer := Ptr.all; M : Boolean; X : Integer; @@ -135,7 +169,8 @@ is if P >= Max or else (Str (P) /= 'E' and then Str (P) /= 'e') then - return 0; + Exp := 0; + return; end if; -- We have an E/e, see if sign follows @@ -146,7 +181,8 @@ is P := P + 1; if P > Max then - return 0; + Exp := 0; + return; else M := False; end if; @@ -155,7 +191,8 @@ is P := P + 1; if P > Max or else not Real then - return 0; + Exp := 0; + return; else M := True; end if; @@ -165,7 +202,8 @@ is end if; if Str (P) not in '0' .. '9' then - return 0; + Exp := 0; + return; end if; -- Scan out the exponent value as an unsigned integer. Values larger @@ -176,28 +214,52 @@ is X := 0; - loop - if X < (Integer'Last / 10) then - X := X * 10 + (Character'Pos (Str (P)) - Character'Pos ('0')); - end if; + declare + Rest : constant String := Str (P .. Max) with Ghost; + Last : constant Natural := Last_Number_Ghost (Rest) with Ghost; - P := P + 1; + begin + pragma Assert (Is_Natural_Format_Ghost (Rest)); - exit when P > Max; + loop + pragma Assert (Str (P) = Rest (P)); + pragma Assert (Str (P) in '0' .. '9'); - if Str (P) = '_' then - Scan_Underscore (Str, P, Ptr, Max, False); - else - exit when Str (P) not in '0' .. '9'; - end if; - end loop; + if X < (Integer'Last / 10) then + X := X * 10 + (Character'Pos (Str (P)) - Character'Pos ('0')); + end if; + + pragma Loop_Invariant (X >= 0); + pragma Loop_Invariant (P in P'Loop_Entry .. Last); + pragma Loop_Invariant (Str (P) in '0' .. '9'); + pragma Loop_Invariant + (Scan_Natural_Ghost (Rest, P'Loop_Entry, 0) + = (if P = Max + or else Rest (P + 1) not in '0' .. '9' | '_' + or else X >= Integer'Last / 10 + then + X + else + Scan_Natural_Ghost (Rest, P + 1, X))); + + P := P + 1; + + exit when P > Max; + + if Str (P) = '_' then + Scan_Underscore (Str, P, Ptr, Max, False); + else + exit when Str (P) not in '0' .. '9'; + end if; + end loop; + end; if M then X := -X; end if; Ptr.all := P; - return X; + Exp := X; end Scan_Exponent; -------------------- @@ -209,10 +271,8 @@ is Ptr : not null access Integer; Max : Integer; Start : out Positive) - with - SPARK_Mode => Off -- Not proved yet is - P : Natural := Ptr.all; + P : Integer := Ptr.all; begin if P > Max then @@ -224,6 +284,12 @@ is while Str (P) = ' ' loop P := P + 1; + pragma Loop_Invariant (Ptr.all = Ptr.all'Loop_Entry); + pragma Loop_Invariant (P in Ptr.all .. Max); + pragma Loop_Invariant (for some J in P .. Max => Str (J) /= ' '); + pragma Loop_Invariant + (for all J in Ptr.all .. P - 1 => Str (J) = ' '); + if P > Max then Ptr.all := P; Bad_Value (Str); @@ -232,6 +298,8 @@ is Start := P; + pragma Assert (Start = First_Non_Space_Ghost (Str (Ptr.all .. Max))); + -- Skip past an initial plus sign if Str (P) = '+' then @@ -256,10 +324,8 @@ is Max : Integer; Minus : out Boolean; Start : out Positive) - with - SPARK_Mode => Off -- Not proved yet is - P : Natural := Ptr.all; + P : Integer := Ptr.all; begin -- Deal with case of null string (all blanks). As per spec, we raise @@ -274,6 +340,12 @@ is while Str (P) = ' ' loop P := P + 1; + pragma Loop_Invariant (Ptr.all = Ptr.all'Loop_Entry); + pragma Loop_Invariant (P in Ptr.all .. Max); + pragma Loop_Invariant (for some J in P .. Max => Str (J) /= ' '); + pragma Loop_Invariant + (for all J in Ptr.all .. P - 1 => Str (J) = ' '); + if P > Max then Ptr.all := P; Bad_Value (Str); @@ -282,6 +354,8 @@ is Start := P; + pragma Assert (Start = First_Non_Space_Ghost (Str (Ptr.all .. Max))); + -- Remember an initial minus sign if Str (P) = '-' then @@ -315,15 +389,14 @@ is -- Scan_Trailing_Blanks -- -------------------------- - procedure Scan_Trailing_Blanks (Str : String; P : Positive) - with - SPARK_Mode => Off -- Not proved yet - is + procedure Scan_Trailing_Blanks (Str : String; P : Positive) is begin for J in P .. Str'Last loop if Str (J) /= ' ' then Bad_Value (Str); end if; + + pragma Loop_Invariant (for all K in P .. J => Str (K) = ' '); end loop; end Scan_Trailing_Blanks; @@ -337,8 +410,6 @@ is Ptr : not null access Integer; Max : Integer; Ext : Boolean) - with - SPARK_Mode => Off -- Not proved yet is C : Character; diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads --- a/gcc/ada/libgnat/s-valuti.ads +++ b/gcc/ada/libgnat/s-valuti.ads @@ -47,6 +47,7 @@ with System.Case_Util; package System.Val_Util with SPARK_Mode, Pure is + pragma Unevaluated_Use_Of_Old (Allow); procedure Bad_Value (S : String) with @@ -62,6 +63,17 @@ is -- Ghost function that returns True if S has only space characters from -- index From to index To. + function First_Non_Space_Ghost (S : String) return Positive + with + Ghost, + Pre => not Only_Space_Ghost (S, S'First, S'Last), + Post => First_Non_Space_Ghost'Result in S'Range + and then S (First_Non_Space_Ghost'Result) /= ' ' + and then Only_Space_Ghost + (S, S'First, First_Non_Space_Ghost'Result - 1); + -- Ghost function that returns the index of the first non-space character + -- in S, which necessarily exists given the precondition on S. + procedure Normalize_String (S : in out String; F, L : out Integer) @@ -96,7 +108,27 @@ is Ptr : not null access Integer; Max : Integer; Minus : out Boolean; - Start : out Positive); + Start : out Positive) + with + Pre => + -- Ptr.all .. Max is either an empty range, or a valid range in Str + (Ptr.all > Max or else (Ptr.all >= Str'First and then Max <= Str'Last)) + and then not Only_Space_Ghost (Str, Ptr.all, Max) + and then + (declare + F : constant Positive := + First_Non_Space_Ghost (Str (Ptr.all .. Max)); + begin + (if Str (F) in '+' | '-' then + F <= Max - 1 and then Str (F + 1) /= ' ')), + Post => + (declare + F : constant Positive := + First_Non_Space_Ghost (Str (Ptr.all'Old .. Max)); + begin + Minus = (Str (F) = '-') + and then Ptr.all = (if Str (F) in '+' | '-' then F + 1 else F) + and then Start = F); -- The Str, Ptr, Max parameters are as for the scan routines (Str is the -- string to be scanned starting at Ptr.all, and Max is the index of the -- last character in the string). Scan_Sign first scans out any initial @@ -121,17 +153,150 @@ is (Str : String; Ptr : not null access Integer; Max : Integer; - Start : out Positive); + Start : out Positive) + with + Pre => + -- Ptr.all .. Max is either an empty range, or a valid range in Str + (Ptr.all > Max or else (Ptr.all >= Str'First and then Max <= Str'Last)) + and then not Only_Space_Ghost (Str, Ptr.all, Max) + and then + (declare + F : constant Positive := + First_Non_Space_Ghost (Str (Ptr.all .. Max)); + begin + (if Str (F) = '+' then + F <= Max - 1 and then Str (F + 1) /= ' ')), + Post => + (declare + F : constant Positive := + First_Non_Space_Ghost (Str (Ptr.all'Old .. Max)); + begin + Ptr.all = (if Str (F) = '+' then F + 1 else F) + and then Start = F); -- Same as Scan_Sign, but allows only plus, not minus. This is used for -- modular types. - function Scan_Exponent + function Only_Number_Ghost (Str : String; From, To : Integer) return Boolean + is + (for all J in From .. To => Str (J) in '0' .. '9' | '_') + with + Ghost, + Pre => From > To or else (From >= Str'First and then To <= Str'Last); + -- Ghost function that returns True if S has only number characters from + -- index From to index To. + + function Last_Number_Ghost (Str : String) return Positive + with + Ghost, + Pre => Str /= "" and then Str (Str'First) in '0' .. '9', + Post => Last_Number_Ghost'Result in Str'Range + and then (if Last_Number_Ghost'Result < Str'Last then + Str (Last_Number_Ghost'Result + 1) not in '0' .. '9' | '_') + and then Only_Number_Ghost (Str, Str'First, Last_Number_Ghost'Result); + -- Ghost function that returns the index of the last character in S that + -- is either a figure or underscore, which necessarily exists given the + -- precondition on S. + + function Is_Natural_Format_Ghost (Str : String) return Boolean is + (Str /= "" + and then Str (Str'First) in '0' .. '9' + and then + (declare + L : constant Positive := Last_Number_Ghost (Str); + begin + Str (L) in '0' .. '9' + 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 + -- natural number, consisting in a sequence of figures possibly separated + -- by single underscores. It may be followed by other characters. + + function Scan_Natural_Ghost + (Str : String; + P : Natural; + Acc : Natural) + return Natural + is + (if Str (P) = '_' then + Scan_Natural_Ghost (Str, P + 1, Acc) + else + (declare + Shift_Acc : constant Natural := + Acc * 10 + (Character'Pos (Str (P)) - Character'Pos ('0')); + begin + (if P = Str'Last + or else Str (P + 1) not in '0' .. '9' | '_' + or else Shift_Acc >= Integer'Last / 10 + then + Shift_Acc + else + Scan_Natural_Ghost (Str, P + 1, Shift_Acc)))) + with + Ghost, + Subprogram_Variant => (Increases => P), + Pre => Is_Natural_Format_Ghost (Str) + and then P in Str'First .. Last_Number_Ghost (Str) + and then Acc < Integer'Last / 10; + -- Ghost function that recursively computes the natural number in Str, up + -- to the first number greater or equal to Natural'Last / 10, assuming Acc + -- has been scanned already and scanning continues at index P. + + procedure Scan_Exponent (Str : String; Ptr : not null access Integer; Max : Integer; - Real : Boolean := False) return Integer + Exp : out Integer; + Real : Boolean := False) with - SPARK_Mode => Off; -- Function with side-effect through Ptr + Pre => + -- Ptr.all .. Max is either an empty range, or a valid range in Str + (Ptr.all > Max or else (Ptr.all >= Str'First and then Max <= Str'Last)) + and then + Max < Natural'Last + and then + (if Ptr.all < Max and then Str (Ptr.all) in 'E' | 'e' then + (declare + Plus_Sign : constant Boolean := Str (Ptr.all + 1) = '+'; + Minus_Sign : constant Boolean := Str (Ptr.all + 1) = '-'; + Sign : constant Boolean := Plus_Sign or Minus_Sign; + begin + (if Minus_Sign and not Real then True + elsif Sign + and then (Ptr.all > Max - 2 + or else Str (Ptr.all + 2) not in '0' .. '9') + then True + else + (declare + Start : constant Natural := + (if Sign then Ptr.all + 2 else Ptr.all + 1); + begin + Is_Natural_Format_Ghost (Str (Start .. Max)))))), + Post => + (if Ptr.all'Old < Max and then Str (Ptr.all'Old) in 'E' | 'e' then + (declare + Plus_Sign : constant Boolean := Str (Ptr.all'Old + 1) = '+'; + Minus_Sign : constant Boolean := Str (Ptr.all'Old + 1) = '-'; + Sign : constant Boolean := Plus_Sign or Minus_Sign; + Unchanged : constant Boolean := + Exp = 0 and Ptr.all = Ptr.all'Old; + begin + (if Minus_Sign and not Real then Unchanged + elsif Sign + and then (Ptr.all'Old > Max - 2 + or else Str (Ptr.all'Old + 2) not in '0' .. '9') + then Unchanged + else + (declare + Start : constant Natural := + (if Sign then Ptr.all'Old + 2 else Ptr.all'Old + 1); + Value : constant Natural := + Scan_Natural_Ghost (Str (Start .. Max), Start, 0); + begin + Exp = (if Minus_Sign then -Value else Value)))) + else + Exp = 0 and Ptr.all = Ptr.all'Old); -- Called to scan a possible exponent. Str, Ptr, Max are as described above -- for Scan_Sign. If Ptr.all < Max and Str (Ptr.all) = 'E' or 'e', then an -- exponent is scanned out, with the exponent value returned in Exp, and @@ -146,18 +311,37 @@ is -- This routine must not be called with Str'Last = Positive'Last. There is -- no check for this case, the caller must ensure this condition is met. - procedure Scan_Trailing_Blanks (Str : String; P : Positive); + procedure Scan_Trailing_Blanks (Str : String; P : Positive) + with + Pre => P >= Str'First + and then Only_Space_Ghost (Str, P, Str'Last); -- Checks that the remainder of the field Str (P .. Str'Last) is all -- blanks. Raises Constraint_Error if a non-blank character is found. + pragma Warnings + (GNATprove, Off, """Ptr"" is not modified", + Reason => "Ptr is actually modified when raising an exception"); procedure Scan_Underscore (Str : String; P : in out Natural; Ptr : not null access Integer; Max : Integer; - Ext : Boolean); + Ext : Boolean) + with + Pre => P in Str'Range + and then Str (P) = '_' + and then Max in Str'Range + and then P < Max + and then + (if Ext then + Str (P + 1) in '0' .. '9' | 'A' .. 'F' | 'a' .. 'f' + else + Str (P + 1) in '0' .. '9'), + Post => + P = P'Old + 1 + and then Ptr.all = Ptr.all; -- Called if an underscore is encountered while scanning digits. Str (P) - -- contains the underscore. Ptr it the pointer to be returned to the + -- contains the underscore. Ptr is the pointer to be returned to the -- ultimate caller of the scan routine, Max is the maximum subscript in -- Str, and Ext indicates if extended digits are allowed. In the case -- where the underscore is invalid, Constraint_Error is raised with Ptr @@ -166,5 +350,6 @@ is -- -- This routine must not be called with Str'Last = Positive'Last. There is -- no check for this case, the caller must ensure this condition is met. + pragma Warnings (GNATprove, On, """Ptr"" is not modified"); end System.Val_Util;