public inbox for gcc-cvs@sourceware.org help / color / mirror / Atom feed
From: Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> To: gcc-cvs@gcc.gnu.org Subject: [gcc r13-352] [Ada] Proof of 'Image support for signed integers Date: Thu, 12 May 2022 12:40:32 +0000 (GMT) [thread overview] Message-ID: <20220512124032.36717383D802@sourceware.org> (raw) https://gcc.gnu.org/g:91d68769419b64ef9843c4c1eac5261217693b1e commit r13-352-g91d68769419b64ef9843c4c1eac5261217693b1e Author: Yannick Moy <moy@adacore.com> Date: Fri Feb 4 15:20:20 2022 +0100 [Ada] Proof of 'Image support for signed integers Prove System.Image_I, similarly to the proof done for System.Image_U. The contracts make the connection between the result of Image_Integer, the available space computed with System.Width_U and the result of 'Value as computed by Value_Integer. I/O units that now depend on non-pure units are also marked not Pure anymore. gcc/ada/ * libgnat/s-imagef.adb: Adapt to new signature of Image_I, by providing ghost imported subprograms. For now, no contract is used on these subprograms, as System.Image_F is not proved. * libgnat/s-imagef.ads: Add modular type Uns as formal parameter, to use in defining Int_Params for instantiating Image_I. * libgnat/s-imagei.adb: Add contracts and ghost code. * libgnat/s-imagei.ads: Replace Int formal parameter by package Int_Params, which bundles type Int and Uns with ghost subprograms. Add contracts. * libgnat/s-imfi128.ads: Adapt to new formal of Image_F. * libgnat/s-imfi32.ads: Adapt to new formal of Image_F. * libgnat/s-imfi64.ads: Adapt to new formal of Image_F. * libgnat/s-imgint.ads: Adapt to new formals of Image_I. * libgnat/s-imglli.ads: Adapt to new formals of Image_I. * libgnat/s-imgllli.ads: Adapt to new formals of Image_I. * libgnat/s-valint.ads: Adapt to new formals of Value_I. * libgnat/s-vallli.ads: Adapt to new formals of Value_I. * libgnat/s-valllli.ads: Adapt to new formals of Value_I. * libgnat/s-valuei.adb (Prove_Scan_Only_Decimal_Ghost): New ghost lemma. * libgnat/s-valuei.ads: New formal parameters to prove the new lemma. * libgnat/s-valuti.ads (Int_Params): Define a generic package to be used as a trait-like formal parameter in Image_I and other generics that need to instantiate Image_I. * libgnat/s-widthu.ads (Big_10): Qualify the 10 literal. Diff: --- gcc/ada/libgnat/s-imagef.adb | 80 ++++++++- gcc/ada/libgnat/s-imagef.ads | 1 + gcc/ada/libgnat/s-imagei.adb | 365 +++++++++++++++++++++++++++++++++++++++++- gcc/ada/libgnat/s-imagei.ads | 60 ++++++- gcc/ada/libgnat/s-imfi128.ads | 3 +- gcc/ada/libgnat/s-imfi32.ads | 3 +- gcc/ada/libgnat/s-imfi64.ads | 3 +- gcc/ada/libgnat/s-imgint.ads | 45 +++++- gcc/ada/libgnat/s-imglli.ads | 45 +++++- gcc/ada/libgnat/s-imgllli.ads | 46 +++++- gcc/ada/libgnat/s-valint.ads | 8 +- gcc/ada/libgnat/s-vallli.ads | 8 +- gcc/ada/libgnat/s-valllli.ads | 8 +- gcc/ada/libgnat/s-valuei.adb | 53 ++++++ gcc/ada/libgnat/s-valuei.ads | 53 ++++-- gcc/ada/libgnat/s-valuti.ads | 35 ++++ gcc/ada/libgnat/s-widthu.ads | 2 +- 17 files changed, 786 insertions(+), 32 deletions(-) diff --git a/gcc/ada/libgnat/s-imagef.adb b/gcc/ada/libgnat/s-imagef.adb index 14e9d066fc0..2166ece6be9 100644 --- a/gcc/ada/libgnat/s-imagef.adb +++ b/gcc/ada/libgnat/s-imagef.adb @@ -31,9 +31,24 @@ with System.Image_I; with System.Img_Util; use System.Img_Util; +with System.Val_Util; package body System.Image_F is + -- Contracts, ghost code, loop invariants and assertions in this unit are + -- meant for analysis only, not for run-time checking, as it would be too + -- costly otherwise. This is enforced by setting the assertion policy to + -- Ignore. + + pragma Assertion_Policy (Assert => Ignore, + Assert_And_Cut => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Pre => Ignore, + Post => Ignore, + Subprogram_Variant => Ignore); + Maxdigs : constant Natural := Int'Width - 2; -- Maximum number of decimal digits that can be represented in an Int. -- The "-2" accounts for the sign and one extra digit, since we need the @@ -54,7 +69,70 @@ package body System.Image_F is -- if the small is larger than 1, and smaller than 2**(Int'Size - 1) / 10 -- if the small is smaller than 1. - package Image_I is new System.Image_I (Int); + -- Define ghost subprograms without implementation (marked as Import) to + -- create a suitable package Int_Params for type Int, as instantiations + -- of System.Image_F use for this type one of the derived integer types + -- defined in Interfaces, instead of the standard signed integer types + -- which are used to define System.Img_*.Int_Params. + + type Uns_Option (Overflow : Boolean := False) is record + case Overflow is + when True => + null; + when False => + Value : Uns := 0; + end case; + end record; + + Unsigned_Width_Ghost : constant Natural := Int'Width; + + function Wrap_Option (Value : Uns) return Uns_Option + with Ghost, Import; + function Only_Decimal_Ghost + (Str : String; + From, To : Integer) + return Boolean + with Ghost, Import; + function Hexa_To_Unsigned_Ghost (X : Character) return Uns + with Ghost, Import; + function Scan_Based_Number_Ghost + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + return Uns_Option + with Ghost, Import; + function Is_Integer_Ghost (Str : String) return Boolean + with Ghost, Import; + procedure Prove_Iter_Scan_Based_Number_Ghost + (Str1, Str2 : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + with Ghost, Import; + procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) + with Ghost, Import; + function Abs_Uns_Of_Int (Val : Int) return Uns + with Ghost, Import; + function Value_Integer (Str : String) return Int + with Ghost, Import; + + package Int_Params is new Val_Util.Int_Params + (Int => Int, + Uns => Uns, + Uns_Option => Uns_Option, + Unsigned_Width_Ghost => Unsigned_Width_Ghost, + Wrap_Option => Wrap_Option, + Only_Decimal_Ghost => Only_Decimal_Ghost, + Hexa_To_Unsigned_Ghost => Hexa_To_Unsigned_Ghost, + Scan_Based_Number_Ghost => Scan_Based_Number_Ghost, + Is_Integer_Ghost => Is_Integer_Ghost, + Prove_Iter_Scan_Based_Number_Ghost => Prove_Iter_Scan_Based_Number_Ghost, + Prove_Scan_Only_Decimal_Ghost => Prove_Scan_Only_Decimal_Ghost, + Abs_Uns_Of_Int => Abs_Uns_Of_Int, + Value_Integer => Value_Integer); + + package Image_I is new System.Image_I (Int_Params); procedure Set_Image_Integer (V : Int; diff --git a/gcc/ada/libgnat/s-imagef.ads b/gcc/ada/libgnat/s-imagef.ads index c16d2c58d41..13ea22fae9f 100644 --- a/gcc/ada/libgnat/s-imagef.ads +++ b/gcc/ada/libgnat/s-imagef.ads @@ -36,6 +36,7 @@ generic type Int is range <>; + type Uns is mod <>; with procedure Scaled_Divide (X, Y, Z : Int; diff --git a/gcc/ada/libgnat/s-imagei.adb b/gcc/ada/libgnat/s-imagei.adb index e7199af63e9..f340d139e26 100644 --- a/gcc/ada/libgnat/s-imagei.adb +++ b/gcc/ada/libgnat/s-imagei.adb @@ -29,18 +29,140 @@ -- -- ------------------------------------------------------------------------------ +with Ada.Numerics.Big_Numbers.Big_Integers_Ghost; +use Ada.Numerics.Big_Numbers.Big_Integers_Ghost; + package body System.Image_I is + -- Ghost code, loop invariants and assertions in this unit are meant for + -- analysis only, not for run-time checking, as it would be too costly + -- otherwise. This is enforced by setting the assertion policy to Ignore. + + pragma Assertion_Policy (Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore, + Assert_And_Cut => Ignore, + Pre => Ignore, + Post => Ignore, + Subprogram_Variant => Ignore); + + -- As a use_clause for Int_Params cannot be used for instances of this + -- generic in System specs, rename all constants and subprograms. + + Unsigned_Width_Ghost : constant Natural := Int_Params.Unsigned_Width_Ghost; + + function Wrap_Option (Value : Uns) return Uns_Option + renames Int_Params.Wrap_Option; + function Only_Decimal_Ghost + (Str : String; + From, To : Integer) + return Boolean + renames Int_Params.Only_Decimal_Ghost; + function Hexa_To_Unsigned_Ghost (X : Character) return Uns + renames Int_Params.Hexa_To_Unsigned_Ghost; + function Scan_Based_Number_Ghost + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + return Uns_Option + renames Int_Params.Scan_Based_Number_Ghost; + function Is_Integer_Ghost (Str : String) return Boolean + renames Int_Params.Is_Integer_Ghost; + procedure Prove_Iter_Scan_Based_Number_Ghost + (Str1, Str2 : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + renames Int_Params.Prove_Iter_Scan_Based_Number_Ghost; + procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) + renames Int_Params.Prove_Scan_Only_Decimal_Ghost; + function Abs_Uns_Of_Int (Val : Int) return Uns + renames Int_Params.Abs_Uns_Of_Int; + function Value_Integer (Str : String) return Int + renames Int_Params.Value_Integer; + subtype Non_Positive is Int range Int'First .. 0; + function Uns_Of_Non_Positive (T : Non_Positive) return Uns is + (if T = Int'First then Uns (Int'Last) + 1 else Uns (-T)); + procedure Set_Digits (T : Non_Positive; S : in out String; - P : in out Natural); + P : in out Natural) + with + Pre => P < Integer'Last + and then S'Last < Integer'Last + and then S'First <= P + 1 + and then S'First <= S'Last + and then P <= S'Last - Unsigned_Width_Ghost + 1, + Post => S (S'First .. P'Old) = S'Old (S'First .. P'Old) + and then P in P'Old + 1 .. S'Last + and then Only_Decimal_Ghost (S, From => P'Old + 1, To => P) + and then Scan_Based_Number_Ghost (S, From => P'Old + 1, To => P) + = Wrap_Option (Uns_Of_Non_Positive (T)); -- Set digits of absolute value of T, which is zero or negative. We work -- with the negative of the value so that the largest negative number is -- not a special case. + package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns); + + function Big (Arg : Uns) return Big_Integer renames + Unsigned_Conversion.To_Big_Integer; + + function From_Big (Arg : Big_Integer) return Uns renames + Unsigned_Conversion.From_Big_Integer; + + Big_10 : constant Big_Integer := Big (10) with Ghost; + + ------------------ + -- Local Lemmas -- + ------------------ + + procedure Lemma_Non_Zero (X : Uns) + with + Ghost, + Pre => X /= 0, + Post => Big (X) /= 0; + + procedure Lemma_Div_Commutation (X, Y : Uns) + with + Ghost, + Pre => Y /= 0, + Post => Big (X) / Big (Y) = Big (X / Y); + + procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) + with + Ghost, + Post => X / Y / Z = X / (Y * Z); + + --------------------------- + -- Lemma_Div_Commutation -- + --------------------------- + + procedure Lemma_Non_Zero (X : Uns) is null; + procedure Lemma_Div_Commutation (X, Y : Uns) is null; + + --------------------- + -- Lemma_Div_Twice -- + --------------------- + + procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) is + XY : constant Big_Natural := X / Y; + YZ : constant Big_Natural := Y * Z; + XYZ : constant Big_Natural := X / Y / Z; + R : constant Big_Natural := (XY rem Z) * Y + (X rem Y); + begin + pragma Assert (X = XY * Y + (X rem Y)); + pragma Assert (XY = XY / Z * Z + (XY rem Z)); + pragma Assert (X = XYZ * YZ + R); + pragma Assert ((XY rem Z) * Y <= (Z - 1) * Y); + pragma Assert (R <= YZ - 1); + pragma Assert (X / YZ = (XYZ * YZ + R) / YZ); + pragma Assert (X / YZ = XYZ + R / YZ); + end Lemma_Div_Twice; + ------------------- -- Image_Integer -- ------------------- @@ -52,6 +174,39 @@ package body System.Image_I is is pragma Assert (S'First = 1); + procedure Prove_Value_Integer + with + Ghost, + Pre => S'First = 1 + and then S'Last < Integer'Last + and then P in 2 .. S'Last + and then S (1) in ' ' | '-' + and then (S (1) = '-') = (V < 0) + and then Only_Decimal_Ghost (S, From => 2, To => P) + and then Scan_Based_Number_Ghost (S, From => 2, To => P) + = Wrap_Option (Abs_Uns_Of_Int (V)), + Post => Is_Integer_Ghost (S (1 .. P)) + and then Value_Integer (S (1 .. P)) = V; + -- Ghost lemma to prove the value of Value_Integer from the value of + -- Scan_Based_Number_Ghost and the sign on a decimal string. + + ------------------------- + -- Prove_Value_Integer -- + ------------------------- + + procedure Prove_Value_Integer is + Str : constant String := S (1 .. P); + begin + pragma Assert (Str'First = 1); + pragma Assert (Only_Decimal_Ghost (Str, From => 2, To => P)); + Prove_Iter_Scan_Based_Number_Ghost (S, Str, From => 2, To => P); + pragma Assert (Scan_Based_Number_Ghost (Str, From => 2, To => P) + = Wrap_Option (Abs_Uns_Of_Int (V))); + Prove_Scan_Only_Decimal_Ghost (Str, V); + end Prove_Value_Integer; + + -- Start of processing for Image_Integer + begin if V >= 0 then S (1) := ' '; @@ -63,7 +218,16 @@ package body System.Image_I is pragma Assert (P < S'Last - 1); end if; - Set_Image_Integer (V, S, P); + declare + P_Prev : constant Integer := P with Ghost; + Offset : constant Positive := (if V >= 0 then 1 else 2) with Ghost; + begin + Set_Image_Integer (V, S, P); + + pragma Assert (P_Prev + Offset = 2); + end; + + Prove_Value_Integer; end Image_Integer; ---------------- @@ -77,6 +241,106 @@ package body System.Image_I is is Nb_Digits : Natural := 0; Value : Non_Positive := T; + + -- Local ghost variables + + Pow : Big_Positive := 1 with Ghost; + S_Init : constant String := S with Ghost; + Uns_T : constant Uns := Uns_Of_Non_Positive (T) with Ghost; + Uns_Value : Uns := Uns_Of_Non_Positive (Value) with Ghost; + Prev, Cur : Uns_Option with Ghost; + Prev_Value : Uns with Ghost; + Prev_S : String := S with Ghost; + + -- Local ghost lemmas + + procedure Prove_Character_Val (RU : Uns; RI : Int) + with + Ghost, + Pre => RU in 0 .. 9 + and then RI in 0 .. 9, + Post => Character'Val (48 + RU) in '0' .. '9' + and then Character'Val (48 + RI) in '0' .. '9'; + -- Ghost lemma to prove the value of a character corresponding to the + -- next figure. + + procedure Prove_Hexa_To_Unsigned_Ghost (RU : Uns; RI : Int) + with + Ghost, + Pre => RU in 0 .. 9 + and then RI in 0 .. 9, + Post => Hexa_To_Unsigned_Ghost (Character'Val (48 + RU)) = RU + and then Hexa_To_Unsigned_Ghost (Character'Val (48 + RI)) = Uns (RI); + -- Ghost lemma to prove that Hexa_To_Unsigned_Ghost returns the source + -- figure when applied to the corresponding character. + + procedure Prove_Unchanged + with + Ghost, + Pre => P <= S'Last + and then S_Init'First = S'First + and then S_Init'Last = S'Last + and then (for all K in S'First .. P => S (K) = S_Init (K)), + Post => S (S'First .. P) = S_Init (S'First .. P); + -- Ghost lemma to prove that the part of string S before P has not been + -- modified. + + procedure Prove_Uns_Of_Non_Positive_Value + with + Ghost, + Pre => Uns_Value = Uns_Of_Non_Positive (Value), + Post => Uns_Value / 10 = Uns_Of_Non_Positive (Value / 10) + and then Uns_Value rem 10 = Uns_Of_Non_Positive (Value rem 10); + -- Ghost lemma to prove that the relation between Value and its unsigned + -- version is preserved. + + procedure Prove_Iter_Scan + (Str1, Str2 : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + with + Ghost, + Pre => Str1'Last /= Positive'Last + and then + (From > To or else (From >= Str1'First and then To <= Str1'Last)) + and then Only_Decimal_Ghost (Str1, From, To) + and then Str1'First = Str2'First + and then Str1'Last = Str2'Last + and then (for all J in From .. To => Str1 (J) = Str2 (J)), + Post => + Scan_Based_Number_Ghost (Str1, From, To, Base, Acc) + = Scan_Based_Number_Ghost (Str2, From, To, Base, Acc); + -- Ghost lemma to prove that the result of Scan_Based_Number_Ghost only + -- depends on the value of the argument string in the (From .. To) range + -- of indexes. This is a wrapper on Prove_Iter_Scan_Based_Number_Ghost + -- so that we can call it here on ghost arguments. + + ----------------------------- + -- Local lemma null bodies -- + ----------------------------- + + procedure Prove_Character_Val (RU : Uns; RI : Int) is null; + procedure Prove_Hexa_To_Unsigned_Ghost (RU : Uns; RI : Int) is null; + procedure Prove_Unchanged is null; + procedure Prove_Uns_Of_Non_Positive_Value is null; + + --------------------- + -- Prove_Iter_Scan -- + --------------------- + + procedure Prove_Iter_Scan + (Str1, Str2 : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + is + begin + Prove_Iter_Scan_Based_Number_Ghost (Str1, Str2, From, To, Base, Acc); + end Prove_Iter_Scan; + + -- Start of processing for Set_Digits + begin pragma Assert (P >= S'First - 1 and P < S'Last); -- No check is done since, as documented in the Set_Image_Integer @@ -86,19 +350,116 @@ package body System.Image_I is -- First we compute the number of characters needed for representing -- the number. loop + Lemma_Div_Commutation (Uns_Of_Non_Positive (Value), 10); + Lemma_Div_Twice (Big (Uns_Of_Non_Positive (T)), + Big_10 ** Nb_Digits, Big_10); + Prove_Uns_Of_Non_Positive_Value; + Value := Value / 10; Nb_Digits := Nb_Digits + 1; + + Uns_Value := Uns_Value / 10; + Pow := Pow * 10; + + pragma Loop_Invariant (Uns_Value = Uns_Of_Non_Positive (Value)); + pragma Loop_Invariant (Nb_Digits in 1 .. Unsigned_Width_Ghost - 1); + pragma Loop_Invariant (Pow = Big_10 ** Nb_Digits); + pragma Loop_Invariant (Big (Uns_Value) = Big (Uns_T) / Pow); + pragma Loop_Variant (Increases => Value); + exit when Value = 0; + + Lemma_Non_Zero (Uns_Value); + pragma Assert (Pow <= Big (Uns'Last)); end loop; Value := T; + Uns_Value := Uns_Of_Non_Positive (T); + Pow := 1; + + pragma Assert (Uns_Value = From_Big (Big (Uns_T) / Big_10 ** 0)); -- We now populate digits from the end of the string to the beginning for J in reverse 1 .. Nb_Digits loop + Lemma_Div_Commutation (Uns_Value, 10); + Lemma_Div_Twice (Big (Uns_T), Big_10 ** (Nb_Digits - J), Big_10); + Prove_Character_Val (Uns_Value rem 10, -(Value rem 10)); + Prove_Hexa_To_Unsigned_Ghost (Uns_Value rem 10, -(Value rem 10)); + Prove_Uns_Of_Non_Positive_Value; + pragma Assert (Uns_Value rem 10 = Uns_Of_Non_Positive (Value rem 10)); + pragma Assert (Uns_Value rem 10 = Uns (-(Value rem 10))); + + Prev_Value := Uns_Value; + Prev_S := S; + Pow := Pow * 10; + Uns_Value := Uns_Value / 10; + S (P + J) := Character'Val (48 - (Value rem 10)); Value := Value / 10; + + pragma Assert (S (P + J) in '0' .. '9'); + pragma Assert (Hexa_To_Unsigned_Ghost (S (P + J)) = + From_Big (Big (Uns_T) / Big_10 ** (Nb_Digits - J)) rem 10); + pragma Assert + (for all K in P + J + 1 .. P + Nb_Digits => S (K) in '0' .. '9'); + + Prev := Scan_Based_Number_Ghost + (Str => S, + From => P + J + 1, + To => P + Nb_Digits, + Base => 10, + Acc => Prev_Value); + Cur := Scan_Based_Number_Ghost + (Str => S, + From => P + J, + To => P + Nb_Digits, + Base => 10, + Acc => Uns_Value); + pragma Assert (Prev_Value = 10 * Uns_Value + (Prev_Value rem 10)); + pragma Assert + (Prev_Value rem 10 = Hexa_To_Unsigned_Ghost (S (P + J))); + pragma Assert + (Prev_Value = 10 * Uns_Value + Hexa_To_Unsigned_Ghost (S (P + J))); + + if J /= Nb_Digits then + Prove_Iter_Scan + (Prev_S, S, P + J + 1, P + Nb_Digits, 10, Prev_Value); + end if; + + pragma Assert (Prev = Cur); + pragma Assert (Prev = Wrap_Option (Uns_T)); + + pragma Loop_Invariant (Uns_Value = Uns_Of_Non_Positive (Value)); + pragma Loop_Invariant (Uns_Value <= Uns'Last / 10); + pragma Loop_Invariant + (for all K in S'First .. P => S (K) = S_Init (K)); + pragma Loop_Invariant (Only_Decimal_Ghost (S, P + J, P + Nb_Digits)); + pragma Loop_Invariant + (for all K in P + J .. P + Nb_Digits => S (K) in '0' .. '9'); + pragma Loop_Invariant (Pow = Big_10 ** (Nb_Digits - J + 1)); + pragma Loop_Invariant (Big (Uns_Value) = Big (Uns_T) / Pow); + pragma Loop_Invariant + (Scan_Based_Number_Ghost + (Str => S, + From => P + J, + To => P + Nb_Digits, + Base => 10, + Acc => Uns_Value) + = Wrap_Option (Uns_T)); end loop; + pragma Assert (Big (Uns_Value) = Big (Uns_T) / Big_10 ** (Nb_Digits)); + pragma Assert (Uns_Value = 0); + Prove_Unchanged; + pragma Assert + (Scan_Based_Number_Ghost + (Str => S, + From => P + 1, + To => P + Nb_Digits, + Base => 10, + Acc => Uns_Value) + = Wrap_Option (Uns_T)); + P := P + Nb_Digits; end Set_Digits; diff --git a/gcc/ada/libgnat/s-imagei.ads b/gcc/ada/libgnat/s-imagei.ads index 7d2434b7c45..10116d123ed 100644 --- a/gcc/ada/libgnat/s-imagei.ads +++ b/gcc/ada/libgnat/s-imagei.ads @@ -33,17 +33,45 @@ -- signed integer types, and also for conversion operations required in -- Text_IO.Integer_IO for such types. +-- 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); + +with System.Val_Util; + generic - type Int is range <>; + with package Int_Params is new System.Val_Util.Int_Params (<>); package System.Image_I is - pragma Pure; + + subtype Int is Int_Params.Int; + use type Int_Params.Int; + + subtype Uns is Int_Params.Uns; + use type Int_Params.Uns; + + subtype Uns_Option is Int_Params.Uns_Option; + use type Int_Params.Uns_Option; procedure Image_Integer (V : Int; S : in out String; - P : out Natural); + P : out Natural) + with + Pre => S'First = 1 + and then S'Last < Integer'Last + and then S'Last >= Int_Params.Unsigned_Width_Ghost, + Post => P in S'Range + and then Int_Params.Value_Integer (S (1 .. P)) = V; -- Computes Int'Image (V) and stores the result in S (1 .. P) -- setting the resulting value of P. The caller guarantees that S -- is long enough to hold the result, and that S'First is 1. @@ -51,7 +79,31 @@ package System.Image_I is procedure Set_Image_Integer (V : Int; S : in out String; - P : in out Natural); + P : in out Natural) + with + Pre => P < Integer'Last + and then S'Last < Integer'Last + and then S'First <= P + 1 + and then S'First <= S'Last + and then + (if V >= 0 then + P <= S'Last - Int_Params.Unsigned_Width_Ghost + 1 + else + P <= S'Last - Int_Params.Unsigned_Width_Ghost), + Post => S (S'First .. P'Old) = S'Old (S'First .. P'Old) + and then + (declare + Minus : constant Boolean := S (P'Old + 1) = '-'; + Offset : constant Positive := (if V >= 0 then 1 else 2); + Abs_V : constant Uns := Int_Params.Abs_Uns_Of_Int (V); + begin + Minus = (V < 0) + and then P in P'Old + Offset .. S'Last + and then Int_Params.Only_Decimal_Ghost + (S, From => P'Old + Offset, To => P) + and then Int_Params.Scan_Based_Number_Ghost + (S, From => P'Old + Offset, To => P) + = Int_Params.Wrap_Option (Abs_V)); -- Stores the image of V in S starting at S (P + 1), P is updated to point -- to the last character stored. The value stored is identical to the value -- of Int'Image (V) except that no leading space is stored when V is diff --git a/gcc/ada/libgnat/s-imfi128.ads b/gcc/ada/libgnat/s-imfi128.ads index 4614455a4e9..7f64b83e9a8 100644 --- a/gcc/ada/libgnat/s-imfi128.ads +++ b/gcc/ada/libgnat/s-imfi128.ads @@ -39,8 +39,9 @@ with System.Image_F; package System.Img_Fixed_128 is subtype Int128 is Interfaces.Integer_128; + subtype Uns128 is Interfaces.Unsigned_128; - package Impl is new Image_F (Int128, Arith_128.Scaled_Divide128); + package Impl is new Image_F (Int128, Uns128, Arith_128.Scaled_Divide128); procedure Image_Fixed128 (V : Int128; diff --git a/gcc/ada/libgnat/s-imfi32.ads b/gcc/ada/libgnat/s-imfi32.ads index 492cc928120..e5c6ff8cbc8 100644 --- a/gcc/ada/libgnat/s-imfi32.ads +++ b/gcc/ada/libgnat/s-imfi32.ads @@ -39,8 +39,9 @@ with System.Image_F; package System.Img_Fixed_32 is subtype Int32 is Interfaces.Integer_32; + subtype Uns32 is Interfaces.Unsigned_32; - package Impl is new Image_F (Int32, Arith_32.Scaled_Divide32); + package Impl is new Image_F (Int32, Uns32, Arith_32.Scaled_Divide32); procedure Image_Fixed32 (V : Int32; diff --git a/gcc/ada/libgnat/s-imfi64.ads b/gcc/ada/libgnat/s-imfi64.ads index d51634c9414..91f4daf54eb 100644 --- a/gcc/ada/libgnat/s-imfi64.ads +++ b/gcc/ada/libgnat/s-imfi64.ads @@ -39,8 +39,9 @@ with System.Image_F; package System.Img_Fixed_64 is subtype Int64 is Interfaces.Integer_64; + subtype Uns64 is Interfaces.Unsigned_64; - package Impl is new Image_F (Int64, Arith_64.Scaled_Divide64); + package Impl is new Image_F (Int64, Uns64, Arith_64.Scaled_Divide64); procedure Image_Fixed64 (V : Int64; diff --git a/gcc/ada/libgnat/s-imgint.ads b/gcc/ada/libgnat/s-imgint.ads index 7b1fe22f3e6..fd5bea31c2a 100644 --- a/gcc/ada/libgnat/s-imgint.ads +++ b/gcc/ada/libgnat/s-imgint.ads @@ -33,12 +33,51 @@ -- signed integer types up to Integer, and also for conversion operations -- required in Text_IO.Integer_IO for such types. +-- 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); + with System.Image_I; +with System.Unsigned_Types; +with System.Val_Int; +with System.Val_Uns; +with System.Val_Util; +with System.Wid_Uns; + +package System.Img_Int + with SPARK_Mode +is + subtype Unsigned is Unsigned_Types.Unsigned; -package System.Img_Int is - pragma Pure; + package Int_Params is new Val_Util.Int_Params + (Int => Integer, + Uns => Unsigned, + Uns_Option => Val_Uns.Impl.Uns_Option, + Unsigned_Width_Ghost => + Wid_Uns.Width_Unsigned (0, Unsigned'Last), + Only_Decimal_Ghost => Val_Uns.Impl.Only_Decimal_Ghost, + Hexa_To_Unsigned_Ghost => + Val_Uns.Impl.Hexa_To_Unsigned_Ghost, + Wrap_Option => Val_Uns.Impl.Wrap_Option, + Scan_Based_Number_Ghost => + Val_Uns.Impl.Scan_Based_Number_Ghost, + Prove_Iter_Scan_Based_Number_Ghost => + Val_Uns.Impl.Prove_Iter_Scan_Based_Number_Ghost, + Is_Integer_Ghost => Val_Int.Impl.Is_Integer_Ghost, + Prove_Scan_Only_Decimal_Ghost => + Val_Int.Impl.Prove_Scan_Only_Decimal_Ghost, + Abs_Uns_Of_Int => Val_Int.Impl.Abs_Uns_Of_Int, + Value_Integer => Val_Int.Impl.Value_Integer); - package Impl is new Image_I (Integer); + package Impl is new Image_I (Int_Params); procedure Image_Integer (V : Integer; diff --git a/gcc/ada/libgnat/s-imglli.ads b/gcc/ada/libgnat/s-imglli.ads index fc773ae28d2..20f108c8e45 100644 --- a/gcc/ada/libgnat/s-imglli.ads +++ b/gcc/ada/libgnat/s-imglli.ads @@ -33,12 +33,51 @@ -- signed integer types larger than Integer, and also for conversion -- operations required in Text_IO.Integer_IO for such types. +-- 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); + with System.Image_I; +with System.Unsigned_Types; +with System.Val_LLI; +with System.Val_LLU; +with System.Val_Util; +with System.Wid_LLU; + +package System.Img_LLI + with SPARK_Mode +is + subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned; -package System.Img_LLI is - pragma Pure; + package Int_Params is new Val_Util.Int_Params + (Int => Long_Long_Integer, + Uns => Long_Long_Unsigned, + Uns_Option => Val_LLU.Impl.Uns_Option, + Unsigned_Width_Ghost => + Wid_LLU.Width_Long_Long_Unsigned (0, Long_Long_Unsigned'Last), + Only_Decimal_Ghost => Val_LLU.Impl.Only_Decimal_Ghost, + Hexa_To_Unsigned_Ghost => + Val_LLU.Impl.Hexa_To_Unsigned_Ghost, + Wrap_Option => Val_LLU.Impl.Wrap_Option, + Scan_Based_Number_Ghost => + Val_LLU.Impl.Scan_Based_Number_Ghost, + Prove_Iter_Scan_Based_Number_Ghost => + Val_LLU.Impl.Prove_Iter_Scan_Based_Number_Ghost, + Is_Integer_Ghost => Val_LLI.Impl.Is_Integer_Ghost, + Prove_Scan_Only_Decimal_Ghost => + Val_LLI.Impl.Prove_Scan_Only_Decimal_Ghost, + Abs_Uns_Of_Int => Val_LLI.Impl.Abs_Uns_Of_Int, + Value_Integer => Val_LLI.Impl.Value_Integer); - package Impl is new Image_I (Long_Long_Integer); + package Impl is new Image_I (Int_Params); procedure Image_Long_Long_Integer (V : Long_Long_Integer; diff --git a/gcc/ada/libgnat/s-imgllli.ads b/gcc/ada/libgnat/s-imgllli.ads index a5a10525924..989c296d759 100644 --- a/gcc/ada/libgnat/s-imgllli.ads +++ b/gcc/ada/libgnat/s-imgllli.ads @@ -33,12 +33,52 @@ -- signed integer types larger than Long_Long_Integer, and also for conversion -- operations required in Text_IO.Integer_IO for such types. +-- 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); + with System.Image_I; +with System.Unsigned_Types; +with System.Val_LLLI; +with System.Val_LLLU; +with System.Val_Util; +with System.Wid_LLLU; + +package System.Img_LLLI + with SPARK_Mode +is + subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned; -package System.Img_LLLI is - pragma Pure; + package Int_Params is new Val_Util.Int_Params + (Int => Long_Long_Long_Integer, + Uns => Long_Long_Long_Unsigned, + Uns_Option => Val_LLLU.Impl.Uns_Option, + Unsigned_Width_Ghost => + Wid_LLLU.Width_Long_Long_Long_Unsigned + (0, Long_Long_Long_Unsigned'Last), + Only_Decimal_Ghost => Val_LLLU.Impl.Only_Decimal_Ghost, + Hexa_To_Unsigned_Ghost => + Val_LLLU.Impl.Hexa_To_Unsigned_Ghost, + Wrap_Option => Val_LLLU.Impl.Wrap_Option, + Scan_Based_Number_Ghost => + Val_LLLU.Impl.Scan_Based_Number_Ghost, + Prove_Iter_Scan_Based_Number_Ghost => + Val_LLLU.Impl.Prove_Iter_Scan_Based_Number_Ghost, + Is_Integer_Ghost => Val_LLLI.Impl.Is_Integer_Ghost, + Prove_Scan_Only_Decimal_Ghost => + Val_LLLI.Impl.Prove_Scan_Only_Decimal_Ghost, + Abs_Uns_Of_Int => Val_LLLI.Impl.Abs_Uns_Of_Int, + Value_Integer => Val_LLLI.Impl.Value_Integer); - package Impl is new Image_I (Long_Long_Long_Integer); + package Impl is new Image_I (Int_Params); procedure Image_Long_Long_Long_Integer (V : Long_Long_Long_Integer; diff --git a/gcc/ada/libgnat/s-valint.ads b/gcc/ada/libgnat/s-valint.ads index c0d47aa1ce7..9e47f1bc9f0 100644 --- a/gcc/ada/libgnat/s-valint.ads +++ b/gcc/ada/libgnat/s-valint.ads @@ -57,6 +57,8 @@ package System.Val_Int with SPARK_Mode is (Int => Integer, Uns => Unsigned, Scan_Raw_Unsigned => Val_Uns.Scan_Raw_Unsigned, + Uns_Option => Val_Uns.Impl.Uns_Option, + Wrap_Option => Val_Uns.Impl.Wrap_Option, Is_Raw_Unsigned_Format_Ghost => Val_Uns.Impl.Is_Raw_Unsigned_Format_Ghost, Raw_Unsigned_Overflows_Ghost => @@ -64,7 +66,11 @@ package System.Val_Int with SPARK_Mode is Scan_Raw_Unsigned_Ghost => Val_Uns.Impl.Scan_Raw_Unsigned_Ghost, Raw_Unsigned_Last_Ghost => - Val_Uns.Impl.Raw_Unsigned_Last_Ghost); + Val_Uns.Impl.Raw_Unsigned_Last_Ghost, + Only_Decimal_Ghost => + Val_Uns.Impl.Only_Decimal_Ghost, + Scan_Based_Number_Ghost => + Val_Uns.Impl.Scan_Based_Number_Ghost); procedure Scan_Integer (Str : String; diff --git a/gcc/ada/libgnat/s-vallli.ads b/gcc/ada/libgnat/s-vallli.ads index dfb1729e41c..5bccb1a726b 100644 --- a/gcc/ada/libgnat/s-vallli.ads +++ b/gcc/ada/libgnat/s-vallli.ads @@ -58,6 +58,8 @@ package System.Val_LLI with SPARK_Mode is Uns => Long_Long_Unsigned, Scan_Raw_Unsigned => Val_LLU.Scan_Raw_Long_Long_Unsigned, + Uns_Option => Val_LLU.Impl.Uns_Option, + Wrap_Option => Val_LLU.Impl.Wrap_Option, Is_Raw_Unsigned_Format_Ghost => Val_LLU.Impl.Is_Raw_Unsigned_Format_Ghost, Raw_Unsigned_Overflows_Ghost => @@ -65,7 +67,11 @@ package System.Val_LLI with SPARK_Mode is Scan_Raw_Unsigned_Ghost => Val_LLU.Impl.Scan_Raw_Unsigned_Ghost, Raw_Unsigned_Last_Ghost => - Val_LLU.Impl.Raw_Unsigned_Last_Ghost); + Val_LLU.Impl.Raw_Unsigned_Last_Ghost, + Only_Decimal_Ghost => + Val_LLU.Impl.Only_Decimal_Ghost, + Scan_Based_Number_Ghost => + Val_LLU.Impl.Scan_Based_Number_Ghost); procedure Scan_Long_Long_Integer (Str : String; diff --git a/gcc/ada/libgnat/s-valllli.ads b/gcc/ada/libgnat/s-valllli.ads index 84bca5878ed..586c7379d21 100644 --- a/gcc/ada/libgnat/s-valllli.ads +++ b/gcc/ada/libgnat/s-valllli.ads @@ -58,6 +58,8 @@ package System.Val_LLLI with SPARK_Mode is Uns => Long_Long_Long_Unsigned, Scan_Raw_Unsigned => Val_LLLU.Scan_Raw_Long_Long_Long_Unsigned, + Uns_Option => Val_LLLU.Impl.Uns_Option, + Wrap_Option => Val_LLLU.Impl.Wrap_Option, Is_Raw_Unsigned_Format_Ghost => Val_LLLU.Impl.Is_Raw_Unsigned_Format_Ghost, Raw_Unsigned_Overflows_Ghost => @@ -65,7 +67,11 @@ package System.Val_LLLI with SPARK_Mode is Scan_Raw_Unsigned_Ghost => Val_LLLU.Impl.Scan_Raw_Unsigned_Ghost, Raw_Unsigned_Last_Ghost => - Val_LLLU.Impl.Raw_Unsigned_Last_Ghost); + Val_LLLU.Impl.Raw_Unsigned_Last_Ghost, + Only_Decimal_Ghost => + Val_LLLU.Impl.Only_Decimal_Ghost, + Scan_Based_Number_Ghost => + Val_LLLU.Impl.Scan_Based_Number_Ghost); procedure Scan_Long_Long_Long_Integer (Str : String; diff --git a/gcc/ada/libgnat/s-valuei.adb b/gcc/ada/libgnat/s-valuei.adb index 68d898448bf..b453ffc38da 100644 --- a/gcc/ada/libgnat/s-valuei.adb +++ b/gcc/ada/libgnat/s-valuei.adb @@ -41,6 +41,59 @@ package body System.Value_I is Assert_And_Cut => Ignore, Subprogram_Variant => Ignore); + ----------------------------------- + -- Prove_Scan_Only_Decimal_Ghost -- + ----------------------------------- + + procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) is + Non_Blank : constant Positive := First_Non_Space_Ghost + (Str, Str'First, Str'Last); + pragma Assert + (if Val < 0 then Non_Blank = Str'First + else + Only_Space_Ghost (Str, Str'First, Str'First) + and then Non_Blank = Str'First + 1); + Minus : constant Boolean := Str (Non_Blank) = '-'; + Fst_Num : constant Positive := + (if Minus then Non_Blank + 1 else Non_Blank); + pragma Assert (Fst_Num = Str'First + 1); + Uval : constant Uns := + Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last); + + procedure Unique_Int_Of_Uns (Val1, Val2 : Int) + with + Pre => Uns_Is_Valid_Int (Minus, Uval) + and then Is_Int_Of_Uns (Minus, Uval, Val1) + and then Is_Int_Of_Uns (Minus, Uval, Val2), + Post => Val1 = Val2; + -- Local proof of the unicity of the signed representation + + procedure Unique_Int_Of_Uns (Val1, Val2 : Int) is null; + + -- Start of processing for Prove_Scan_Only_Decimal_Ghost + + begin + pragma Assert (Minus = (Val < 0)); + pragma Assert (Uval = Abs_Uns_Of_Int (Val)); + pragma Assert (if Minus then Uval <= Uns (Int'Last) + 1 + else Uval <= Uns (Int'Last)); + pragma Assert (Uns_Is_Valid_Int (Minus, Uval)); + pragma Assert + (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First + elsif Minus then Val = -(Int (Uval)) + else Val = Int (Uval)); + pragma Assert (Is_Int_Of_Uns (Minus, Uval, Val)); + pragma Assert + (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))); + pragma Assert + (not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Str'Last)); + pragma Assert (Only_Space_Ghost + (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last)); + pragma Assert (Is_Integer_Ghost (Str)); + pragma Assert (Is_Value_Integer_Ghost (Str, Val)); + Unique_Int_Of_Uns (Val, Value_Integer (Str)); + end Prove_Scan_Only_Decimal_Ghost; + ------------------ -- Scan_Integer -- ------------------ diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads index a7e20abec65..d2e857a3de3 100644 --- a/gcc/ada/libgnat/s-valuei.ads +++ b/gcc/ada/libgnat/s-valuei.ads @@ -56,19 +56,31 @@ generic -- Additional parameters for ghost subprograms used inside contracts + type Uns_Option is private; + with function Wrap_Option (Value : Uns) return Uns_Option; with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean; with function Raw_Unsigned_Overflows_Ghost - (Str : String; - From, To : Integer) - return Boolean; + (Str : String; + From, To : Integer) + return Boolean; with function Scan_Raw_Unsigned_Ghost - (Str : String; - From, To : Integer) - return Uns; + (Str : String; + From, To : Integer) + return Uns; with function Raw_Unsigned_Last_Ghost - (Str : String; - From, To : Integer) - return Positive; + (Str : String; + From, To : Integer) + return Positive; + with function Only_Decimal_Ghost + (Str : String; + From, To : Integer) + return Boolean; + with function Scan_Based_Number_Ghost + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + return Uns_Option; package System.Value_I is pragma Preelaborate; @@ -96,6 +108,13 @@ package System.Value_I is Post => True; -- Return True if Uval (or -Uval when Minus is True) is equal to Val + function Abs_Uns_Of_Int (Val : Int) return Uns is + (if Val = Int'First then Uns (Int'Last) + 1 + elsif Val < 0 then Uns (-Val) + else Uns (Val)) + with Ghost; + -- Return the unsigned absolute value of Val + procedure Scan_Integer (Str : String; Ptr : not null access Integer; @@ -238,6 +257,22 @@ package System.Value_I is -- argument of the attribute. Constraint_Error is raised if the string is -- malformed, or if the value is out of range. + procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) + with + Ghost, + Pre => Str'Last /= Positive'Last + and then Str'Length >= 2 + and then Str (Str'First) in ' ' | '-' + and then (Str (Str'First) = '-') = (Val < 0) + and then Only_Decimal_Ghost (Str, Str'First + 1, Str'Last) + and then Scan_Based_Number_Ghost (Str, Str'First + 1, Str'Last) + = Wrap_Option (Abs_Uns_Of_Int (Val)), + Post => Is_Integer_Ghost (Slide_If_Necessary (Str)) + and then Value_Integer (Str) = Val; + -- Ghost lemma used in the proof of 'Image implementation, to prove that + -- the result of Value_Integer on a decimal string is the same as the + -- signing the result of Scan_Based_Number_Ghost. + private ---------------- diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads index 5c0f2a5d6bd..db1051b7e3f 100644 --- a/gcc/ada/libgnat/s-valuti.ads +++ b/gcc/ada/libgnat/s-valuti.ads @@ -376,6 +376,41 @@ is -- no check for this case, the caller must ensure this condition is met. pragma Warnings (GNATprove, On, """Ptr"" is not modified"); + -- Bundle Int type with other types, constants and subprograms used in + -- ghost code, so that this package can be instantiated once and used + -- multiple times as generic formal for a given Int type. + generic + type Int is range <>; + type Uns is mod <>; + type Uns_Option is private; + + Unsigned_Width_Ghost : Natural; + + with function Wrap_Option (Value : Uns) return Uns_Option; + with function Only_Decimal_Ghost + (Str : String; + From, To : Integer) + return Boolean; + with function Hexa_To_Unsigned_Ghost (X : Character) return Uns; + with function Scan_Based_Number_Ghost + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + return Uns_Option; + with function Is_Integer_Ghost (Str : String) return Boolean; + with procedure Prove_Iter_Scan_Based_Number_Ghost + (Str1, Str2 : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0); + with procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int); + with function Abs_Uns_Of_Int (Val : Int) return Uns; + with function Value_Integer (Str : String) return Int; + + package Int_Params is + end Int_Params; + private ------------------------ diff --git a/gcc/ada/libgnat/s-widthu.ads b/gcc/ada/libgnat/s-widthu.ads index 7bad3fd758e..2c583b31c6c 100644 --- a/gcc/ada/libgnat/s-widthu.ads +++ b/gcc/ada/libgnat/s-widthu.ads @@ -59,7 +59,7 @@ is function Big (Arg : Uns) return Big_Integer renames Unsigned_Conversion.To_Big_Integer; - Big_10 : constant Big_Integer := Big (10) with Ghost; + Big_10 : constant Big_Integer := Big (Uns'(10)) with Ghost; -- Maximum value of exponent for 10 that fits in Uns'Base function Max_Log10 return Natural is
reply other threads:[~2022-05-12 12:40 UTC|newest] Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions: You may reply publicly to this message via plain-text email using any one of the following methods: * Save the following mbox file, import it into your mail client, and reply-to-all from there: mbox Avoid top-posting and favor interleaved quoting: https://en.wikipedia.org/wiki/Posting_style#Interleaved_style * Reply using the --to, --cc, and --in-reply-to switches of git-send-email(1): git send-email \ --in-reply-to=20220512124032.36717383D802@sourceware.org \ --to=pmderodat@gcc.gnu.org \ --cc=gcc-cvs@gcc.gnu.org \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting the In-Reply-To header via mailto: links, try the mailto: linkBe sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).