* [COMMITTED] ada: Refactor the proof of the Value and Image runtime units
@ 2023-07-06 11:39 Marc Poulhiès
0 siblings, 0 replies; only message in thread
From: Marc Poulhiès @ 2023-07-06 11:39 UTC (permalink / raw)
To: gcc-patches; +Cc: Claire Dross
From: Claire Dross <dross@adacore.com>
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.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/Makefile.rtl | 7 +
gcc/ada/libgnat/s-imagef.adb | 12 +-
gcc/ada/libgnat/s-imagei.adb | 4 +-
gcc/ada/libgnat/s-imagei.ads | 17 +-
gcc/ada/libgnat/s-imageu.adb | 81 ++----
gcc/ada/libgnat/s-imageu.ads | 20 +-
gcc/ada/libgnat/s-imgboo.adb | 6 +-
gcc/ada/libgnat/s-imgint.ads | 13 +-
gcc/ada/libgnat/s-imglli.ads | 14 +-
gcc/ada/libgnat/s-imgllli.ads | 14 +-
gcc/ada/libgnat/s-imglllu.ads | 10 +-
gcc/ada/libgnat/s-imgllu.ads | 9 +-
gcc/ada/libgnat/s-imguns.ads | 9 +-
gcc/ada/libgnat/s-vaispe.adb | 10 +-
gcc/ada/libgnat/s-vaispe.ads | 42 +--
gcc/ada/libgnat/s-valboo.adb | 2 +-
gcc/ada/libgnat/s-valboo.ads | 12 +-
gcc/ada/libgnat/s-valint.ads | 5 +-
gcc/ada/libgnat/s-vallli.ads | 5 +-
gcc/ada/libgnat/s-valllli.ads | 5 +-
gcc/ada/libgnat/s-vallllu.ads | 3 +-
gcc/ada/libgnat/s-valllu.ads | 3 +-
gcc/ada/libgnat/s-valspe.adb | 82 ++++++
gcc/ada/libgnat/s-valspe.ads | 211 +++++++++++++++
gcc/ada/libgnat/s-valuei.adb | 6 +-
gcc/ada/libgnat/s-valuei.ads | 21 +-
gcc/ada/libgnat/s-valueu.adb | 1 +
gcc/ada/libgnat/s-valueu.ads | 8 +-
gcc/ada/libgnat/s-valuns.ads | 3 +-
gcc/ada/libgnat/s-valuti.adb | 50 +---
gcc/ada/libgnat/s-valuti.ads | 474 ++--------------------------------
gcc/ada/libgnat/s-vauspe.ads | 53 +---
gcc/ada/libgnat/s-vs_int.ads | 59 +++++
gcc/ada/libgnat/s-vs_lli.ads | 60 +++++
gcc/ada/libgnat/s-vs_llu.ads | 58 +++++
gcc/ada/libgnat/s-vs_uns.ads | 57 ++++
gcc/ada/libgnat/s-vsllli.ads | 60 +++++
gcc/ada/libgnat/s-vslllu.ads | 58 +++++
38 files changed, 835 insertions(+), 729 deletions(-)
create mode 100644 gcc/ada/libgnat/s-valspe.adb
create mode 100644 gcc/ada/libgnat/s-valspe.ads
create mode 100644 gcc/ada/libgnat/s-vs_int.ads
create mode 100644 gcc/ada/libgnat/s-vs_lli.ads
create mode 100644 gcc/ada/libgnat/s-vs_llu.ads
create mode 100644 gcc/ada/libgnat/s-vs_uns.ads
create mode 100644 gcc/ada/libgnat/s-vsllli.ads
create mode 100644 gcc/ada/libgnat/s-vslllu.ads
diff --git a/gcc/ada/Makefile.rtl b/gcc/ada/Makefile.rtl
index ca4c528a7e0..b94caa45b10 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 a10dfdc82a5..3f6bfa20cb2 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 a56d635d9b9..cbe03e74c35 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 38c6e6e4fe2..7e39f8697bc 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 eb1d054e62d..919b401c2d2 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 1c58ea1d692..cec52636e2c 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 fd1d9a6b2fc..fb3301a4270 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 320edc92f28..fe938994c5a 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 1d34e77ead3..809ca106282 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 05dec5e4dcc..727388f3d34 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 888d782e3d1..09c8965dd81 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 b00dc663c81..9709c961a13 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 2bd72164f7c..7c79a669b81 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 b1a38842773..a13dc6a8a2d 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 e74202d736e..33cc1f686bc 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 41c54bf7d69..f988c97ff24 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 4866900e1ca..d48219953a0 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 d3df7dbedd1..d8393ac3305 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 93d96bcb0f9..fb10b668113 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 e31b692ccde..8122da8c3ab 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 4dcf4c8ec83..0957f843ad0 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 c4d73d0b9b2..e8605054a24 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 00000000000..56e6ed77209
--- /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 00000000000..dd861e5029f
--- /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 5932a0108b7..71bfc0cbf7d 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 0ff25f51718..baf1f866535 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 9c77caa3bcb..7aeed3bed0d 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 6cc0260d101..fabaa36d627 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 357e5d67bba..11761539e4b 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 ee37c1a636b..5dfc307a46a 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 22d0612bc32..cdd56c0de68 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 bdd97b52e07..a6f81d715c4 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 00000000000..739a30c4389
--- /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 00000000000..e3a1179fb98
--- /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 00000000000..f6d933485c4
--- /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 00000000000..5f21684aa69
--- /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 00000000000..f70290b93de
--- /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 00000000000..0a53cfe9b9f
--- /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;
--
2.40.0
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2023-07-06 11:39 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-07-06 11:39 [COMMITTED] ada: Refactor the proof of the Value and Image runtime units Marc Poulhiès
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).