public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r13-2363] [Ada] Fix proof of runtime unit System.Value* and System.Image*
@ 2022-09-02 7:52 Marc Poulhiès
0 siblings, 0 replies; only message in thread
From: Marc Poulhiès @ 2022-09-02 7:52 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:b3ae28dca103a45bb97ec5b47acad9b9380d1113
commit r13-2363-gb3ae28dca103a45bb97ec5b47acad9b9380d1113
Author: Claire Dross <dross@adacore.com>
Date: Thu Jul 7 16:04:24 2022 +0200
[Ada] Fix proof of runtime unit System.Value* and System.Image*
Refactor specification of the Value* and Image* units and fix proofs.
gcc/ada/
* libgnat/a-nbnbig.ads: Add Always_Return annotation.
* libgnat/s-vaispe.ads: New ghost unit for the specification of
System.Value_I. Restore proofs.
* libgnat/s-vauspe.ads: New ghost unit for the specification of
System.Value_U. Restore proofs.
* libgnat/s-valuei.adb: The specification only subprograms are
moved to System.Value_I_Spec. Restore proofs.
* libgnat/s-valueu.adb: The specification only subprograms are
moved to System.Value_U_Spec. Restore proofs.
* libgnat/s-valuti.ads
(Uns_Params): Generic unit used to bundle together the
specification functions of System.Value_U_Spec.
(Int_Params): Generic unit used to bundle together the
specification functions of System.Value_I_Spec.
* libgnat/s-imagef.adb: It is now possible to instantiate the
appropriate specification units instead of creating imported ghost
subprograms.
* libgnat/s-imagei.adb: Update to refactoring of specifications
and fix proofs.
* libgnat/s-imageu.adb: Likewise.
* libgnat/s-imgint.ads: Ghost parameters are grouped together in a
package now.
* libgnat/s-imglli.ads: Likewise.
* libgnat/s-imgllu.ads: Likewise.
* libgnat/s-imgllli.ads: Likewise.
* libgnat/s-imglllu.ads: Likewise.
* libgnat/s-imguns.ads: Likewise.
* libgnat/s-vallli.ads: Likewise.
* libgnat/s-valllli.ads: Likewise.
* libgnat/s-imagei.ads: Likewise.
* libgnat/s-imageu.ads: Likewise.
* libgnat/s-vaispe.adb: Likewise.
* libgnat/s-valint.ads: Likewise.
* libgnat/s-valuei.ads: Likewise.
* libgnat/s-valueu.ads: Likewise.
* libgnat/s-vauspe.adb: Likewise.
Diff:
---
gcc/ada/libgnat/a-nbnbig.ads | 2 +
gcc/ada/libgnat/s-imagef.adb | 73 +----
gcc/ada/libgnat/s-imagei.adb | 252 ++++++++---------
gcc/ada/libgnat/s-imagei.ads | 36 +--
gcc/ada/libgnat/s-imageu.adb | 194 ++++++-------
gcc/ada/libgnat/s-imageu.ads | 44 +--
gcc/ada/libgnat/s-imgint.ads | 27 +-
gcc/ada/libgnat/s-imglli.ads | 30 +-
gcc/ada/libgnat/s-imgllli.ads | 27 +-
gcc/ada/libgnat/s-imglllu.ads | 18 +-
gcc/ada/libgnat/s-imgllu.ads | 18 +-
gcc/ada/libgnat/s-imguns.ads | 18 +-
gcc/ada/libgnat/s-vaispe.adb | 87 ++++++
gcc/ada/libgnat/s-vaispe.ads | 199 +++++++++++++
gcc/ada/libgnat/s-valint.ads | 21 +-
gcc/ada/libgnat/s-vallli.ads | 22 +-
gcc/ada/libgnat/s-valllli.ads | 22 +-
gcc/ada/libgnat/s-valuei.adb | 95 +++----
gcc/ada/libgnat/s-valuei.ads | 188 ++-----------
gcc/ada/libgnat/s-valueu.adb | 444 +++++++++--------------------
gcc/ada/libgnat/s-valueu.ads | 478 +------------------------------
gcc/ada/libgnat/s-valuti.ads | 268 ++++++++++++++++--
gcc/ada/libgnat/s-vauspe.adb | 198 +++++++++++++
gcc/ada/libgnat/s-vauspe.ads | 639 ++++++++++++++++++++++++++++++++++++++++++
24 files changed, 1853 insertions(+), 1547 deletions(-)
diff --git a/gcc/ada/libgnat/a-nbnbig.ads b/gcc/ada/libgnat/a-nbnbig.ads
index f574e78f8dc..3979f147d2a 100644
--- a/gcc/ada/libgnat/a-nbnbig.ads
+++ b/gcc/ada/libgnat/a-nbnbig.ads
@@ -32,6 +32,8 @@ package Ada.Numerics.Big_Numbers.Big_Integers_Ghost with
Ghost,
Pure
is
+ pragma Annotate (GNATprove, Always_Return, Big_Integers_Ghost);
+
type Big_Integer is private
with Integer_Literal => From_Universal_Image;
diff --git a/gcc/ada/libgnat/s-imagef.adb b/gcc/ada/libgnat/s-imagef.adb
index fd8e848438e..bfe85403888 100644
--- a/gcc/ada/libgnat/s-imagef.adb
+++ b/gcc/ada/libgnat/s-imagef.adb
@@ -31,7 +31,8 @@
with System.Image_I;
with System.Img_Util; use System.Img_Util;
-with System.Val_Util;
+with System.Value_I_Spec;
+with System.Value_U_Spec;
package body System.Image_F is
@@ -69,70 +70,16 @@ 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.
- -- Define ghost subprograms without implementation (marked as Import) to
- -- create a suitable package Int_Params for type Int, as instantiations
- -- of System.Image_F use for this type one of the derived integer types
- -- defined in Interfaces, instead of the standard signed integer types
- -- which are used to define System.Img_*.Int_Params.
-
- type Uns_Option (Overflow : Boolean := False) is record
- case Overflow is
- when True =>
- null;
- when False =>
- Value : Uns := 0;
- end case;
- end record;
-
Unsigned_Width_Ghost : constant Natural := Int'Width;
- function Wrap_Option (Value : Uns) return Uns_Option
- with Ghost, Import;
- function Only_Decimal_Ghost
- (Str : String;
- From, To : Integer)
- return Boolean
- with Ghost, Import;
- function Hexa_To_Unsigned_Ghost (X : Character) return Uns
- with Ghost, Import;
- function Scan_Based_Number_Ghost
- (Str : String;
- From, To : Integer;
- Base : Uns := 10;
- Acc : Uns := 0)
- return Uns_Option
- with Ghost, Import;
- function Is_Integer_Ghost (Str : String) return Boolean
- with Ghost, Import;
- procedure Prove_Iter_Scan_Based_Number_Ghost
- (Str1, Str2 : String;
- From, To : Integer;
- Base : Uns := 10;
- Acc : Uns := 0)
- with Ghost, Import;
- procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
- with Ghost, Import;
- function Abs_Uns_Of_Int (Val : Int) return Uns
- with Ghost, Import;
- function Value_Integer (Str : String) return Int
- with Ghost, Import;
-
- package Int_Params is new Val_Util.Int_Params
- (Int => Int,
- Uns => Uns,
- Uns_Option => Uns_Option,
- Unsigned_Width_Ghost => Unsigned_Width_Ghost,
- Wrap_Option => Wrap_Option,
- Only_Decimal_Ghost => Only_Decimal_Ghost,
- Hexa_To_Unsigned_Ghost => Hexa_To_Unsigned_Ghost,
- Scan_Based_Number_Ghost => Scan_Based_Number_Ghost,
- Is_Integer_Ghost => Is_Integer_Ghost,
- Prove_Iter_Scan_Based_Number_Ghost => Prove_Iter_Scan_Based_Number_Ghost,
- Prove_Scan_Only_Decimal_Ghost => Prove_Scan_Only_Decimal_Ghost,
- Abs_Uns_Of_Int => Abs_Uns_Of_Int,
- Value_Integer => Value_Integer);
-
- package Image_I is new System.Image_I (Int_Params);
+ 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 Image_I is new System.Image_I
+ (Int => Int,
+ Uns => Uns,
+ Unsigned_Width_Ghost => Unsigned_Width_Ghost,
+ Int_Params => Int_Spec.Int_Params);
procedure Set_Image_Integer
(V : Int;
diff --git a/gcc/ada/libgnat/s-imagei.adb b/gcc/ada/libgnat/s-imagei.adb
index ff853d3ac6b..8997e3c5a75 100644
--- a/gcc/ada/libgnat/s-imagei.adb
+++ b/gcc/ada/libgnat/s-imagei.adb
@@ -46,42 +46,6 @@ package body System.Image_I is
Post => Ignore,
Subprogram_Variant => Ignore);
- -- As a use_clause for Int_Params cannot be used for instances of this
- -- generic in System specs, rename all constants and subprograms.
-
- Unsigned_Width_Ghost : constant Natural := Int_Params.Unsigned_Width_Ghost;
-
- function Wrap_Option (Value : Uns) return Uns_Option
- renames Int_Params.Wrap_Option;
- function Only_Decimal_Ghost
- (Str : String;
- From, To : Integer)
- return Boolean
- renames Int_Params.Only_Decimal_Ghost;
- function Hexa_To_Unsigned_Ghost (X : Character) return Uns
- renames Int_Params.Hexa_To_Unsigned_Ghost;
- function Scan_Based_Number_Ghost
- (Str : String;
- From, To : Integer;
- Base : Uns := 10;
- Acc : Uns := 0)
- return Uns_Option
- renames Int_Params.Scan_Based_Number_Ghost;
- function Is_Integer_Ghost (Str : String) return Boolean
- renames Int_Params.Is_Integer_Ghost;
- procedure Prove_Iter_Scan_Based_Number_Ghost
- (Str1, Str2 : String;
- From, To : Integer;
- Base : Uns := 10;
- Acc : Uns := 0)
- renames Int_Params.Prove_Iter_Scan_Based_Number_Ghost;
- procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
- renames Int_Params.Prove_Scan_Only_Decimal_Ghost;
- function Abs_Uns_Of_Int (Val : Int) return Uns
- renames Int_Params.Abs_Uns_Of_Int;
- function Value_Integer (Str : String) return Int
- renames Int_Params.Value_Integer;
-
subtype Non_Positive is Int range Int'First .. 0;
function Uns_Of_Non_Positive (T : Non_Positive) return Uns is
@@ -99,9 +63,9 @@ package body System.Image_I 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 Only_Decimal_Ghost (S, From => P'Old + 1, To => P)
- and then Scan_Based_Number_Ghost (S, From => P'Old + 1, To => P)
- = Wrap_Option (Uns_Of_Non_Positive (T));
+ and then UP.Only_Decimal_Ghost (S, From => P'Old + 1, To => P)
+ and then UP.Scan_Based_Number_Ghost (S, From => P'Old + 1, To => P)
+ = UP.Wrap_Option (Uns_Of_Non_Positive (T));
-- Set digits of absolute value of T, which is zero or negative. We work
-- with the negative of the value so that the largest negative number is
-- not a special case.
@@ -182,11 +146,12 @@ package body System.Image_I is
and then P in 2 .. S'Last
and then S (1) in ' ' | '-'
and then (S (1) = '-') = (V < 0)
- and then Only_Decimal_Ghost (S, From => 2, To => P)
- and then Scan_Based_Number_Ghost (S, From => 2, To => P)
- = Wrap_Option (Abs_Uns_Of_Int (V)),
- Post => Is_Integer_Ghost (S (1 .. P))
- and then Value_Integer (S (1 .. P)) = V;
+ 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)
+ 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
-- Scan_Based_Number_Ghost and the sign on a decimal string.
@@ -198,11 +163,14 @@ package body System.Image_I is
Str : constant String := S (1 .. P);
begin
pragma Assert (Str'First = 1);
- pragma Assert (Only_Decimal_Ghost (Str, From => 2, To => P));
- Prove_Iter_Scan_Based_Number_Ghost (S, Str, From => 2, To => P);
- pragma Assert (Scan_Based_Number_Ghost (Str, From => 2, To => P)
- = Wrap_Option (Abs_Uns_Of_Int (V)));
- Prove_Scan_Only_Decimal_Ghost (Str, V);
+ pragma Assert (Str (2) /= ' ');
+ pragma Assert
+ (UP.Only_Decimal_Ghost (Str, From => 2, To => P));
+ UP.Prove_Scan_Based_Number_Ghost_Eq (S, Str, From => 2, To => P);
+ pragma Assert
+ (UP.Scan_Based_Number_Ghost (Str, From => 2, To => P)
+ = UP.Wrap_Option (IP.Abs_Uns_Of_Int (V)));
+ IP.Prove_Scan_Only_Decimal_Ghost (Str, V);
end Prove_Value_Integer;
-- Start of processing for Image_Integer
@@ -226,6 +194,8 @@ package body System.Image_I is
pragma Assert (P_Prev + Offset = 2);
end;
+ pragma Assert (if V >= 0 then S (1) = ' ');
+ pragma Assert (S (1) in ' ' | '-');
Prove_Value_Integer;
end Image_Integer;
@@ -248,42 +218,78 @@ package body System.Image_I is
S_Init : constant String := S with Ghost;
Uns_T : constant Uns := Uns_Of_Non_Positive (T) with Ghost;
Uns_Value : Uns := Uns_Of_Non_Positive (Value) with Ghost;
- Prev, Cur : Uns_Option with Ghost;
Prev_Value : Uns with Ghost;
Prev_S : String := S with Ghost;
-- Local ghost lemmas
- procedure Prove_Character_Val (RU : Uns; RI : Int)
+ procedure Prove_Character_Val (RU : Uns; RI : Non_Positive)
with
Ghost,
- Pre => RU in 0 .. 9
- and then RI in 0 .. 9,
- Post => Character'Val (48 + RU) in '0' .. '9'
- and then Character'Val (48 + RI) in '0' .. '9';
+ Post => RU rem 10 in 0 .. 9
+ and then -(RI rem 10) in 0 .. 9
+ and then Character'Val (48 + RU rem 10) in '0' .. '9'
+ and then Character'Val (48 - RI rem 10) in '0' .. '9';
-- Ghost lemma to prove the value of a character corresponding to the
-- next figure.
+ procedure Prove_Euclidian (Val, Quot, Rest : Uns)
+ with
+ Ghost,
+ Pre => Quot = Val / 10
+ and then Rest = Val rem 10,
+ Post => Uns'Last - Rest >= 10 * Quot and then Val = 10 * Quot + Rest;
+ -- Ghost lemma to prove the relation between the quotient/remainder of
+ -- division by 10 and the initial value.
+
procedure Prove_Hexa_To_Unsigned_Ghost (RU : Uns; RI : Int)
with
Ghost,
Pre => RU in 0 .. 9
and then RI in 0 .. 9,
- Post => Hexa_To_Unsigned_Ghost (Character'Val (48 + RU)) = RU
- and then Hexa_To_Unsigned_Ghost (Character'Val (48 + RI)) = Uns (RI);
+ Post => UP.Hexa_To_Unsigned_Ghost
+ (Character'Val (48 + RU)) = RU
+ and then UP.Hexa_To_Unsigned_Ghost
+ (Character'Val (48 + RI)) = Uns (RI);
-- Ghost lemma to prove that Hexa_To_Unsigned_Ghost returns the source
-- figure when applied to the corresponding character.
- procedure Prove_Unchanged
- with
- Ghost,
- Pre => P <= S'Last
- and then S_Init'First = S'First
- and then S_Init'Last = S'Last
- and then (for all K in S'First .. P => S (K) = S_Init (K)),
- Post => S (S'First .. P) = S_Init (S'First .. P);
- -- Ghost lemma to prove that the part of string S before P has not been
- -- modified.
+ procedure Prove_Scan_Iter
+ (S, Prev_S : String;
+ V, Prev_V, Res : Uns;
+ P, Max : Natural)
+ with
+ Ghost,
+ Pre =>
+ S'First = Prev_S'First and then S'Last = Prev_S'Last
+ and then S'Last < Natural'Last and then
+ Max in S'Range and then P in S'First .. Max and then
+ (for all I in P + 1 .. Max => Prev_S (I) in '0' .. '9')
+ 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 - UP.Hexa_To_Unsigned_Ghost (S (P))
+ >= 10 * V
+ and then Prev_V =
+ V * 10 + UP.Hexa_To_Unsigned_Ghost (S (P))
+ and then
+ (if P = Max then Prev_V = Res
+ else UP.Scan_Based_Number_Ghost
+ (Str => Prev_S,
+ From => P + 1,
+ To => Max,
+ Base => 10,
+ Acc => Prev_V) = UP.Wrap_Option (Res)),
+ Post =>
+ (for all I in P .. Max => S (I) in '0' .. '9')
+ and then UP.Scan_Based_Number_Ghost
+ (Str => S,
+ From => P,
+ To => Max,
+ Base => 10,
+ Acc => V) = UP.Wrap_Option (Res);
+ -- Ghost lemma to prove that Scan_Based_Number_Ghost is preserved
+ -- through an iteration of the loop.
procedure Prove_Uns_Of_Non_Positive_Value
with
@@ -294,50 +300,44 @@ package body System.Image_I is
-- Ghost lemma to prove that the relation between Value and its unsigned
-- version is preserved.
- procedure Prove_Iter_Scan
- (Str1, Str2 : String;
- From, To : Integer;
- Base : Uns := 10;
- Acc : Uns := 0)
- with
- Ghost,
- Pre => Str1'Last /= Positive'Last
- and then
- (From > To or else (From >= Str1'First and then To <= Str1'Last))
- and then Only_Decimal_Ghost (Str1, From, To)
- and then Str1'First = Str2'First
- and then Str1'Last = Str2'Last
- and then (for all J in From .. To => Str1 (J) = Str2 (J)),
- Post =>
- Scan_Based_Number_Ghost (Str1, From, To, Base, Acc)
- = Scan_Based_Number_Ghost (Str2, From, To, Base, Acc);
- -- Ghost lemma to prove that the result of Scan_Based_Number_Ghost only
- -- depends on the value of the argument string in the (From .. To) range
- -- of indexes. This is a wrapper on Prove_Iter_Scan_Based_Number_Ghost
- -- so that we can call it here on ghost arguments.
-
-----------------------------
-- Local lemma null bodies --
-----------------------------
- procedure Prove_Character_Val (RU : Uns; RI : Int) is null;
+ procedure Prove_Character_Val (RU : Uns; RI : Non_Positive) is null;
+ procedure Prove_Euclidian (Val, Quot, Rest : Uns) is null;
procedure Prove_Hexa_To_Unsigned_Ghost (RU : Uns; RI : Int) is null;
- procedure Prove_Unchanged is null;
procedure Prove_Uns_Of_Non_Positive_Value is null;
---------------------
- -- Prove_Iter_Scan --
+ -- Prove_Scan_Iter --
---------------------
- procedure Prove_Iter_Scan
- (Str1, Str2 : String;
- From, To : Integer;
- Base : Uns := 10;
- Acc : Uns := 0)
+ procedure Prove_Scan_Iter
+ (S, Prev_S : String;
+ V, Prev_V, Res : Uns;
+ P, Max : Natural)
is
+ pragma Unreferenced (Res);
begin
- Prove_Iter_Scan_Based_Number_Ghost (Str1, Str2, From, To, Base, Acc);
- end Prove_Iter_Scan;
+ UP.Lemma_Scan_Based_Number_Ghost_Step
+ (Str => S,
+ From => P,
+ To => Max,
+ Base => 10,
+ Acc => V);
+ if P < Max then
+ UP.Prove_Scan_Based_Number_Ghost_Eq
+ (Prev_S, S, P + 1, Max, 10, Prev_V);
+ else
+ UP.Lemma_Scan_Based_Number_Ghost_Base
+ (Str => S,
+ From => P + 1,
+ To => Max,
+ Base => 10,
+ Acc => Prev_V);
+ end if;
+ end Prove_Scan_Iter;
-- Start of processing for Set_Digits
@@ -383,13 +383,9 @@ package body System.Image_I is
for J in reverse 1 .. Nb_Digits loop
Lemma_Div_Commutation (Uns_Value, 10);
Lemma_Div_Twice (Big (Uns_T), Big_10 ** (Nb_Digits - J), Big_10);
- Prove_Character_Val (Uns_Value rem 10, -(Value rem 10));
+ Prove_Character_Val (Uns_Value, Value);
Prove_Hexa_To_Unsigned_Ghost (Uns_Value rem 10, -(Value rem 10));
Prove_Uns_Of_Non_Positive_Value;
- pragma Assert (Uns_Value rem 10 = Uns_Of_Non_Positive (Value rem 10));
- pragma Assert (Uns_Value rem 10 = Uns (-(Value rem 10)));
- pragma Assert
- (Uns_Value = From_Big (Big (Uns_T) / Big_10 ** (Nb_Digits - J)));
Prev_Value := Uns_Value;
Prev_S := S;
@@ -399,68 +395,44 @@ package body System.Image_I is
S (P + J) := Character'Val (48 - (Value rem 10));
Value := Value / 10;
- pragma Assert (S (P + J) in '0' .. '9');
- pragma Assert (Hexa_To_Unsigned_Ghost (S (P + J)) =
- From_Big (Big (Uns_T) / Big_10 ** (Nb_Digits - J)) rem 10);
- pragma Assert
- (for all K in P + J + 1 .. P + Nb_Digits => S (K) in '0' .. '9');
+ Prove_Euclidian
+ (Val => Prev_Value,
+ Quot => Uns_Value,
+ Rest => UP.Hexa_To_Unsigned_Ghost (S (P + J)));
- Prev := Scan_Based_Number_Ghost
- (Str => S,
- From => P + J + 1,
- To => P + Nb_Digits,
- Base => 10,
- Acc => Prev_Value);
- Cur := Scan_Based_Number_Ghost
- (Str => S,
- From => P + J,
- To => P + Nb_Digits,
- Base => 10,
- Acc => Uns_Value);
- pragma Assert (Prev_Value = 10 * Uns_Value + (Prev_Value rem 10));
- pragma Assert
- (Prev_Value rem 10 = Hexa_To_Unsigned_Ghost (S (P + J)));
- pragma Assert
- (Prev_Value = 10 * Uns_Value + Hexa_To_Unsigned_Ghost (S (P + J)));
-
- if J /= Nb_Digits then
- Prove_Iter_Scan
- (Prev_S, S, P + J + 1, P + Nb_Digits, 10, Prev_Value);
- end if;
-
- pragma Assert (Prev = Cur);
- pragma Assert (Prev = Wrap_Option (Uns_T));
+ Prove_Scan_Iter
+ (S, Prev_S, Uns_Value, Prev_Value, Uns_T, P + J, P + Nb_Digits);
pragma Loop_Invariant (Uns_Value = Uns_Of_Non_Positive (Value));
pragma Loop_Invariant (Uns_Value <= Uns'Last / 10);
pragma Loop_Invariant
(for all K in S'First .. P => S (K) = S_Init (K));
- pragma Loop_Invariant (Only_Decimal_Ghost (S, P + J, P + Nb_Digits));
+ pragma Loop_Invariant
+ (UP.Only_Decimal_Ghost (S, P + J, P + Nb_Digits));
pragma Loop_Invariant
(for all K in P + J .. P + Nb_Digits => S (K) in '0' .. '9');
pragma Loop_Invariant (Pow = Big_10 ** (Nb_Digits - J + 1));
pragma Loop_Invariant (Big (Uns_Value) = Big (Uns_T) / Pow);
pragma Loop_Invariant
- (Scan_Based_Number_Ghost
+ (UP.Scan_Based_Number_Ghost
(Str => S,
From => P + J,
To => P + Nb_Digits,
Base => 10,
Acc => Uns_Value)
- = Wrap_Option (Uns_T));
+ = UP.Wrap_Option (Uns_T));
end loop;
pragma Assert (Big (Uns_Value) = Big (Uns_T) / Big_10 ** (Nb_Digits));
pragma Assert (Uns_Value = 0);
- Prove_Unchanged;
pragma Assert
- (Scan_Based_Number_Ghost
+ (UP.Scan_Based_Number_Ghost
(Str => S,
From => P + 1,
To => P + Nb_Digits,
Base => 10,
Acc => Uns_Value)
- = Wrap_Option (Uns_T));
+ = UP.Wrap_Option (Uns_T));
P := P + Nb_Digits;
end Set_Digits;
diff --git a/gcc/ada/libgnat/s-imagei.ads b/gcc/ada/libgnat/s-imagei.ads
index 10116d123ed..575c60abb2c 100644
--- a/gcc/ada/libgnat/s-imagei.ads
+++ b/gcc/ada/libgnat/s-imagei.ads
@@ -48,19 +48,19 @@ pragma Assertion_Policy (Pre => Ignore,
with System.Val_Util;
generic
+ type Int is range <>;
+ type Uns is mod <>;
- with package Int_Params is new System.Val_Util.Int_Params (<>);
+ Unsigned_Width_Ghost : Natural;
-package System.Image_I is
-
- subtype Int is Int_Params.Int;
- use type Int_Params.Int;
+ with package Int_Params is new System.Val_Util.Int_Params
+ (Int => Int, Uns => Uns, others => <>)
+ with Ghost;
- subtype Uns is Int_Params.Uns;
- use type Int_Params.Uns;
-
- subtype Uns_Option is Int_Params.Uns_Option;
- use type Int_Params.Uns_Option;
+package System.Image_I is
+ package IP renames Int_Params;
+ package UP renames IP.Uns_Params;
+ use type UP.Uns_Option;
procedure Image_Integer
(V : Int;
@@ -69,9 +69,9 @@ package System.Image_I is
with
Pre => S'First = 1
and then S'Last < Integer'Last
- and then S'Last >= Int_Params.Unsigned_Width_Ghost,
+ and then S'Last >= Unsigned_Width_Ghost,
Post => P in S'Range
- and then Int_Params.Value_Integer (S (1 .. P)) = V;
+ and then IP.Is_Value_Integer_Ghost (S (1 .. P), V);
-- Computes Int'Image (V) and stores the result in S (1 .. P)
-- setting the resulting value of P. The caller guarantees that S
-- is long enough to hold the result, and that S'First is 1.
@@ -87,23 +87,23 @@ package System.Image_I is
and then S'First <= S'Last
and then
(if V >= 0 then
- P <= S'Last - Int_Params.Unsigned_Width_Ghost + 1
+ P <= S'Last - Unsigned_Width_Ghost + 1
else
- P <= S'Last - Int_Params.Unsigned_Width_Ghost),
+ P <= S'Last - Unsigned_Width_Ghost),
Post => S (S'First .. P'Old) = S'Old (S'First .. P'Old)
and then
(declare
Minus : constant Boolean := S (P'Old + 1) = '-';
Offset : constant Positive := (if V >= 0 then 1 else 2);
- Abs_V : constant Uns := Int_Params.Abs_Uns_Of_Int (V);
+ Abs_V : constant Uns := IP.Abs_Uns_Of_Int (V);
begin
Minus = (V < 0)
and then P in P'Old + Offset .. S'Last
- and then Int_Params.Only_Decimal_Ghost
+ and then UP.Only_Decimal_Ghost
(S, From => P'Old + Offset, To => P)
- and then Int_Params.Scan_Based_Number_Ghost
+ and then UP.Scan_Based_Number_Ghost
(S, From => P'Old + Offset, To => P)
- = Int_Params.Wrap_Option (Abs_V));
+ = UP.Wrap_Option (Abs_V));
-- Stores the image of V in S starting at S (P + 1), P is updated to point
-- to the last character stored. The value stored is identical to the value
-- of Int'Image (V) except that no leading space is stored when V is
diff --git a/gcc/ada/libgnat/s-imageu.adb b/gcc/ada/libgnat/s-imageu.adb
index 69324878010..0e1c2bb593f 100644
--- a/gcc/ada/libgnat/s-imageu.adb
+++ b/gcc/ada/libgnat/s-imageu.adb
@@ -147,11 +147,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 Only_Decimal_Ghost (S, From => 2, To => P)
- and then Scan_Based_Number_Ghost (S, From => 2, To => P)
- = Wrap_Option (V),
- Post => Is_Unsigned_Ghost (S (1 .. P))
- and then Value_Unsigned (S (1 .. P)) = V;
+ 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);
-- Ghost lemma to prove the value of Value_Unsigned from the value of
-- Scan_Based_Number_Ghost on a decimal string.
@@ -163,11 +164,15 @@ package body System.Image_U is
Str : constant String := S (1 .. P);
begin
pragma Assert (Str'First = 1);
- pragma Assert (Only_Decimal_Ghost (Str, From => 2, To => P));
- Prove_Iter_Scan_Based_Number_Ghost (S, Str, From => 2, To => P);
- pragma Assert (Scan_Based_Number_Ghost (Str, From => 2, To => P)
- = Wrap_Option (V));
- Prove_Scan_Only_Decimal_Ghost (Str, V);
+ pragma Assert (S (2) /= ' ');
+ pragma Assert
+ (Uns_Params.Only_Decimal_Ghost (Str, From => 2, To => P));
+ Uns_Params.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);
end Prove_Value_Unsigned;
-- Start of processing for Image_Unsigned
@@ -196,7 +201,6 @@ package body System.Image_U is
Pow : Big_Positive := 1 with Ghost;
S_Init : constant String := S with Ghost;
- Prev, Cur : Uns_Option with Ghost;
Prev_Value : Uns with Ghost;
Prev_S : String := S with Ghost;
@@ -205,8 +209,8 @@ package body System.Image_U is
procedure Prove_Character_Val (R : Uns)
with
Ghost,
- Pre => R in 0 .. 9,
- Post => Character'Val (48 + R) in '0' .. '9';
+ Post => R rem 10 in 0 .. 9
+ and then Character'Val (48 + R rem 10) in '0' .. '9';
-- Ghost lemma to prove the value of a character corresponding to the
-- next figure.
@@ -215,7 +219,7 @@ package body System.Image_U is
Ghost,
Pre => Quot = Val / 10
and then Rest = Val rem 10,
- Post => Val = 10 * Quot + Rest;
+ Post => Uns'Last - Rest >= 10 * Quot and then Val = 10 * Quot + Rest;
-- Ghost lemma to prove the relation between the quotient/remainder of
-- division by 10 and the initial value.
@@ -223,42 +227,46 @@ package body System.Image_U is
with
Ghost,
Pre => R in 0 .. 9,
- Post => Hexa_To_Unsigned_Ghost (Character'Val (48 + R)) = R;
+ Post => Uns_Params.Hexa_To_Unsigned_Ghost (Character'Val (48 + R)) = R;
-- Ghost lemma to prove that Hexa_To_Unsigned_Ghost returns the source
-- figure when applied to the corresponding character.
- procedure Prove_Unchanged
- with
- Ghost,
- Pre => P <= S'Last
- and then S_Init'First = S'First
- and then S_Init'Last = S'Last
- and then (for all K in S'First .. P => S (K) = S_Init (K)),
- Post => S (S'First .. P) = S_Init (S'First .. P);
- -- Ghost lemma to prove that the part of string S before P has not been
- -- modified.
-
- procedure Prove_Iter_Scan
- (Str1, Str2 : String;
- From, To : Integer;
- Base : Uns := 10;
- Acc : Uns := 0)
- with
- Ghost,
- Pre => Str1'Last /= Positive'Last
- and then
- (From > To or else (From >= Str1'First and then To <= Str1'Last))
- and then Only_Decimal_Ghost (Str1, From, To)
- and then Str1'First = Str2'First
- and then Str1'Last = Str2'Last
- and then (for all J in From .. To => Str1 (J) = Str2 (J)),
- Post =>
- Scan_Based_Number_Ghost (Str1, From, To, Base, Acc)
- = Scan_Based_Number_Ghost (Str2, From, To, Base, Acc);
- -- Ghost lemma to prove that the result of Scan_Based_Number_Ghost only
- -- depends on the value of the argument string in the (From .. To) range
- -- of indexes. This is a wrapper on Prove_Iter_Scan_Based_Number_Ghost
- -- so that we can call it here on ghost arguments.
+ procedure Prove_Scan_Iter
+ (S, Prev_S : String;
+ V, Prev_V, Res : Uns;
+ P, Max : Natural)
+ with
+ Ghost,
+ Pre =>
+ S'First = Prev_S'First and then S'Last = Prev_S'Last
+ and then S'Last < Natural'Last and then
+ Max in S'Range and then P in S'First .. Max and then
+ (for all I in P + 1 .. Max => Prev_S (I) in '0' .. '9')
+ 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))
+ >= 10 * V
+ and then Prev_V =
+ V * 10 + Uns_Params.Hexa_To_Unsigned_Ghost (S (P))
+ and then
+ (if P = Max then Prev_V = Res
+ else Uns_Params.Scan_Based_Number_Ghost
+ (Str => Prev_S,
+ From => P + 1,
+ To => Max,
+ Base => 10,
+ Acc => Prev_V) = Uns_Params.Wrap_Option (Res)),
+ Post =>
+ (for all I in P .. Max => S (I) in '0' .. '9')
+ and then Uns_Params.Scan_Based_Number_Ghost
+ (Str => S,
+ From => P,
+ To => Max,
+ Base => 10,
+ Acc => V) = Uns_Params.Wrap_Option (Res);
+ -- Ghost lemma to prove that Scan_Based_Number_Ghost is preserved
+ -- through an iteration of the loop.
-----------------------------
-- Local lemma null bodies --
@@ -267,21 +275,36 @@ package body System.Image_U is
procedure Prove_Character_Val (R : Uns) is null;
procedure Prove_Euclidian (Val, Quot, Rest : Uns) is null;
procedure Prove_Hexa_To_Unsigned_Ghost (R : Uns) is null;
- procedure Prove_Unchanged is null;
---------------------
- -- Prove_Iter_Scan --
+ -- Prove_Scan_Iter --
---------------------
- procedure Prove_Iter_Scan
- (Str1, Str2 : String;
- From, To : Integer;
- Base : Uns := 10;
- Acc : Uns := 0)
+ procedure Prove_Scan_Iter
+ (S, Prev_S : String;
+ V, Prev_V, Res : Uns;
+ P, Max : Natural)
is
+ pragma Unreferenced (Res);
begin
- Prove_Iter_Scan_Based_Number_Ghost (Str1, Str2, From, To, Base, Acc);
- end Prove_Iter_Scan;
+ Uns_Params.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
+ (Prev_S, S, P + 1, Max, 10, Prev_V);
+ else
+ Uns_Params.Lemma_Scan_Based_Number_Ghost_Base
+ (Str => S,
+ From => P + 1,
+ To => Max,
+ Base => 10,
+ Acc => Prev_V);
+ end if;
+ end Prove_Scan_Iter;
-- Start of processing for Set_Image_Unsigned
@@ -313,6 +336,7 @@ package body System.Image_U is
Lemma_Non_Zero (Value);
pragma Assert (Pow <= Big (Uns'Last));
end loop;
+ pragma Assert (Big (V) / (Big_10 ** Nb_Digits) = 0);
Value := V;
Pow := 1;
@@ -323,77 +347,43 @@ package body System.Image_U is
for J in reverse 1 .. Nb_Digits loop
Lemma_Div_Commutation (Value, 10);
Lemma_Div_Twice (Big (V), Big_10 ** (Nb_Digits - J), Big_10);
- Prove_Character_Val (Value rem 10);
+ Prove_Character_Val (Value);
Prove_Hexa_To_Unsigned_Ghost (Value rem 10);
Prev_Value := Value;
Prev_S := S;
Pow := Pow * 10;
-
S (P + J) := Character'Val (48 + (Value rem 10));
Value := Value / 10;
- pragma Assert (S (P + J) in '0' .. '9');
- pragma Assert (Hexa_To_Unsigned_Ghost (S (P + J)) =
- From_Big (Big (V) / Big_10 ** (Nb_Digits - J)) rem 10);
- pragma Assert
- (for all K in P + J + 1 .. P + Nb_Digits => S (K) in '0' .. '9');
- pragma Assert
- (for all K in P + J + 1 .. P + Nb_Digits =>
- Hexa_To_Unsigned_Ghost (S (K)) =
- From_Big (Big (V) / Big_10 ** (Nb_Digits - (K - P))) rem 10);
-
- Prev := Scan_Based_Number_Ghost
- (Str => S,
- From => P + J + 1,
- To => P + Nb_Digits,
- Base => 10,
- Acc => Prev_Value);
- Cur := Scan_Based_Number_Ghost
- (Str => S,
- From => P + J,
- To => P + Nb_Digits,
- Base => 10,
- Acc => Value);
-
- if J /= Nb_Digits then
- Prove_Euclidian (Val => Prev_Value,
- Quot => Value,
- Rest => Hexa_To_Unsigned_Ghost (S (P + J)));
- pragma Assert
- (Prev_Value = 10 * Value + Hexa_To_Unsigned_Ghost (S (P + J)));
- Prove_Iter_Scan
- (Prev_S, S, P + J + 1, P + Nb_Digits, 10, Prev_Value);
- end if;
+ Prove_Euclidian
+ (Val => Prev_Value,
+ Quot => Value,
+ Rest => Uns_Params.Hexa_To_Unsigned_Ghost (S (P + J)));
- pragma Assert (Prev = Cur);
- pragma Assert (Prev = Wrap_Option (V));
+ Prove_Scan_Iter
+ (S, Prev_S, Value, Prev_Value, V, P + J, P + Nb_Digits);
pragma Loop_Invariant (Value <= Uns'Last / 10);
pragma Loop_Invariant
(for all K in S'First .. P => S (K) = S_Init (K));
- pragma Loop_Invariant (Only_Decimal_Ghost (S, P + J, P + Nb_Digits));
- pragma Loop_Invariant
- (for all K in P + J .. P + Nb_Digits => S (K) in '0' .. '9');
pragma Loop_Invariant
- (for all K in P + J .. P + Nb_Digits =>
- Hexa_To_Unsigned_Ghost (S (K)) =
- From_Big (Big (V) / Big_10 ** (Nb_Digits - (K - P))) rem 10);
+ (Uns_Params.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
- (Scan_Based_Number_Ghost
+ (Uns_Params.Scan_Based_Number_Ghost
(Str => S,
From => P + J,
To => P + Nb_Digits,
Base => 10,
Acc => Value)
- = Wrap_Option (V));
+ = Uns_Params.Wrap_Option (V));
end loop;
+ pragma Assert (Big (Value) = Big (V) / (Big_10 ** Nb_Digits));
pragma Assert (Value = 0);
- Prove_Unchanged;
-
P := P + Nb_Digits;
end Set_Image_Unsigned;
diff --git a/gcc/ada/libgnat/s-imageu.ads b/gcc/ada/libgnat/s-imageu.ads
index 789cf65a9d2..3d80ea9af5a 100644
--- a/gcc/ada/libgnat/s-imageu.ads
+++ b/gcc/ada/libgnat/s-imageu.ads
@@ -45,45 +45,22 @@ pragma Assertion_Policy (Pre => Ignore,
Ghost => Ignore,
Subprogram_Variant => Ignore);
+with System.Val_Util;
+
generic
type Uns is mod <>;
- type Uns_Option is private;
-- Additional parameters for ghost subprograms used inside contracts
Unsigned_Width_Ghost : Natural;
- with function Wrap_Option (Value : Uns) return Uns_Option
- with Ghost;
- with function Only_Decimal_Ghost
- (Str : String;
- From, To : Integer)
- return Boolean
- with Ghost;
- with function Hexa_To_Unsigned_Ghost (X : Character) return Uns
- with Ghost;
- with function Scan_Based_Number_Ghost
- (Str : String;
- From, To : Integer;
- Base : Uns := 10;
- Acc : Uns := 0) return Uns_Option
- with Ghost;
- with function Is_Unsigned_Ghost (Str : String) return Boolean
- with Ghost;
- with function Value_Unsigned (Str : String) return Uns;
- with procedure Prove_Iter_Scan_Based_Number_Ghost
- (Str1, Str2 : String;
- From, To : Integer;
- Base : Uns := 10;
- Acc : Uns := 0)
- with Ghost;
- with procedure Prove_Scan_Only_Decimal_Ghost
- (Str : String;
- Val : Uns)
- with Ghost;
+ with package Uns_Params is new System.Val_Util.Uns_Params
+ (Uns => Uns, others => <>)
+ with Ghost;
package System.Image_U is
+ use all type Uns_Params.Uns_Option;
procedure Image_Unsigned
(V : Uns;
@@ -94,7 +71,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 Value_Unsigned (S (1 .. P)) = V;
+ and then Uns_Params.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
@@ -112,9 +89,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 Only_Decimal_Ghost (S, From => P'Old + 1, To => P)
- and then Scan_Based_Number_Ghost (S, From => P'Old + 1, To => P)
- = Wrap_Option (V);
+ and then Uns_Params.Only_Decimal_Ghost (S, From => P'Old + 1, To => P)
+ and then Uns_Params.Scan_Based_Number_Ghost
+ (S, From => P'Old + 1, To => P)
+ = Uns_Params.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-imgint.ads b/gcc/ada/libgnat/s-imgint.ads
index fd5bea31c2a..8672e58b083 100644
--- a/gcc/ada/libgnat/s-imgint.ads
+++ b/gcc/ada/libgnat/s-imgint.ads
@@ -48,8 +48,6 @@ pragma Assertion_Policy (Pre => Ignore,
with System.Image_I;
with System.Unsigned_Types;
with System.Val_Int;
-with System.Val_Uns;
-with System.Val_Util;
with System.Wid_Uns;
package System.Img_Int
@@ -57,27 +55,12 @@ package System.Img_Int
is
subtype Unsigned is Unsigned_Types.Unsigned;
- package Int_Params is new Val_Util.Int_Params
- (Int => Integer,
- Uns => Unsigned,
- Uns_Option => Val_Uns.Impl.Uns_Option,
- Unsigned_Width_Ghost =>
+ package Impl is new Image_I
+ (Int => Integer,
+ Uns => Unsigned,
+ Unsigned_Width_Ghost =>
Wid_Uns.Width_Unsigned (0, Unsigned'Last),
- Only_Decimal_Ghost => Val_Uns.Impl.Only_Decimal_Ghost,
- Hexa_To_Unsigned_Ghost =>
- Val_Uns.Impl.Hexa_To_Unsigned_Ghost,
- Wrap_Option => Val_Uns.Impl.Wrap_Option,
- Scan_Based_Number_Ghost =>
- Val_Uns.Impl.Scan_Based_Number_Ghost,
- Prove_Iter_Scan_Based_Number_Ghost =>
- Val_Uns.Impl.Prove_Iter_Scan_Based_Number_Ghost,
- Is_Integer_Ghost => Val_Int.Impl.Is_Integer_Ghost,
- Prove_Scan_Only_Decimal_Ghost =>
- Val_Int.Impl.Prove_Scan_Only_Decimal_Ghost,
- Abs_Uns_Of_Int => Val_Int.Impl.Abs_Uns_Of_Int,
- Value_Integer => Val_Int.Impl.Value_Integer);
-
- package Impl is new Image_I (Int_Params);
+ Int_Params => System.Val_Int.Impl.Spec.Int_Params);
procedure Image_Integer
(V : Integer;
diff --git a/gcc/ada/libgnat/s-imglli.ads b/gcc/ada/libgnat/s-imglli.ads
index 20f108c8e45..99c1951348d 100644
--- a/gcc/ada/libgnat/s-imglli.ads
+++ b/gcc/ada/libgnat/s-imglli.ads
@@ -48,8 +48,6 @@ pragma Assertion_Policy (Pre => Ignore,
with System.Image_I;
with System.Unsigned_Types;
with System.Val_LLI;
-with System.Val_LLU;
-with System.Val_Util;
with System.Wid_LLU;
package System.Img_LLI
@@ -57,27 +55,13 @@ package System.Img_LLI
is
subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
- package Int_Params is new Val_Util.Int_Params
- (Int => Long_Long_Integer,
- Uns => Long_Long_Unsigned,
- Uns_Option => Val_LLU.Impl.Uns_Option,
- Unsigned_Width_Ghost =>
- Wid_LLU.Width_Long_Long_Unsigned (0, Long_Long_Unsigned'Last),
- Only_Decimal_Ghost => Val_LLU.Impl.Only_Decimal_Ghost,
- Hexa_To_Unsigned_Ghost =>
- Val_LLU.Impl.Hexa_To_Unsigned_Ghost,
- Wrap_Option => Val_LLU.Impl.Wrap_Option,
- Scan_Based_Number_Ghost =>
- Val_LLU.Impl.Scan_Based_Number_Ghost,
- Prove_Iter_Scan_Based_Number_Ghost =>
- Val_LLU.Impl.Prove_Iter_Scan_Based_Number_Ghost,
- Is_Integer_Ghost => Val_LLI.Impl.Is_Integer_Ghost,
- Prove_Scan_Only_Decimal_Ghost =>
- Val_LLI.Impl.Prove_Scan_Only_Decimal_Ghost,
- Abs_Uns_Of_Int => Val_LLI.Impl.Abs_Uns_Of_Int,
- Value_Integer => Val_LLI.Impl.Value_Integer);
-
- package Impl is new Image_I (Int_Params);
+ 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);
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 989c296d759..931c288d20e 100644
--- a/gcc/ada/libgnat/s-imgllli.ads
+++ b/gcc/ada/libgnat/s-imgllli.ads
@@ -48,8 +48,6 @@ pragma Assertion_Policy (Pre => Ignore,
with System.Image_I;
with System.Unsigned_Types;
with System.Val_LLLI;
-with System.Val_LLLU;
-with System.Val_Util;
with System.Wid_LLLU;
package System.Img_LLLI
@@ -57,28 +55,13 @@ package System.Img_LLLI
is
subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
- package Int_Params is new Val_Util.Int_Params
- (Int => Long_Long_Long_Integer,
- Uns => Long_Long_Long_Unsigned,
- Uns_Option => Val_LLLU.Impl.Uns_Option,
- Unsigned_Width_Ghost =>
+ 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),
- Only_Decimal_Ghost => Val_LLLU.Impl.Only_Decimal_Ghost,
- Hexa_To_Unsigned_Ghost =>
- Val_LLLU.Impl.Hexa_To_Unsigned_Ghost,
- Wrap_Option => Val_LLLU.Impl.Wrap_Option,
- Scan_Based_Number_Ghost =>
- Val_LLLU.Impl.Scan_Based_Number_Ghost,
- Prove_Iter_Scan_Based_Number_Ghost =>
- Val_LLLU.Impl.Prove_Iter_Scan_Based_Number_Ghost,
- Is_Integer_Ghost => Val_LLLI.Impl.Is_Integer_Ghost,
- Prove_Scan_Only_Decimal_Ghost =>
- Val_LLLI.Impl.Prove_Scan_Only_Decimal_Ghost,
- Abs_Uns_Of_Int => Val_LLLI.Impl.Abs_Uns_Of_Int,
- Value_Integer => Val_LLLI.Impl.Value_Integer);
-
- package Impl is new Image_I (Int_Params);
+ Int_Params => System.Val_LLLI.Impl.Spec.Int_Params);
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 0116aa83bc7..53b39a8fdd2 100644
--- a/gcc/ada/libgnat/s-imglllu.ads
+++ b/gcc/ada/libgnat/s-imglllu.ads
@@ -56,23 +56,11 @@ is
subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
package Impl is new Image_U
- (Uns => Long_Long_Long_Unsigned,
- Uns_Option => Val_LLLU.Impl.Uns_Option,
- Unsigned_Width_Ghost =>
+ (Uns => Long_Long_Long_Unsigned,
+ Unsigned_Width_Ghost =>
Wid_LLLU.Width_Long_Long_Long_Unsigned
(0, Long_Long_Long_Unsigned'Last),
- Only_Decimal_Ghost => Val_LLLU.Impl.Only_Decimal_Ghost,
- Hexa_To_Unsigned_Ghost =>
- Val_LLLU.Impl.Hexa_To_Unsigned_Ghost,
- Wrap_Option => Val_LLLU.Impl.Wrap_Option,
- Scan_Based_Number_Ghost =>
- Val_LLLU.Impl.Scan_Based_Number_Ghost,
- Is_Unsigned_Ghost => Val_LLLU.Impl.Is_Unsigned_Ghost,
- Value_Unsigned => Val_LLLU.Impl.Value_Unsigned,
- Prove_Iter_Scan_Based_Number_Ghost =>
- Val_LLLU.Impl.Prove_Iter_Scan_Based_Number_Ghost,
- Prove_Scan_Only_Decimal_Ghost =>
- Val_LLLU.Impl.Prove_Scan_Only_Decimal_Ghost);
+ Uns_Params => System.Val_LLLU.Impl.Spec.Uns_Params);
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 67372d77227..28339cd7afe 100644
--- a/gcc/ada/libgnat/s-imgllu.ads
+++ b/gcc/ada/libgnat/s-imgllu.ads
@@ -56,22 +56,10 @@ is
subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
package Impl is new Image_U
- (Uns => Long_Long_Unsigned,
- Uns_Option => Val_LLU.Impl.Uns_Option,
- Unsigned_Width_Ghost =>
+ (Uns => Long_Long_Unsigned,
+ Unsigned_Width_Ghost =>
Wid_LLU.Width_Long_Long_Unsigned (0, Long_Long_Unsigned'Last),
- Only_Decimal_Ghost => Val_LLU.Impl.Only_Decimal_Ghost,
- Hexa_To_Unsigned_Ghost =>
- Val_LLU.Impl.Hexa_To_Unsigned_Ghost,
- Wrap_Option => Val_LLU.Impl.Wrap_Option,
- Scan_Based_Number_Ghost =>
- Val_LLU.Impl.Scan_Based_Number_Ghost,
- Is_Unsigned_Ghost => Val_LLU.Impl.Is_Unsigned_Ghost,
- Value_Unsigned => Val_LLU.Impl.Value_Unsigned,
- Prove_Iter_Scan_Based_Number_Ghost =>
- Val_LLU.Impl.Prove_Iter_Scan_Based_Number_Ghost,
- Prove_Scan_Only_Decimal_Ghost =>
- Val_LLU.Impl.Prove_Scan_Only_Decimal_Ghost);
+ Uns_Params => System.Val_LLU.Impl.Spec.Uns_Params);
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 fa903cece7a..120bd5db7df 100644
--- a/gcc/ada/libgnat/s-imguns.ads
+++ b/gcc/ada/libgnat/s-imguns.ads
@@ -56,22 +56,10 @@ is
subtype Unsigned is Unsigned_Types.Unsigned;
package Impl is new Image_U
- (Uns => Unsigned,
- Uns_Option => Val_Uns.Impl.Uns_Option,
- Unsigned_Width_Ghost =>
+ (Uns => Unsigned,
+ Unsigned_Width_Ghost =>
Wid_Uns.Width_Unsigned (0, Unsigned'Last),
- Only_Decimal_Ghost => Val_Uns.Impl.Only_Decimal_Ghost,
- Hexa_To_Unsigned_Ghost =>
- Val_Uns.Impl.Hexa_To_Unsigned_Ghost,
- Wrap_Option => Val_Uns.Impl.Wrap_Option,
- Scan_Based_Number_Ghost =>
- Val_Uns.Impl.Scan_Based_Number_Ghost,
- Is_Unsigned_Ghost => Val_Uns.Impl.Is_Unsigned_Ghost,
- Value_Unsigned => Val_Uns.Impl.Value_Unsigned,
- Prove_Iter_Scan_Based_Number_Ghost =>
- Val_Uns.Impl.Prove_Iter_Scan_Based_Number_Ghost,
- Prove_Scan_Only_Decimal_Ghost =>
- Val_Uns.Impl.Prove_Scan_Only_Decimal_Ghost);
+ Uns_Params => System.Val_Uns.Impl.Spec.Uns_Params);
procedure Image_Unsigned
(V : Unsigned;
diff --git a/gcc/ada/libgnat/s-vaispe.adb b/gcc/ada/libgnat/s-vaispe.adb
new file mode 100644
index 00000000000..dca2fd782f5
--- /dev/null
+++ b/gcc/ada/libgnat/s-vaispe.adb
@@ -0,0 +1,87 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT COMPILER COMPONENTS --
+-- --
+-- S Y S T E M . V A L U E _ I _ S P E C --
+-- --
+-- B o d y --
+-- --
+-- Copyright (C) 2022-2022, 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. --
+-- --
+------------------------------------------------------------------------------
+
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore,
+ Subprogram_Variant => Ignore);
+
+package body System.Value_I_Spec is
+
+ -----------------------------------
+ -- Prove_Scan_Only_Decimal_Ghost --
+ -----------------------------------
+
+ procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) is
+ Non_Blank : constant Positive := First_Non_Space_Ghost
+ (Str, Str'First, Str'Last);
+ pragma Assert (Str (Str'First + 1) /= ' ');
+ pragma Assert
+ (if Val < 0 then Non_Blank = Str'First
+ else
+ Str (Str'First) = ' '
+ and then Non_Blank = Str'First + 1);
+ Minus : constant Boolean := Str (Non_Blank) = '-';
+ Fst_Num : constant Positive :=
+ (if Minus then Non_Blank + 1 else Non_Blank);
+ pragma Assert (Fst_Num = Str'First + 1);
+ Uval : constant Uns := Abs_Uns_Of_Int (Val);
+
+ procedure Prove_Conversion_Is_Identity (Val : Int; Uval : Uns)
+ with
+ Pre => Minus = (Val < 0)
+ and then Uval = Abs_Uns_Of_Int (Val),
+ Post => Uns_Is_Valid_Int (Minus, Uval)
+ and then Is_Int_Of_Uns (Minus, Uval, Val);
+ -- Local proof of the unicity of the signed representation
+
+ procedure Prove_Conversion_Is_Identity (Val : Int; Uval : Uns) is null;
+
+ -- Start of processing for Prove_Scan_Only_Decimal_Ghost
+
+ begin
+ Prove_Conversion_Is_Identity (Val, Uval);
+ pragma Assert
+ (Uns_Params.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);
+ pragma Assert
+ (Uns_Params.Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last));
+ pragma Assert (Only_Space_Ghost
+ (Str, Uns_Params.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));
+ end Prove_Scan_Only_Decimal_Ghost;
+
+end System.Value_I_Spec;
diff --git a/gcc/ada/libgnat/s-vaispe.ads b/gcc/ada/libgnat/s-vaispe.ads
new file mode 100644
index 00000000000..5a5e051620a
--- /dev/null
+++ b/gcc/ada/libgnat/s-vaispe.ads
@@ -0,0 +1,199 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT COMPILER COMPONENTS --
+-- --
+-- S Y S T E M . V A L U E _ I _ S P E C --
+-- --
+-- S p e c --
+-- --
+-- Copyright (C) 2022-2022, 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 the specification entities using for the formal
+-- verification of the routines for scanning signed integer values.
+
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore. Postconditions and
+-- contract cases should not be executed at runtime as well, in order not to
+-- slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore,
+ Subprogram_Variant => Ignore);
+
+with System.Val_Util; use System.Val_Util;
+
+generic
+
+ type Int is range <>;
+
+ type Uns is mod <>;
+
+ -- Additional parameters for specification subprograms on modular Unsigned
+ -- integers.
+
+ with package Uns_Params is new System.Val_Util.Uns_Params
+ (Uns => Uns, others => <>)
+ with Ghost;
+
+package System.Value_I_Spec with
+ Ghost,
+ SPARK_Mode,
+ Annotate => (GNATprove, Always_Return)
+is
+ pragma Preelaborate;
+ use all type Uns_Params.Uns_Option;
+
+ function Uns_Is_Valid_Int (Minus : Boolean; Uval : Uns) return Boolean is
+ (if Minus then Uval <= Uns (Int'Last) + 1
+ else Uval <= Uns (Int'Last))
+ with Post => True;
+ -- Return True if Uval (or -Uval when Minus is True) is a valid number of
+ -- type Int.
+
+ function Is_Int_Of_Uns
+ (Minus : Boolean;
+ Uval : Uns;
+ Val : Int)
+ return Boolean
+ is
+ (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First
+ elsif Minus then Val = -(Int (Uval))
+ else Val = Int (Uval))
+ with
+ Pre => Uns_Is_Valid_Int (Minus, Uval),
+ Post => True;
+ -- Return True if Uval (or -Uval when Minus is True) is equal to Val
+
+ function Abs_Uns_Of_Int (Val : Int) return Uns is
+ (if Val = Int'First then Uns (Int'Last) + 1
+ elsif Val < 0 then Uns (-Val)
+ else Uns (Val));
+ -- Return the unsigned absolute value of Val
+
+ function Slide_To_1 (Str : String) return String
+ with
+ Post =>
+ Only_Space_Ghost (Str, Str'First, Str'Last) =
+ (for all J in Str'First .. Str'Last =>
+ Slide_To_1'Result (J - Str'First + 1) = ' ');
+ -- Slides Str so that it starts at 1
+
+ function Slide_If_Necessary (Str : String) return String is
+ (if Str'Last = Positive'Last then Slide_To_1 (Str) else Str);
+ -- If Str'Last = Positive'Last then slides Str so that it starts at 1
+
+ function Is_Integer_Ghost (Str : String) return Boolean is
+ (declare
+ Non_Blank : constant Positive := First_Non_Space_Ghost
+ (Str, Str'First, Str'Last);
+ 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
+ (Str, Fst_Num, Str'Last)
+ and then
+ Uns_Is_Valid_Int
+ (Minus => Str (Non_Blank) = '-',
+ Uval => Uns_Params.Scan_Raw_Unsigned_Ghost
+ (Str, Fst_Num, Str'Last))
+ and then Only_Space_Ghost
+ (Str, Uns_Params.Raw_Unsigned_Last_Ghost
+ (Str, Fst_Num, Str'Last), Str'Last))
+ with
+ Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+ and then Str'Last /= Positive'Last,
+ Post => True;
+ -- Ghost function that determines if Str has the correct format for a
+ -- signed number, consisting in some blank characters, an optional
+ -- sign, a raw unsigned number which does not overflow and then some
+ -- more blank characters.
+
+ function Is_Value_Integer_Ghost (Str : String; Val : Int) return Boolean is
+ (declare
+ Non_Blank : constant Positive := First_Non_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);
+ begin
+ Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-',
+ Uval => Uval,
+ Val => Val))
+ with
+ Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+ and then Str'Last /= Positive'Last
+ and then Is_Integer_Ghost (Str),
+ Post => True;
+ -- Ghost function that returns True if Val is the value corresponding to
+ -- the signed number represented by Str.
+
+ procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
+ with
+ Ghost,
+ Pre => Str'Last /= Positive'Last
+ and then Str'Length >= 2
+ and then Str (Str'First) in ' ' | '-'
+ and then (Str (Str'First) = '-') = (Val < 0)
+ and then Uns_Params.Only_Decimal_Ghost (Str, Str'First + 1, Str'Last)
+ and then Uns_Params.Scan_Based_Number_Ghost
+ (Str, Str'First + 1, Str'Last)
+ = Uns_Params.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
+
+ ----------------
+ -- Slide_To_1 --
+ ----------------
+
+ function Slide_To_1 (Str : String) return String is
+ (declare
+ Res : constant String (1 .. Str'Length) := Str;
+ begin
+ Res);
+
+end System.Value_I_Spec;
diff --git a/gcc/ada/libgnat/s-valint.ads b/gcc/ada/libgnat/s-valint.ads
index 9e47f1bc9f0..3872d7cc7e1 100644
--- a/gcc/ada/libgnat/s-valint.ads
+++ b/gcc/ada/libgnat/s-valint.ads
@@ -54,23 +54,10 @@ package System.Val_Int with SPARK_Mode is
subtype Unsigned is Unsigned_Types.Unsigned;
package Impl is new Value_I
- (Int => Integer,
- Uns => Unsigned,
- Scan_Raw_Unsigned => Val_Uns.Scan_Raw_Unsigned,
- Uns_Option => Val_Uns.Impl.Uns_Option,
- Wrap_Option => Val_Uns.Impl.Wrap_Option,
- Is_Raw_Unsigned_Format_Ghost =>
- Val_Uns.Impl.Is_Raw_Unsigned_Format_Ghost,
- Raw_Unsigned_Overflows_Ghost =>
- Val_Uns.Impl.Raw_Unsigned_Overflows_Ghost,
- Scan_Raw_Unsigned_Ghost =>
- Val_Uns.Impl.Scan_Raw_Unsigned_Ghost,
- Raw_Unsigned_Last_Ghost =>
- Val_Uns.Impl.Raw_Unsigned_Last_Ghost,
- Only_Decimal_Ghost =>
- Val_Uns.Impl.Only_Decimal_Ghost,
- Scan_Based_Number_Ghost =>
- Val_Uns.Impl.Scan_Based_Number_Ghost);
+ (Int => Integer,
+ Uns => Unsigned,
+ Scan_Raw_Unsigned => Val_Uns.Scan_Raw_Unsigned,
+ Uns_Params => System.Val_Uns.Impl.Spec.Uns_Params);
procedure Scan_Integer
(Str : String;
diff --git a/gcc/ada/libgnat/s-vallli.ads b/gcc/ada/libgnat/s-vallli.ads
index 5bccb1a726b..85bf28203b5 100644
--- a/gcc/ada/libgnat/s-vallli.ads
+++ b/gcc/ada/libgnat/s-vallli.ads
@@ -54,24 +54,10 @@ package System.Val_LLI with SPARK_Mode is
subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
package Impl is new Value_I
- (Int => Long_Long_Integer,
- Uns => Long_Long_Unsigned,
- Scan_Raw_Unsigned =>
- Val_LLU.Scan_Raw_Long_Long_Unsigned,
- Uns_Option => Val_LLU.Impl.Uns_Option,
- Wrap_Option => Val_LLU.Impl.Wrap_Option,
- Is_Raw_Unsigned_Format_Ghost =>
- Val_LLU.Impl.Is_Raw_Unsigned_Format_Ghost,
- Raw_Unsigned_Overflows_Ghost =>
- Val_LLU.Impl.Raw_Unsigned_Overflows_Ghost,
- Scan_Raw_Unsigned_Ghost =>
- Val_LLU.Impl.Scan_Raw_Unsigned_Ghost,
- Raw_Unsigned_Last_Ghost =>
- Val_LLU.Impl.Raw_Unsigned_Last_Ghost,
- Only_Decimal_Ghost =>
- Val_LLU.Impl.Only_Decimal_Ghost,
- Scan_Based_Number_Ghost =>
- Val_LLU.Impl.Scan_Based_Number_Ghost);
+ (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);
procedure Scan_Long_Long_Integer
(Str : String;
diff --git a/gcc/ada/libgnat/s-valllli.ads b/gcc/ada/libgnat/s-valllli.ads
index 586c7379d21..e53fb0b0357 100644
--- a/gcc/ada/libgnat/s-valllli.ads
+++ b/gcc/ada/libgnat/s-valllli.ads
@@ -54,24 +54,10 @@ package System.Val_LLLI with SPARK_Mode is
subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
package Impl is new Value_I
- (Int => Long_Long_Long_Integer,
- Uns => Long_Long_Long_Unsigned,
- Scan_Raw_Unsigned =>
- Val_LLLU.Scan_Raw_Long_Long_Long_Unsigned,
- Uns_Option => Val_LLLU.Impl.Uns_Option,
- Wrap_Option => Val_LLLU.Impl.Wrap_Option,
- Is_Raw_Unsigned_Format_Ghost =>
- Val_LLLU.Impl.Is_Raw_Unsigned_Format_Ghost,
- Raw_Unsigned_Overflows_Ghost =>
- Val_LLLU.Impl.Raw_Unsigned_Overflows_Ghost,
- Scan_Raw_Unsigned_Ghost =>
- Val_LLLU.Impl.Scan_Raw_Unsigned_Ghost,
- Raw_Unsigned_Last_Ghost =>
- Val_LLLU.Impl.Raw_Unsigned_Last_Ghost,
- Only_Decimal_Ghost =>
- Val_LLLU.Impl.Only_Decimal_Ghost,
- Scan_Based_Number_Ghost =>
- Val_LLLU.Impl.Scan_Based_Number_Ghost);
+ (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);
procedure Scan_Long_Long_Long_Integer
(Str : String;
diff --git a/gcc/ada/libgnat/s-valuei.adb b/gcc/ada/libgnat/s-valuei.adb
index b453ffc38da..51764b20c9d 100644
--- a/gcc/ada/libgnat/s-valuei.adb
+++ b/gcc/ada/libgnat/s-valuei.adb
@@ -41,59 +41,6 @@ package body System.Value_I is
Assert_And_Cut => Ignore,
Subprogram_Variant => Ignore);
- -----------------------------------
- -- Prove_Scan_Only_Decimal_Ghost --
- -----------------------------------
-
- procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) is
- Non_Blank : constant Positive := First_Non_Space_Ghost
- (Str, Str'First, Str'Last);
- pragma Assert
- (if Val < 0 then Non_Blank = Str'First
- else
- Only_Space_Ghost (Str, Str'First, Str'First)
- and then Non_Blank = Str'First + 1);
- Minus : constant Boolean := Str (Non_Blank) = '-';
- Fst_Num : constant Positive :=
- (if Minus then Non_Blank + 1 else Non_Blank);
- pragma Assert (Fst_Num = Str'First + 1);
- Uval : constant Uns :=
- Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last);
-
- procedure Unique_Int_Of_Uns (Val1, Val2 : Int)
- with
- Pre => Uns_Is_Valid_Int (Minus, Uval)
- and then Is_Int_Of_Uns (Minus, Uval, Val1)
- and then Is_Int_Of_Uns (Minus, Uval, Val2),
- Post => Val1 = Val2;
- -- Local proof of the unicity of the signed representation
-
- procedure Unique_Int_Of_Uns (Val1, Val2 : Int) is null;
-
- -- Start of processing for Prove_Scan_Only_Decimal_Ghost
-
- begin
- pragma Assert (Minus = (Val < 0));
- pragma Assert (Uval = Abs_Uns_Of_Int (Val));
- pragma Assert (if Minus then Uval <= Uns (Int'Last) + 1
- else Uval <= Uns (Int'Last));
- pragma Assert (Uns_Is_Valid_Int (Minus, Uval));
- pragma Assert
- (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First
- elsif Minus then Val = -(Int (Uval))
- else Val = Int (Uval));
- pragma Assert (Is_Int_Of_Uns (Minus, Uval, Val));
- pragma Assert
- (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
- pragma Assert
- (not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Str'Last));
- pragma Assert (Only_Space_Ghost
- (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last));
- pragma Assert (Is_Integer_Ghost (Str));
- pragma Assert (Is_Value_Integer_Ghost (Str, Val));
- Unique_Int_Of_Uns (Val, Value_Integer (Str));
- end Prove_Scan_Only_Decimal_Ghost;
-
------------------
-- Scan_Integer --
------------------
@@ -104,6 +51,25 @@ package body System.Value_I is
Max : Integer;
Res : out Int)
is
+ procedure Prove_Is_Int_Of_Uns
+ (Minus : Boolean;
+ Uval : Uns;
+ Val : Int)
+ with Ghost,
+ Pre => Spec.Uns_Is_Valid_Int (Minus, Uval)
+ and then
+ (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First
+ elsif Minus then Val = -(Int (Uval))
+ else Val = Int (Uval)),
+ Post => Spec.Is_Int_Of_Uns (Minus, Uval, Val);
+ -- Unfold the definition of Is_Int_Of_Uns
+
+ procedure Prove_Is_Int_Of_Uns
+ (Minus : Boolean;
+ Uval : Uns;
+ Val : Int)
+ is null;
+
Uval : Uns;
-- Unsigned result
@@ -131,7 +97,8 @@ package body System.Value_I is
end if;
Scan_Raw_Unsigned (Str, Ptr, Max, Uval);
- pragma Assert (Uval = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max));
+ pragma Assert
+ (Uval = Uns_Params.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max));
-- Deal with overflow cases, and also with largest negative number
@@ -152,6 +119,11 @@ package body System.Value_I is
else
Res := Int (Uval);
end if;
+
+ Prove_Is_Int_Of_Uns
+ (Minus => Str (Non_Blank) = '-',
+ Uval => Uval,
+ Val => Res);
end Scan_Integer;
-------------------
@@ -167,7 +139,15 @@ package body System.Value_I is
if Str'Last = Positive'Last then
declare
subtype NT is String (1 .. Str'Length);
+ procedure Prove_Is_Integer_Ghost with
+ Ghost,
+ Pre => Str'Length < Natural'Last
+ and then not Only_Space_Ghost (Str, Str'First, Str'Last)
+ and then Spec.Is_Integer_Ghost (Spec.Slide_To_1 (Str)),
+ Post => Spec.Is_Integer_Ghost (NT (Str));
+ procedure Prove_Is_Integer_Ghost is null;
begin
+ Prove_Is_Integer_Ghost;
return Value_Integer (NT (Str));
end;
@@ -187,8 +167,6 @@ package body System.Value_I is
else Non_Blank)
with Ghost;
begin
- pragma Assert
- (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
declare
P_Acc : constant not null access Integer := P'Access;
@@ -197,12 +175,13 @@ package body System.Value_I is
end;
pragma Assert
- (P = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last));
+ (P = Uns_Params.Raw_Unsigned_Last_Ghost
+ (Str, Fst_Num, Str'Last));
Scan_Trailing_Blanks (Str, P);
pragma Assert
- (Is_Value_Integer_Ghost (Slide_If_Necessary (Str), V));
+ (Spec.Is_Value_Integer_Ghost (Spec.Slide_If_Necessary (Str), V));
return V;
end;
end if;
diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads
index 5e42773b36a..3f78db6ee43 100644
--- a/gcc/ada/libgnat/s-valuei.ads
+++ b/gcc/ada/libgnat/s-valuei.ads
@@ -39,6 +39,7 @@ pragma Assertion_Policy (Pre => Ignore,
Subprogram_Variant => Ignore);
with System.Val_Util; use System.Val_Util;
+with System.Value_I_Spec;
generic
@@ -54,71 +55,15 @@ generic
-- Additional parameters for ghost subprograms used inside contracts
- type Uns_Option is private;
- with function Wrap_Option (Value : Uns) return Uns_Option
- with Ghost;
- with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean
- with Ghost;
- with function Raw_Unsigned_Overflows_Ghost
- (Str : String;
- From, To : Integer)
- return Boolean
- with Ghost;
- with function Scan_Raw_Unsigned_Ghost
- (Str : String;
- From, To : Integer)
- return Uns
- with Ghost;
- with function Raw_Unsigned_Last_Ghost
- (Str : String;
- From, To : Integer)
- return Positive
- with Ghost;
- with function Only_Decimal_Ghost
- (Str : String;
- From, To : Integer)
- return Boolean
- with Ghost;
- with function Scan_Based_Number_Ghost
- (Str : String;
- From, To : Integer;
- Base : Uns := 10;
- Acc : Uns := 0)
- return Uns_Option
- with Ghost;
+ with package Uns_Params is new System.Val_Util.Uns_Params
+ (Uns => Uns, others => <>)
+ with Ghost;
package System.Value_I is
pragma Preelaborate;
+ use all type Uns_Params.Uns_Option;
- function Uns_Is_Valid_Int (Minus : Boolean; Uval : Uns) return Boolean is
- (if Minus then Uval <= Uns (Int'Last) + 1
- else Uval <= Uns (Int'Last))
- with Ghost,
- Post => True;
- -- Return True if Uval (or -Uval when Minus is True) is a valid number of
- -- type Int.
-
- function Is_Int_Of_Uns
- (Minus : Boolean;
- Uval : Uns;
- Val : Int)
- return Boolean
- is
- (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First
- elsif Minus then Val = -(Int (Uval))
- else Val = Int (Uval))
- with
- Ghost,
- Pre => Uns_Is_Valid_Int (Minus, Uval),
- Post => True;
- -- Return True if Uval (or -Uval when Minus is True) is equal to Val
-
- function Abs_Uns_Of_Int (Val : Int) return Uns is
- (if Val = Int'First then Uns (Int'Last) + 1
- elsif Val < 0 then Uns (-Val)
- else Uns (Val))
- with Ghost;
- -- Return the unsigned absolute value of Val
+ package Spec is new System.Value_I_Spec (Int, Uns, Uns_Params);
procedure Scan_Integer
(Str : String;
@@ -139,11 +84,13 @@ package System.Value_I is
(if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
else Non_Blank);
begin
- Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max))
- and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Max)
- and then Uns_Is_Valid_Int
+ Uns_Params.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max))
+ and then Uns_Params.Raw_Unsigned_No_Overflow_Ghost
+ (Str, Fst_Num, Max)
+ and then Spec.Uns_Is_Valid_Int
(Minus => Str (Non_Blank) = '-',
- Uval => Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max))),
+ Uval => Uns_Params.Scan_Raw_Unsigned_Ghost
+ (Str, Fst_Num, Max))),
Post =>
(declare
Non_Blank : constant Positive := First_Non_Space_Ghost
@@ -152,12 +99,13 @@ package System.Value_I is
(if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
else Non_Blank);
Uval : constant Uns :=
- Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max);
+ Uns_Params.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max);
begin
- Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-',
- Uval => Uval,
- Val => Res)
- and then Ptr.all = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Max));
+ Spec.Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-',
+ Uval => Uval,
+ Val => Res)
+ and then Ptr.all = Uns_Params.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
-- scanned extends no further than Str (Max). There are three cases for the
@@ -183,111 +131,17 @@ package System.Value_I is
-- special case of an all-blank string, and Ptr is unchanged, and hence
-- is greater than Max as required in this case.
- function Slide_To_1 (Str : String) return String
- with
- Ghost,
- Post =>
- Only_Space_Ghost (Str, Str'First, Str'Last) =
- (for all J in Str'First .. Str'Last =>
- Slide_To_1'Result (J - Str'First + 1) = ' ');
- -- Slides Str so that it starts at 1
-
- function Slide_If_Necessary (Str : String) return String is
- (if Str'Last = Positive'Last then Slide_To_1 (Str) else Str)
- with
- Ghost,
- Post =>
- Only_Space_Ghost (Str, Str'First, Str'Last) =
- Only_Space_Ghost (Slide_If_Necessary'Result,
- Slide_If_Necessary'Result'First,
- Slide_If_Necessary'Result'Last);
- -- If Str'Last = Positive'Last then slides Str so that it starts at 1
-
- function Is_Integer_Ghost (Str : String) return Boolean is
- (declare
- Non_Blank : constant Positive := First_Non_Space_Ghost
- (Str, Str'First, Str'Last);
- Fst_Num : constant Positive :=
- (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank);
- begin
- Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))
- and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Str'Last)
- and then
- Uns_Is_Valid_Int
- (Minus => Str (Non_Blank) = '-',
- Uval => Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last))
- and then Only_Space_Ghost
- (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last))
- with
- Ghost,
- Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
- and then Str'Last /= Positive'Last,
- Post => True;
- -- Ghost function that determines if Str has the correct format for a
- -- signed number, consisting in some blank characters, an optional
- -- sign, a raw unsigned number which does not overflow and then some
- -- more blank characters.
-
- function Is_Value_Integer_Ghost (Str : String; Val : Int) return Boolean is
- (declare
- Non_Blank : constant Positive := First_Non_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 :=
- Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last);
- begin
- Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-',
- Uval => Uval,
- Val => Val))
- with
- Ghost,
- Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
- and then Str'Last /= Positive'Last
- and then Is_Integer_Ghost (Str),
- Post => True;
- -- Ghost function that returns True if Val is the value corresponding to
- -- the signed number represented by Str.
-
function Value_Integer (Str : String) return Int
with
Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
and then Str'Length /= Positive'Last
- and then Is_Integer_Ghost (Slide_If_Necessary (Str)),
- Post => Is_Value_Integer_Ghost
- (Slide_If_Necessary (Str), Value_Integer'Result),
+ and then Spec.Is_Integer_Ghost (Spec.Slide_If_Necessary (Str)),
+ Post => Spec.Is_Value_Integer_Ghost
+ (Spec.Slide_If_Necessary (Str), Value_Integer'Result),
Subprogram_Variant => (Decreases => Str'First);
-- Used in computing X'Value (Str) where X is a signed integer type whose
-- base range does not exceed the base range of Integer. Str is the string
-- argument of the attribute. Constraint_Error is raised if the string is
-- malformed, or if the value is out of range.
- procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
- with
- Ghost,
- Pre => Str'Last /= Positive'Last
- and then Str'Length >= 2
- and then Str (Str'First) in ' ' | '-'
- and then (Str (Str'First) = '-') = (Val < 0)
- and then Only_Decimal_Ghost (Str, Str'First + 1, Str'Last)
- and then Scan_Based_Number_Ghost (Str, Str'First + 1, Str'Last)
- = Wrap_Option (Abs_Uns_Of_Int (Val)),
- Post => Is_Integer_Ghost (Slide_If_Necessary (Str))
- and then Value_Integer (Str) = Val;
- -- Ghost lemma used in the proof of 'Image implementation, to prove that
- -- the result of Value_Integer on a decimal string is the same as the
- -- signing the result of Scan_Based_Number_Ghost.
-
-private
-
- ----------------
- -- Slide_To_1 --
- ----------------
-
- function Slide_To_1 (Str : String) return String is
- (declare
- Res : constant String (1 .. Str'Length) := Str;
- begin
- Res);
-
end System.Value_I;
diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb
index f5a6881dbc5..8f19086508b 100644
--- a/gcc/ada/libgnat/s-valueu.adb
+++ b/gcc/ada/libgnat/s-valueu.adb
@@ -41,9 +41,12 @@ package body System.Value_U is
Assert_And_Cut => Ignore,
Subprogram_Variant => Ignore);
+ use type Spec.Uns_Option;
+ use type Spec.Split_Value_Ghost;
+
-- Local lemmas
- procedure Lemma_Digit_Is_Before_Last
+ procedure Lemma_Digit_Not_Last
(Str : String;
P : Integer;
From : Integer;
@@ -54,257 +57,47 @@ package body System.Value_U is
and then To in From .. Str'Last
and then Str (From) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
and then P in From .. To
- and then Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F',
- Post => P /= Last_Hexa_Ghost (Str (From .. To)) + 1;
- -- If the character at position P is a digit, P cannot be the position of
- -- of the first non-digit in Str.
+ and then P <= Spec.Last_Hexa_Ghost (Str (From .. To)) + 1
+ and then Spec.Is_Based_Format_Ghost (Str (From .. To)),
+ Post =>
+ (if Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+ then P <= Spec.Last_Hexa_Ghost (Str (From .. To)));
- procedure Lemma_End_Of_Scan
+ procedure Lemma_Underscore_Not_Last
(Str : String;
+ P : Integer;
From : Integer;
- To : Integer;
- Base : Uns;
- Acc : Uns)
- with Ghost,
- Pre => Str'Last /= Positive'Last and then From > To,
- Post => Scan_Based_Number_Ghost (Str, From, To, Base, Acc) =
- (False, Acc);
- -- Unfold the definition of Scan_Based_Number_Ghost on an empty string
-
- procedure Lemma_Scan_Digit
- (Str : String;
- P : Integer;
- Lst : Integer;
- Digit : Uns;
- Base : Uns;
- Old_Acc : Uns;
- Acc : Uns;
- Scan_Val : Uns_Option;
- Old_Overflow : Boolean;
- Overflow : Boolean)
- with Ghost,
- Pre => Str'Last /= Positive'Last
- and then Lst in Str'Range
- and then P in Str'First .. Lst
- and then Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
- and then Digit = Hexa_To_Unsigned_Ghost (Str (P))
- and then Only_Hexa_Ghost (Str, P, Lst)
- and then Base in 2 .. 16
- and then (if Digit < Base and then Old_Acc <= Uns'Last / Base
- then Acc = Base * Old_Acc + Digit)
- and then (if Digit >= Base
- or else Old_Acc > Uns'Last / Base
- or else (Old_Acc > (Uns'Last - Base + 1) / Base
- and then Acc < Uns'Last / Base)
- then Overflow
- else Overflow = Old_Overflow)
- and then
- (if not Old_Overflow then
- Scan_Val = Scan_Based_Number_Ghost
- (Str, P, Lst, Base, Old_Acc)),
- Post =>
- (if not Overflow then
- Scan_Val = Scan_Based_Number_Ghost
- (Str, P + 1, Lst, Base, Acc))
- and then
- (if Overflow then Old_Overflow or else Scan_Val.Overflow);
- -- Unfold the definition of Scan_Based_Number_Ghost when the string starts
- -- with a digit.
-
- procedure Lemma_Scan_Underscore
- (Str : String;
- P : Integer;
- From : Integer;
- To : Integer;
- Lst : Integer;
- Base : Uns;
- Acc : Uns;
- Scan_Val : Uns_Option;
- Overflow : Boolean;
- Ext : Boolean)
+ To : Integer)
with Ghost,
Pre => Str'Last /= Positive'Last
and then From in Str'Range
and then To in From .. Str'Last
- and then Lst <= To
- and then P in From .. Lst + 1
- and then P <= To
- and then
- (if Ext then
- Is_Based_Format_Ghost (Str (From .. To))
- and then Lst = Last_Hexa_Ghost (Str (From .. To))
- else Is_Natural_Format_Ghost (Str (From .. To))
- and then Lst = Last_Number_Ghost (Str (From .. To)))
+ and then Str (From) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+ and then P in From .. To
and then Str (P) = '_'
- and then
- (if not Overflow then
- Scan_Val = Scan_Based_Number_Ghost (Str, P, Lst, Base, Acc)),
- Post => P + 1 <= Lst
- and then
- (if Ext then Str (P + 1) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
- else Str (P + 1) in '0' .. '9')
- and then
- (if not Overflow then
- Scan_Val = Scan_Based_Number_Ghost (Str, P + 1, Lst, Base, Acc));
- -- Unfold the definition of Scan_Based_Number_Ghost when the string starts
- -- with an underscore.
+ and then P <= Spec.Last_Hexa_Ghost (Str (From .. To)) + 1
+ and then Spec.Is_Based_Format_Ghost (Str (From .. To)),
+ Post => P + 1 <= Spec.Last_Hexa_Ghost (Str (From .. To))
+ and then Str (P + 1) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
-----------------------------
-- Local lemma null bodies --
-----------------------------
- procedure Lemma_Digit_Is_Before_Last
+ procedure Lemma_Digit_Not_Last
(Str : String;
P : Integer;
From : Integer;
To : Integer)
is null;
- procedure Lemma_End_Of_Scan
- (Str : String;
- From : Integer;
- To : Integer;
- Base : Uns;
- Acc : Uns)
- is null;
-
- procedure Lemma_Scan_Underscore
- (Str : String;
- P : Integer;
- From : Integer;
- To : Integer;
- Lst : Integer;
- Base : Uns;
- Acc : Uns;
- Scan_Val : Uns_Option;
- Overflow : Boolean;
- Ext : Boolean)
+ procedure Lemma_Underscore_Not_Last
+ (Str : String;
+ P : Integer;
+ From : Integer;
+ To : Integer)
is null;
- ---------------------
- -- Last_Hexa_Ghost --
- ---------------------
-
- function Last_Hexa_Ghost (Str : String) return Positive is
- begin
- for J in Str'Range loop
- if Str (J) not in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_' then
- return J - 1;
- end if;
-
- pragma Loop_Invariant
- (for all K in Str'First .. J =>
- Str (K) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_');
- end loop;
-
- return Str'Last;
- end Last_Hexa_Ghost;
-
- ----------------------
- -- Lemma_Scan_Digit --
- ----------------------
-
- procedure Lemma_Scan_Digit
- (Str : String;
- P : Integer;
- Lst : Integer;
- Digit : Uns;
- Base : Uns;
- Old_Acc : Uns;
- Acc : Uns;
- Scan_Val : Uns_Option;
- Old_Overflow : Boolean;
- Overflow : Boolean)
- is
- pragma Unreferenced (Str, P, Lst, Scan_Val, Overflow, Old_Overflow);
- begin
- if Digit >= Base then
- null;
-
- elsif Old_Acc <= (Uns'Last - Base + 1) / Base then
- pragma Assert (not Scan_Overflows_Ghost (Digit, Base, Old_Acc));
-
- elsif Old_Acc > Uns'Last / Base then
- null;
-
- else
- pragma Assert
- ((Acc < Uns'Last / Base) =
- Scan_Overflows_Ghost (Digit, Base, Old_Acc));
- end if;
- end Lemma_Scan_Digit;
-
- ----------------------------------------
- -- Prove_Iter_Scan_Based_Number_Ghost --
- ----------------------------------------
-
- procedure Prove_Iter_Scan_Based_Number_Ghost
- (Str1, Str2 : String;
- From, To : Integer;
- Base : Uns := 10;
- Acc : Uns := 0)
- is
- begin
- if From > To then
- null;
- elsif Str1 (From) = '_' then
- Prove_Iter_Scan_Based_Number_Ghost
- (Str1, Str2, From + 1, To, Base, Acc);
- elsif Scan_Overflows_Ghost
- (Hexa_To_Unsigned_Ghost (Str1 (From)), Base, Acc)
- then
- null;
- else
- Prove_Iter_Scan_Based_Number_Ghost
- (Str1, Str2, From + 1, To, Base,
- Base * Acc + Hexa_To_Unsigned_Ghost (Str1 (From)));
- end if;
- end Prove_Iter_Scan_Based_Number_Ghost;
-
- -----------------------------------
- -- Prove_Scan_Only_Decimal_Ghost --
- -----------------------------------
-
- procedure Prove_Scan_Only_Decimal_Ghost
- (Str : String;
- Val : Uns)
- is
- Non_Blank : constant Positive := First_Non_Space_Ghost
- (Str, Str'First, Str'Last);
- pragma Assert (Non_Blank = Str'First + 1);
- Fst_Num : constant Positive :=
- (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
- pragma Assert (Fst_Num = Str'First + 1);
- Last_Num_Init : constant Integer :=
- Last_Number_Ghost (Str (Str'First + 1 .. Str'Last));
- pragma Assert (Last_Num_Init = Str'Last);
- Starts_As_Based : constant Boolean :=
- Last_Num_Init < Str'Last - 1
- and then Str (Last_Num_Init + 1) in '#' | ':'
- and then Str (Last_Num_Init + 2) in
- '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
- pragma Assert (Starts_As_Based = False);
- Last_Num_Based : constant Integer :=
- (if Starts_As_Based
- then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Str'Last))
- else Last_Num_Init);
- pragma Assert (Last_Num_Based = Str'Last);
- begin
- pragma Assert
- (Is_Opt_Exponent_Format_Ghost (Str (Str'Last + 1 .. Str'Last)));
- pragma Assert
- (Is_Natural_Format_Ghost (Str (Str'First + 1 .. Str'Last)));
- pragma Assert
- (Is_Raw_Unsigned_Format_Ghost (Str (Str'First + 1 .. Str'Last)));
- pragma Assert
- (not Raw_Unsigned_Overflows_Ghost (Str, Str'First + 1, Str'Last));
- pragma Assert (Val = Exponent_Unsigned_Ghost (Val, 0, 10).Value);
- pragma Assert
- (Val = Scan_Raw_Unsigned_Ghost (Str, Str'First + 1, Str'Last));
- pragma Assert (Is_Unsigned_Ghost (Str));
- pragma Assert (Is_Value_Unsigned_Ghost (Str, Val));
- end Prove_Scan_Only_Decimal_Ghost;
-
-----------------------
-- Scan_Raw_Unsigned --
-----------------------
@@ -341,8 +134,8 @@ package body System.Value_U is
Last_Num_Init : constant Integer :=
Last_Number_Ghost (Str (Ptr.all .. Max))
with Ghost;
- Init_Val : constant Uns_Option :=
- Scan_Based_Number_Ghost (Str, Ptr.all, Last_Num_Init)
+ Init_Val : constant Spec.Uns_Option :=
+ Spec.Scan_Based_Number_Ghost (Str, Ptr.all, Last_Num_Init)
with Ghost;
Starts_As_Based : constant Boolean :=
Last_Num_Init < Max - 1
@@ -352,7 +145,7 @@ package body System.Value_U is
with Ghost;
Last_Num_Based : constant Integer :=
(if Starts_As_Based
- then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Max))
+ then Spec.Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Max))
else Last_Num_Init)
with Ghost;
Is_Based : constant Boolean :=
@@ -360,9 +153,9 @@ package body System.Value_U is
and then Last_Num_Based < Max
and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1)
with Ghost;
- Based_Val : constant Uns_Option :=
+ Based_Val : constant Spec.Uns_Option :=
(if Starts_As_Based and then not Init_Val.Overflow
- then Scan_Based_Number_Ghost
+ then Spec.Scan_Based_Number_Ghost
(Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
else Init_Val)
with Ghost;
@@ -379,6 +172,7 @@ package body System.Value_U is
end if;
P := Ptr.all;
+ Spec.Lemma_Scan_Based_Number_Ghost_Step (Str, P, Last_Num_Init);
Uval := Character'Pos (Str (P)) - Character'Pos ('0');
P := P + 1;
@@ -392,9 +186,6 @@ package body System.Value_U is
Umax10 : constant Uns := Uns'Last / 10;
-- Numbers bigger than Umax10 overflow if multiplied by 10
- Old_Uval : Uns with Ghost;
- Old_Overflow : Boolean with Ghost;
-
begin
-- Loop through decimal digits
loop
@@ -403,7 +194,7 @@ package body System.Value_U is
(if Overflow then Init_Val.Overflow);
pragma Loop_Invariant
(if not Overflow
- then Init_Val = Scan_Based_Number_Ghost
+ then Init_Val = Spec.Scan_Based_Number_Ghost
(Str, P, Last_Num_Init, Acc => Uval));
exit when P > Max;
@@ -414,9 +205,8 @@ package body System.Value_U is
if Digit > 9 then
if Str (P) = '_' then
- Lemma_Scan_Underscore
- (Str, P, Ptr_Old, Max, Last_Num_Init, 10, Uval,
- Init_Val, Overflow, False);
+ Spec.Lemma_Scan_Based_Number_Ghost_Underscore
+ (Str, P, Last_Num_Init, Acc => Uval);
Scan_Underscore (Str, P, Ptr, Max, False);
else
exit;
@@ -425,11 +215,19 @@ package body System.Value_U is
-- Accumulate result, checking for overflow
else
- Old_Uval := Uval;
- Old_Overflow := Overflow;
+ Spec.Lemma_Scan_Based_Number_Ghost_Step
+ (Str, P, Last_Num_Init, Acc => Uval);
+ Spec.Lemma_Scan_Based_Number_Ghost_Overflow
+ (Str, P, Last_Num_Init, Acc => Uval);
if Uval <= Umax then
+ pragma Assert
+ (Spec.Hexa_To_Unsigned_Ghost (Str (P)) = Digit);
Uval := 10 * Uval + Digit;
+ pragma Assert
+ (if not Overflow
+ then Init_Val = Spec.Scan_Based_Number_Ghost
+ (Str, P + 1, Last_Num_Init, Acc => Uval));
elsif Uval > Umax10 then
Overflow := True;
@@ -440,17 +238,17 @@ package body System.Value_U is
if Uval < Umax10 then
Overflow := True;
end if;
+ pragma Assert
+ (if not Overflow
+ then Init_Val = Spec.Scan_Based_Number_Ghost
+ (Str, P + 1, Last_Num_Init, Acc => Uval));
end if;
- Lemma_Scan_Digit
- (Str, P, Last_Num_Init, Digit, 10, Old_Uval, Uval, Init_Val,
- Old_Overflow, Overflow);
-
P := P + 1;
end if;
end loop;
- pragma Assert (P = Last_Num_Init + 1);
- pragma Assert (Init_Val.Overflow = Overflow);
+ Spec.Lemma_Scan_Based_Number_Ghost_Base
+ (Str, P, Last_Num_Init, Acc => Uval);
end;
pragma Assert_And_Cut
@@ -488,18 +286,14 @@ package body System.Value_U is
UmaxB : constant Uns := Uns'Last / Base;
-- Numbers bigger than UmaxB overflow if multiplied by base
- Old_Uval : Uns with Ghost;
- Old_Overflow : Boolean with Ghost;
-
begin
pragma Assert
(if Str (P) in '0' .. '9' | 'A' .. 'F' | 'a' .. 'f'
- then Is_Based_Format_Ghost (Str (P .. Max)));
+ then Spec.Is_Based_Format_Ghost (Str (P .. Max)));
-- Loop to scan out based integer value
loop
-
-- We require a digit at this stage
if Str (P) in '0' .. '9' then
@@ -519,6 +313,8 @@ package body System.Value_U is
-- already stored in Ptr.all.
else
+ Spec.Lemma_Scan_Based_Number_Ghost_Base
+ (Str, P, Last_Num_Based, Base, Uval);
Uval := Base;
Base := 10;
pragma Assert (Ptr.all = Last_Num_Init + 1);
@@ -529,25 +325,25 @@ package body System.Value_U is
exit;
end if;
- Lemma_Digit_Is_Before_Last (Str, P, Last_Num_Init + 2, Max);
-
pragma Loop_Invariant (P in P'Loop_Entry .. Last_Num_Based);
pragma Loop_Invariant
(Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
- and then Digit = Hexa_To_Unsigned_Ghost (Str (P)));
+ and then Digit = Spec.Hexa_To_Unsigned_Ghost (Str (P)));
pragma Loop_Invariant
(if Overflow'Loop_Entry then Overflow);
pragma Loop_Invariant
(if Overflow then
- Overflow'Loop_Entry or else Based_Val.Overflow);
+ (Overflow'Loop_Entry or else Based_Val.Overflow));
pragma Loop_Invariant
(if not Overflow
- then Based_Val = Scan_Based_Number_Ghost
+ then Based_Val = Spec.Scan_Based_Number_Ghost
(Str, P, Last_Num_Based, Base, Uval));
pragma Loop_Invariant (Ptr.all = Last_Num_Init + 1);
- Old_Uval := Uval;
- Old_Overflow := Overflow;
+ Spec.Lemma_Scan_Based_Number_Ghost_Step
+ (Str, P, Last_Num_Based, Base, Uval);
+ Spec.Lemma_Scan_Based_Number_Ghost_Overflow
+ (Str, P, Last_Num_Based, Base, Uval);
-- If digit is too large, just signal overflow and continue.
-- The idea here is to keep scanning as long as the input is
@@ -560,6 +356,10 @@ package body System.Value_U is
elsif Uval <= Umax then
Uval := Base * Uval + Digit;
+ pragma Assert
+ (if not Overflow
+ then Based_Val = Spec.Scan_Based_Number_Ghost
+ (Str, P + 1, Last_Num_Based, Base, Uval));
elsif Uval > UmaxB then
Overflow := True;
@@ -570,6 +370,10 @@ package body System.Value_U is
if Uval < UmaxB then
Overflow := True;
end if;
+ pragma Assert
+ (if not Overflow
+ then Based_Val = Spec.Scan_Based_Number_Ghost
+ (Str, P + 1, Last_Num_Based, Base, Uval));
end if;
-- If at end of string with no base char, not a based number
@@ -579,10 +383,6 @@ package body System.Value_U is
P := P + 1;
- Lemma_Scan_Digit
- (Str, P - 1, Last_Num_Based, Digit, Base, Old_Uval, Uval,
- Based_Val, Old_Overflow, Overflow);
-
if P > Max then
Ptr.all := P;
Bad_Value (Str);
@@ -592,48 +392,54 @@ package body System.Value_U is
if Str (P) = Base_Char then
Ptr.all := P + 1;
+ pragma Assert (P = Last_Num_Based + 1);
pragma Assert (Ptr.all = Last_Num_Based + 2);
+ pragma Assert (Starts_As_Based);
+ pragma Assert (Last_Num_Based < Max);
+ pragma Assert (Str (Last_Num_Based + 1) = Base_Char);
+ pragma Assert (Base_Char = Str (Last_Num_Init + 1));
pragma Assert (Is_Based);
- pragma Assert
- (if not Overflow then
- Based_Val = Scan_Based_Number_Ghost
- (Str, P, Last_Num_Based, Base, Uval));
- Lemma_End_Of_Scan (Str, P, Last_Num_Based, Base, Uval);
- pragma Assert (if not Overflow then Uval = Based_Val.Value);
+ Spec.Lemma_Scan_Based_Number_Ghost_Base
+ (Str, P, Last_Num_Based, Base, Uval);
exit;
-- Deal with underscore
elsif Str (P) = '_' then
- Lemma_Scan_Underscore
- (Str, P, Last_Num_Init + 2, Max, Last_Num_Based, Base,
- Uval, Based_Val, Overflow, True);
+ Lemma_Underscore_Not_Last (Str, P, Last_Num_Init + 2, Max);
+ Spec.Lemma_Scan_Based_Number_Ghost_Underscore
+ (Str, P, Last_Num_Based, Base, Uval);
Scan_Underscore (Str, P, Ptr, Max, True);
pragma Assert
(if not Overflow
- then Based_Val = Scan_Based_Number_Ghost
+ then Based_Val = Spec.Scan_Based_Number_Ghost
(Str, P, Last_Num_Based, Base, Uval));
+ pragma Assert (Str (P) /= '_');
+ pragma Assert (Str (P) /= Base_Char);
end if;
+
+ Lemma_Digit_Not_Last (Str, P, Last_Num_Init + 2, Max);
+ pragma Assert (Str (P) /= '_');
+ pragma Assert (Str (P) /= Base_Char);
end loop;
end;
pragma Assert
(if Starts_As_Based then P = Last_Num_Based + 1
else P = Last_Num_Init + 2);
+ pragma Assert
+ (Last_Num_Init < Max - 1
+ and then Str (Last_Num_Init + 1) in '#' | ':');
pragma Assert
(Overflow =
(Init_Val.Overflow
or else Init_Val.Value not in 2 .. 16
or else (Starts_As_Based and then Based_Val.Overflow)));
+ pragma Assert
+ (Overflow /= Spec.Scan_Split_No_Overflow_Ghost (Str, Ptr_Old, Max));
end if;
pragma Assert_And_Cut
- (Overflow =
- (Init_Val.Overflow
- or else
- (Last_Num_Init < Max - 1
- and then Str (Last_Num_Init + 1) in '#' | ':'
- and then Init_Val.Value not in 2 .. 16)
- or else (Starts_As_Based and then Based_Val.Overflow))
+ (Overflow /= Spec.Scan_Split_No_Overflow_Ghost (Str, Ptr_Old, Max)
and then
(if not Overflow then
(if Is_Based then Uval = Based_Val.Value
@@ -649,10 +455,12 @@ package body System.Value_U is
Scan_Exponent (Str, Ptr, Max, Expon);
- pragma Assert (Ptr.all = Raw_Unsigned_Last_Ghost (Str, Ptr_Old, Max));
pragma Assert
- (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. Max))
- then Expon = Scan_Exponent_Ghost (Str (First_Exp .. Max)));
+ (Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Ptr_Old, Max));
+ pragma Assert
+ (if not Overflow
+ then Spec.Scan_Split_Value_Ghost (Str, Ptr_Old, Max) =
+ (Uval, Base, Expon));
if Expon /= 0 and then Uval /= 0 then
@@ -664,8 +472,8 @@ package body System.Value_U is
UmaxB : constant Uns := Uns'Last / Base;
-- Numbers bigger than UmaxB overflow if multiplied by base
- Res_Val : constant Uns_Option :=
- Exponent_Unsigned_Ghost (Uval, Expon, Base)
+ Res_Val : constant Spec.Uns_Option :=
+ Spec.Exponent_Unsigned_Ghost (Uval, Expon, Base)
with Ghost;
begin
for J in 1 .. Expon loop
@@ -674,48 +482,45 @@ package body System.Value_U is
pragma Loop_Invariant
(if Overflow
then Overflow'Loop_Entry or else Res_Val.Overflow);
+ pragma Loop_Invariant (Uval /= 0);
pragma Loop_Invariant
(if not Overflow
- then Res_Val = Exponent_Unsigned_Ghost
+ then Res_Val = Spec.Exponent_Unsigned_Ghost
(Uval, Expon - J + 1, Base));
pragma Assert
- ((Uval > UmaxB) = Scan_Overflows_Ghost (0, Base, Uval));
+ ((Uval > UmaxB) = Spec.Scan_Overflows_Ghost (0, Base, Uval));
if Uval > UmaxB then
+ Spec.Lemma_Exponent_Unsigned_Ghost_Overflow
+ (Uval, Expon - J + 1, Base);
Overflow := True;
exit;
end if;
+ Spec.Lemma_Exponent_Unsigned_Ghost_Step
+ (Uval, Expon - J + 1, Base);
+
Uval := Uval * Base;
end loop;
+ Spec.Lemma_Exponent_Unsigned_Ghost_Base (Uval, 0, Base);
+
pragma Assert
- (Overflow = (Init_Val.Overflow
- or else
- (Last_Num_Init < Max - 1
- and then Str (Last_Num_Init + 1) in '#' | ':'
- and then Init_Val.Value not in 2 .. 16)
- or else (Starts_As_Based and then Based_Val.Overflow)
- or else Res_Val.Overflow));
- pragma Assert
- (Overflow = Raw_Unsigned_Overflows_Ghost (Str, Ptr_Old, Max));
- pragma Assert
- (Exponent_Unsigned_Ghost (Uval, 0, Base) = (False, Uval));
- pragma Assert
- (if not Overflow then Uval = Res_Val.Value);
- pragma Assert
- (if not Overflow then
- Uval = Scan_Raw_Unsigned_Ghost (Str, Ptr_Old, Max));
+ (Overflow /=
+ Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Ptr_Old, Max));
+ pragma Assert (if not Overflow then Res_Val = (False, Uval));
end;
end if;
+ Spec.Lemma_Exponent_Unsigned_Ghost_Base (Uval, Expon, Base);
pragma Assert
(if Expon = 0 or else Uval = 0 then
- Exponent_Unsigned_Ghost (Uval, Expon, Base) = (False, Uval));
+ Spec.Exponent_Unsigned_Ghost (Uval, Expon, Base) = (False, Uval));
pragma Assert
- (Overflow = Raw_Unsigned_Overflows_Ghost (Str, Ptr_Old, Max));
+ (Overflow /=
+ Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Ptr_Old, Max));
pragma Assert
(if not Overflow then
- Uval = Scan_Raw_Unsigned_Ghost (Str, Ptr_Old, Max));
+ Uval = Spec.Scan_Raw_Unsigned_Ghost (Str, Ptr_Old, Max));
-- Return result, dealing with overflow
@@ -774,7 +579,15 @@ package body System.Value_U is
if Str'Last = Positive'Last then
declare
subtype NT is String (1 .. Str'Length);
+ procedure Prove_Is_Unsigned_Ghost with
+ Ghost,
+ Pre => Str'Length < Natural'Last
+ and then not Only_Space_Ghost (Str, Str'First, Str'Last)
+ and then Spec.Is_Unsigned_Ghost (Spec.Slide_To_1 (Str)),
+ Post => Spec.Is_Unsigned_Ghost (NT (Str));
+ procedure Prove_Is_Unsigned_Ghost is null;
begin
+ Prove_Is_Unsigned_Ghost;
return Value_Unsigned (NT (Str));
end;
@@ -784,7 +597,6 @@ package body System.Value_U is
declare
V : Uns;
P : aliased Integer := Str'First;
-
Non_Blank : constant Positive := First_Non_Space_Ghost
(Str, Str'First, Str'Last)
with Ghost;
@@ -792,9 +604,6 @@ package body System.Value_U is
(if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank)
with Ghost;
begin
- pragma Assert
- (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
-
declare
P_Acc : constant not null access Integer := P'Access;
begin
@@ -802,14 +611,15 @@ package body System.Value_U is
end;
pragma Assert
- (P = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last));
+ (P = Spec.Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last));
pragma Assert
- (V = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last));
+ (V = Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last));
Scan_Trailing_Blanks (Str, P);
pragma Assert
- (Is_Value_Unsigned_Ghost (Slide_If_Necessary (Str), V));
+ (Spec.Is_Value_Unsigned_Ghost
+ (Spec.Slide_If_Necessary (Str), V));
return V;
end;
end if;
diff --git a/gcc/ada/libgnat/s-valueu.ads b/gcc/ada/libgnat/s-valueu.ads
index 1508b6ecb1c..466b96a6fa6 100644
--- a/gcc/ada/libgnat/s-valueu.ads
+++ b/gcc/ada/libgnat/s-valueu.ads
@@ -44,6 +44,7 @@ pragma Assertion_Policy (Pre => Ignore,
Ghost => Ignore,
Subprogram_Variant => Ignore);
+with System.Value_U_Spec;
with System.Val_Util; use System.Val_Util;
generic
@@ -53,317 +54,7 @@ generic
package System.Value_U is
pragma Preelaborate;
- type Uns_Option (Overflow : Boolean := False) is record
- case Overflow is
- when True =>
- null;
- when False =>
- Value : Uns := 0;
- end case;
- end record;
-
- function Wrap_Option (Value : Uns) return Uns_Option is
- (Overflow => False, Value => Value)
- with
- Ghost;
-
- function Only_Decimal_Ghost
- (Str : String;
- From, To : Integer)
- return Boolean
- is
- (for all J in From .. To => Str (J) in '0' .. '9')
- with
- Ghost,
- Pre => From > To or else (From >= Str'First and then To <= Str'Last);
- -- Ghost function that returns True if S has only decimal characters
- -- from index From to index To.
-
- function Only_Hexa_Ghost (Str : String; From, To : Integer) return Boolean
- is
- (for all J in From .. To =>
- Str (J) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_')
- with
- Ghost,
- Pre => From > To or else (From >= Str'First and then To <= Str'Last);
- -- Ghost function that returns True if S has only hexadecimal characters
- -- from index From to index To.
-
- function Last_Hexa_Ghost (Str : String) return Positive
- with
- Ghost,
- Pre => Str /= ""
- and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F',
- Post => Last_Hexa_Ghost'Result in Str'Range
- and then (if Last_Hexa_Ghost'Result < Str'Last then
- Str (Last_Hexa_Ghost'Result + 1) not in
- '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_')
- and then Only_Hexa_Ghost (Str, Str'First, Last_Hexa_Ghost'Result);
- -- Ghost function that returns the index of the last character in S that
- -- is either an hexadecimal digit or an underscore, which necessarily
- -- exists given the precondition on Str.
-
- function Is_Based_Format_Ghost (Str : String) return Boolean
- is
- (Str /= ""
- and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
- and then
- (declare
- L : constant Positive := Last_Hexa_Ghost (Str);
- begin
- Str (L) /= '_'
- 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
- -- based number, consisting in a sequence of hexadecimal digits possibly
- -- separated by single underscores. It may be followed by other characters.
-
- function Hexa_To_Unsigned_Ghost (X : Character) return Uns is
- (case X is
- when '0' .. '9' => Character'Pos (X) - Character'Pos ('0'),
- when 'a' .. 'f' => Character'Pos (X) - Character'Pos ('a') + 10,
- when 'A' .. 'F' => Character'Pos (X) - Character'Pos ('A') + 10,
- when others => raise Program_Error)
- with
- Ghost,
- Pre => X in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
- -- Ghost function that computes the value corresponding to an hexadecimal
- -- digit.
-
- function Scan_Overflows_Ghost
- (Digit : Uns;
- Base : Uns;
- Acc : Uns) return Boolean
- is
- (Digit >= Base
- or else Acc > Uns'Last / Base
- or else Uns'Last - Digit < Base * Acc)
- with Ghost;
- -- Ghost function which returns True if Digit + Base * Acc overflows or
- -- Digit is greater than Base, as this is used by the algorithm for the
- -- test of overflow.
-
- function Scan_Based_Number_Ghost
- (Str : String;
- From, To : Integer;
- Base : Uns := 10;
- Acc : Uns := 0) return Uns_Option
- with
- Ghost,
- Subprogram_Variant => (Increases => From),
- Pre => Str'Last /= Positive'Last
- and then
- (From > To or else (From >= Str'First and then To <= Str'Last))
- and then Only_Hexa_Ghost (Str, From, To);
- -- Ghost function that recursively computes the based number in Str,
- -- assuming Acc has been scanned already and scanning continues at index
- -- From.
-
- function Exponent_Unsigned_Ghost
- (Value : Uns;
- Exp : Natural;
- Base : Uns := 10) return Uns_Option
- with
- Ghost,
- Subprogram_Variant => (Decreases => Exp);
- -- Ghost function that recursively computes Value * Base ** Exp
-
- function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean is
- (Is_Natural_Format_Ghost (Str)
- and then
- (declare
- Last_Num_Init : constant Integer := Last_Number_Ghost (Str);
- Starts_As_Based : constant Boolean :=
- Last_Num_Init < Str'Last - 1
- and then Str (Last_Num_Init + 1) in '#' | ':'
- and then Str (Last_Num_Init + 2) in
- '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
- Last_Num_Based : constant Integer :=
- (if Starts_As_Based
- then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Str'Last))
- else Last_Num_Init);
- Is_Based : constant Boolean :=
- Starts_As_Based
- and then Last_Num_Based < Str'Last
- and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
- First_Exp : constant Integer :=
- (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
- begin
- (if Starts_As_Based then
- Is_Based_Format_Ghost (Str (Last_Num_Init + 2 .. Str'Last))
- and then Last_Num_Based < Str'Last)
- and then Is_Opt_Exponent_Format_Ghost
- (Str (First_Exp .. Str'Last))))
- with
- Ghost,
- Pre => Str'Last /= Positive'Last,
- Post => True;
- -- Ghost function that determines if Str has the correct format for an
- -- unsigned number without a sign character.
- -- It is a natural number in base 10, optionally followed by a based
- -- number surrounded by delimiters # or :, optionally followed by an
- -- exponent part.
-
- function Raw_Unsigned_Overflows_Ghost
- (Str : String;
- From, To : Integer)
- return Boolean
- is
- (declare
- Last_Num_Init : constant Integer :=
- Last_Number_Ghost (Str (From .. To));
- Init_Val : constant Uns_Option :=
- Scan_Based_Number_Ghost (Str, From, Last_Num_Init);
- Starts_As_Based : constant Boolean :=
- Last_Num_Init < To - 1
- and then Str (Last_Num_Init + 1) in '#' | ':'
- and then Str (Last_Num_Init + 2) in
- '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
- Last_Num_Based : constant Integer :=
- (if Starts_As_Based
- then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
- else Last_Num_Init);
- Is_Based : constant Boolean :=
- Starts_As_Based
- and then Last_Num_Based < To
- and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
- Based_Val : constant Uns_Option :=
- (if Starts_As_Based and then not Init_Val.Overflow
- then Scan_Based_Number_Ghost
- (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
- else Init_Val);
- First_Exp : constant Integer :=
- (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
- Expon : constant Natural :=
- (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
- then Scan_Exponent_Ghost (Str (First_Exp .. To))
- else 0);
- begin
- Init_Val.Overflow
- or else
- (Last_Num_Init < To - 1
- and then Str (Last_Num_Init + 1) in '#' | ':'
- and then Init_Val.Value not in 2 .. 16)
- or else
- (Starts_As_Based
- and then Based_Val.Overflow)
- or else
- (Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
- and then
- (declare
- Base : constant Uns :=
- (if Is_Based then Init_Val.Value else 10);
- Value : constant Uns :=
- (if Is_Based then Based_Val.Value else Init_Val.Value);
- begin
- Exponent_Unsigned_Ghost
- (Value, Expon, Base).Overflow)))
- with
- Ghost,
- Pre => Str'Last /= Positive'Last
- and then From in Str'Range
- and then To in From .. Str'Last
- and then Str (From) in '0' .. '9',
- Post => True;
- -- Ghost function that determines if the computation of the unsigned number
- -- represented by Str will overflow. The computation overflows if either:
- -- * The computation of the decimal part overflows,
- -- * The decimal part is followed by a valid delimiter for a based
- -- part, and the number corresponding to the base is not a valid base,
- -- * The computation of the based part overflows, or
- -- * There is an exponent and the computation of the exponentiation
- -- overflows.
-
- function Scan_Raw_Unsigned_Ghost
- (Str : String;
- From, To : Integer)
- return Uns
- is
- (declare
- Last_Num_Init : constant Integer :=
- Last_Number_Ghost (Str (From .. To));
- Init_Val : constant Uns_Option :=
- Scan_Based_Number_Ghost (Str, From, Last_Num_Init);
- Starts_As_Based : constant Boolean :=
- Last_Num_Init < To - 1
- and then Str (Last_Num_Init + 1) in '#' | ':'
- and then Str (Last_Num_Init + 2) in
- '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
- Last_Num_Based : constant Integer :=
- (if Starts_As_Based
- then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
- else Last_Num_Init);
- Is_Based : constant Boolean :=
- Starts_As_Based
- and then Last_Num_Based < To
- and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
- Based_Val : constant Uns_Option :=
- (if Starts_As_Based and then not Init_Val.Overflow
- then Scan_Based_Number_Ghost
- (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
- else Init_Val);
- First_Exp : constant Integer :=
- (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
- Expon : constant Natural :=
- (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
- then Scan_Exponent_Ghost (Str (First_Exp .. To))
- else 0);
- Base : constant Uns :=
- (if Is_Based then Init_Val.Value else 10);
- Value : constant Uns :=
- (if Is_Based then Based_Val.Value else Init_Val.Value);
- begin
- Exponent_Unsigned_Ghost (Value, Expon, Base).Value)
- with
- Ghost,
- Pre => Str'Last /= Positive'Last
- and then From in Str'Range
- and then To in From .. Str'Last
- and then Str (From) in '0' .. '9'
- and then not Raw_Unsigned_Overflows_Ghost (Str, From, To),
- Post => True;
- -- Ghost function that scans an unsigned number without a sign character
-
- function Raw_Unsigned_Last_Ghost
- (Str : String;
- From, To : Integer)
- return Positive
- is
- (declare
- Last_Num_Init : constant Integer :=
- Last_Number_Ghost (Str (From .. To));
- Starts_As_Based : constant Boolean :=
- Last_Num_Init < To - 1
- and then Str (Last_Num_Init + 1) in '#' | ':'
- and then Str (Last_Num_Init + 2) in
- '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
- Last_Num_Based : constant Integer :=
- (if Starts_As_Based
- then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
- else Last_Num_Init);
- Is_Based : constant Boolean :=
- Starts_As_Based
- and then Last_Num_Based < To
- and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
- First_Exp : constant Integer :=
- (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
- begin
- (if not Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
- then First_Exp
- elsif Str (First_Exp + 1) in '-' | '+' then
- Last_Number_Ghost (Str (First_Exp + 2 .. To)) + 1
- else Last_Number_Ghost (Str (First_Exp + 1 .. To)) + 1))
- with
- Ghost,
- Pre => Str'Last /= Positive'Last
- and then From in Str'Range
- and then To in From .. Str'Last
- and then Str (From) in '0' .. '9',
- Post => Raw_Unsigned_Last_Ghost'Result in From .. To + 1;
- -- Ghost function that returns the position of the cursor once an unsigned
- -- number has been seen.
+ package Spec is new System.Value_U_Spec (Uns);
procedure Scan_Raw_Unsigned
(Str : String;
@@ -373,10 +64,10 @@ package System.Value_U is
with Pre => Str'Last /= Positive'Last
and then Ptr.all in Str'Range
and then Max in Ptr.all .. Str'Last
- and then Is_Raw_Unsigned_Format_Ghost (Str (Ptr.all .. Max)),
- Post => not Raw_Unsigned_Overflows_Ghost (Str, Ptr.all'Old, Max)
- and Res = Scan_Raw_Unsigned_Ghost (Str, Ptr.all'Old, Max)
- and Ptr.all = Raw_Unsigned_Last_Ghost (Str, Ptr.all'Old, Max);
+ and then Spec.Is_Raw_Unsigned_Format_Ghost (Str (Ptr.all .. Max)),
+ Post => Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Ptr.all'Old, Max)
+ and Res = Spec.Scan_Raw_Unsigned_Ghost (Str, Ptr.all'Old, Max)
+ and Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Ptr.all'Old, Max);
-- This function scans the string starting at Str (Ptr.all) for a valid
-- integer according to the syntax described in (RM 3.5(43)). The substring
@@ -464,7 +155,7 @@ package System.Value_U is
Fst_Num : constant Positive :=
(if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
begin
- Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max))),
+ Spec.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max))),
Post =>
(declare
Non_Blank : constant Positive :=
@@ -472,9 +163,9 @@ package System.Value_U is
Fst_Num : constant Positive :=
(if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
begin
- not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Max)
- and then Res = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max)
- and then Ptr.all = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Max));
+ Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Max)
+ and then Res = Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max)
+ and then Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Fst_Num, Max));
-- Same as Scan_Raw_Unsigned, except scans optional leading
-- blanks, and an optional leading plus sign.
@@ -482,157 +173,18 @@ package System.Value_U is
-- Note: if a minus sign is present, Constraint_Error will be raised.
-- Note: trailing blanks are not scanned.
- function Slide_To_1 (Str : String) return String
- with Ghost,
- Post =>
- Only_Space_Ghost (Str, Str'First, Str'Last) =
- (for all J in Str'First .. Str'Last =>
- Slide_To_1'Result (J - Str'First + 1) = ' ');
- -- Slides Str so that it starts at 1
-
- function Slide_If_Necessary (Str : String) return String is
- (if Str'Last = Positive'Last then Slide_To_1 (Str) else Str)
- with Ghost,
- Post =>
- Only_Space_Ghost (Str, Str'First, Str'Last) =
- Only_Space_Ghost (Slide_If_Necessary'Result,
- Slide_If_Necessary'Result'First,
- Slide_If_Necessary'Result'Last);
- -- If Str'Last = Positive'Last then slides Str so that it starts at 1
-
- function Is_Unsigned_Ghost (Str : String) return Boolean is
- (declare
- Non_Blank : constant Positive := First_Non_Space_Ghost
- (Str, Str'First, Str'Last);
- Fst_Num : constant Positive :=
- (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
- begin
- Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))
- and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Str'Last)
- and then Only_Space_Ghost
- (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last))
- with Ghost,
- Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
- and then Str'Last /= Positive'Last,
- Post => True;
- -- Ghost function that determines if Str has the correct format for an
- -- unsigned number, consisting in some blank characters, an optional
- -- + sign, a raw unsigned number which does not overflow and then some
- -- more blank characters.
-
- function Is_Value_Unsigned_Ghost (Str : String; Val : Uns) return Boolean is
- (declare
- Non_Blank : constant Positive := First_Non_Space_Ghost
- (Str, Str'First, Str'Last);
- Fst_Num : constant Positive :=
- (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
- begin
- Val = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last))
- with Ghost,
- Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
- and then Str'Last /= Positive'Last
- and then Is_Unsigned_Ghost (Str),
- Post => True;
- -- Ghost function that returns True if Val is the value corresponding to
- -- the unsigned number represented by Str.
-
function Value_Unsigned
(Str : String) return Uns
- with Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
- and then Str'Length /= Positive'Last
- and then Is_Unsigned_Ghost (Slide_If_Necessary (Str)),
+ with Pre => Str'Length /= Positive'Last
+ and then not Only_Space_Ghost (Str, Str'First, Str'Last)
+ and then Spec.Is_Unsigned_Ghost (Spec.Slide_If_Necessary (Str)),
Post =>
- Is_Value_Unsigned_Ghost
- (Slide_If_Necessary (Str), Value_Unsigned'Result),
+ Spec.Is_Value_Unsigned_Ghost
+ (Spec.Slide_If_Necessary (Str), Value_Unsigned'Result),
Subprogram_Variant => (Decreases => Str'First);
-- Used in computing X'Value (Str) where X is a modular integer type whose
-- modulus does not exceed the range of System.Unsigned_Types.Unsigned. Str
-- is the string argument of the attribute. Constraint_Error is raised if
-- the string is malformed, or if the value is out of range.
- procedure Prove_Iter_Scan_Based_Number_Ghost
- (Str1, Str2 : String;
- From, To : Integer;
- Base : Uns := 10;
- Acc : Uns := 0)
- with
- Ghost,
- Subprogram_Variant => (Increases => From),
- Pre => Str1'Last /= Positive'Last
- and then Str2'Last /= Positive'Last
- and then
- (From > To or else (From >= Str1'First and then To <= Str1'Last))
- and then
- (From > To or else (From >= Str2'First and then To <= Str2'Last))
- and then Only_Hexa_Ghost (Str1, From, To)
- and then (for all J in From .. To => Str1 (J) = Str2 (J)),
- Post =>
- Scan_Based_Number_Ghost (Str1, From, To, Base, Acc)
- = Scan_Based_Number_Ghost (Str2, From, To, Base, Acc);
- -- Ghost lemma used in the proof of 'Image implementation, to prove the
- -- preservation of Scan_Based_Number_Ghost across an update in the string
- -- in lower indexes.
-
- procedure Prove_Scan_Only_Decimal_Ghost
- (Str : String;
- Val : Uns)
- with
- Ghost,
- Pre => Str'Last /= Positive'Last
- and then Str'Length >= 2
- and then Str (Str'First) = ' '
- and then Only_Decimal_Ghost (Str, Str'First + 1, Str'Last)
- and then Scan_Based_Number_Ghost (Str, Str'First + 1, Str'Last)
- = Wrap_Option (Val),
- Post => Is_Unsigned_Ghost (Slide_If_Necessary (Str))
- and then Value_Unsigned (Str) = Val;
- -- Ghost lemma used in the proof of 'Image implementation, to prove that
- -- the result of Value_Unsigned on a decimal string is the same as the
- -- result of Scan_Based_Number_Ghost.
-
-private
-
- -----------------------------
- -- Exponent_Unsigned_Ghost --
- -----------------------------
-
- function Exponent_Unsigned_Ghost
- (Value : Uns;
- Exp : Natural;
- Base : Uns := 10) return Uns_Option
- is
- (if Exp = 0 or Value = 0 then (Overflow => False, Value => Value)
- elsif Scan_Overflows_Ghost (0, Base, Value) then (Overflow => True)
- else Exponent_Unsigned_Ghost (Value * Base, Exp - 1, Base));
-
- -----------------------------
- -- Scan_Based_Number_Ghost --
- -----------------------------
-
- function Scan_Based_Number_Ghost
- (Str : String;
- From, To : Integer;
- Base : Uns := 10;
- Acc : Uns := 0) return Uns_Option
- is
- (if From > To then (Overflow => False, Value => Acc)
- elsif Str (From) = '_'
- then Scan_Based_Number_Ghost (Str, From + 1, To, Base, Acc)
- elsif Scan_Overflows_Ghost
- (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc)
- then (Overflow => True)
- else Scan_Based_Number_Ghost
- (Str, From + 1, To, Base,
- Base * Acc + Hexa_To_Unsigned_Ghost (Str (From))));
-
- ----------------
- -- Slide_To_1 --
- ----------------
-
- function Slide_To_1 (Str : String) return String is
- (declare
- Res : constant String (1 .. Str'Length) := Str;
- begin
- Res);
-
end System.Value_U;
diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads
index 2b89b1246f2..7c2da17aa53 100644
--- a/gcc/ada/libgnat/s-valuti.ads
+++ b/gcc/ada/libgnat/s-valuti.ads
@@ -374,48 +374,274 @@ is
-- no check for this case, the caller must ensure this condition is met.
pragma Warnings (GNATprove, On, """Ptr"" is not modified");
- -- Bundle Int type with other types, constants and subprograms used in
+ -- 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 Int type.
+ -- multiple times as generic formal for a given Uns type.
generic
- type Int is range <>;
type Uns is mod <>;
- type Uns_Option is private;
+ 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;
- Unsigned_Width_Ghost : Natural;
+ 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 Wrap_Option (Value : Uns) return Uns_Option
- with Ghost;
- with function Only_Decimal_Ghost
+ with function P_Scan_Raw_Unsigned_Ghost
(Str : String;
From, To : Integer)
- return Boolean
- with Ghost;
- with function Hexa_To_Unsigned_Ghost (X : Character) return Uns
- with Ghost;
- with function Scan_Based_Number_Ghost
+ return Uns
+ with Ghost;
+ with procedure P_Lemma_Scan_Based_Number_Ghost_Base
(Str : String;
From, To : Integer;
Base : Uns := 10;
Acc : Uns := 0)
- return Uns_Option
- with Ghost;
- with function Is_Integer_Ghost (Str : String) return Boolean
- with Ghost;
- with procedure Prove_Iter_Scan_Based_Number_Ghost
+ 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 procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
+ with function P_Is_Integer_Ghost (Str : String) return Boolean
with Ghost;
- with function Abs_Uns_Of_Int (Val : Int) return Uns
+ with function P_Is_Value_Integer_Ghost
+ (Str : String;
+ Val : Int) return Boolean
with Ghost;
- with function Value_Integer (Str : String) return Int
+ 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
diff --git a/gcc/ada/libgnat/s-vauspe.adb b/gcc/ada/libgnat/s-vauspe.adb
new file mode 100644
index 00000000000..1a870b9b997
--- /dev/null
+++ b/gcc/ada/libgnat/s-vauspe.adb
@@ -0,0 +1,198 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT COMPILER COMPONENTS --
+-- --
+-- S Y S T E M . V A L U E _ U _ S P E C --
+-- --
+-- B o d y --
+-- --
+-- Copyright (C) 2022-2022, 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. --
+-- --
+------------------------------------------------------------------------------
+
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore,
+ Subprogram_Variant => Ignore);
+
+package body System.Value_U_Spec with SPARK_Mode is
+
+ -----------------------------
+ -- Exponent_Unsigned_Ghost --
+ -----------------------------
+
+ function Exponent_Unsigned_Ghost
+ (Value : Uns;
+ Exp : Natural;
+ Base : Uns := 10) return Uns_Option
+ is
+ (if Exp = 0 or Value = 0 then (Overflow => False, Value => Value)
+ elsif Scan_Overflows_Ghost (0, Base, Value) then (Overflow => True)
+ else Exponent_Unsigned_Ghost (Value * Base, Exp - 1, Base));
+
+ ---------------------
+ -- Last_Hexa_Ghost --
+ ---------------------
+
+ function Last_Hexa_Ghost (Str : String) return Positive is
+ begin
+ for J in Str'Range loop
+ if Str (J) not in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_' then
+ return J - 1;
+ end if;
+
+ pragma Loop_Invariant
+ (for all K in Str'First .. J =>
+ Str (K) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_');
+ end loop;
+
+ return Str'Last;
+ end Last_Hexa_Ghost;
+
+ -----------------------------
+ -- Lemmas with null bodies --
+ -----------------------------
+
+ procedure Lemma_Scan_Based_Number_Ghost_Base
+ (Str : String;
+ From, To : Integer;
+ Base : Uns := 10;
+ Acc : Uns := 0)
+ is null;
+
+ procedure Lemma_Scan_Based_Number_Ghost_Underscore
+ (Str : String;
+ From, To : Integer;
+ Base : Uns := 10;
+ Acc : Uns := 0)
+ is null;
+
+ procedure Lemma_Scan_Based_Number_Ghost_Overflow
+ (Str : String;
+ From, To : Integer;
+ Base : Uns := 10;
+ Acc : Uns := 0)
+ is null;
+
+ procedure Lemma_Scan_Based_Number_Ghost_Step
+ (Str : String;
+ From, To : Integer;
+ Base : Uns := 10;
+ Acc : Uns := 0)
+ is null;
+
+ procedure Lemma_Exponent_Unsigned_Ghost_Base
+ (Value : Uns;
+ Exp : Natural;
+ Base : Uns := 10)
+ is null;
+
+ procedure Lemma_Exponent_Unsigned_Ghost_Overflow
+ (Value : Uns;
+ Exp : Natural;
+ Base : Uns := 10)
+ is null;
+
+ procedure Lemma_Exponent_Unsigned_Ghost_Step
+ (Value : Uns;
+ Exp : Natural;
+ Base : Uns := 10)
+ is null;
+
+ --------------------------------------
+ -- Prove_Scan_Based_Number_Ghost_Eq --
+ --------------------------------------
+
+ procedure Prove_Scan_Based_Number_Ghost_Eq
+ (Str1, Str2 : String;
+ From, To : Integer;
+ Base : Uns := 10;
+ Acc : Uns := 0)
+ is
+ begin
+ if From > To then
+ null;
+ elsif Str1 (From) = '_' then
+ Prove_Scan_Based_Number_Ghost_Eq
+ (Str1, Str2, From + 1, To, Base, Acc);
+ elsif Scan_Overflows_Ghost
+ (Hexa_To_Unsigned_Ghost (Str1 (From)), Base, Acc)
+ then
+ null;
+ else
+ Prove_Scan_Based_Number_Ghost_Eq
+ (Str1, Str2, From + 1, To, Base,
+ Base * Acc + Hexa_To_Unsigned_Ghost (Str1 (From)));
+ end if;
+ end Prove_Scan_Based_Number_Ghost_Eq;
+
+ -----------------------------------
+ -- Prove_Scan_Only_Decimal_Ghost --
+ -----------------------------------
+
+ procedure Prove_Scan_Only_Decimal_Ghost
+ (Str : String;
+ Val : Uns)
+ is
+ pragma Assert (Str (Str'First + 1) /= ' ');
+ Non_Blank : constant Positive := First_Non_Space_Ghost
+ (Str, Str'First, Str'Last);
+ pragma Assert (Non_Blank = Str'First + 1);
+ Fst_Num : constant Positive :=
+ (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
+ pragma Assert (Fst_Num = Str'First + 1);
+ begin
+ pragma Assert
+ (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
+ pragma Assert
+ (Scan_Split_No_Overflow_Ghost (Str, Str'First + 1, Str'Last));
+ pragma Assert
+ ((Val, 10, 0) = Scan_Split_Value_Ghost (Str, Str'First + 1, Str'Last));
+ pragma Assert
+ (Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last));
+ pragma Assert (Val = Exponent_Unsigned_Ghost (Val, 0, 10).Value);
+ pragma Assert (Is_Unsigned_Ghost (Str));
+ pragma Assert (Is_Value_Unsigned_Ghost (Str, Val));
+ end Prove_Scan_Only_Decimal_Ghost;
+
+ -----------------------------
+ -- Scan_Based_Number_Ghost --
+ -----------------------------
+
+ function Scan_Based_Number_Ghost
+ (Str : String;
+ From, To : Integer;
+ Base : Uns := 10;
+ Acc : Uns := 0) return Uns_Option
+ is
+ (if From > To then (Overflow => False, Value => Acc)
+ elsif Str (From) = '_'
+ then Scan_Based_Number_Ghost (Str, From + 1, To, Base, Acc)
+ elsif Scan_Overflows_Ghost
+ (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc)
+ then (Overflow => True)
+ else Scan_Based_Number_Ghost
+ (Str, From + 1, To, Base,
+ Base * Acc + Hexa_To_Unsigned_Ghost (Str (From))));
+
+end System.Value_U_Spec;
diff --git a/gcc/ada/libgnat/s-vauspe.ads b/gcc/ada/libgnat/s-vauspe.ads
new file mode 100644
index 00000000000..0d5c19e8c53
--- /dev/null
+++ b/gcc/ada/libgnat/s-vauspe.ads
@@ -0,0 +1,639 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT COMPILER COMPONENTS --
+-- --
+-- S Y S T E M . V A L U E _ U _ S P E C --
+-- --
+-- S p e c --
+-- --
+-- Copyright (C) 2022-2022, 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 the specification entities using for the formal
+-- verification of the routines for scanning modular Unsigned values.
+
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore. Postconditions and
+-- contract cases should not be executed at runtime as well, in order not to
+-- slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore,
+ Subprogram_Variant => Ignore);
+
+with System.Val_Util; use System.Val_Util;
+
+generic
+
+ type Uns is mod <>;
+
+package System.Value_U_Spec with
+ Ghost,
+ SPARK_Mode,
+ Annotate => (GNATprove, Always_Return)
+is
+ pragma Preelaborate;
+
+ type Uns_Option (Overflow : Boolean := False) is record
+ case Overflow is
+ when True =>
+ null;
+ when False =>
+ Value : Uns := 0;
+ end case;
+ end record;
+
+ function Wrap_Option (Value : Uns) return Uns_Option is
+ (Overflow => False, Value => Value);
+
+ function Only_Decimal_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 decimal characters
+ -- from index From to index To.
+
+ function Only_Hexa_Ghost (Str : String; From, To : Integer) return Boolean
+ is
+ (for all J in From .. To =>
+ Str (J) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_')
+ with
+ Pre => From > To or else (From >= Str'First and then To <= Str'Last);
+ -- Ghost function that returns True if S has only hexadecimal characters
+ -- from index From to index To.
+
+ function Last_Hexa_Ghost (Str : String) return Positive
+ with
+ Pre => Str /= ""
+ and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F',
+ Post => Last_Hexa_Ghost'Result in Str'Range
+ and then (if Last_Hexa_Ghost'Result < Str'Last then
+ Str (Last_Hexa_Ghost'Result + 1) not in
+ '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_')
+ and then Only_Hexa_Ghost (Str, Str'First, Last_Hexa_Ghost'Result);
+ -- Ghost function that returns the index of the last character in S that
+ -- is either an hexadecimal digit or an underscore, which necessarily
+ -- exists given the precondition on Str.
+
+ function Is_Based_Format_Ghost (Str : String) return Boolean
+ is
+ (Str /= ""
+ and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+ and then
+ (declare
+ L : constant Positive := Last_Hexa_Ghost (Str);
+ begin
+ Str (L) /= '_'
+ 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
+ -- based number, consisting in a sequence of hexadecimal digits possibly
+ -- separated by single underscores. It may be followed by other characters.
+
+ function Hexa_To_Unsigned_Ghost (X : Character) return Uns is
+ (case X is
+ when '0' .. '9' => Character'Pos (X) - Character'Pos ('0'),
+ when 'a' .. 'f' => Character'Pos (X) - Character'Pos ('a') + 10,
+ when 'A' .. 'F' => Character'Pos (X) - Character'Pos ('A') + 10,
+ when others => raise Program_Error)
+ with
+ Pre => X in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+ -- Ghost function that computes the value corresponding to an hexadecimal
+ -- digit.
+
+ function Scan_Overflows_Ghost
+ (Digit : Uns;
+ Base : Uns;
+ Acc : Uns) return Boolean
+ is
+ (Digit >= Base
+ or else Acc > Uns'Last / Base
+ or else Uns'Last - Digit < Base * Acc);
+ -- Ghost function which returns True if Digit + Base * Acc overflows or
+ -- Digit is greater than Base, as this is used by the algorithm for the
+ -- test of overflow.
+
+ function Scan_Based_Number_Ghost
+ (Str : String;
+ From, To : Integer;
+ Base : Uns := 10;
+ Acc : Uns := 0) return Uns_Option
+ with
+ Subprogram_Variant => (Increases => From),
+ Pre => Str'Last /= Positive'Last
+ and then
+ (From > To or else (From >= Str'First and then To <= Str'Last))
+ and then Only_Hexa_Ghost (Str, From, To);
+ -- Ghost function that recursively computes the based number in Str,
+ -- assuming Acc has been scanned already and scanning continues at index
+ -- From.
+
+ -- Lemmas unfolding the recursive definition of Scan_Based_Number_Ghost
+
+ procedure Lemma_Scan_Based_Number_Ghost_Base
+ (Str : String;
+ From, To : Integer;
+ Base : Uns := 10;
+ Acc : Uns := 0)
+ with
+ Global => null,
+ Pre => Str'Last /= Positive'Last
+ and then
+ (From > To or else (From >= Str'First and then To <= Str'Last))
+ and then Only_Hexa_Ghost (Str, From, To),
+ Post =>
+ (if From > To
+ then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) =
+ (Overflow => False, Value => Acc));
+ -- Base case: Scan_Based_Number_Ghost returns Acc if From is bigger than To
+
+ procedure Lemma_Scan_Based_Number_Ghost_Underscore
+ (Str : String;
+ From, To : Integer;
+ Base : Uns := 10;
+ Acc : Uns := 0)
+ with
+ Global => null,
+ Pre => Str'Last /= Positive'Last
+ and then
+ (From > To or else (From >= Str'First and then To <= Str'Last))
+ and then Only_Hexa_Ghost (Str, From, To),
+ Post =>
+ (if From <= To and then Str (From) = '_'
+ then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) =
+ Scan_Based_Number_Ghost (Str, From + 1, To, Base, Acc));
+ -- Underscore case: underscores are ignored while scanning
+
+ procedure Lemma_Scan_Based_Number_Ghost_Overflow
+ (Str : String;
+ From, To : Integer;
+ Base : Uns := 10;
+ Acc : Uns := 0)
+ with
+ Global => null,
+ Pre => Str'Last /= Positive'Last
+ and then
+ (From > To or else (From >= Str'First and then To <= Str'Last))
+ and then Only_Hexa_Ghost (Str, From, To),
+ Post =>
+ (if From <= To
+ and then Str (From) /= '_'
+ and then Scan_Overflows_Ghost
+ (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc)
+ then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) =
+ (Overflow => True));
+ -- Overflow case: scanning a digit which causes an overflow
+
+ procedure Lemma_Scan_Based_Number_Ghost_Step
+ (Str : String;
+ From, To : Integer;
+ Base : Uns := 10;
+ Acc : Uns := 0)
+ with
+ Global => null,
+ Pre => Str'Last /= Positive'Last
+ and then
+ (From > To or else (From >= Str'First and then To <= Str'Last))
+ and then Only_Hexa_Ghost (Str, From, To),
+ Post =>
+ (if From <= To
+ and then Str (From) /= '_'
+ and then not Scan_Overflows_Ghost
+ (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc)
+ then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) =
+ Scan_Based_Number_Ghost
+ (Str, From + 1, To, Base,
+ Base * Acc + Hexa_To_Unsigned_Ghost (Str (From))));
+ -- Normal case: scanning a digit without overflows
+
+ function Exponent_Unsigned_Ghost
+ (Value : Uns;
+ Exp : Natural;
+ Base : Uns := 10) return Uns_Option
+ with
+ Subprogram_Variant => (Decreases => Exp);
+ -- Ghost function that recursively computes Value * Base ** Exp
+
+ -- Lemmas unfolding the recursive definition of Exponent_Unsigned_Ghost
+
+ procedure Lemma_Exponent_Unsigned_Ghost_Base
+ (Value : Uns;
+ Exp : Natural;
+ Base : Uns := 10)
+ with
+ Post =>
+ (if Exp = 0 or Value = 0
+ then Exponent_Unsigned_Ghost (Value, Exp, Base) =
+ (Overflow => False, Value => Value));
+ -- Base case: Exponent_Unsigned_Ghost returns 0 if Value or Exp is 0
+
+ procedure Lemma_Exponent_Unsigned_Ghost_Overflow
+ (Value : Uns;
+ Exp : Natural;
+ Base : Uns := 10)
+ with
+ Post =>
+ (if Exp /= 0
+ and then Value /= 0
+ and then Scan_Overflows_Ghost (0, Base, Value)
+ then Exponent_Unsigned_Ghost (Value, Exp, Base) = (Overflow => True));
+ -- Overflow case: the next multiplication overflows
+
+ procedure Lemma_Exponent_Unsigned_Ghost_Step
+ (Value : Uns;
+ Exp : Natural;
+ Base : Uns := 10)
+ with
+ Post =>
+ (if Exp /= 0
+ and then Value /= 0
+ and then not Scan_Overflows_Ghost (0, Base, Value)
+ then Exponent_Unsigned_Ghost (Value, Exp, Base) =
+ Exponent_Unsigned_Ghost (Value * Base, Exp - 1, Base));
+ -- Normal case: exponentiation without overflows
+
+ function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean is
+ (Is_Natural_Format_Ghost (Str)
+ and then
+ (declare
+ Last_Num_Init : constant Integer := Last_Number_Ghost (Str);
+ Starts_As_Based : constant Boolean :=
+ Last_Num_Init < Str'Last - 1
+ and then Str (Last_Num_Init + 1) in '#' | ':'
+ and then Str (Last_Num_Init + 2) in
+ '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+ Last_Num_Based : constant Integer :=
+ (if Starts_As_Based
+ then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Str'Last))
+ else Last_Num_Init);
+ Is_Based : constant Boolean :=
+ Starts_As_Based
+ and then Last_Num_Based < Str'Last
+ and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
+ First_Exp : constant Integer :=
+ (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
+ begin
+ (if Starts_As_Based then
+ Is_Based_Format_Ghost (Str (Last_Num_Init + 2 .. Str'Last))
+ and then Last_Num_Based < Str'Last)
+ and then Is_Opt_Exponent_Format_Ghost
+ (Str (First_Exp .. Str'Last))))
+ with
+ Pre => Str'Last /= Positive'Last;
+ -- Ghost function that determines if Str has the correct format for an
+ -- unsigned number without a sign character.
+ -- It is a natural number in base 10, optionally followed by a based
+ -- number surrounded by delimiters # or :, optionally followed by an
+ -- exponent part.
+
+ type Split_Value_Ghost is record
+ Value : Uns;
+ Base : Uns;
+ Expon : Natural;
+ end record;
+
+ function Scan_Split_No_Overflow_Ghost
+ (Str : String;
+ From, To : Integer)
+ return Boolean
+ is
+ (declare
+ Last_Num_Init : constant Integer :=
+ Last_Number_Ghost (Str (From .. To));
+ Init_Val : constant Uns_Option :=
+ Scan_Based_Number_Ghost (Str, From, Last_Num_Init);
+ Starts_As_Based : constant Boolean :=
+ Last_Num_Init < To - 1
+ and then Str (Last_Num_Init + 1) in '#' | ':'
+ and then Str (Last_Num_Init + 2) in
+ '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+ Last_Num_Based : constant Integer :=
+ (if Starts_As_Based
+ then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
+ else Last_Num_Init);
+ Based_Val : constant Uns_Option :=
+ (if Starts_As_Based and then not Init_Val.Overflow
+ then Scan_Based_Number_Ghost
+ (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
+ else Init_Val);
+ begin
+ not Init_Val.Overflow
+ and then
+ (Last_Num_Init >= To - 1
+ or else Str (Last_Num_Init + 1) not in '#' | ':'
+ or else Init_Val.Value in 2 .. 16)
+ and then
+ (not Starts_As_Based
+ or else not Based_Val.Overflow))
+ with
+ Pre => Str'Last /= Positive'Last
+ and then From in Str'Range
+ and then To in From .. Str'Last
+ and then Str (From) in '0' .. '9';
+ -- Ghost function that determines if an overflow might occur while scanning
+ -- the representation of an unsigned number. The computation overflows if
+ -- either:
+ -- * The computation of the decimal part overflows,
+ -- * The decimal part is followed by a valid delimiter for a based
+ -- part, and the number corresponding to the base is not a valid base,
+ -- or
+ -- * The computation of the based part overflows.
+
+ pragma Warnings (Off, "constant * is not referenced");
+ function Scan_Split_Value_Ghost
+ (Str : String;
+ From, To : Integer)
+ return Split_Value_Ghost
+ is
+ (declare
+ Last_Num_Init : constant Integer :=
+ Last_Number_Ghost (Str (From .. To));
+ Init_Val : constant Uns_Option :=
+ Scan_Based_Number_Ghost (Str, From, Last_Num_Init);
+ Starts_As_Based : constant Boolean :=
+ Last_Num_Init < To - 1
+ and then Str (Last_Num_Init + 1) in '#' | ':'
+ and then Str (Last_Num_Init + 2) in
+ '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+ Last_Num_Based : constant Integer :=
+ (if Starts_As_Based
+ then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
+ else Last_Num_Init);
+ Is_Based : constant Boolean :=
+ Starts_As_Based
+ and then Last_Num_Based < To
+ and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
+ Based_Val : constant Uns_Option :=
+ (if Starts_As_Based and then not Init_Val.Overflow
+ then Scan_Based_Number_Ghost
+ (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
+ else Init_Val);
+ First_Exp : constant Integer :=
+ (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
+ Expon : constant Natural :=
+ (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
+ then Scan_Exponent_Ghost (Str (First_Exp .. To))
+ else 0);
+ Base : constant Uns :=
+ (if Is_Based then Init_Val.Value else 10);
+ Value : constant Uns :=
+ (if Is_Based then Based_Val.Value else Init_Val.Value);
+ begin
+ (Value => Value, Base => Base, Expon => Expon))
+ with
+ Pre => Str'Last /= Positive'Last
+ and then From in Str'Range
+ and then To in From .. Str'Last
+ and then Str (From) in '0' .. '9'
+ and then Scan_Split_No_Overflow_Ghost (Str, From, To);
+ -- Ghost function that scans an unsigned number without a sign character
+ -- and return a record containing the values scanned for its value, its
+ -- base, and its exponent.
+ pragma Warnings (On, "constant * is not referenced");
+
+ function Raw_Unsigned_No_Overflow_Ghost
+ (Str : String;
+ From, To : Integer)
+ return Boolean
+ is
+ (Scan_Split_No_Overflow_Ghost (Str, From, To)
+ and then
+ (declare
+ Val : constant Split_Value_Ghost := Scan_Split_Value_Ghost
+ (Str, From, To);
+ begin
+ not Exponent_Unsigned_Ghost
+ (Val.Value, Val.Expon, Val.Base).Overflow))
+ with
+ Pre => Str'Last /= Positive'Last
+ and then From in Str'Range
+ and then To in From .. Str'Last
+ and then Str (From) in '0' .. '9';
+ -- Ghost function that determines if the computation of the unsigned number
+ -- represented by Str will overflow. The computation overflows if either:
+ -- * The scan of the string overflows, or
+ -- * The computation of the exponentiation overflows.
+
+ function Scan_Raw_Unsigned_Ghost
+ (Str : String;
+ From, To : Integer)
+ return Uns
+ is
+ (declare
+ Val : constant Split_Value_Ghost := Scan_Split_Value_Ghost
+ (Str, From, To);
+ begin
+ Exponent_Unsigned_Ghost (Val.Value, Val.Expon, Val.Base).Value)
+ with
+ Pre => Str'Last /= Positive'Last
+ and then From in Str'Range
+ and then To in From .. Str'Last
+ and then Str (From) in '0' .. '9'
+ and then Raw_Unsigned_No_Overflow_Ghost (Str, From, To);
+ -- Ghost function that scans an unsigned number without a sign character
+
+ function Raw_Unsigned_Last_Ghost
+ (Str : String;
+ From, To : Integer)
+ return Positive
+ is
+ (declare
+ Last_Num_Init : constant Integer :=
+ Last_Number_Ghost (Str (From .. To));
+ Starts_As_Based : constant Boolean :=
+ Last_Num_Init < To - 1
+ and then Str (Last_Num_Init + 1) in '#' | ':'
+ and then Str (Last_Num_Init + 2) in
+ '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+ Last_Num_Based : constant Integer :=
+ (if Starts_As_Based
+ then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
+ else Last_Num_Init);
+ Is_Based : constant Boolean :=
+ Starts_As_Based
+ and then Last_Num_Based < To
+ and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
+ First_Exp : constant Integer :=
+ (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
+ begin
+ (if not Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
+ then First_Exp
+ elsif Str (First_Exp + 1) in '-' | '+' then
+ Last_Number_Ghost (Str (First_Exp + 2 .. To)) + 1
+ else Last_Number_Ghost (Str (First_Exp + 1 .. To)) + 1))
+ with
+ Pre => Str'Last /= Positive'Last
+ and then From in Str'Range
+ and then To in From .. Str'Last
+ and then Str (From) in '0' .. '9';
+ -- Ghost function that returns the position of the cursor once an unsigned
+ -- number has been seen.
+
+ function Slide_To_1 (Str : String) return String
+ with
+ Post =>
+ Only_Space_Ghost (Str, Str'First, Str'Last) =
+ (for all J in Str'First .. Str'Last =>
+ Slide_To_1'Result (J - Str'First + 1) = ' ');
+ -- Slides Str so that it starts at 1
+
+ function Slide_If_Necessary (Str : String) return String is
+ (if Str'Last = Positive'Last then Slide_To_1 (Str) else Str);
+ -- If Str'Last = Positive'Last then slides Str so that it starts at 1
+
+ function Is_Unsigned_Ghost (Str : String) return Boolean is
+ (declare
+ Non_Blank : constant Positive := First_Non_Space_Ghost
+ (Str, Str'First, Str'Last);
+ Fst_Num : constant Positive :=
+ (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
+ begin
+ Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))
+ and then Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last)
+ and then Only_Space_Ghost
+ (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last))
+ with
+ Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+ and then Str'Last /= Positive'Last;
+ -- Ghost function that determines if Str has the correct format for an
+ -- unsigned number, consisting in some blank characters, an optional
+ -- + sign, a raw unsigned number which does not overflow and then some
+ -- more blank characters.
+
+ function Is_Value_Unsigned_Ghost (Str : String; Val : Uns) return Boolean is
+ (declare
+ Non_Blank : constant Positive := First_Non_Space_Ghost
+ (Str, Str'First, Str'Last);
+ Fst_Num : constant Positive :=
+ (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
+ begin
+ Val = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last))
+ with
+ Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+ and then Str'Last /= Positive'Last
+ and then Is_Unsigned_Ghost (Str);
+ -- Ghost function that returns True if Val is the value corresponding to
+ -- the unsigned number represented by Str.
+
+ procedure Prove_Scan_Based_Number_Ghost_Eq
+ (Str1, Str2 : String;
+ From, To : Integer;
+ Base : Uns := 10;
+ Acc : Uns := 0)
+ with
+ Subprogram_Variant => (Increases => From),
+ Pre => Str1'Last /= Positive'Last
+ and then Str2'Last /= Positive'Last
+ and then
+ (From > To or else (From >= Str1'First and then To <= Str1'Last))
+ and then
+ (From > To or else (From >= Str2'First and then To <= Str2'Last))
+ and then Only_Hexa_Ghost (Str1, From, To)
+ and then (for all J in From .. To => Str1 (J) = Str2 (J)),
+ Post =>
+ Scan_Based_Number_Ghost (Str1, From, To, Base, Acc)
+ = Scan_Based_Number_Ghost (Str2, From, To, Base, Acc);
+ -- Scan_Based_Number_Ghost returns the same value on two slices which are
+ -- equal.
+
+ procedure Prove_Scan_Only_Decimal_Ghost
+ (Str : String;
+ Val : Uns)
+ with
+ Pre => Str'Last /= Positive'Last
+ and then Str'Length >= 2
+ and then Str (Str'First) = ' '
+ and then Only_Decimal_Ghost (Str, Str'First + 1, Str'Last)
+ and then Scan_Based_Number_Ghost (Str, Str'First + 1, Str'Last)
+ = Wrap_Option (Val),
+ Post => Is_Unsigned_Ghost (Slide_If_Necessary (Str))
+ and then
+ Is_Value_Unsigned_Ghost (Slide_If_Necessary (Str), Val);
+ -- Ghost lemma used in the proof of 'Image implementation, to prove that
+ -- the result of Value_Unsigned on a decimal string is the same as the
+ -- result of Scan_Based_Number_Ghost.
+
+ -- 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 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
+
+ ----------------
+ -- Slide_To_1 --
+ ----------------
+
+ function Slide_To_1 (Str : String) return String is
+ (declare
+ Res : constant String (1 .. Str'Length) := Str;
+ begin
+ Res);
+
+end System.Value_U_Spec;
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-09-02 7:52 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-09-02 7:52 [gcc r13-2363] [Ada] Fix proof of runtime unit System.Value* and System.Image* 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).