From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 1914) id 0166D385841A; Wed, 5 Jan 2022 11:34:13 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 0166D385841A MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Pierre-Marie de Rodat To: gcc-cvs@gcc.gnu.org Subject: [gcc r12-6234] [Ada] Introduce expression functions for contract of Scan_Exponent X-Act-Checkin: gcc X-Git-Author: Claire Dross X-Git-Refname: refs/heads/master X-Git-Oldrev: a6505936a35e7a5c66e36f7c4e2032c5c7f64838 X-Git-Newrev: c239773dd1892ede85ed936029fd2bf863fbe93a Message-Id: <20220105113413.0166D385841A@sourceware.org> Date: Wed, 5 Jan 2022 11:34:13 +0000 (GMT) X-BeenThere: gcc-cvs@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-cvs mailing list List-Unsubscribe: , List-Archive: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 05 Jan 2022 11:34:13 -0000 https://gcc.gnu.org/g:c239773dd1892ede85ed936029fd2bf863fbe93a commit r12-6234-gc239773dd1892ede85ed936029fd2bf863fbe93a Author: Claire Dross Date: Wed Dec 1 14:03:23 2021 +0100 [Ada] Introduce expression functions for contract of Scan_Exponent gcc/ada/ * libgnat/s-valuti.ads (Starts_As_Exponent_Format_Ghost): Ghost function to determine if a string is recognized as something which might be an exponent. (Is_Opt_Exponent_Format_Ghost): Ghost function to determine if a string has the correct format for an optional exponent. (Scan_Exponent): Use ghost functions to factorize contracts. Diff: --- gcc/ada/libgnat/s-valuti.ads | 92 ++++++++++++++++++++++++++------------------ 1 file changed, 54 insertions(+), 38 deletions(-) diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads index 7483f2c0c03..f542bf6bb48 100644 --- a/gcc/ada/libgnat/s-valuti.ads +++ b/gcc/ada/libgnat/s-valuti.ads @@ -213,6 +213,50 @@ is -- natural number, consisting in a sequence of figures possibly separated -- by single underscores. It may be followed by other characters. + function Starts_As_Exponent_Format_Ghost + (Str : String; + Real : Boolean) return Boolean + is + (Str'Length > 1 + and then Str (Str'First) in 'E' | 'e' + and then + (declare + Plus_Sign : constant Boolean := Str (Str'First + 1) = '+'; + Minus_Sign : constant Boolean := Str (Str'First + 1) = '-'; + Sign : constant Boolean := Plus_Sign or Minus_Sign; + begin + (if Minus_Sign then Real) + and then (if Sign then Str'Length > 2) + and then + (declare + Start : constant Natural := + (if Sign then Str'First + 2 else Str'First + 1); + begin + Str (Start) in '0' .. '9'))) + with + Ghost; + -- Ghost function that determines if Str is recognized as something which + -- might be an exponent, ie. it starts with an 'e', capitalized or not, + -- followed by an optional sign which can only be '-' if we are working on + -- real numbers (Real is True), and then a digit in decimal notation. + + function Is_Opt_Exponent_Format_Ghost + (Str : String; + Real : Boolean) return Boolean + is + (not Starts_As_Exponent_Format_Ghost (Str, Real) + or else + (declare + Start : constant Natural := + (if Str (Str'First + 1) in '+' | '-' then Str'First + 2 + else Str'First + 1); + begin Is_Natural_Format_Ghost (Str (Start .. Str'Last)))) + with + Ghost; + -- Ghost function that determines if Str has the correct format for an + -- optional exponent, that is, either it does not start as an exponent, or + -- it is in a correct format for a natural number. + function Scan_Natural_Ghost (Str : String; P : Natural; @@ -238,50 +282,22 @@ is 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)))))), + and then Max < Natural'Last + and then Is_Opt_Exponent_Format_Ghost (Str (Ptr.all .. Max), Real), Post => - (if Ptr.all'Old < Max and then Str (Ptr.all'Old) in 'E' | 'e' then + (if Starts_As_Exponent_Format_Ghost (Str (Ptr.all'Old .. Max), Real) + 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; + 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 - (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); + 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