diff options
| author | Claire Dross <dross@adacore.com> | 2023-06-15 16:22:11 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-07-06 13:36:10 +0200 |
| commit | 70bcf5c4d39abb26106bb00faceb411c5b8d0c1b (patch) | |
| tree | 9ad344a94dab247734ecefa65a34ed77727bbfc2 | |
| parent | 15e2d19ff46527d56407eaea64161943efc3e2b7 (diff) | |
| download | gcc-70bcf5c4d39abb26106bb00faceb411c5b8d0c1b.zip gcc-70bcf5c4d39abb26106bb00faceb411c5b8d0c1b.tar.gz gcc-70bcf5c4d39abb26106bb00faceb411c5b8d0c1b.tar.bz2 | |
ada: Refactor the proof of the Value and Image runtime units
The aim of this refactoring is to avoid unnecessary dependencies
between Image and Value units even though they share the same
specification functions. These functions are grouped inside ghost
packages which are then withed by Image and Value units.
gcc/ada/
* libgnat/s-vs_int.ads: Instance of Value_I_Spec for Integer.
* libgnat/s-vs_lli.ads: Instance of Value_I_Spec for
Long_Long_Integer.
* libgnat/s-vsllli.ads: Instance of Value_I_Spec for
Long_Long_Long_Integer.
* libgnat/s-vs_uns.ads: Instance of Value_U_Spec for Unsigned.
* libgnat/s-vs_llu.ads: Instance of Value_U_Spec for
Long_Long_Unsigned.
* libgnat/s-vslllu.ads: Instance of Value_U_Spec for
Long_Long_Long_Unsigned.
* libgnat/s-imagei.ads: Take instances of Value_*_Spec as
parameters.
* libgnat/s-imagei.adb: Idem.
* libgnat/s-imageu.ads: Idem.
* libgnat/s-imageu.adb: Idem.
* libgnat/s-valuei.ads: Idem.
* libgnat/s-valuei.adb: Idem.
* libgnat/s-valueu.ads: Idem.
* libgnat/s-valueu.adb: Idem.
* libgnat/s-imgint.ads: Adapt instance to new ghost parameters.
* libgnat/s-imglli.ads: Adapt instance to new ghost parameters.
* libgnat/s-imgllli.ads: Adapt instance to new ghost parameters.
* libgnat/s-imglllu.ads: Adapt instance to new ghost parameters.
* libgnat/s-imgllu.ads: Adapt instance to new ghost parameters.
* libgnat/s-imguns.ads: Adapt instance to new ghost parameters.
* libgnat/s-valint.ads: Adapt instance to new ghost parameters.
* libgnat/s-vallli.ads: Adapt instance to new ghost parameters.
* libgnat/s-valllli.ads: Adapt instance to new ghost parameters.
* libgnat/s-vallllu.ads: Adapt instance to new ghost parameters.
* libgnat/s-valllu.ads: Adapt instance to new ghost parameters.
* libgnat/s-valuns.ads: Adapt instance to new ghost parameters.
* libgnat/s-vaispe.ads: Take instance of Value_U_Spec as parameter
and remove unused declaration.
* libgnat/s-vaispe.adb: Idem.
* libgnat/s-vauspe.ads: Remove unused declaration.
* libgnat/s-valspe.ads: Factor out the specification part of
Val_Util.
* libgnat/s-valspe.adb: Idem.
* libgnat/s-valuti.ads: Move specification to Val_Spec.
* libgnat/s-valuti.adb: Idem.
* libgnat/s-valboo.ads: Use Val_Spec.
* libgnat/s-valboo.adb: Idem.
* libgnat/s-imgboo.adb: Idem.
* libgnat/s-imagef.adb: Adapt instances to new ghost parameters.
* Makefile.rtl: List new files.
38 files changed, 835 insertions, 729 deletions
diff --git a/gcc/ada/Makefile.rtl b/gcc/ada/Makefile.rtl index ca4c528..b94caa4 100644 --- a/gcc/ada/Makefile.rtl +++ b/gcc/ada/Makefile.rtl @@ -772,6 +772,7 @@ GNATRTL_NONTASKING_OBJS= \ s-vallli$(objext) \ s-valllu$(objext) \ s-valrea$(objext) \ + s-valspe$(objext) \ s-valued$(objext) \ s-valuef$(objext) \ s-valuei$(objext) \ @@ -785,6 +786,10 @@ GNATRTL_NONTASKING_OBJS= \ s-veboop$(objext) \ s-vector$(objext) \ s-vercon$(objext) \ + s-vs_int$(objext) \ + s-vs_lli$(objext) \ + s-vs_llu$(objext) \ + s-vs_uns$(objext) \ s-wchcnv$(objext) \ s-wchcon$(objext) \ s-wchjis$(objext) \ @@ -1030,6 +1035,8 @@ GNATRTL_128BIT_OBJS = \ s-vafi128$(objext) \ s-valllli$(objext) \ s-vallllu$(objext) \ + s-vsllli$(objext) \ + s-vslllu$(objext) \ s-widllli$(objext) \ s-widlllu$(objext) diff --git a/gcc/ada/libgnat/s-imagef.adb b/gcc/ada/libgnat/s-imagef.adb index a10dfdc..3f6bfa2 100644 --- a/gcc/ada/libgnat/s-imagef.adb +++ b/gcc/ada/libgnat/s-imagef.adb @@ -70,16 +70,14 @@ 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. - Unsigned_Width_Ghost : constant Natural := Int'Width; - package Uns_Spec is new System.Value_U_Spec (Uns); - package Int_Spec is new System.Value_I_Spec (Int, Uns, Uns_Spec.Uns_Params); + package Int_Spec is new System.Value_I_Spec (Int, Uns, Uns_Spec); package Image_I is new System.Image_I - (Int => Int, - Uns => Uns, - Unsigned_Width_Ghost => Unsigned_Width_Ghost, - Int_Params => Int_Spec.Int_Params); + (Int => Int, + Uns => Uns, + U_Spec => Uns_Spec, + I_Spec => Int_Spec); procedure Set_Image_Integer (V : Int; diff --git a/gcc/ada/libgnat/s-imagei.adb b/gcc/ada/libgnat/s-imagei.adb index a56d635..cbe03e7 100644 --- a/gcc/ada/libgnat/s-imagei.adb +++ b/gcc/ada/libgnat/s-imagei.adb @@ -32,6 +32,8 @@ with Ada.Numerics.Big_Numbers.Big_Integers_Ghost; use Ada.Numerics.Big_Numbers.Big_Integers_Ghost; +with System.Val_Spec; + package body System.Image_I is -- Ghost code, loop invariants and assertions in this unit are meant for @@ -149,7 +151,7 @@ package body System.Image_I is and then UP.Only_Decimal_Ghost (S, From => 2, To => P) and then UP.Scan_Based_Number_Ghost (S, From => 2, To => P) = UP.Wrap_Option (IP.Abs_Uns_Of_Int (V)), - Post => not System.Val_Util.Only_Space_Ghost (S, 1, P) + Post => not System.Val_Spec.Only_Space_Ghost (S, 1, P) and then IP.Is_Integer_Ghost (S (1 .. P)) and then IP.Is_Value_Integer_Ghost (S (1 .. P), V); -- Ghost lemma to prove the value of Value_Integer from the value of diff --git a/gcc/ada/libgnat/s-imagei.ads b/gcc/ada/libgnat/s-imagei.ads index 38c6e6e..7e39f86 100644 --- a/gcc/ada/libgnat/s-imagei.ads +++ b/gcc/ada/libgnat/s-imagei.ads @@ -45,23 +45,26 @@ pragma Assertion_Policy (Pre => Ignore, Ghost => Ignore, Subprogram_Variant => Ignore); -with System.Val_Util; +with System.Value_I_Spec; +with System.Value_U_Spec; generic type Int is range <>; type Uns is mod <>; - Unsigned_Width_Ghost : Natural; + -- Additional parameters for ghost subprograms used inside contracts - with package Int_Params is new System.Val_Util.Int_Params - (Int => Int, Uns => Uns, others => <>) - with Ghost; + with package U_Spec is new System.Value_U_Spec (Uns => Uns) with Ghost; + with package I_Spec is new System.Value_I_Spec + (Int => Int, Uns => Uns, U_Spec => U_Spec) with Ghost; package System.Image_I is - package IP renames Int_Params; - package UP renames IP.Uns_Params; + package IP renames I_Spec; + package UP renames U_Spec; use type UP.Uns_Option; + Unsigned_Width_Ghost : constant Natural := U_Spec.Max_Log10 + 2 with Ghost; + procedure Image_Integer (V : Int; S : in out String; diff --git a/gcc/ada/libgnat/s-imageu.adb b/gcc/ada/libgnat/s-imageu.adb index eb1d054..919b401 100644 --- a/gcc/ada/libgnat/s-imageu.adb +++ b/gcc/ada/libgnat/s-imageu.adb @@ -31,6 +31,7 @@ with Ada.Numerics.Big_Numbers.Big_Integers_Ghost; use Ada.Numerics.Big_Numbers.Big_Integers_Ghost; +with System.Val_Spec; package body System.Image_U is @@ -54,17 +55,6 @@ package body System.Image_U is 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 -- ------------------ @@ -86,11 +76,6 @@ package body System.Image_U is 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 -- --------------------------- @@ -117,18 +102,6 @@ package body System.Image_U is 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 -- -------------------- @@ -147,12 +120,12 @@ package body System.Image_U is and then S'Last < Integer'Last and then P in 2 .. S'Last and then S (1) = ' ' - and then Uns_Params.Only_Decimal_Ghost (S, From => 2, To => P) - and then Uns_Params.Scan_Based_Number_Ghost (S, From => 2, To => P) - = Uns_Params.Wrap_Option (V), - Post => not System.Val_Util.Only_Space_Ghost (S, 1, P) - and then Uns_Params.Is_Unsigned_Ghost (S (1 .. P)) - and then Uns_Params.Is_Value_Unsigned_Ghost (S (1 .. P), V); + and then U_Spec.Only_Decimal_Ghost (S, From => 2, To => P) + and then U_Spec.Scan_Based_Number_Ghost (S, From => 2, To => P) + = U_Spec.Wrap_Option (V), + Post => not System.Val_Spec.Only_Space_Ghost (S, 1, P) + and then U_Spec.Is_Unsigned_Ghost (S (1 .. P)) + and then U_Spec.Is_Value_Unsigned_Ghost (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. @@ -166,13 +139,13 @@ package body System.Image_U is pragma Assert (Str'First = 1); pragma Assert (S (2) /= ' '); pragma Assert - (Uns_Params.Only_Decimal_Ghost (Str, From => 2, To => P)); - Uns_Params.Prove_Scan_Based_Number_Ghost_Eq + (U_Spec.Only_Decimal_Ghost (Str, From => 2, To => P)); + U_Spec.Prove_Scan_Based_Number_Ghost_Eq (S, Str, From => 2, To => P); pragma Assert - (Uns_Params.Scan_Based_Number_Ghost (Str, From => 2, To => P) - = Uns_Params.Wrap_Option (V)); - Uns_Params.Prove_Scan_Only_Decimal_Ghost (Str, V); + (U_Spec.Scan_Based_Number_Ghost (Str, From => 2, To => P) + = U_Spec.Wrap_Option (V)); + U_Spec.Prove_Scan_Only_Decimal_Ghost (Str, V); end Prove_Value_Unsigned; -- Start of processing for Image_Unsigned @@ -227,7 +200,7 @@ package body System.Image_U is with Ghost, Pre => R in 0 .. 9, - Post => Uns_Params.Hexa_To_Unsigned_Ghost (Character'Val (48 + R)) = R; + Post => U_Spec.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. @@ -245,26 +218,26 @@ package body System.Image_U is and then (for all I in P + 1 .. Max => Prev_S (I) = S (I)) and then S (P) in '0' .. '9' and then V <= Uns'Last / 10 - and then Uns'Last - Uns_Params.Hexa_To_Unsigned_Ghost (S (P)) + and then Uns'Last - U_Spec.Hexa_To_Unsigned_Ghost (S (P)) >= 10 * V and then Prev_V = - V * 10 + Uns_Params.Hexa_To_Unsigned_Ghost (S (P)) + V * 10 + U_Spec.Hexa_To_Unsigned_Ghost (S (P)) and then (if P = Max then Prev_V = Res - else Uns_Params.Scan_Based_Number_Ghost + else U_Spec.Scan_Based_Number_Ghost (Str => Prev_S, From => P + 1, To => Max, Base => 10, - Acc => Prev_V) = Uns_Params.Wrap_Option (Res)), + Acc => Prev_V) = U_Spec.Wrap_Option (Res)), Post => (for all I in P .. Max => S (I) in '0' .. '9') - and then Uns_Params.Scan_Based_Number_Ghost + and then U_Spec.Scan_Based_Number_Ghost (Str => S, From => P, To => Max, Base => 10, - Acc => V) = Uns_Params.Wrap_Option (Res); + Acc => V) = U_Spec.Wrap_Option (Res); -- Ghost lemma to prove that Scan_Based_Number_Ghost is preserved -- through an iteration of the loop. @@ -287,17 +260,17 @@ package body System.Image_U is is pragma Unreferenced (Res); begin - Uns_Params.Lemma_Scan_Based_Number_Ghost_Step + U_Spec.Lemma_Scan_Based_Number_Ghost_Step (Str => S, From => P, To => Max, Base => 10, Acc => V); if P < Max then - Uns_Params.Prove_Scan_Based_Number_Ghost_Eq + U_Spec.Prove_Scan_Based_Number_Ghost_Eq (Prev_S, S, P + 1, Max, 10, Prev_V); else - Uns_Params.Lemma_Scan_Based_Number_Ghost_Base + U_Spec.Lemma_Scan_Based_Number_Ghost_Base (Str => S, From => P + 1, To => Max, @@ -314,8 +287,6 @@ package body System.Image_U is -- 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 @@ -359,7 +330,7 @@ package body System.Image_U is Prove_Euclidian (Val => Prev_Value, Quot => Value, - Rest => Uns_Params.Hexa_To_Unsigned_Ghost (S (P + J))); + Rest => U_Spec.Hexa_To_Unsigned_Ghost (S (P + J))); Prove_Scan_Iter (S, Prev_S, Value, Prev_Value, V, P + J, P + Nb_Digits); @@ -368,18 +339,18 @@ package body System.Image_U is pragma Loop_Invariant (for all K in S'First .. P => S (K) = S_Init (K)); pragma Loop_Invariant - (Uns_Params.Only_Decimal_Ghost + (U_Spec.Only_Decimal_Ghost (S, From => P + J, To => P + Nb_Digits)); pragma Loop_Invariant (Pow = Big_10 ** (Nb_Digits - J + 1)); pragma Loop_Invariant (Big (Value) = Big (V) / Pow); pragma Loop_Invariant - (Uns_Params.Scan_Based_Number_Ghost + (U_Spec.Scan_Based_Number_Ghost (Str => S, From => P + J, To => P + Nb_Digits, Base => 10, Acc => Value) - = Uns_Params.Wrap_Option (V)); + = U_Spec.Wrap_Option (V)); end loop; pragma Assert (Big (Value) = Big (V) / (Big_10 ** Nb_Digits)); pragma Assert (Value = 0); diff --git a/gcc/ada/libgnat/s-imageu.ads b/gcc/ada/libgnat/s-imageu.ads index 1c58ea1..cec5263 100644 --- a/gcc/ada/libgnat/s-imageu.ads +++ b/gcc/ada/libgnat/s-imageu.ads @@ -45,7 +45,7 @@ pragma Assertion_Policy (Pre => Ignore, Ghost => Ignore, Subprogram_Variant => Ignore); -with System.Val_Util; +with System.Value_U_Spec; generic @@ -53,14 +53,12 @@ generic -- Additional parameters for ghost subprograms used inside contracts - Unsigned_Width_Ghost : Natural; - - with package Uns_Params is new System.Val_Util.Uns_Params - (Uns => Uns, others => <>) - with Ghost; + with package U_Spec is new System.Value_U_Spec (Uns => Uns) with Ghost; package System.Image_U is - use all type Uns_Params.Uns_Option; + use all type U_Spec.Uns_Option; + + Unsigned_Width_Ghost : constant Natural := U_Spec.Max_Log10 + 2 with Ghost; procedure Image_Unsigned (V : Uns; @@ -71,7 +69,7 @@ package System.Image_U is and then S'Last < Integer'Last and then S'Last >= Unsigned_Width_Ghost, Post => P in S'Range - and then Uns_Params.Is_Value_Unsigned_Ghost (S (1 .. P), V); + and then U_Spec.Is_Value_Unsigned_Ghost (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 @@ -89,10 +87,10 @@ package System.Image_U is 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 Uns_Params.Only_Decimal_Ghost (S, From => P'Old + 1, To => P) - and then Uns_Params.Scan_Based_Number_Ghost + and then U_Spec.Only_Decimal_Ghost (S, From => P'Old + 1, To => P) + and then U_Spec.Scan_Based_Number_Ghost (S, From => P'Old + 1, To => P) - = Uns_Params.Wrap_Option (V); + = U_Spec.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-imgboo.adb b/gcc/ada/libgnat/s-imgboo.adb index fd1d9a6..fb3301a 100644 --- a/gcc/ada/libgnat/s-imgboo.adb +++ b/gcc/ada/libgnat/s-imgboo.adb @@ -37,7 +37,7 @@ pragma Assertion_Policy (Ghost => Ignore, Loop_Invariant => Ignore, Assert => Ignore); -with System.Val_Util; +with System.Val_Spec; package body System.Img_Bool with SPARK_Mode @@ -58,12 +58,12 @@ is S (1 .. 4) := "TRUE"; P := 4; pragma Assert - (System.Val_Util.First_Non_Space_Ghost (S, S'First, S'Last) = 1); + (System.Val_Spec.First_Non_Space_Ghost (S, S'First, S'Last) = 1); else S (1 .. 5) := "FALSE"; P := 5; pragma Assert - (System.Val_Util.First_Non_Space_Ghost (S, S'First, S'Last) = 1); + (System.Val_Spec.First_Non_Space_Ghost (S, S'First, S'Last) = 1); end if; end Image_Boolean; diff --git a/gcc/ada/libgnat/s-imgint.ads b/gcc/ada/libgnat/s-imgint.ads index 320edc9..fe93899 100644 --- a/gcc/ada/libgnat/s-imgint.ads +++ b/gcc/ada/libgnat/s-imgint.ads @@ -47,8 +47,8 @@ pragma Assertion_Policy (Pre => Ignore, with System.Image_I; with System.Unsigned_Types; -with System.Val_Int; -with System.Wid_Uns; +with System.Vs_Int; +with System.Vs_Uns; package System.Img_Int with SPARK_Mode @@ -56,11 +56,10 @@ is subtype Unsigned is Unsigned_Types.Unsigned; package Impl is new Image_I - (Int => Integer, - Uns => Unsigned, - Unsigned_Width_Ghost => - Wid_Uns.Width_Unsigned (0, Unsigned'Last), - Int_Params => System.Val_Int.Impl.Spec.Int_Params); + (Int => Integer, + Uns => Unsigned, + U_Spec => System.Vs_Uns.Spec, + I_Spec => System.Vs_Int.Spec); procedure Image_Integer (V : Integer; diff --git a/gcc/ada/libgnat/s-imglli.ads b/gcc/ada/libgnat/s-imglli.ads index 1d34e77..809ca10 100644 --- a/gcc/ada/libgnat/s-imglli.ads +++ b/gcc/ada/libgnat/s-imglli.ads @@ -47,8 +47,8 @@ pragma Assertion_Policy (Pre => Ignore, with System.Image_I; with System.Unsigned_Types; -with System.Val_LLI; -with System.Wid_LLU; +with System.Vs_LLI; +with System.Vs_LLU; package System.Img_LLI with SPARK_Mode @@ -56,12 +56,10 @@ is subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned; package Impl is new Image_I - (Int => Long_Long_Integer, - Uns => Long_Long_Unsigned, - Unsigned_Width_Ghost => - Wid_LLU.Width_Long_Long_Unsigned - (0, Long_Long_Unsigned'Last), - Int_Params => System.Val_LLI.Impl.Spec.Int_Params); + (Int => Long_Long_Integer, + Uns => Long_Long_Unsigned, + U_Spec => System.Vs_LLU.Spec, + I_Spec => System.Vs_LLI.Spec); 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 05dec5e..727388f 100644 --- a/gcc/ada/libgnat/s-imgllli.ads +++ b/gcc/ada/libgnat/s-imgllli.ads @@ -47,8 +47,8 @@ pragma Assertion_Policy (Pre => Ignore, with System.Image_I; with System.Unsigned_Types; -with System.Val_LLLI; -with System.Wid_LLLU; +with System.Vs_LLLI; +with System.Vs_LLLU; package System.Img_LLLI with SPARK_Mode @@ -56,12 +56,10 @@ is subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned; package Impl is new Image_I - (Int => Long_Long_Long_Integer, - Uns => Long_Long_Long_Unsigned, - Unsigned_Width_Ghost => - Wid_LLLU.Width_Long_Long_Long_Unsigned - (0, Long_Long_Long_Unsigned'Last), - Int_Params => System.Val_LLLI.Impl.Spec.Int_Params); + (Int => Long_Long_Long_Integer, + Uns => Long_Long_Long_Unsigned, + U_Spec => System.Vs_LLLU.Spec, + I_Spec => System.Vs_LLLI.Spec); procedure Image_Long_Long_Long_Integer (V : Long_Long_Long_Integer; diff --git a/gcc/ada/libgnat/s-imglllu.ads b/gcc/ada/libgnat/s-imglllu.ads index 888d782..09c8965 100644 --- a/gcc/ada/libgnat/s-imglllu.ads +++ b/gcc/ada/libgnat/s-imglllu.ads @@ -47,8 +47,7 @@ pragma Assertion_Policy (Pre => Ignore, with System.Image_U; with System.Unsigned_Types; -with System.Val_LLLU; -with System.Wid_LLLU; +with System.Vs_LLLU; package System.Img_LLLU with SPARK_Mode @@ -56,11 +55,8 @@ is subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned; package Impl is new Image_U - (Uns => Long_Long_Long_Unsigned, - Unsigned_Width_Ghost => - Wid_LLLU.Width_Long_Long_Long_Unsigned - (0, Long_Long_Long_Unsigned'Last), - Uns_Params => System.Val_LLLU.Impl.Spec.Uns_Params); + (Uns => Long_Long_Long_Unsigned, + U_Spec => System.Vs_LLLU.Spec); 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 b00dc66..9709c96 100644 --- a/gcc/ada/libgnat/s-imgllu.ads +++ b/gcc/ada/libgnat/s-imgllu.ads @@ -47,8 +47,7 @@ pragma Assertion_Policy (Pre => Ignore, with System.Image_U; with System.Unsigned_Types; -with System.Val_LLU; -with System.Wid_LLU; +with System.Vs_LLU; package System.Img_LLU with SPARK_Mode @@ -56,10 +55,8 @@ is subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned; package Impl is new Image_U - (Uns => Long_Long_Unsigned, - Unsigned_Width_Ghost => - Wid_LLU.Width_Long_Long_Unsigned (0, Long_Long_Unsigned'Last), - Uns_Params => System.Val_LLU.Impl.Spec.Uns_Params); + (Uns => Long_Long_Unsigned, + U_Spec => System.Vs_LLU.Spec); procedure Image_Long_Long_Unsigned (V : Long_Long_Unsigned; diff --git a/gcc/ada/libgnat/s-imguns.ads b/gcc/ada/libgnat/s-imguns.ads index 2bd7216..7c79a66 100644 --- a/gcc/ada/libgnat/s-imguns.ads +++ b/gcc/ada/libgnat/s-imguns.ads @@ -47,8 +47,7 @@ pragma Assertion_Policy (Pre => Ignore, with System.Image_U; with System.Unsigned_Types; -with System.Val_Uns; -with System.Wid_Uns; +with System.Vs_Uns; package System.Img_Uns with SPARK_Mode @@ -56,10 +55,8 @@ is subtype Unsigned is Unsigned_Types.Unsigned; package Impl is new Image_U - (Uns => Unsigned, - Unsigned_Width_Ghost => - Wid_Uns.Width_Unsigned (0, Unsigned'Last), - Uns_Params => System.Val_Uns.Impl.Spec.Uns_Params); + (Uns => Unsigned, + U_Spec => System.Vs_Uns.Spec); procedure Image_Unsigned (V : Unsigned; diff --git a/gcc/ada/libgnat/s-vaispe.adb b/gcc/ada/libgnat/s-vaispe.adb index b1a3884..a13dc6a 100644 --- a/gcc/ada/libgnat/s-vaispe.adb +++ b/gcc/ada/libgnat/s-vaispe.adb @@ -71,14 +71,14 @@ package body System.Value_I_Spec is begin Prove_Conversion_Is_Identity (Val, Uval); pragma Assert - (Uns_Params.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))); + (U_Spec.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))); pragma Assert - (Uns_Params.Scan_Split_No_Overflow_Ghost (Str, Fst_Num, Str'Last)); - Uns_Params.Lemma_Exponent_Unsigned_Ghost_Base (Uval, 0, 10); + (U_Spec.Scan_Split_No_Overflow_Ghost (Str, Fst_Num, Str'Last)); + U_Spec.Lemma_Exponent_Unsigned_Ghost_Base (Uval, 0, 10); pragma Assert - (Uns_Params.Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last)); + (U_Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last)); pragma Assert (Only_Space_Ghost - (Str, Uns_Params.Raw_Unsigned_Last_Ghost + (Str, U_Spec.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)); diff --git a/gcc/ada/libgnat/s-vaispe.ads b/gcc/ada/libgnat/s-vaispe.ads index e74202d7..33cc1f6 100644 --- a/gcc/ada/libgnat/s-vaispe.ads +++ b/gcc/ada/libgnat/s-vaispe.ads @@ -44,7 +44,8 @@ pragma Assertion_Policy (Pre => Ignore, Ghost => Ignore, Subprogram_Variant => Ignore); -with System.Val_Util; use System.Val_Util; +with System.Value_U_Spec; +with System.Val_Spec; use System.Val_Spec; generic @@ -52,12 +53,9 @@ generic type Uns is mod <>; - -- Additional parameters for specification subprograms on modular Unsigned - -- integers. + -- Additional parameters for ghost subprograms used inside contracts - with package Uns_Params is new System.Val_Util.Uns_Params - (Uns => Uns, others => <>) - with Ghost; + with package U_Spec is new System.Value_U_Spec (Uns => Uns) with Ghost; package System.Value_I_Spec with Ghost, @@ -65,7 +63,7 @@ package System.Value_I_Spec with Always_Terminates is pragma Preelaborate; - use all type Uns_Params.Uns_Option; + use all type U_Spec.Uns_Option; function Uns_Is_Valid_Int (Minus : Boolean; Uval : Uns) return Boolean is (if Minus then Uval <= Uns (Int'Last) + 1 @@ -113,16 +111,16 @@ is Fst_Num : constant Positive := (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank); begin - Uns_Params.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)) - and then Uns_Params.Raw_Unsigned_No_Overflow_Ghost + U_Spec.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)) + and then U_Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last) and then Uns_Is_Valid_Int (Minus => Str (Non_Blank) = '-', - Uval => Uns_Params.Scan_Raw_Unsigned_Ghost + Uval => U_Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last)) and then Only_Space_Ghost - (Str, Uns_Params.Raw_Unsigned_Last_Ghost + (Str, U_Spec.Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last)) with Pre => not Only_Space_Ghost (Str, Str'First, Str'Last) @@ -140,7 +138,7 @@ is Fst_Num : constant Positive := (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank); Uval : constant Uns := - Uns_Params.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last); + U_Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last); begin Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-', Uval => Uval, @@ -160,30 +158,16 @@ is and then Str'Length >= 2 and then Str (Str'First) in ' ' | '-' and then (Str (Str'First) = '-') = (Val < 0) - and then Uns_Params.Only_Decimal_Ghost (Str, Str'First + 1, Str'Last) - and then Uns_Params.Scan_Based_Number_Ghost + and then U_Spec.Only_Decimal_Ghost (Str, Str'First + 1, Str'Last) + and then U_Spec.Scan_Based_Number_Ghost (Str, Str'First + 1, Str'Last) - = Uns_Params.Wrap_Option (Abs_Uns_Of_Int (Val)), + = U_Spec.Wrap_Option (Abs_Uns_Of_Int (Val)), Post => Is_Integer_Ghost (Slide_If_Necessary (Str)) and then Is_Value_Integer_Ghost (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. - -- 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. - - package Int_Params is new System.Val_Util.Int_Params - (Uns => Uns, - Int => Int, - P_Uns_Params => Uns_Params, - P_Is_Integer_Ghost => Is_Integer_Ghost, - P_Is_Value_Integer_Ghost => Is_Value_Integer_Ghost, - P_Is_Int_Of_Uns => Is_Int_Of_Uns, - P_Abs_Uns_Of_Int => Abs_Uns_Of_Int, - P_Prove_Scan_Only_Decimal_Ghost => Prove_Scan_Only_Decimal_Ghost); - private ---------------- diff --git a/gcc/ada/libgnat/s-valboo.adb b/gcc/ada/libgnat/s-valboo.adb index 41c54bf..f988c97 100644 --- a/gcc/ada/libgnat/s-valboo.adb +++ b/gcc/ada/libgnat/s-valboo.adb @@ -55,7 +55,7 @@ is begin Normalize_String (S, F, L); - pragma Assert (F = System.Val_Util.First_Non_Space_Ghost + pragma Assert (F = System.Val_Spec.First_Non_Space_Ghost (S, Str'First, Str'Last)); if S (F .. L) = "TRUE" then diff --git a/gcc/ada/libgnat/s-valboo.ads b/gcc/ada/libgnat/s-valboo.ads index 4866900..d482199 100644 --- a/gcc/ada/libgnat/s-valboo.ads +++ b/gcc/ada/libgnat/s-valboo.ads @@ -40,7 +40,7 @@ pragma Assertion_Policy (Pre => Ignore, Contract_Cases => Ignore, Ghost => Ignore); -with System.Val_Util; +with System.Val_Spec; package System.Val_Bool with SPARK_Mode @@ -48,10 +48,10 @@ is pragma Preelaborate; function Is_Boolean_Image_Ghost (Str : String) return Boolean is - (not System.Val_Util.Only_Space_Ghost (Str, Str'First, Str'Last) + (not System.Val_Spec.Only_Space_Ghost (Str, Str'First, Str'Last) and then (declare - F : constant Positive := System.Val_Util.First_Non_Space_Ghost + F : constant Positive := System.Val_Spec.First_Non_Space_Ghost (Str, Str'First, Str'Last); begin (F <= Str'Last - 3 @@ -61,7 +61,7 @@ is and then Str (F + 3) in 'e' | 'E' and then (if F + 3 < Str'Last then - System.Val_Util.Only_Space_Ghost (Str, F + 4, Str'Last))) + System.Val_Spec.Only_Space_Ghost (Str, F + 4, Str'Last))) or else (F <= Str'Last - 4 and then Str (F) in 'f' | 'F' @@ -71,7 +71,7 @@ is and then Str (F + 4) in 'e' | 'E' and then (if F + 4 < Str'Last then - System.Val_Util.Only_Space_Ghost (Str, F + 5, Str'Last))))) + System.Val_Spec.Only_Space_Ghost (Str, F + 5, Str'Last))))) with Ghost; -- Ghost function that returns True iff Str is the image of a boolean, that @@ -83,7 +83,7 @@ is Pre => Is_Boolean_Image_Ghost (Str), Post => Value_Boolean'Result = - (Str (System.Val_Util.First_Non_Space_Ghost + (Str (System.Val_Spec.First_Non_Space_Ghost (Str, Str'First, Str'Last)) in 't' | 'T'); -- Computes Boolean'Value (Str) diff --git a/gcc/ada/libgnat/s-valint.ads b/gcc/ada/libgnat/s-valint.ads index d3df7db..d8393ac 100644 --- a/gcc/ada/libgnat/s-valint.ads +++ b/gcc/ada/libgnat/s-valint.ads @@ -47,6 +47,8 @@ pragma Assertion_Policy (Pre => Ignore, with System.Unsigned_Types; with System.Val_Uns; with System.Value_I; +with System.Vs_Int; +with System.Vs_Uns; package System.Val_Int with SPARK_Mode is pragma Preelaborate; @@ -57,7 +59,8 @@ package System.Val_Int with SPARK_Mode is (Int => Integer, Uns => Unsigned, Scan_Raw_Unsigned => Val_Uns.Scan_Raw_Unsigned, - Uns_Params => System.Val_Uns.Impl.Spec.Uns_Params); + U_Spec => System.Vs_Uns.Spec, + Spec => System.Vs_Int.Spec); procedure Scan_Integer (Str : String; diff --git a/gcc/ada/libgnat/s-vallli.ads b/gcc/ada/libgnat/s-vallli.ads index 93d96bc..fb10b66 100644 --- a/gcc/ada/libgnat/s-vallli.ads +++ b/gcc/ada/libgnat/s-vallli.ads @@ -47,6 +47,8 @@ pragma Assertion_Policy (Pre => Ignore, with System.Unsigned_Types; with System.Val_LLU; with System.Value_I; +with System.Vs_LLI; +with System.Vs_LLU; package System.Val_LLI with SPARK_Mode is pragma Preelaborate; @@ -57,7 +59,8 @@ package System.Val_LLI with SPARK_Mode is (Int => Long_Long_Integer, Uns => Long_Long_Unsigned, Scan_Raw_Unsigned => Val_LLU.Scan_Raw_Long_Long_Unsigned, - Uns_Params => System.Val_LLU.Impl.Spec.Uns_Params); + U_Spec => System.Vs_LLU.Spec, + Spec => System.Vs_LLI.Spec); procedure Scan_Long_Long_Integer (Str : String; diff --git a/gcc/ada/libgnat/s-valllli.ads b/gcc/ada/libgnat/s-valllli.ads index e31b692..8122da8 100644 --- a/gcc/ada/libgnat/s-valllli.ads +++ b/gcc/ada/libgnat/s-valllli.ads @@ -47,6 +47,8 @@ pragma Assertion_Policy (Pre => Ignore, with System.Unsigned_Types; with System.Val_LLLU; with System.Value_I; +with System.Vs_LLLI; +with System.Vs_LLLU; package System.Val_LLLI with SPARK_Mode is pragma Preelaborate; @@ -57,7 +59,8 @@ package System.Val_LLLI with SPARK_Mode is (Int => Long_Long_Long_Integer, Uns => Long_Long_Long_Unsigned, Scan_Raw_Unsigned => Val_LLLU.Scan_Raw_Long_Long_Long_Unsigned, - Uns_Params => System.Val_LLLU.Impl.Spec.Uns_Params); + U_Spec => System.Vs_LLLU.Spec, + Spec => System.Vs_LLLI.Spec); procedure Scan_Long_Long_Long_Integer (Str : String; diff --git a/gcc/ada/libgnat/s-vallllu.ads b/gcc/ada/libgnat/s-vallllu.ads index 4dcf4c8..0957f84 100644 --- a/gcc/ada/libgnat/s-vallllu.ads +++ b/gcc/ada/libgnat/s-vallllu.ads @@ -46,13 +46,14 @@ pragma Assertion_Policy (Pre => Ignore, with System.Unsigned_Types; with System.Value_U; +with System.Vs_LLLU; package System.Val_LLLU with SPARK_Mode is pragma Preelaborate; subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned; - package Impl is new Value_U (Long_Long_Long_Unsigned); + package Impl is new Value_U (Long_Long_Long_Unsigned, System.Vs_LLLU.Spec); procedure Scan_Raw_Long_Long_Long_Unsigned (Str : String; diff --git a/gcc/ada/libgnat/s-valllu.ads b/gcc/ada/libgnat/s-valllu.ads index c4d73d0..e860505 100644 --- a/gcc/ada/libgnat/s-valllu.ads +++ b/gcc/ada/libgnat/s-valllu.ads @@ -46,13 +46,14 @@ pragma Assertion_Policy (Pre => Ignore, with System.Unsigned_Types; with System.Value_U; +with System.Vs_LLU; package System.Val_LLU with SPARK_Mode is pragma Preelaborate; subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned; - package Impl is new Value_U (Long_Long_Unsigned); + package Impl is new Value_U (Long_Long_Unsigned, System.Vs_LLU.Spec); procedure Scan_Raw_Long_Long_Unsigned (Str : String; diff --git a/gcc/ada/libgnat/s-valspe.adb b/gcc/ada/libgnat/s-valspe.adb new file mode 100644 index 0000000..56e6ed7 --- /dev/null +++ b/gcc/ada/libgnat/s-valspe.adb @@ -0,0 +1,82 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- S Y S T E M . V A L _ S P E C -- +-- -- +-- B o d y -- +-- -- +-- Copyright (C) 2023-2023, Free Software Foundation, Inc. -- +-- -- +-- GNAT is free software; you can redistribute it and/or modify it under -- +-- terms of the GNU General Public License as published by the Free Soft- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- <http://www.gnu.org/licenses/>. -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +-- 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); + +package body System.Val_Spec + with SPARK_Mode +is + + --------------------------- + -- First_Non_Space_Ghost -- + --------------------------- + + function First_Non_Space_Ghost + (S : String; + From, To : Integer) return Positive + is + begin + for J in From .. To loop + if S (J) /= ' ' then + return J; + end if; + + pragma Loop_Invariant (for all K in From .. 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; + +end System.Val_Spec; diff --git a/gcc/ada/libgnat/s-valspe.ads b/gcc/ada/libgnat/s-valspe.ads new file mode 100644 index 0000000..dd861e5 --- /dev/null +++ b/gcc/ada/libgnat/s-valspe.ads @@ -0,0 +1,211 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- S Y S T E M . V A L _ S P E C -- +-- -- +-- S p e c -- +-- -- +-- Copyright (C) 2023-2023, Free Software Foundation, Inc. -- +-- -- +-- GNAT is free software; you can redistribute it and/or modify it under -- +-- terms of the GNU General Public License as published by the Free Soft- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- <http://www.gnu.org/licenses/>. -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +-- This package provides some common specification functions used by the +-- s-valxxx files. + +-- 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); + +package System.Val_Spec with + SPARK_Mode, + Pure, + Ghost +is + pragma Unevaluated_Use_Of_Old (Allow); + + function Only_Space_Ghost (S : String; From, To : Integer) return Boolean is + (for all J in From .. To => S (J) = ' ') + with + Pre => From > To or else (From >= S'First and then To <= S'Last), + Post => True; + -- Ghost function that returns True if S has only space characters from + -- index From to index To. + + function First_Non_Space_Ghost + (S : String; + From, To : Integer) return Positive + with + Pre => From in S'Range + and then To in S'Range + and then not Only_Space_Ghost (S, From, To), + Post => First_Non_Space_Ghost'Result in From .. To + and then S (First_Non_Space_Ghost'Result) /= ' ' + and then Only_Space_Ghost + (S, From, 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 Only_Number_Ghost (Str : String; From, To : Integer) return Boolean + is + (for all J in From .. To => Str (J) in '0' .. '9' | '_') + with + 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 + 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 Str. + + 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) /= '_')))); + -- 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 Starts_As_Exponent_Format_Ghost + (Str : String; + Real : Boolean := False) 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'))); + -- 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 := False) 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)))); + -- 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; + Acc : Natural) + return Natural + with + Subprogram_Variant => (Increases => P), + Pre => Str /= "" and then Str (Str'First) in '0' .. '9' + and then Str'Last < Natural'Last + and then P in Str'First .. Last_Number_Ghost (Str) + 1; + -- 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. + + function Scan_Exponent_Ghost + (Str : String; + Real : Boolean := False) + return Integer + is + (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; + Start : constant Natural := + (if Sign then Str'First + 2 else Str'First + 1); + Value : constant Natural := + Scan_Natural_Ghost (Str (Start .. Str'Last), Start, 0); + begin + (if Minus_Sign then -Value else Value)) + with + Pre => Str'Last < Natural'Last + and then Starts_As_Exponent_Format_Ghost (Str, Real), + Post => (if not Real then Scan_Exponent_Ghost'Result >= 0); + -- Ghost function that scans an exponent + +private + + ------------------------ + -- Scan_Natural_Ghost -- + ------------------------ + + function Scan_Natural_Ghost + (Str : String; + P : Natural; + Acc : Natural) + return Natural + is + (if P > Str'Last + or else Str (P) not in '0' .. '9' | '_' + or else Acc >= Integer'Last / 10 + then + Acc + elsif Str (P) = '_' then + Scan_Natural_Ghost (Str, P + 1, Acc) + else + (declare + Shift_Acc : constant Natural := + Acc * 10 + + (Integer'(Character'Pos (Str (P))) - + Integer'(Character'Pos ('0'))); + begin + Scan_Natural_Ghost (Str, P + 1, Shift_Acc))); + +end System.Val_Spec; diff --git a/gcc/ada/libgnat/s-valuei.adb b/gcc/ada/libgnat/s-valuei.adb index 5932a01..71bfc0c 100644 --- a/gcc/ada/libgnat/s-valuei.adb +++ b/gcc/ada/libgnat/s-valuei.adb @@ -29,6 +29,8 @@ -- -- ------------------------------------------------------------------------------ +with System.Val_Util; use System.Val_Util; + package body System.Value_I is -- Ghost code, loop invariants and assertions in this unit are meant for @@ -98,7 +100,7 @@ package body System.Value_I is Scan_Raw_Unsigned (Str, Ptr, Max, Uval); pragma Assert - (Uval = Uns_Params.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max)); + (Uval = U_Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max)); -- Deal with overflow cases, and also with largest negative number @@ -175,7 +177,7 @@ package body System.Value_I is end; pragma Assert - (P = Uns_Params.Raw_Unsigned_Last_Ghost + (P = U_Spec.Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last)); Scan_Trailing_Blanks (Str, P); diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads index 0ff25f5..baf1f86 100644 --- a/gcc/ada/libgnat/s-valuei.ads +++ b/gcc/ada/libgnat/s-valuei.ads @@ -38,8 +38,9 @@ pragma Assertion_Policy (Pre => Ignore, Ghost => Ignore, Subprogram_Variant => Ignore); -with System.Val_Util; use System.Val_Util; +with System.Val_Spec; use System.Val_Spec; with System.Value_I_Spec; +with System.Value_U_Spec; generic @@ -55,15 +56,13 @@ generic -- Additional parameters for ghost subprograms used inside contracts - with package Uns_Params is new System.Val_Util.Uns_Params - (Uns => Uns, others => <>) + with package U_Spec is new System.Value_U_Spec (Uns => Uns) with Ghost; + with package Spec is new System.Value_I_Spec + (Int => Int, Uns => Uns, U_Spec => U_Spec) with Ghost; package System.Value_I is pragma Preelaborate; - use all type Uns_Params.Uns_Option; - - package Spec is new System.Value_I_Spec (Int, Uns, Uns_Params); procedure Scan_Integer (Str : String; @@ -84,12 +83,12 @@ package System.Value_I is (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank); begin - Uns_Params.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max)) - and then Uns_Params.Raw_Unsigned_No_Overflow_Ghost + U_Spec.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max)) + and then U_Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Max) and then Spec.Uns_Is_Valid_Int (Minus => Str (Non_Blank) = '-', - Uval => Uns_Params.Scan_Raw_Unsigned_Ghost + Uval => U_Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max))), Post => (declare @@ -99,12 +98,12 @@ package System.Value_I is (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank); Uval : constant Uns := - Uns_Params.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max); + U_Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max); begin Spec.Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-', Uval => Uval, Val => Res) - and then Ptr.all = Uns_Params.Raw_Unsigned_Last_Ghost + and then Ptr.all = U_Spec.Raw_Unsigned_Last_Ghost (Str, Fst_Num, Max)); -- This procedure scans the string starting at Str (Ptr.all) for a valid -- integer according to the syntax described in (RM 3.5(43)). The substring diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb index 9c77caa..7aeed3b 100644 --- a/gcc/ada/libgnat/s-valueu.adb +++ b/gcc/ada/libgnat/s-valueu.adb @@ -30,6 +30,7 @@ ------------------------------------------------------------------------------ with System.SPARK.Cut_Operations; use System.SPARK.Cut_Operations; +with System.Val_Util; use System.Val_Util; package body System.Value_U is diff --git a/gcc/ada/libgnat/s-valueu.ads b/gcc/ada/libgnat/s-valueu.ads index 6cc0260..fabaa36 100644 --- a/gcc/ada/libgnat/s-valueu.ads +++ b/gcc/ada/libgnat/s-valueu.ads @@ -45,17 +45,19 @@ pragma Assertion_Policy (Pre => Ignore, Subprogram_Variant => Ignore); with System.Value_U_Spec; -with System.Val_Util; use System.Val_Util; +with System.Val_Spec; use System.Val_Spec; generic type Uns is mod <>; + -- Additional parameters for ghost subprograms used inside contracts + + with package Spec is new System.Value_U_Spec (Uns => Uns) with Ghost; + package System.Value_U is pragma Preelaborate; - package Spec is new System.Value_U_Spec (Uns); - procedure Scan_Raw_Unsigned (Str : String; Ptr : not null access Integer; diff --git a/gcc/ada/libgnat/s-valuns.ads b/gcc/ada/libgnat/s-valuns.ads index 357e5d6..1176153 100644 --- a/gcc/ada/libgnat/s-valuns.ads +++ b/gcc/ada/libgnat/s-valuns.ads @@ -46,13 +46,14 @@ pragma Assertion_Policy (Pre => Ignore, with System.Unsigned_Types; with System.Value_U; +with System.Vs_Uns; package System.Val_Uns with SPARK_Mode is pragma Preelaborate; subtype Unsigned is Unsigned_Types.Unsigned; - package Impl is new Value_U (Unsigned); + package Impl is new Value_U (Unsigned, System.Vs_Uns.Spec); procedure Scan_Raw_Unsigned (Str : String; diff --git a/gcc/ada/libgnat/s-valuti.adb b/gcc/ada/libgnat/s-valuti.adb index ee37c1a..5dfc307 100644 --- a/gcc/ada/libgnat/s-valuti.adb +++ b/gcc/ada/libgnat/s-valuti.adb @@ -62,44 +62,6 @@ is end if; end Bad_Value; - --------------------------- - -- First_Non_Space_Ghost -- - --------------------------- - - function First_Non_Space_Ghost - (S : String; - From, To : Integer) return Positive - is - begin - for J in From .. To loop - if S (J) /= ' ' then - return J; - end if; - - pragma Loop_Invariant (for all K in From .. 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 -- ---------------------- @@ -224,10 +186,10 @@ is declare Rest : constant String := Str (P .. Max) with Ghost; - Last : constant Natural := Last_Number_Ghost (Rest) with Ghost; + Last : constant Natural := Sp.Last_Number_Ghost (Rest) with Ghost; begin - pragma Assert (Is_Natural_Format_Ghost (Rest)); + pragma Assert (Sp.Is_Natural_Format_Ghost (Rest)); loop pragma Assert (Str (P) in '0' .. '9'); @@ -240,8 +202,8 @@ is pragma Loop_Invariant (P in Rest'First .. Last); pragma Loop_Invariant (Str (P) in '0' .. '9'); pragma Loop_Invariant - (Scan_Natural_Ghost (Rest, Rest'First, 0) - = Scan_Natural_Ghost (Rest, P + 1, X)); + (Sp.Scan_Natural_Ghost (Rest, Rest'First, 0) + = Sp.Scan_Natural_Ghost (Rest, P + 1, X)); P := P + 1; @@ -301,7 +263,7 @@ is Start := P; - pragma Assert (Start = First_Non_Space_Ghost (Str, Ptr.all, Max)); + pragma Assert (Start = Sp.First_Non_Space_Ghost (Str, Ptr.all, Max)); -- Skip past an initial plus sign @@ -357,7 +319,7 @@ is Start := P; - pragma Assert (Start = First_Non_Space_Ghost (Str, Ptr.all, Max)); + pragma Assert (Start = Sp.First_Non_Space_Ghost (Str, Ptr.all, Max)); -- Remember an initial minus sign diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads index 22d0612..cdd56c0 100644 --- a/gcc/ada/libgnat/s-valuti.ads +++ b/gcc/ada/libgnat/s-valuti.ads @@ -43,12 +43,15 @@ pragma Assertion_Policy (Pre => Ignore, Ghost => Ignore); with System.Case_Util; +with System.Val_Spec; package System.Val_Util with SPARK_Mode, Pure is pragma Unevaluated_Use_Of_Old (Allow); + package Sp renames System.Val_Spec; + procedure Bad_Value (S : String) with Depends => (null => S), @@ -56,46 +59,22 @@ is pragma No_Return (Bad_Value); -- Raises constraint error with message: bad input for 'Value: "xxx" - function Only_Space_Ghost (S : String; From, To : Integer) return Boolean is - (for all J in From .. To => S (J) = ' ') - with - Ghost, - Pre => From > To or else (From >= S'First and then To <= S'Last), - Post => True; - -- Ghost function that returns True if S has only space characters from - -- index From to index To. - - function First_Non_Space_Ghost - (S : String; - From, To : Integer) return Positive - with - Ghost, - Pre => From in S'Range - and then To in S'Range - and then not Only_Space_Ghost (S, From, To), - Post => First_Non_Space_Ghost'Result in From .. To - and then S (First_Non_Space_Ghost'Result) /= ' ' - and then Only_Space_Ghost - (S, From, 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) with - Post => (if Only_Space_Ghost (S'Old, S'First, S'Last) then + Post => (if Sp.Only_Space_Ghost (S'Old, S'First, S'Last) then F > L else F >= S'First and then L <= S'Last and then F <= L - and then Only_Space_Ghost (S'Old, S'First, F - 1) + and then Sp.Only_Space_Ghost (S'Old, S'First, F - 1) and then S'Old (F) /= ' ' and then S'Old (L) /= ' ' and then (if L < S'Last then - Only_Space_Ghost (S'Old, L + 1, S'Last)) + Sp.Only_Space_Ghost (S'Old, L + 1, S'Last)) and then (if S'Old (F) /= ''' then (for all J in S'Range => @@ -119,18 +98,18 @@ 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 not Only_Space_Ghost (Str, Ptr.all, Max) + and then not Sp.Only_Space_Ghost (Str, Ptr.all, Max) and then (declare F : constant Positive := - First_Non_Space_Ghost (Str, Ptr.all, Max); + Sp.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); + Sp.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) @@ -164,142 +143,24 @@ 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 not Only_Space_Ghost (Str, Ptr.all, Max) + and then not Sp.Only_Space_Ghost (Str, Ptr.all, Max) and then (declare F : constant Positive := - First_Non_Space_Ghost (Str, Ptr.all, Max); + Sp.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); + Sp.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 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 Str. - - 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 Starts_As_Exponent_Format_Ghost - (Str : String; - Real : Boolean := False) 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 := False) 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; - Acc : Natural) - return Natural - with - Ghost, - Subprogram_Variant => (Increases => P), - Pre => Str /= "" and then Str (Str'First) in '0' .. '9' - and then Str'Last < Natural'Last - and then P in Str'First .. Last_Number_Ghost (Str) + 1; - -- 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. - - function Scan_Exponent_Ghost - (Str : String; - Real : Boolean := False) - return Integer - is - (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; - Start : constant Natural := - (if Sign then Str'First + 2 else Str'First + 1); - Value : constant Natural := - Scan_Natural_Ghost (Str (Start .. Str'Last), Start, 0); - begin - (if Minus_Sign then -Value else Value)) - with - Ghost, - Pre => Str'Last < Natural'Last - and then Starts_As_Exponent_Format_Ghost (Str, Real), - Post => (if not Real then Scan_Exponent_Ghost'Result >= 0); - -- Ghost function that scans an exponent - procedure Scan_Exponent (Str : String; Ptr : not null access Integer; @@ -311,14 +172,15 @@ is -- 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 Is_Opt_Exponent_Format_Ghost (Str (Ptr.all .. Max), Real), + and then Sp.Is_Opt_Exponent_Format_Ghost (Str (Ptr.all .. Max), Real), Post => - (if Starts_As_Exponent_Format_Ghost (Str (Ptr.all'Old .. Max), Real) - then Exp = Scan_Exponent_Ghost (Str (Ptr.all'Old .. Max), Real) + (if Sp.Starts_As_Exponent_Format_Ghost (Str (Ptr.all'Old .. Max), Real) + then Exp = Sp.Scan_Exponent_Ghost (Str (Ptr.all'Old .. Max), Real) and then (if Str (Ptr.all'Old + 1) in '-' | '+' then - Ptr.all = Last_Number_Ghost (Str (Ptr.all'Old + 2 .. Max)) + 1 - else Ptr.all = Last_Number_Ghost (Str (Ptr.all'Old + 1 .. Max)) + 1) + Ptr.all = Sp.Last_Number_Ghost (Str (Ptr.all'Old + 2 .. Max)) + 1 + else + Ptr.all = Sp.Last_Number_Ghost (Str (Ptr.all'Old + 1 .. Max)) + 1) 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 @@ -337,7 +199,7 @@ is procedure Scan_Trailing_Blanks (Str : String; P : Positive) with Pre => P >= Str'First - and then Only_Space_Ghost (Str, P, Str'Last); + and then Sp.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. @@ -375,302 +237,4 @@ is -- no check for this case, the caller must ensure this condition is met. pragma Warnings (GNATprove, On, """Ptr"" is not modified"); - -- Bundle Uns 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 Uns type. - generic - type Uns is mod <>; - type P_Uns_Option is private with Ghost; - with function P_Wrap_Option (Value : Uns) return P_Uns_Option - with Ghost; - with function P_Hexa_To_Unsigned_Ghost (X : Character) return Uns - with Ghost; - with function P_Scan_Overflows_Ghost - (Digit : Uns; - Base : Uns; - Acc : Uns) return Boolean - with Ghost; - with function P_Is_Raw_Unsigned_Format_Ghost - (Str : String) return Boolean - with Ghost; - with function P_Scan_Split_No_Overflow_Ghost - (Str : String; - From, To : Integer) - return Boolean - with Ghost; - with function P_Raw_Unsigned_No_Overflow_Ghost - (Str : String; - From, To : Integer) - return Boolean - with Ghost; - - with function P_Exponent_Unsigned_Ghost - (Value : Uns; - Exp : Natural; - Base : Uns := 10) return P_Uns_Option - with Ghost; - with procedure P_Lemma_Exponent_Unsigned_Ghost_Base - (Value : Uns; - Exp : Natural; - Base : Uns := 10) - with Ghost; - with procedure P_Lemma_Exponent_Unsigned_Ghost_Overflow - (Value : Uns; - Exp : Natural; - Base : Uns := 10) - with Ghost; - with procedure P_Lemma_Exponent_Unsigned_Ghost_Step - (Value : Uns; - Exp : Natural; - Base : Uns := 10) - with Ghost; - - with function P_Scan_Raw_Unsigned_Ghost - (Str : String; - From, To : Integer) - return Uns - with Ghost; - with procedure P_Lemma_Scan_Based_Number_Ghost_Base - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - with Ghost; - with procedure P_Lemma_Scan_Based_Number_Ghost_Underscore - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - with Ghost; - with procedure P_Lemma_Scan_Based_Number_Ghost_Overflow - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - with Ghost; - with procedure P_Lemma_Scan_Based_Number_Ghost_Step - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - with Ghost; - - with function P_Raw_Unsigned_Last_Ghost - (Str : String; - From, To : Integer) - return Positive - with Ghost; - with function P_Only_Decimal_Ghost - (Str : String; - From, To : Integer) - return Boolean - with Ghost; - with function P_Scan_Based_Number_Ghost - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - return P_Uns_Option - with Ghost; - with function P_Is_Unsigned_Ghost (Str : String) return Boolean - with Ghost; - with function P_Is_Value_Unsigned_Ghost - (Str : String; - Val : Uns) return Boolean - with Ghost; - - with procedure P_Prove_Scan_Only_Decimal_Ghost - (Str : String; - Val : Uns) - with Ghost; - with procedure P_Prove_Scan_Based_Number_Ghost_Eq - (Str1, Str2 : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - with Ghost; - - package Uns_Params is - subtype Uns_Option is P_Uns_Option with Ghost; - function Wrap_Option (Value : Uns) return Uns_Option renames - P_Wrap_Option; - function Hexa_To_Unsigned_Ghost - (X : Character) return Uns - renames P_Hexa_To_Unsigned_Ghost; - function Scan_Overflows_Ghost - (Digit : Uns; - Base : Uns; - Acc : Uns) return Boolean - renames P_Scan_Overflows_Ghost; - function Is_Raw_Unsigned_Format_Ghost - (Str : String) return Boolean - renames P_Is_Raw_Unsigned_Format_Ghost; - function Scan_Split_No_Overflow_Ghost - (Str : String; - From, To : Integer) return Boolean - renames P_Scan_Split_No_Overflow_Ghost; - function Raw_Unsigned_No_Overflow_Ghost - (Str : String; - From, To : Integer) return Boolean - renames P_Raw_Unsigned_No_Overflow_Ghost; - - function Exponent_Unsigned_Ghost - (Value : Uns; - Exp : Natural; - Base : Uns := 10) return Uns_Option - renames P_Exponent_Unsigned_Ghost; - procedure Lemma_Exponent_Unsigned_Ghost_Base - (Value : Uns; - Exp : Natural; - Base : Uns := 10) - renames P_Lemma_Exponent_Unsigned_Ghost_Base; - procedure Lemma_Exponent_Unsigned_Ghost_Overflow - (Value : Uns; - Exp : Natural; - Base : Uns := 10) - renames P_Lemma_Exponent_Unsigned_Ghost_Overflow; - procedure Lemma_Exponent_Unsigned_Ghost_Step - (Value : Uns; - Exp : Natural; - Base : Uns := 10) - renames P_Lemma_Exponent_Unsigned_Ghost_Step; - - function Scan_Raw_Unsigned_Ghost - (Str : String; - From, To : Integer) return Uns - renames P_Scan_Raw_Unsigned_Ghost; - procedure Lemma_Scan_Based_Number_Ghost_Base - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - renames P_Lemma_Scan_Based_Number_Ghost_Base; - procedure Lemma_Scan_Based_Number_Ghost_Underscore - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - renames P_Lemma_Scan_Based_Number_Ghost_Underscore; - procedure Lemma_Scan_Based_Number_Ghost_Overflow - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - renames P_Lemma_Scan_Based_Number_Ghost_Overflow; - procedure Lemma_Scan_Based_Number_Ghost_Step - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - renames P_Lemma_Scan_Based_Number_Ghost_Step; - - function Raw_Unsigned_Last_Ghost - (Str : String; - From, To : Integer) return Positive - renames P_Raw_Unsigned_Last_Ghost; - function Only_Decimal_Ghost - (Str : String; - From, To : Integer) return Boolean - renames P_Only_Decimal_Ghost; - function Scan_Based_Number_Ghost - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) return Uns_Option - renames P_Scan_Based_Number_Ghost; - function Is_Unsigned_Ghost (Str : String) return Boolean - renames P_Is_Unsigned_Ghost; - function Is_Value_Unsigned_Ghost - (Str : String; - Val : Uns) return Boolean - renames P_Is_Value_Unsigned_Ghost; - - procedure Prove_Scan_Only_Decimal_Ghost - (Str : String; - Val : Uns) - renames P_Prove_Scan_Only_Decimal_Ghost; - procedure Prove_Scan_Based_Number_Ghost_Eq - (Str1, Str2 : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - renames P_Prove_Scan_Based_Number_Ghost_Eq; - end Uns_Params; - - -- 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 <>; - - with package P_Uns_Params is new System.Val_Util.Uns_Params - (Uns => Uns, others => <>) - with Ghost; - - with function P_Abs_Uns_Of_Int (Val : Int) return Uns - with Ghost; - with function P_Is_Int_Of_Uns - (Minus : Boolean; - Uval : Uns; - Val : Int) - return Boolean - with Ghost; - with function P_Is_Integer_Ghost (Str : String) return Boolean - with Ghost; - with function P_Is_Value_Integer_Ghost - (Str : String; - Val : Int) return Boolean - with Ghost; - with procedure P_Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) - with Ghost; - - package Int_Params is - package Uns_Params renames P_Uns_Params; - function Abs_Uns_Of_Int (Val : Int) return Uns renames - P_Abs_Uns_Of_Int; - function Is_Int_Of_Uns - (Minus : Boolean; - Uval : Uns; - Val : Int) - return Boolean - renames P_Is_Int_Of_Uns; - function Is_Integer_Ghost (Str : String) return Boolean renames - P_Is_Integer_Ghost; - function Is_Value_Integer_Ghost - (Str : String; - Val : Int) return Boolean - renames P_Is_Value_Integer_Ghost; - procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) renames - P_Prove_Scan_Only_Decimal_Ghost; - end Int_Params; - -private - - ------------------------ - -- Scan_Natural_Ghost -- - ------------------------ - - function Scan_Natural_Ghost - (Str : String; - P : Natural; - Acc : Natural) - return Natural - is - (if P > Str'Last - or else Str (P) not in '0' .. '9' | '_' - or else Acc >= Integer'Last / 10 - then - Acc - elsif Str (P) = '_' then - Scan_Natural_Ghost (Str, P + 1, Acc) - else - (declare - Shift_Acc : constant Natural := - Acc * 10 + - (Integer'(Character'Pos (Str (P))) - - Integer'(Character'Pos ('0'))); - begin - Scan_Natural_Ghost (Str, P + 1, Shift_Acc))); - end System.Val_Util; diff --git a/gcc/ada/libgnat/s-vauspe.ads b/gcc/ada/libgnat/s-vauspe.ads index bdd97b5..a6f81d7 100644 --- a/gcc/ada/libgnat/s-vauspe.ads +++ b/gcc/ada/libgnat/s-vauspe.ads @@ -44,7 +44,7 @@ pragma Assertion_Policy (Pre => Ignore, Ghost => Ignore, Subprogram_Variant => Ignore); -with System.Val_Util; use System.Val_Util; +with System.Val_Spec; use System.Val_Spec; generic @@ -57,6 +57,17 @@ package System.Value_U_Spec with is pragma Preelaborate; + -- 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; + type Uns_Option (Overflow : Boolean := False) is record case Overflow is when True => @@ -598,46 +609,6 @@ is -- ghost code, so that this package can be instantiated once and used -- multiple times as generic formal for a given Int type. - package Uns_Params is new System.Val_Util.Uns_Params - (Uns => Uns, - P_Uns_Option => Uns_Option, - P_Wrap_Option => Wrap_Option, - P_Hexa_To_Unsigned_Ghost => Hexa_To_Unsigned_Ghost, - P_Scan_Overflows_Ghost => Scan_Overflows_Ghost, - P_Is_Raw_Unsigned_Format_Ghost => - Is_Raw_Unsigned_Format_Ghost, - P_Scan_Split_No_Overflow_Ghost => - Scan_Split_No_Overflow_Ghost, - P_Raw_Unsigned_No_Overflow_Ghost => - Raw_Unsigned_No_Overflow_Ghost, - P_Exponent_Unsigned_Ghost => Exponent_Unsigned_Ghost, - P_Lemma_Exponent_Unsigned_Ghost_Base => - Lemma_Exponent_Unsigned_Ghost_Base, - P_Lemma_Exponent_Unsigned_Ghost_Overflow => - Lemma_Exponent_Unsigned_Ghost_Overflow, - P_Lemma_Exponent_Unsigned_Ghost_Step => - Lemma_Exponent_Unsigned_Ghost_Step, - P_Scan_Raw_Unsigned_Ghost => Scan_Raw_Unsigned_Ghost, - P_Lemma_Scan_Based_Number_Ghost_Base => - Lemma_Scan_Based_Number_Ghost_Base, - P_Lemma_Scan_Based_Number_Ghost_Underscore => - Lemma_Scan_Based_Number_Ghost_Underscore, - P_Lemma_Scan_Based_Number_Ghost_Overflow => - Lemma_Scan_Based_Number_Ghost_Overflow, - P_Lemma_Scan_Based_Number_Ghost_Step => - Lemma_Scan_Based_Number_Ghost_Step, - P_Raw_Unsigned_Last_Ghost => Raw_Unsigned_Last_Ghost, - P_Only_Decimal_Ghost => Only_Decimal_Ghost, - P_Scan_Based_Number_Ghost => Scan_Based_Number_Ghost, - P_Is_Unsigned_Ghost => - Is_Unsigned_Ghost, - P_Is_Value_Unsigned_Ghost => - Is_Value_Unsigned_Ghost, - P_Prove_Scan_Only_Decimal_Ghost => - Prove_Scan_Only_Decimal_Ghost, - P_Prove_Scan_Based_Number_Ghost_Eq => - Prove_Scan_Based_Number_Ghost_Eq); - private ---------------- diff --git a/gcc/ada/libgnat/s-vs_int.ads b/gcc/ada/libgnat/s-vs_int.ads new file mode 100644 index 0000000..739a30c --- /dev/null +++ b/gcc/ada/libgnat/s-vs_int.ads @@ -0,0 +1,59 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- S Y S T E M . V S _ I N T -- +-- -- +-- S p e c -- +-- -- +-- Copyright (C) 2023-2023, Free Software Foundation, Inc. -- +-- -- +-- GNAT is free software; you can redistribute it and/or modify it under -- +-- terms of the GNU General Public License as published by the Free Soft- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- <http://www.gnu.org/licenses/>. -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +-- This package contains specification functions for scanning signed Integer +-- values for use in Text_IO.Integer_IO, and the Value attribute. + +-- 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.Unsigned_Types; +with System.Value_I_Spec; +with System.Vs_Uns; + +package System.Vs_Int with SPARK_Mode, Ghost is + pragma Preelaborate; + + subtype Unsigned is Unsigned_Types.Unsigned; + + package Spec is new System.Value_I_Spec + (Integer, Unsigned, System.Vs_Uns.Spec); + +end System.Vs_Int; diff --git a/gcc/ada/libgnat/s-vs_lli.ads b/gcc/ada/libgnat/s-vs_lli.ads new file mode 100644 index 0000000..e3a1179 --- /dev/null +++ b/gcc/ada/libgnat/s-vs_lli.ads @@ -0,0 +1,60 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- S Y S T E M . V S _ L L I -- +-- -- +-- S p e c -- +-- -- +-- Copyright (C) 2023-2023, Free Software Foundation, Inc. -- +-- -- +-- GNAT is free software; you can redistribute it and/or modify it under -- +-- terms of the GNU General Public License as published by the Free Soft- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- <http://www.gnu.org/licenses/>. -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +-- This package contains specification functions for scanning +-- Long_Long_Integer values for use in Text_IO.Integer_IO, and the Value +-- attribute. + +-- 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.Unsigned_Types; +with System.Value_I_Spec; +with System.Vs_LLU; + +package System.Vs_LLI with SPARK_Mode, Ghost is + pragma Preelaborate; + + subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned; + + package Spec is new System.Value_I_Spec + (Long_Long_Integer, Long_Long_Unsigned, System.Vs_LLU.Spec); + +end System.Vs_LLI; diff --git a/gcc/ada/libgnat/s-vs_llu.ads b/gcc/ada/libgnat/s-vs_llu.ads new file mode 100644 index 0000000..f6d9334 --- /dev/null +++ b/gcc/ada/libgnat/s-vs_llu.ads @@ -0,0 +1,58 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- S Y S T E M . V S _ L L U -- +-- -- +-- S p e c -- +-- -- +-- Copyright (C) 2023-2023, Free Software Foundation, Inc. -- +-- -- +-- GNAT is free software; you can redistribute it and/or modify it under -- +-- terms of the GNU General Public License as published by the Free Soft- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- <http://www.gnu.org/licenses/>. -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +-- This package contains specification functions for scanning +-- Long_Long_Unsigned values for use in Text_IO.Modular_IO, and the Value +-- attribute. + +-- 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.Unsigned_Types; +with System.Value_U_Spec; + +package System.Vs_LLU with SPARK_Mode, Ghost is + pragma Preelaborate; + + subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned; + + package Spec is new System.Value_U_Spec (Long_Long_Unsigned); + +end System.Vs_LLU; diff --git a/gcc/ada/libgnat/s-vs_uns.ads b/gcc/ada/libgnat/s-vs_uns.ads new file mode 100644 index 0000000..5f21684 --- /dev/null +++ b/gcc/ada/libgnat/s-vs_uns.ads @@ -0,0 +1,57 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- S Y S T E M . V S _ U N S -- +-- -- +-- S p e c -- +-- -- +-- Copyright (C) 2023-2023, Free Software Foundation, Inc. -- +-- -- +-- GNAT is free software; you can redistribute it and/or modify it under -- +-- terms of the GNU General Public License as published by the Free Soft- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- <http://www.gnu.org/licenses/>. -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +-- This package contains specification functions for scanning modular Unsigned +-- values for use in Text_IO.Modular_IO, and the Value attribute. + +-- 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.Unsigned_Types; +with System.Value_U_Spec; + +package System.Vs_Uns with SPARK_Mode, Ghost is + pragma Preelaborate; + + subtype Unsigned is Unsigned_Types.Unsigned; + + package Spec is new System.Value_U_Spec (Unsigned); + +end System.Vs_Uns; diff --git a/gcc/ada/libgnat/s-vsllli.ads b/gcc/ada/libgnat/s-vsllli.ads new file mode 100644 index 0000000..f70290b --- /dev/null +++ b/gcc/ada/libgnat/s-vsllli.ads @@ -0,0 +1,60 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- S Y S T E M . V S _ L L L I -- +-- -- +-- S p e c -- +-- -- +-- Copyright (C) 2023-2023, Free Software Foundation, Inc. -- +-- -- +-- GNAT is free software; you can redistribute it and/or modify it under -- +-- terms of the GNU General Public License as published by the Free Soft- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- <http://www.gnu.org/licenses/>. -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +-- This package contains specification functions for scanning +-- Long_Long_Long_Integer values for use in Text_IO.Integer_IO, and the Value +-- attribute. + +-- 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.Unsigned_Types; +with System.Value_I_Spec; +with System.Vs_LLLU; + +package System.Vs_LLLI with SPARK_Mode, Ghost is + pragma Preelaborate; + + subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned; + + package Spec is new System.Value_I_Spec + (Long_Long_Long_Integer, Long_Long_Long_Unsigned, System.Vs_LLLU.Spec); + +end System.Vs_LLLI; diff --git a/gcc/ada/libgnat/s-vslllu.ads b/gcc/ada/libgnat/s-vslllu.ads new file mode 100644 index 0000000..0a53cfe --- /dev/null +++ b/gcc/ada/libgnat/s-vslllu.ads @@ -0,0 +1,58 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- S Y S T E M . V S _ L L L U -- +-- -- +-- S p e c -- +-- -- +-- Copyright (C) 2023-2023, Free Software Foundation, Inc. -- +-- -- +-- GNAT is free software; you can redistribute it and/or modify it under -- +-- terms of the GNU General Public License as published by the Free Soft- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- <http://www.gnu.org/licenses/>. -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +-- This package contains specification functions for scanning +-- Long_Long_Long_Unsigned values for use in Text_IO.Modular_IO, and the Value +-- attribute. + +-- 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.Unsigned_Types; +with System.Value_U_Spec; + +package System.Vs_LLLU with SPARK_Mode, Ghost is + pragma Preelaborate; + + subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned; + + package Spec is new System.Value_U_Spec (Long_Long_Long_Unsigned); + +end System.Vs_LLLU; |