s-vallli$(objext) \
s-valllu$(objext) \
s-valrea$(objext) \
+ s-valspe$(objext) \
s-valued$(objext) \
s-valuef$(objext) \
s-valuei$(objext) \
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) \
s-vafi128$(objext) \
s-valllli$(objext) \
s-vallllu$(objext) \
+ s-vsllli$(objext) \
+ s-vslllu$(objext) \
s-widllli$(objext) \
s-widlllu$(objext)
-- 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;
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
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
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;
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
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 --
------------------
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 --
---------------------------
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 --
--------------------
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.
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
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.
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.
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,
-- 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
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);
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);
Ghost => Ignore,
Subprogram_Variant => Ignore);
-with System.Val_Util;
+with System.Value_U_Spec;
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;
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
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
Loop_Invariant => Ignore,
Assert => Ignore);
-with System.Val_Util;
+with System.Val_Spec;
package body System.Img_Bool
with SPARK_Mode
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;
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
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;
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
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;
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
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;
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
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;
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
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;
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
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;
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));
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
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,
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
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)
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,
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
----------------
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
Contract_Cases => Ignore,
Ghost => Ignore);
-with System.Val_Util;
+with System.Val_Spec;
package System.Val_Bool
with SPARK_Mode
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
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'
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
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)
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;
(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;
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;
(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;
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;
(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;
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;
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;
--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- 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;
--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- 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;
-- --
------------------------------------------------------------------------------
+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
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
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);
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
-- 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;
(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
(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
------------------------------------------------------------------------------
with System.SPARK.Cut_Operations; use System.SPARK.Cut_Operations;
+with System.Val_Util; use System.Val_Util;
package body System.Value_U is
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;
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;
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 --
----------------------
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');
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;
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
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
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),
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 =>
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)
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;
-- 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
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.
-- 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;
Ghost => Ignore,
Subprogram_Variant => Ignore);
-with System.Val_Util; use System.Val_Util;
+with System.Val_Spec; use System.Val_Spec;
generic
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 =>
-- 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
----------------
--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- 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;
--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- 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;
--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- 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;
--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- 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;
--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- 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;
--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- 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;
projects / thirdparty / gcc.git / commitdiff
