diff options
27 files changed, 793 insertions, 186 deletions
diff --git a/gcc/ada/gcc-interface/Make-lang.in b/gcc/ada/gcc-interface/Make-lang.in index a8d8899..1e245ed 100644 --- a/gcc/ada/gcc-interface/Make-lang.in +++ b/gcc/ada/gcc-interface/Make-lang.in @@ -486,6 +486,8 @@ GNAT_ADA_OBJS+= \ ada/libgnat/a-except.o \ ada/libgnat/a-exctra.o \ ada/libgnat/a-ioexce.o \ + ada/libgnat/a-nubinu.o \ + ada/libgnat/a-numeri.o \ ada/libgnat/ada.o \ ada/libgnat/g-byorma.o \ ada/libgnat/g-heasor.o \ @@ -542,7 +544,8 @@ GNAT_ADA_OBJS+= \ ada/libgnat/s-wchcnv.o \ ada/libgnat/s-wchcon.o \ ada/libgnat/s-wchjis.o \ - ada/libgnat/s-wchstw.o + ada/libgnat/s-wchstw.o \ + ada/libgnat/s-widuns.o endif # Object files for gnat executables @@ -649,6 +652,8 @@ GNATBIND_OBJS += \ ada/libgnat/a-assert.o \ ada/libgnat/a-elchha.o \ ada/libgnat/a-except.o \ + ada/libgnat/a-nubinu.o \ + ada/libgnat/a-numeri.o \ ada/libgnat/ada.o \ ada/libgnat/g-byorma.o \ ada/libgnat/g-hesora.o \ @@ -693,6 +698,7 @@ GNATBIND_OBJS += \ ada/libgnat/s-wchcon.o \ ada/libgnat/s-wchjis.o \ ada/libgnat/s-wchstw.o \ + ada/libgnat/s-widuns.o \ ada/adaint.o \ ada/argv.o \ ada/cio.o \ diff --git a/gcc/ada/libgnat/s-imaged.ads b/gcc/ada/libgnat/s-imaged.ads index 41c7515..f23eac8 100644 --- a/gcc/ada/libgnat/s-imaged.ads +++ b/gcc/ada/libgnat/s-imaged.ads @@ -38,7 +38,6 @@ generic type Int is range <>; package System.Image_D is - pragma Pure; procedure Image_Decimal (V : Int; diff --git a/gcc/ada/libgnat/s-imagef.ads b/gcc/ada/libgnat/s-imagef.ads index 67892b1..c16d2c5 100644 --- a/gcc/ada/libgnat/s-imagef.ads +++ b/gcc/ada/libgnat/s-imagef.ads @@ -43,7 +43,6 @@ generic Round : Boolean); package System.Image_F is - pragma Pure; procedure Image_Fixed (V : Int; diff --git a/gcc/ada/libgnat/s-imager.ads b/gcc/ada/libgnat/s-imager.ads index 2a6a321..6828b6f 100644 --- a/gcc/ada/libgnat/s-imager.ads +++ b/gcc/ada/libgnat/s-imager.ads @@ -48,7 +48,6 @@ generic P : in out Natural); package System.Image_R is - pragma Pure; procedure Image_Fixed_Point (V : Num; diff --git a/gcc/ada/libgnat/s-imageu.adb b/gcc/ada/libgnat/s-imageu.adb index 3ca5efc..87830df 100644 --- a/gcc/ada/libgnat/s-imageu.adb +++ b/gcc/ada/libgnat/s-imageu.adb @@ -29,8 +29,106 @@ -- -- ------------------------------------------------------------------------------ +with Ada.Numerics.Big_Numbers.Big_Integers_Ghost; +use Ada.Numerics.Big_Numbers.Big_Integers_Ghost; + package body System.Image_U 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, + Subprogram_Variant => Ignore); + + 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; + + -- Maximum value of exponent for 10 that fits in Uns'Base + function Max_Log10 return Natural is + (case Uns'Base'Size is + when 8 => 2, + when 16 => 4, + when 32 => 9, + when 64 => 19, + when 128 => 38, + when others => raise Program_Error) + 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); + + procedure Lemma_Unsigned_Width_Ghost + with + Ghost, + Post => Unsigned_Width_Ghost = Max_Log10 + 2; + + --------------------------- + -- 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; + + -------------------------------- + -- Lemma_Unsigned_Width_Ghost -- + -------------------------------- + + procedure Lemma_Unsigned_Width_Ghost is + begin + pragma Assert (Unsigned_Width_Ghost <= Max_Log10 + 2); + pragma Assert (Big (Uns'Last) > Big_10 ** Max_Log10); + pragma Assert (Big (Uns'Last) < Big_10 ** (Unsigned_Width_Ghost - 1)); + pragma Assert (Unsigned_Width_Ghost >= Max_Log10 + 2); + end Lemma_Unsigned_Width_Ghost; + -------------------- -- Image_Unsigned -- -------------------- @@ -41,10 +139,45 @@ package body System.Image_U is P : out Natural) is pragma Assert (S'First = 1); + + procedure Prove_Value_Unsigned + with + Ghost, + Pre => S'First = 1 + and then S'Last < Integer'Last + and then P in 2 .. S'Last + and then S (1) = ' ' + and then Only_Decimal_Ghost (S, From => 2, To => P) + and then Scan_Based_Number_Ghost (S, From => 2, To => P) + = Wrap_Option (V), + Post => Is_Unsigned_Ghost (S (1 .. P)) + and then Value_Unsigned (S (1 .. P)) = V; + -- Ghost lemma to prove the value of Value_Unsigned from the value of + -- Scan_Based_Number_Ghost on a decimal string. + + -------------------------- + -- Prove_Value_Unsigned -- + -------------------------- + + procedure Prove_Value_Unsigned 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 (V)); + Prove_Scan_Only_Decimal_Ghost (Str, V); + end Prove_Value_Unsigned; + + -- Start of processing for Image_Unsigned + begin S (1) := ' '; P := 1; Set_Image_Unsigned (V, S, P); + + Prove_Value_Unsigned; end Image_Unsigned; ------------------------ @@ -58,28 +191,203 @@ package body System.Image_U is is Nb_Digits : Natural := 0; Value : Uns := V; + + -- Local ghost variables + + Pow : Big_Positive := 1 with Ghost; + S_Init : constant String := S 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 (R : Uns) + with + Ghost, + Pre => R in 0 .. 9, + Post => Character'Val (48 + R) in '0' .. '9'; + -- Ghost lemma to prove the value of a character corresponding to the + -- next figure. + + procedure Prove_Hexa_To_Unsigned_Ghost (R : Uns) + with + Ghost, + Pre => R in 0 .. 9, + Post => Hexa_To_Unsigned_Ghost (Character'Val (48 + R)) = R; + -- 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_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 (R : Uns) is null; + procedure Prove_Hexa_To_Unsigned_Ghost (R : Uns) is null; + procedure Prove_Unchanged 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_Image_Unsigned + begin pragma Assert (P >= S'First - 1 and then P < S'Last and then P < Natural'Last); -- No check is done since, as documented in the specification, the -- caller guarantees that S is long enough to hold the result. + Lemma_Unsigned_Width_Ghost; + -- First we compute the number of characters needed for representing -- the number. loop + Lemma_Div_Commutation (Value, 10); + Lemma_Div_Twice (Big (V), Big_10 ** Nb_Digits, Big_10); + Value := Value / 10; Nb_Digits := Nb_Digits + 1; + Pow := Pow * 10; + + pragma Loop_Invariant (Nb_Digits in 1 .. Unsigned_Width_Ghost - 1); + pragma Loop_Invariant (Pow = Big_10 ** Nb_Digits); + pragma Loop_Invariant (Big (Value) = Big (V) / Pow); + pragma Loop_Variant (Decreases => Value); + exit when Value = 0; + + Lemma_Non_Zero (Value); + pragma Assert (Pow <= Big (Uns'Last)); end loop; Value := V; + Pow := 1; + + pragma Assert (Value = From_Big (Big (V) / Big_10 ** 0)); -- We now populate digits from the end of the string to the beginning - for J in reverse 1 .. Nb_Digits loop + for J in reverse 1 .. Nb_Digits loop + Lemma_Div_Commutation (Value, 10); + Lemma_Div_Twice (Big (V), Big_10 ** (Nb_Digits - J), Big_10); + Prove_Character_Val (Value rem 10); + Prove_Hexa_To_Unsigned_Ghost (Value rem 10); + + Prev_Value := Value; + Prev_S := S; + Pow := Pow * 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 (V) / Big_10 ** (Nb_Digits - J)) rem 10); + pragma Assert + (for all K in P + J + 1 .. P + Nb_Digits => S (K) in '0' .. '9'); + pragma Assert + (for all K in P + J + 1 .. P + Nb_Digits => + Hexa_To_Unsigned_Ghost (S (K)) = + From_Big (Big (V) / Big_10 ** (Nb_Digits - (K - P))) rem 10); + + 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 => Value); + + if J /= Nb_Digits then + pragma Assert + (Prev_Value = 10 * Value + Hexa_To_Unsigned_Ghost (S (P + J))); + 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 (V)); + + pragma Loop_Invariant (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 + (for all K in P + J .. P + Nb_Digits => + Hexa_To_Unsigned_Ghost (S (K)) = + From_Big (Big (V) / Big_10 ** (Nb_Digits - (K - P))) rem 10); + pragma Loop_Invariant (Pow = Big_10 ** (Nb_Digits - J + 1)); + pragma Loop_Invariant (Big (Value) = Big (V) / Pow); + pragma Loop_Invariant + (Scan_Based_Number_Ghost + (Str => S, + From => P + J, + To => P + Nb_Digits, + Base => 10, + Acc => Value) + = Wrap_Option (V)); end loop; + Prove_Unchanged; + pragma Assert + (Scan_Based_Number_Ghost + (Str => S, + From => P + 1, + To => P + Nb_Digits, + Base => 10, + Acc => Value) + = Wrap_Option (V)); + P := P + Nb_Digits; end Set_Image_Unsigned; diff --git a/gcc/ada/libgnat/s-imageu.ads b/gcc/ada/libgnat/s-imageu.ads index 5983e5d..d3f2981 100644 --- a/gcc/ada/libgnat/s-imageu.ads +++ b/gcc/ada/libgnat/s-imageu.ads @@ -33,17 +33,61 @@ -- modular integer types, and also for conversion operations required in -- Text_IO.Modular_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); + generic type Uns is mod <>; + type Uns_Option is private; + + -- Additional parameters for ghost subprograms used inside contracts + + 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_Unsigned_Ghost (Str : String) return Boolean; + with function Value_Unsigned (Str : String) return Uns; + 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 : Uns); package System.Image_U is - pragma Pure; procedure Image_Unsigned (V : Uns; 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 >= Unsigned_Width_Ghost, + Post => P in S'Range + and then Value_Unsigned (S (1 .. P)) = V; pragma Inline (Image_Unsigned); -- Computes Uns'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 @@ -52,7 +96,18 @@ package System.Image_U is procedure Set_Image_Unsigned (V : Uns; 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 (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 Uns'Image (V) except that no leading space is stored. The caller diff --git a/gcc/ada/libgnat/s-imde128.ads b/gcc/ada/libgnat/s-imde128.ads index e2caac8..2bd339f 100644 --- a/gcc/ada/libgnat/s-imde128.ads +++ b/gcc/ada/libgnat/s-imde128.ads @@ -37,7 +37,6 @@ with Interfaces; with System.Image_D; package System.Img_Decimal_128 is - pragma Pure; subtype Int128 is Interfaces.Integer_128; diff --git a/gcc/ada/libgnat/s-imde32.ads b/gcc/ada/libgnat/s-imde32.ads index 0397d9c..47d7792 100644 --- a/gcc/ada/libgnat/s-imde32.ads +++ b/gcc/ada/libgnat/s-imde32.ads @@ -37,7 +37,6 @@ with Interfaces; with System.Image_D; package System.Img_Decimal_32 is - pragma Pure; subtype Int32 is Interfaces.Integer_32; diff --git a/gcc/ada/libgnat/s-imde64.ads b/gcc/ada/libgnat/s-imde64.ads index c147cb0..d84f5c9 100644 --- a/gcc/ada/libgnat/s-imde64.ads +++ b/gcc/ada/libgnat/s-imde64.ads @@ -37,7 +37,6 @@ with Interfaces; with System.Image_D; package System.Img_Decimal_64 is - pragma Pure; subtype Int64 is Interfaces.Integer_64; diff --git a/gcc/ada/libgnat/s-imfi128.ads b/gcc/ada/libgnat/s-imfi128.ads index 2658454..4614455 100644 --- a/gcc/ada/libgnat/s-imfi128.ads +++ b/gcc/ada/libgnat/s-imfi128.ads @@ -37,7 +37,6 @@ with System.Arith_128; with System.Image_F; package System.Img_Fixed_128 is - pragma Pure; subtype Int128 is Interfaces.Integer_128; diff --git a/gcc/ada/libgnat/s-imfi32.ads b/gcc/ada/libgnat/s-imfi32.ads index d722e51..492cc92 100644 --- a/gcc/ada/libgnat/s-imfi32.ads +++ b/gcc/ada/libgnat/s-imfi32.ads @@ -37,7 +37,6 @@ with System.Arith_32; with System.Image_F; package System.Img_Fixed_32 is - pragma Pure; subtype Int32 is Interfaces.Integer_32; diff --git a/gcc/ada/libgnat/s-imfi64.ads b/gcc/ada/libgnat/s-imfi64.ads index c2e9f1b..d51634c 100644 --- a/gcc/ada/libgnat/s-imfi64.ads +++ b/gcc/ada/libgnat/s-imfi64.ads @@ -37,7 +37,6 @@ with System.Arith_64; with System.Image_F; package System.Img_Fixed_64 is - pragma Pure; subtype Int64 is Interfaces.Integer_64; diff --git a/gcc/ada/libgnat/s-imgflt.ads b/gcc/ada/libgnat/s-imgflt.ads index 59e5087..cc7df51 100644 --- a/gcc/ada/libgnat/s-imgflt.ads +++ b/gcc/ada/libgnat/s-imgflt.ads @@ -38,7 +38,6 @@ with System.Powten_Flt; with System.Unsigned_Types; package System.Img_Flt is - pragma Pure; package Impl is new Image_R (Float, diff --git a/gcc/ada/libgnat/s-imglfl.ads b/gcc/ada/libgnat/s-imglfl.ads index 2a27986..294990a 100644 --- a/gcc/ada/libgnat/s-imglfl.ads +++ b/gcc/ada/libgnat/s-imglfl.ads @@ -38,7 +38,6 @@ with System.Powten_LFlt; with System.Unsigned_Types; package System.Img_LFlt is - pragma Pure; -- Note that the following instantiation is really for a 32-bit target, -- where 128-bit integer types are not available. For a 64-bit targaet, diff --git a/gcc/ada/libgnat/s-imgllf.ads b/gcc/ada/libgnat/s-imgllf.ads index 074b37d..b10a029 100644 --- a/gcc/ada/libgnat/s-imgllf.ads +++ b/gcc/ada/libgnat/s-imgllf.ads @@ -38,7 +38,6 @@ with System.Powten_LLF; with System.Unsigned_Types; package System.Img_LLF is - pragma Pure; -- Note that the following instantiation is really for a 32-bit target, -- where 128-bit integer types are not available. For a 64-bit targaet, diff --git a/gcc/ada/libgnat/s-imglllu.ads b/gcc/ada/libgnat/s-imglllu.ads index ae918c4..0116aa8 100644 --- a/gcc/ada/libgnat/s-imglllu.ads +++ b/gcc/ada/libgnat/s-imglllu.ads @@ -33,15 +33,46 @@ -- modular integer types larger than Long_Long_Unsigned, and also for -- conversion operations required in Text_IO.Modular_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_U; with System.Unsigned_Types; +with System.Val_LLLU; +with System.Wid_LLLU; -package System.Img_LLLU is - pragma Pure; - +package System.Img_LLLU + with SPARK_Mode +is subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned; - package Impl is new Image_U (Long_Long_Long_Unsigned); + package Impl is new Image_U + (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, + Is_Unsigned_Ghost => Val_LLLU.Impl.Is_Unsigned_Ghost, + Value_Unsigned => Val_LLLU.Impl.Value_Unsigned, + Prove_Iter_Scan_Based_Number_Ghost => + Val_LLLU.Impl.Prove_Iter_Scan_Based_Number_Ghost, + Prove_Scan_Only_Decimal_Ghost => + Val_LLLU.Impl.Prove_Scan_Only_Decimal_Ghost); procedure Image_Long_Long_Long_Unsigned (V : Long_Long_Long_Unsigned; diff --git a/gcc/ada/libgnat/s-imgllu.ads b/gcc/ada/libgnat/s-imgllu.ads index 220228f..67372d7 100644 --- a/gcc/ada/libgnat/s-imgllu.ads +++ b/gcc/ada/libgnat/s-imgllu.ads @@ -33,15 +33,45 @@ -- modular integer types larger than Unsigned, and also for conversion -- operations required in Text_IO.Modular_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_U; with System.Unsigned_Types; +with System.Val_LLU; +with System.Wid_LLU; -package System.Img_LLU is - pragma Pure; - +package System.Img_LLU + with SPARK_Mode +is subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned; - package Impl is new Image_U (Long_Long_Unsigned); + package Impl is new Image_U + (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, + Is_Unsigned_Ghost => Val_LLU.Impl.Is_Unsigned_Ghost, + Value_Unsigned => Val_LLU.Impl.Value_Unsigned, + Prove_Iter_Scan_Based_Number_Ghost => + Val_LLU.Impl.Prove_Iter_Scan_Based_Number_Ghost, + Prove_Scan_Only_Decimal_Ghost => + Val_LLU.Impl.Prove_Scan_Only_Decimal_Ghost); procedure Image_Long_Long_Unsigned (V : Long_Long_Unsigned; diff --git a/gcc/ada/libgnat/s-imgrea.ads b/gcc/ada/libgnat/s-imgrea.ads index ca18d95..8d663b7 100644 --- a/gcc/ada/libgnat/s-imgrea.ads +++ b/gcc/ada/libgnat/s-imgrea.ads @@ -34,7 +34,6 @@ with System.Img_LLF; package System.Img_Real is - pragma Pure; procedure Set_Image_Real (V : Long_Long_Float; diff --git a/gcc/ada/libgnat/s-imguns.ads b/gcc/ada/libgnat/s-imguns.ads index c15a79d..fa903ce 100644 --- a/gcc/ada/libgnat/s-imguns.ads +++ b/gcc/ada/libgnat/s-imguns.ads @@ -33,15 +33,45 @@ -- modular integer types up to Unsigned, and also for conversion operations -- required in Text_IO.Modular_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_U; with System.Unsigned_Types; +with System.Val_Uns; +with System.Wid_Uns; -package System.Img_Uns is - pragma Pure; - +package System.Img_Uns + with SPARK_Mode +is subtype Unsigned is Unsigned_Types.Unsigned; - package Impl is new Image_U (Unsigned); + package Impl is new Image_U + (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, + Is_Unsigned_Ghost => Val_Uns.Impl.Is_Unsigned_Ghost, + Value_Unsigned => Val_Uns.Impl.Value_Unsigned, + Prove_Iter_Scan_Based_Number_Ghost => + Val_Uns.Impl.Prove_Iter_Scan_Based_Number_Ghost, + Prove_Scan_Only_Decimal_Ghost => + Val_Uns.Impl.Prove_Scan_Only_Decimal_Ghost); procedure Image_Unsigned (V : Unsigned; diff --git a/gcc/ada/libgnat/s-imguti.ads b/gcc/ada/libgnat/s-imguti.ads index 541c42b..37e592f 100644 --- a/gcc/ada/libgnat/s-imguti.ads +++ b/gcc/ada/libgnat/s-imguti.ads @@ -32,7 +32,6 @@ -- This package provides some common utilities used by the s-imgxxx files package System.Img_Util is - pragma Pure; Max_Real_Image_Length : constant := 5200; -- If Exp is set to zero and Aft is set to Text_IO.Field'Last (i.e., 255) diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb index 991d4a5..f1456a1 100644 --- a/gcc/ada/libgnat/s-valueu.adb +++ b/gcc/ada/libgnat/s-valueu.adb @@ -234,6 +234,77 @@ package body System.Value_U is end if; end Lemma_Scan_Digit; + ---------------------------------------- + -- Prove_Iter_Scan_Based_Number_Ghost -- + ---------------------------------------- + + procedure Prove_Iter_Scan_Based_Number_Ghost + (Str1, Str2 : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + is + begin + if From > To then + null; + elsif Str1 (From) = '_' then + Prove_Iter_Scan_Based_Number_Ghost + (Str1, Str2, From + 1, To, Base, Acc); + elsif Scan_Overflows_Ghost + (Hexa_To_Unsigned_Ghost (Str1 (From)), Base, Acc) + then + null; + else + Prove_Iter_Scan_Based_Number_Ghost + (Str1, Str2, From + 1, To, Base, + Base * Acc + Hexa_To_Unsigned_Ghost (Str1 (From))); + end if; + end Prove_Iter_Scan_Based_Number_Ghost; + + ----------------------------------- + -- Prove_Scan_Only_Decimal_Ghost -- + ----------------------------------- + + procedure Prove_Scan_Only_Decimal_Ghost + (Str : String; + Val : Uns) + is + Non_Blank : constant Positive := First_Non_Space_Ghost + (Str, Str'First, Str'Last); + pragma Assert (Non_Blank = Str'First + 1); + Fst_Num : constant Positive := + (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank); + pragma Assert (Fst_Num = Str'First + 1); + Last_Num_Init : constant Integer := + Last_Number_Ghost (Str (Str'First + 1 .. Str'Last)); + pragma Assert (Last_Num_Init = Str'Last); + 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'; + pragma Assert (Starts_As_Based = False); + Last_Num_Based : constant Integer := + (if Starts_As_Based + then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Str'Last)) + else Last_Num_Init); + pragma Assert (Last_Num_Based = Str'Last); + begin + pragma Assert + (Is_Opt_Exponent_Format_Ghost (Str (Str'Last + 1 .. Str'Last))); + pragma Assert + (Is_Natural_Format_Ghost (Str (Str'First + 1 .. Str'Last))); + pragma Assert + (Is_Raw_Unsigned_Format_Ghost (Str (Str'First + 1 .. Str'Last))); + pragma Assert + (not Raw_Unsigned_Overflows_Ghost (Str, Str'First + 1, Str'Last)); + pragma Assert (Val = Exponent_Unsigned_Ghost (Val, 0, 10).Value); + pragma Assert + (Val = Scan_Raw_Unsigned_Ghost (Str, Str'First + 1, Str'Last)); + pragma Assert (Is_Unsigned_Ghost (Str)); + pragma Assert (Is_Value_Unsigned_Ghost (Str, Val)); + end Prove_Scan_Only_Decimal_Ghost; + ----------------------- -- Scan_Raw_Unsigned -- ----------------------- diff --git a/gcc/ada/libgnat/s-valueu.ads b/gcc/ada/libgnat/s-valueu.ads index b0e3b1e..6245c47 100644 --- a/gcc/ada/libgnat/s-valueu.ads +++ b/gcc/ada/libgnat/s-valueu.ads @@ -62,7 +62,24 @@ package System.Value_U is when False => Value : Uns := 0; end case; - end record with Ghost; + end record; + + function Wrap_Option (Value : Uns) return Uns_Option is + (Overflow => False, Value => Value) + with + Ghost; + + function Only_Decimal_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 decimal characters + -- from index From to index To. function Only_Hexa_Ghost (Str : String; From, To : Integer) return Boolean is @@ -535,6 +552,46 @@ package System.Value_U is -- is the string argument of the attribute. Constraint_Error is raised if -- the string is malformed, or if the value is out of range. + procedure Prove_Iter_Scan_Based_Number_Ghost + (Str1, Str2 : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + with + Ghost, + Subprogram_Variant => (Increases => From), + Pre => Str1'Last /= Positive'Last + and then Str2'Last /= Positive'Last + and then + (From > To or else (From >= Str1'First and then To <= Str1'Last)) + and then + (From > To or else (From >= Str2'First and then To <= Str2'Last)) + and then Only_Hexa_Ghost (Str1, From, To) + 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 used in the proof of 'Image implementation, to prove the + -- preservation of Scan_Based_Number_Ghost across an update in the string + -- in lower indexes. + + procedure Prove_Scan_Only_Decimal_Ghost + (Str : String; + Val : Uns) + with + Ghost, + Pre => Str'Last /= Positive'Last + and then Str'Length >= 2 + and then Str (Str'First) = ' ' + 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 (Val), + Post => Is_Unsigned_Ghost (Slide_If_Necessary (Str)) + and then Value_Unsigned (Str) = Val; + -- Ghost lemma used in the proof of 'Image implementation, to prove that + -- the result of Value_Unsigned on a decimal string is the same as the + -- result of Scan_Based_Number_Ghost. + private ----------------------------- diff --git a/gcc/ada/libgnat/s-widlllu.ads b/gcc/ada/libgnat/s-widlllu.ads index 802c74a..e9b6f9b 100644 --- a/gcc/ada/libgnat/s-widlllu.ads +++ b/gcc/ada/libgnat/s-widlllu.ads @@ -50,8 +50,11 @@ package System.Wid_LLLU is subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned; - function Width_Long_Long_Long_Unsigned is - new Width_U (Long_Long_Long_Unsigned); - pragma Pure_Function (Width_Long_Long_Long_Unsigned); + package Width_Uns is new Width_U (Long_Long_Long_Unsigned); + + function Width_Long_Long_Long_Unsigned + (Lo, Hi : Long_Long_Long_Unsigned) + return Natural + renames Width_Uns.Width; end System.Wid_LLLU; diff --git a/gcc/ada/libgnat/s-widllu.ads b/gcc/ada/libgnat/s-widllu.ads index eafb04f..7276d02 100644 --- a/gcc/ada/libgnat/s-widllu.ads +++ b/gcc/ada/libgnat/s-widllu.ads @@ -50,7 +50,11 @@ package System.Wid_LLU is subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned; - function Width_Long_Long_Unsigned is new Width_U (Long_Long_Unsigned); - pragma Pure_Function (Width_Long_Long_Unsigned); + package Width_Uns is new Width_U (Long_Long_Unsigned); + + function Width_Long_Long_Unsigned + (Lo, Hi : Long_Long_Unsigned) + return Natural + renames Width_Uns.Width; end System.Wid_LLU; diff --git a/gcc/ada/libgnat/s-widthu.adb b/gcc/ada/libgnat/s-widthu.adb index e23ecef..390942c 100644 --- a/gcc/ada/libgnat/s-widthu.adb +++ b/gcc/ada/libgnat/s-widthu.adb @@ -29,157 +29,138 @@ -- -- ------------------------------------------------------------------------------ -with Ada.Numerics.Big_Numbers.Big_Integers_Ghost; -use Ada.Numerics.Big_Numbers.Big_Integers_Ghost; - -function System.Width_U (Lo, Hi : Uns) return Natural is +package body System.Width_U 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); - - ----------------------- - -- Local Subprograms -- - ----------------------- - - package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns); - - function Big (Arg : Uns) return Big_Integer renames - Unsigned_Conversion.To_Big_Integer; - - -- Maximum value of exponent for 10 that fits in Uns'Base - function Max_Log10 return Natural is - (case Uns'Base'Size is - when 8 => 2, - when 16 => 4, - when 32 => 9, - when 64 => 19, - when 128 => 38, - when others => raise Program_Error) - with Ghost; - - ------------------ - -- Local Lemmas -- - ------------------ - - procedure Lemma_Lower_Mult (A, B, C : Big_Natural) - with - Ghost, - Pre => A <= B, - Post => A * C <= B * C; - - 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_Lower_Mult -- - ---------------------- - - procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is null; - - --------------------------- - -- Lemma_Div_Commutation -- - --------------------------- - - 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; - - -- Local variables - - W : Natural; - T : Uns; - - -- Local ghost variables - - Max_W : constant Natural := Max_Log10 with Ghost; - Big_10 : constant Big_Integer := Big (10) with Ghost; - - Pow : Big_Integer := 1 with Ghost; - T_Init : constant Uns := Uns'Max (Lo, Hi) with Ghost; - --- Start of processing for System.Width_U - -begin - if Lo > Hi then - return 0; - - else - -- Minimum value is 2, one for space, one for digit - - W := 2; - - -- Get max of absolute values + pragma Assertion_Policy (Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore, + Assert_And_Cut => Ignore, + Subprogram_Variant => Ignore); + + function Width (Lo, Hi : Uns) return Natural 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); + + ------------------ + -- Local Lemmas -- + ------------------ + + procedure Lemma_Lower_Mult (A, B, C : Big_Natural) + with + Ghost, + Pre => A <= B, + Post => A * C <= B * C; + + 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_Lower_Mult -- + ---------------------- + + procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is null; + + --------------------------- + -- Lemma_Div_Commutation -- + --------------------------- + + 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; - T := Uns'Max (Lo, Hi); + -- Local variables - -- Increase value if more digits required + W : Natural; + T : Uns; - while T >= 10 loop - Lemma_Div_Commutation (T, 10); - Lemma_Div_Twice (Big (T_Init), Big_10 ** (W - 2), Big_10); + -- Local ghost variables - T := T / 10; - W := W + 1; - Pow := Pow * 10; + Max_W : constant Natural := Max_Log10 with Ghost; + Pow : Big_Integer := 1 with Ghost; + T_Init : constant Uns := Uns'Max (Lo, Hi) with Ghost; - pragma Loop_Invariant (W in 3 .. Max_W + 3); - pragma Loop_Invariant (Pow = Big_10 ** (W - 2)); - pragma Loop_Invariant (Big (T) = Big (T_Init) / Pow); - pragma Loop_Variant (Decreases => T); - end loop; + -- Start of processing for System.Width_U - declare - F : constant Big_Integer := Big_10 ** (W - 2) with Ghost; - Q : constant Big_Integer := Big (T_Init) / F with Ghost; - R : constant Big_Integer := Big (T_Init) rem F with Ghost; - begin - pragma Assert (Q < Big_10); - pragma Assert (Big (T_Init) = Q * F + R); - Lemma_Lower_Mult (Q, Big (9), F); - pragma Assert (Big (T_Init) <= Big (9) * F + F - 1); - pragma Assert (Big (T_Init) < Big_10 * F); - pragma Assert (Big_10 * F = Big_10 ** (W - 1)); - end; - - -- This is an expression of the functional postcondition for Width_U, - -- which cannot be expressed readily as a postcondition as this would - -- require making the instantiation Unsigned_Conversion and function - -- Big available from the spec. - - pragma Assert (Big (Lo) < Big_10 ** (W - 1)); - pragma Assert (Big (Hi) < Big_10 ** (W - 1)); - - return W; - end if; + begin + if Lo > Hi then + return 0; + + else + -- Minimum value is 2, one for space, one for digit + + W := 2; + + -- Get max of absolute values + + T := Uns'Max (Lo, Hi); + + -- Increase value if more digits required + + while T >= 10 loop + Lemma_Div_Commutation (T, 10); + Lemma_Div_Twice (Big (T_Init), Big_10 ** (W - 2), Big_10); + + T := T / 10; + W := W + 1; + Pow := Pow * 10; + + pragma Loop_Invariant (W in 3 .. Max_W + 2); + pragma Loop_Invariant (Pow = Big_10 ** (W - 2)); + pragma Loop_Invariant (Big (T) = Big (T_Init) / Pow); + pragma Loop_Variant (Decreases => T); + end loop; + + declare + F : constant Big_Integer := Big_10 ** (W - 2) with Ghost; + Q : constant Big_Integer := Big (T_Init) / F with Ghost; + R : constant Big_Integer := Big (T_Init) rem F with Ghost; + begin + pragma Assert (Q < Big_10); + pragma Assert (Big (T_Init) = Q * F + R); + Lemma_Lower_Mult (Q, Big (9), F); + pragma Assert (Big (T_Init) <= Big (9) * F + F - 1); + pragma Assert (Big (T_Init) < Big_10 * F); + pragma Assert (Big_10 * F = Big_10 ** (W - 1)); + end; + + return W; + end if; + end Width; end System.Width_U; diff --git a/gcc/ada/libgnat/s-widthu.ads b/gcc/ada/libgnat/s-widthu.ads index 7611e8d..7bad3fd 100644 --- a/gcc/ada/libgnat/s-widthu.ads +++ b/gcc/ada/libgnat/s-widthu.ads @@ -29,16 +29,59 @@ -- -- ------------------------------------------------------------------------------ +-- 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); + -- Compute Width attribute for non-static type derived from a modular integer -- type. The arguments Lo, Hi are the bounds of the type. +with Ada.Numerics.Big_Numbers.Big_Integers_Ghost; +use Ada.Numerics.Big_Numbers.Big_Integers_Ghost; + generic type Uns is mod <>; -function System.Width_U (Lo, Hi : Uns) return Natural -with - Post => (if Lo > Hi then - System.Width_U'Result = 0 - else - System.Width_U'Result > 0); +package System.Width_U + with Pure +is + package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns); + + function Big (Arg : Uns) return Big_Integer renames + Unsigned_Conversion.To_Big_Integer; + + Big_10 : constant Big_Integer := Big (10) with Ghost; + + -- Maximum value of exponent for 10 that fits in Uns'Base + function Max_Log10 return Natural is + (case Uns'Base'Size is + when 8 => 2, + when 16 => 4, + when 32 => 9, + when 64 => 19, + when 128 => 38, + when others => raise Program_Error) + with Ghost; + + function Width (Lo, Hi : Uns) return Natural + with + Post => + (declare + W : constant Natural := System.Width_U.Width'Result; + begin + (if Lo > Hi then W = 0 + else W > 0 + and then W <= Max_Log10 + 2 + and then Big (Lo) < Big_10 ** (W - 1) + and then Big (Hi) < Big_10 ** (W - 1))); + +end System.Width_U; diff --git a/gcc/ada/libgnat/s-widuns.ads b/gcc/ada/libgnat/s-widuns.ads index 19d3261..137b881 100644 --- a/gcc/ada/libgnat/s-widuns.ads +++ b/gcc/ada/libgnat/s-widuns.ads @@ -50,7 +50,9 @@ package System.Wid_Uns is subtype Unsigned is Unsigned_Types.Unsigned; - function Width_Unsigned is new Width_U (Unsigned); - pragma Pure_Function (Width_Unsigned); + package Width_Uns is new Width_U (Unsigned); + + function Width_Unsigned (Lo, Hi : Unsigned) return Natural + renames Width_Uns.Width; end System.Wid_Uns; |