public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r13-352] [Ada] Proof of 'Image support for signed integers
@ 2022-05-12 12:40 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2022-05-12 12:40 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:91d68769419b64ef9843c4c1eac5261217693b1e
commit r13-352-g91d68769419b64ef9843c4c1eac5261217693b1e
Author: Yannick Moy <moy@adacore.com>
Date: Fri Feb 4 15:20:20 2022 +0100
[Ada] Proof of 'Image support for signed integers
Prove System.Image_I, similarly to the proof done for System.Image_U.
The contracts make the connection between the result of Image_Integer,
the available space computed with System.Width_U and the result of
'Value as computed by Value_Integer.
I/O units that now depend on non-pure units are also marked not Pure
anymore.
gcc/ada/
* libgnat/s-imagef.adb: Adapt to new signature of Image_I, by
providing ghost imported subprograms. For now, no contract is
used on these subprograms, as System.Image_F is not proved.
* libgnat/s-imagef.ads: Add modular type Uns as formal
parameter, to use in defining Int_Params for instantiating
Image_I.
* libgnat/s-imagei.adb: Add contracts and ghost code.
* libgnat/s-imagei.ads: Replace Int formal parameter by package
Int_Params, which bundles type Int and Uns with ghost
subprograms. Add contracts.
* libgnat/s-imfi128.ads: Adapt to new formal of Image_F.
* libgnat/s-imfi32.ads: Adapt to new formal of Image_F.
* libgnat/s-imfi64.ads: Adapt to new formal of Image_F.
* libgnat/s-imgint.ads: Adapt to new formals of Image_I.
* libgnat/s-imglli.ads: Adapt to new formals of Image_I.
* libgnat/s-imgllli.ads: Adapt to new formals of Image_I.
* libgnat/s-valint.ads: Adapt to new formals of Value_I.
* libgnat/s-vallli.ads: Adapt to new formals of Value_I.
* libgnat/s-valllli.ads: Adapt to new formals of Value_I.
* libgnat/s-valuei.adb (Prove_Scan_Only_Decimal_Ghost): New
ghost lemma.
* libgnat/s-valuei.ads: New formal parameters to prove the new
lemma.
* libgnat/s-valuti.ads (Int_Params): Define a generic package to
be used as a trait-like formal parameter in Image_I and other
generics that need to instantiate Image_I.
* libgnat/s-widthu.ads (Big_10): Qualify the 10 literal.
Diff:
---
gcc/ada/libgnat/s-imagef.adb | 80 ++++++++-
gcc/ada/libgnat/s-imagef.ads | 1 +
gcc/ada/libgnat/s-imagei.adb | 365 +++++++++++++++++++++++++++++++++++++++++-
gcc/ada/libgnat/s-imagei.ads | 60 ++++++-
gcc/ada/libgnat/s-imfi128.ads | 3 +-
gcc/ada/libgnat/s-imfi32.ads | 3 +-
gcc/ada/libgnat/s-imfi64.ads | 3 +-
gcc/ada/libgnat/s-imgint.ads | 45 +++++-
gcc/ada/libgnat/s-imglli.ads | 45 +++++-
gcc/ada/libgnat/s-imgllli.ads | 46 +++++-
gcc/ada/libgnat/s-valint.ads | 8 +-
gcc/ada/libgnat/s-vallli.ads | 8 +-
gcc/ada/libgnat/s-valllli.ads | 8 +-
gcc/ada/libgnat/s-valuei.adb | 53 ++++++
gcc/ada/libgnat/s-valuei.ads | 53 ++++--
gcc/ada/libgnat/s-valuti.ads | 35 ++++
gcc/ada/libgnat/s-widthu.ads | 2 +-
17 files changed, 786 insertions(+), 32 deletions(-)
diff --git a/gcc/ada/libgnat/s-imagef.adb b/gcc/ada/libgnat/s-imagef.adb
index 14e9d066fc0..2166ece6be9 100644
--- a/gcc/ada/libgnat/s-imagef.adb
+++ b/gcc/ada/libgnat/s-imagef.adb
@@ -31,9 +31,24 @@
with System.Image_I;
with System.Img_Util; use System.Img_Util;
+with System.Val_Util;
package body System.Image_F is
+ -- Contracts, ghost code, loop invariants and assertions in this unit are
+ -- meant for analysis only, not for run-time checking, as it would be too
+ -- costly otherwise. This is enforced by setting the assertion policy to
+ -- Ignore.
+
+ pragma Assertion_Policy (Assert => Ignore,
+ Assert_And_Cut => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore,
+ Loop_Invariant => Ignore,
+ Pre => Ignore,
+ Post => Ignore,
+ Subprogram_Variant => Ignore);
+
Maxdigs : constant Natural := Int'Width - 2;
-- Maximum number of decimal digits that can be represented in an Int.
-- The "-2" accounts for the sign and one extra digit, since we need the
@@ -54,7 +69,70 @@ 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.
- package Image_I is new System.Image_I (Int);
+ -- 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);
procedure Set_Image_Integer
(V : Int;
diff --git a/gcc/ada/libgnat/s-imagef.ads b/gcc/ada/libgnat/s-imagef.ads
index c16d2c58d41..13ea22fae9f 100644
--- a/gcc/ada/libgnat/s-imagef.ads
+++ b/gcc/ada/libgnat/s-imagef.ads
@@ -36,6 +36,7 @@
generic
type Int is range <>;
+ type Uns is mod <>;
with procedure Scaled_Divide
(X, Y, Z : Int;
diff --git a/gcc/ada/libgnat/s-imagei.adb b/gcc/ada/libgnat/s-imagei.adb
index e7199af63e9..f340d139e26 100644
--- a/gcc/ada/libgnat/s-imagei.adb
+++ b/gcc/ada/libgnat/s-imagei.adb
@@ -29,18 +29,140 @@
-- --
------------------------------------------------------------------------------
+with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+
package body System.Image_I is
+ -- Ghost code, loop invariants and assertions in this unit are meant for
+ -- analysis only, not for run-time checking, as it would be too costly
+ -- otherwise. This is enforced by setting the assertion policy to Ignore.
+
+ pragma Assertion_Policy (Ghost => Ignore,
+ Loop_Invariant => Ignore,
+ Assert => Ignore,
+ Assert_And_Cut => Ignore,
+ Pre => Ignore,
+ 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
+ (if T = Int'First then Uns (Int'Last) + 1 else Uns (-T));
+
procedure Set_Digits
(T : Non_Positive;
S : in out String;
- P : in out Natural);
+ P : in out Natural)
+ with
+ Pre => P < Integer'Last
+ and then S'Last < Integer'Last
+ and then S'First <= P + 1
+ and then S'First <= S'Last
+ and then P <= S'Last - Unsigned_Width_Ghost + 1,
+ Post => S (S'First .. P'Old) = S'Old (S'First .. P'Old)
+ and then P in P'Old + 1 .. S'Last
+ and then Only_Decimal_Ghost (S, From => P'Old + 1, To => P)
+ and then Scan_Based_Number_Ghost (S, From => P'Old + 1, To => P)
+ = Wrap_Option (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.
+ package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns);
+
+ function Big (Arg : Uns) return Big_Integer renames
+ Unsigned_Conversion.To_Big_Integer;
+
+ function From_Big (Arg : Big_Integer) return Uns renames
+ Unsigned_Conversion.From_Big_Integer;
+
+ Big_10 : constant Big_Integer := Big (10) with Ghost;
+
+ ------------------
+ -- Local Lemmas --
+ ------------------
+
+ procedure Lemma_Non_Zero (X : Uns)
+ with
+ Ghost,
+ Pre => X /= 0,
+ Post => Big (X) /= 0;
+
+ procedure Lemma_Div_Commutation (X, Y : Uns)
+ with
+ Ghost,
+ Pre => Y /= 0,
+ Post => Big (X) / Big (Y) = Big (X / Y);
+
+ procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive)
+ with
+ Ghost,
+ Post => X / Y / Z = X / (Y * Z);
+
+ ---------------------------
+ -- Lemma_Div_Commutation --
+ ---------------------------
+
+ procedure Lemma_Non_Zero (X : Uns) is null;
+ procedure Lemma_Div_Commutation (X, Y : Uns) is null;
+
+ ---------------------
+ -- Lemma_Div_Twice --
+ ---------------------
+
+ procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) is
+ XY : constant Big_Natural := X / Y;
+ YZ : constant Big_Natural := Y * Z;
+ XYZ : constant Big_Natural := X / Y / Z;
+ R : constant Big_Natural := (XY rem Z) * Y + (X rem Y);
+ begin
+ pragma Assert (X = XY * Y + (X rem Y));
+ pragma Assert (XY = XY / Z * Z + (XY rem Z));
+ pragma Assert (X = XYZ * YZ + R);
+ pragma Assert ((XY rem Z) * Y <= (Z - 1) * Y);
+ pragma Assert (R <= YZ - 1);
+ pragma Assert (X / YZ = (XYZ * YZ + R) / YZ);
+ pragma Assert (X / YZ = XYZ + R / YZ);
+ end Lemma_Div_Twice;
+
-------------------
-- Image_Integer --
-------------------
@@ -52,6 +174,39 @@ package body System.Image_I is
is
pragma Assert (S'First = 1);
+ procedure Prove_Value_Integer
+ with
+ Ghost,
+ Pre => S'First = 1
+ and then S'Last < Integer'Last
+ 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;
+ -- Ghost lemma to prove the value of Value_Integer from the value of
+ -- Scan_Based_Number_Ghost and the sign on a decimal string.
+
+ -------------------------
+ -- Prove_Value_Integer --
+ -------------------------
+
+ procedure Prove_Value_Integer 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);
+ end Prove_Value_Integer;
+
+ -- Start of processing for Image_Integer
+
begin
if V >= 0 then
S (1) := ' ';
@@ -63,7 +218,16 @@ package body System.Image_I is
pragma Assert (P < S'Last - 1);
end if;
- Set_Image_Integer (V, S, P);
+ declare
+ P_Prev : constant Integer := P with Ghost;
+ Offset : constant Positive := (if V >= 0 then 1 else 2) with Ghost;
+ begin
+ Set_Image_Integer (V, S, P);
+
+ pragma Assert (P_Prev + Offset = 2);
+ end;
+
+ Prove_Value_Integer;
end Image_Integer;
----------------
@@ -77,6 +241,106 @@ package body System.Image_I is
is
Nb_Digits : Natural := 0;
Value : Non_Positive := T;
+
+ -- Local ghost variables
+
+ Pow : Big_Positive := 1 with Ghost;
+ 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)
+ 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';
+ -- Ghost lemma to prove the value of a character corresponding to the
+ -- next figure.
+
+ 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);
+ -- 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_Uns_Of_Non_Positive_Value
+ with
+ Ghost,
+ Pre => Uns_Value = Uns_Of_Non_Positive (Value),
+ Post => Uns_Value / 10 = Uns_Of_Non_Positive (Value / 10)
+ and then Uns_Value rem 10 = Uns_Of_Non_Positive (Value rem 10);
+ -- 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_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 --
+ ---------------------
+
+ procedure Prove_Iter_Scan
+ (Str1, Str2 : String;
+ From, To : Integer;
+ Base : Uns := 10;
+ Acc : Uns := 0)
+ is
+ begin
+ Prove_Iter_Scan_Based_Number_Ghost (Str1, Str2, From, To, Base, Acc);
+ end Prove_Iter_Scan;
+
+ -- Start of processing for Set_Digits
+
begin
pragma Assert (P >= S'First - 1 and P < S'Last);
-- No check is done since, as documented in the Set_Image_Integer
@@ -86,19 +350,116 @@ package body System.Image_I is
-- First we compute the number of characters needed for representing
-- the number.
loop
+ Lemma_Div_Commutation (Uns_Of_Non_Positive (Value), 10);
+ Lemma_Div_Twice (Big (Uns_Of_Non_Positive (T)),
+ Big_10 ** Nb_Digits, Big_10);
+ Prove_Uns_Of_Non_Positive_Value;
+
Value := Value / 10;
Nb_Digits := Nb_Digits + 1;
+
+ Uns_Value := Uns_Value / 10;
+ Pow := Pow * 10;
+
+ pragma Loop_Invariant (Uns_Value = Uns_Of_Non_Positive (Value));
+ pragma Loop_Invariant (Nb_Digits in 1 .. Unsigned_Width_Ghost - 1);
+ pragma Loop_Invariant (Pow = Big_10 ** Nb_Digits);
+ pragma Loop_Invariant (Big (Uns_Value) = Big (Uns_T) / Pow);
+ pragma Loop_Variant (Increases => Value);
+
exit when Value = 0;
+
+ Lemma_Non_Zero (Uns_Value);
+ pragma Assert (Pow <= Big (Uns'Last));
end loop;
Value := T;
+ Uns_Value := Uns_Of_Non_Positive (T);
+ Pow := 1;
+
+ pragma Assert (Uns_Value = From_Big (Big (Uns_T) / Big_10 ** 0));
-- We now populate digits from the end of the string to the beginning
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_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)));
+
+ Prev_Value := Uns_Value;
+ Prev_S := S;
+ Pow := Pow * 10;
+ Uns_Value := Uns_Value / 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 (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');
+
+ 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));
+
+ 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
+ (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
+ (Str => S,
+ From => P + J,
+ To => P + Nb_Digits,
+ Base => 10,
+ Acc => Uns_Value)
+ = 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
+ (Str => S,
+ From => P + 1,
+ To => P + Nb_Digits,
+ Base => 10,
+ Acc => Uns_Value)
+ = 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 7d2434b7c45..10116d123ed 100644
--- a/gcc/ada/libgnat/s-imagei.ads
+++ b/gcc/ada/libgnat/s-imagei.ads
@@ -33,17 +33,45 @@
-- signed integer types, and also for conversion operations required in
-- Text_IO.Integer_IO for such types.
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore. Postconditions and
+-- contract cases should not be executed at runtime as well, in order not to
+-- slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore,
+ Subprogram_Variant => Ignore);
+
+with System.Val_Util;
+
generic
- type Int is range <>;
+ with package Int_Params is new System.Val_Util.Int_Params (<>);
package System.Image_I is
- pragma Pure;
+
+ subtype Int is Int_Params.Int;
+ use type Int_Params.Int;
+
+ 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;
procedure Image_Integer
(V : Int;
S : in out String;
- P : out Natural);
+ P : out Natural)
+ with
+ Pre => S'First = 1
+ and then S'Last < Integer'Last
+ and then S'Last >= Int_Params.Unsigned_Width_Ghost,
+ Post => P in S'Range
+ and then Int_Params.Value_Integer (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.
@@ -51,7 +79,31 @@ package System.Image_I is
procedure Set_Image_Integer
(V : Int;
S : in out String;
- P : in out Natural);
+ P : in out Natural)
+ with
+ Pre => P < Integer'Last
+ and then S'Last < Integer'Last
+ and then S'First <= P + 1
+ and then S'First <= S'Last
+ and then
+ (if V >= 0 then
+ P <= S'Last - Int_Params.Unsigned_Width_Ghost + 1
+ else
+ P <= S'Last - Int_Params.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);
+ begin
+ Minus = (V < 0)
+ and then P in P'Old + Offset .. S'Last
+ and then Int_Params.Only_Decimal_Ghost
+ (S, From => P'Old + Offset, To => P)
+ and then Int_Params.Scan_Based_Number_Ghost
+ (S, From => P'Old + Offset, To => P)
+ = Int_Params.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-imfi128.ads b/gcc/ada/libgnat/s-imfi128.ads
index 4614455a4e9..7f64b83e9a8 100644
--- a/gcc/ada/libgnat/s-imfi128.ads
+++ b/gcc/ada/libgnat/s-imfi128.ads
@@ -39,8 +39,9 @@ with System.Image_F;
package System.Img_Fixed_128 is
subtype Int128 is Interfaces.Integer_128;
+ subtype Uns128 is Interfaces.Unsigned_128;
- package Impl is new Image_F (Int128, Arith_128.Scaled_Divide128);
+ package Impl is new Image_F (Int128, Uns128, Arith_128.Scaled_Divide128);
procedure Image_Fixed128
(V : Int128;
diff --git a/gcc/ada/libgnat/s-imfi32.ads b/gcc/ada/libgnat/s-imfi32.ads
index 492cc928120..e5c6ff8cbc8 100644
--- a/gcc/ada/libgnat/s-imfi32.ads
+++ b/gcc/ada/libgnat/s-imfi32.ads
@@ -39,8 +39,9 @@ with System.Image_F;
package System.Img_Fixed_32 is
subtype Int32 is Interfaces.Integer_32;
+ subtype Uns32 is Interfaces.Unsigned_32;
- package Impl is new Image_F (Int32, Arith_32.Scaled_Divide32);
+ package Impl is new Image_F (Int32, Uns32, Arith_32.Scaled_Divide32);
procedure Image_Fixed32
(V : Int32;
diff --git a/gcc/ada/libgnat/s-imfi64.ads b/gcc/ada/libgnat/s-imfi64.ads
index d51634c9414..91f4daf54eb 100644
--- a/gcc/ada/libgnat/s-imfi64.ads
+++ b/gcc/ada/libgnat/s-imfi64.ads
@@ -39,8 +39,9 @@ with System.Image_F;
package System.Img_Fixed_64 is
subtype Int64 is Interfaces.Integer_64;
+ subtype Uns64 is Interfaces.Unsigned_64;
- package Impl is new Image_F (Int64, Arith_64.Scaled_Divide64);
+ package Impl is new Image_F (Int64, Uns64, Arith_64.Scaled_Divide64);
procedure Image_Fixed64
(V : Int64;
diff --git a/gcc/ada/libgnat/s-imgint.ads b/gcc/ada/libgnat/s-imgint.ads
index 7b1fe22f3e6..fd5bea31c2a 100644
--- a/gcc/ada/libgnat/s-imgint.ads
+++ b/gcc/ada/libgnat/s-imgint.ads
@@ -33,12 +33,51 @@
-- signed integer types up to Integer, and also for conversion operations
-- required in Text_IO.Integer_IO for such types.
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore. Postconditions and
+-- contract cases should not be executed at runtime as well, in order not to
+-- slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore,
+ Subprogram_Variant => Ignore);
+
with System.Image_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
+ with SPARK_Mode
+is
+ subtype Unsigned is Unsigned_Types.Unsigned;
-package System.Img_Int is
- pragma Pure;
+ package Int_Params is new Val_Util.Int_Params
+ (Int => Integer,
+ Uns => Unsigned,
+ Uns_Option => Val_Uns.Impl.Uns_Option,
+ Unsigned_Width_Ghost =>
+ Wid_Uns.Width_Unsigned (0, Unsigned'Last),
+ Only_Decimal_Ghost => Val_Uns.Impl.Only_Decimal_Ghost,
+ Hexa_To_Unsigned_Ghost =>
+ Val_Uns.Impl.Hexa_To_Unsigned_Ghost,
+ Wrap_Option => Val_Uns.Impl.Wrap_Option,
+ Scan_Based_Number_Ghost =>
+ Val_Uns.Impl.Scan_Based_Number_Ghost,
+ 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 (Integer);
+ package Impl is new Image_I (Int_Params);
procedure Image_Integer
(V : Integer;
diff --git a/gcc/ada/libgnat/s-imglli.ads b/gcc/ada/libgnat/s-imglli.ads
index fc773ae28d2..20f108c8e45 100644
--- a/gcc/ada/libgnat/s-imglli.ads
+++ b/gcc/ada/libgnat/s-imglli.ads
@@ -33,12 +33,51 @@
-- signed integer types larger than Integer, and also for conversion
-- operations required in Text_IO.Integer_IO for such types.
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore. Postconditions and
+-- contract cases should not be executed at runtime as well, in order not to
+-- slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore,
+ Subprogram_Variant => Ignore);
+
with System.Image_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
+ with SPARK_Mode
+is
+ subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
-package System.Img_LLI is
- pragma Pure;
+ 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 (Long_Long_Integer);
+ package Impl is new Image_I (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 a5a10525924..989c296d759 100644
--- a/gcc/ada/libgnat/s-imgllli.ads
+++ b/gcc/ada/libgnat/s-imgllli.ads
@@ -33,12 +33,52 @@
-- signed integer types larger than Long_Long_Integer, and also for conversion
-- operations required in Text_IO.Integer_IO for such types.
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore. Postconditions and
+-- contract cases should not be executed at runtime as well, in order not to
+-- slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore,
+ Subprogram_Variant => Ignore);
+
with System.Image_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
+ with SPARK_Mode
+is
+ subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
-package System.Img_LLLI is
- pragma Pure;
+ 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 =>
+ 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 (Long_Long_Long_Integer);
+ package Impl is new Image_I (Int_Params);
procedure Image_Long_Long_Long_Integer
(V : Long_Long_Long_Integer;
diff --git a/gcc/ada/libgnat/s-valint.ads b/gcc/ada/libgnat/s-valint.ads
index c0d47aa1ce7..9e47f1bc9f0 100644
--- a/gcc/ada/libgnat/s-valint.ads
+++ b/gcc/ada/libgnat/s-valint.ads
@@ -57,6 +57,8 @@ package System.Val_Int with SPARK_Mode is
(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 =>
@@ -64,7 +66,11 @@ package System.Val_Int with SPARK_Mode is
Scan_Raw_Unsigned_Ghost =>
Val_Uns.Impl.Scan_Raw_Unsigned_Ghost,
Raw_Unsigned_Last_Ghost =>
- Val_Uns.Impl.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);
procedure Scan_Integer
(Str : String;
diff --git a/gcc/ada/libgnat/s-vallli.ads b/gcc/ada/libgnat/s-vallli.ads
index dfb1729e41c..5bccb1a726b 100644
--- a/gcc/ada/libgnat/s-vallli.ads
+++ b/gcc/ada/libgnat/s-vallli.ads
@@ -58,6 +58,8 @@ package System.Val_LLI with SPARK_Mode is
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 =>
@@ -65,7 +67,11 @@ package System.Val_LLI with SPARK_Mode is
Scan_Raw_Unsigned_Ghost =>
Val_LLU.Impl.Scan_Raw_Unsigned_Ghost,
Raw_Unsigned_Last_Ghost =>
- Val_LLU.Impl.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);
procedure Scan_Long_Long_Integer
(Str : String;
diff --git a/gcc/ada/libgnat/s-valllli.ads b/gcc/ada/libgnat/s-valllli.ads
index 84bca5878ed..586c7379d21 100644
--- a/gcc/ada/libgnat/s-valllli.ads
+++ b/gcc/ada/libgnat/s-valllli.ads
@@ -58,6 +58,8 @@ package System.Val_LLLI with SPARK_Mode is
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 =>
@@ -65,7 +67,11 @@ package System.Val_LLLI with SPARK_Mode is
Scan_Raw_Unsigned_Ghost =>
Val_LLLU.Impl.Scan_Raw_Unsigned_Ghost,
Raw_Unsigned_Last_Ghost =>
- Val_LLLU.Impl.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);
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 68d898448bf..b453ffc38da 100644
--- a/gcc/ada/libgnat/s-valuei.adb
+++ b/gcc/ada/libgnat/s-valuei.adb
@@ -41,6 +41,59 @@ 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 --
------------------
diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads
index a7e20abec65..d2e857a3de3 100644
--- a/gcc/ada/libgnat/s-valuei.ads
+++ b/gcc/ada/libgnat/s-valuei.ads
@@ -56,19 +56,31 @@ generic
-- Additional parameters for ghost subprograms used inside contracts
+ type Uns_Option is private;
+ with function Wrap_Option (Value : Uns) return Uns_Option;
with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean;
with function Raw_Unsigned_Overflows_Ghost
- (Str : String;
- From, To : Integer)
- return Boolean;
+ (Str : String;
+ From, To : Integer)
+ return Boolean;
with function Scan_Raw_Unsigned_Ghost
- (Str : String;
- From, To : Integer)
- return Uns;
+ (Str : String;
+ From, To : Integer)
+ return Uns;
with function Raw_Unsigned_Last_Ghost
- (Str : String;
- From, To : Integer)
- return Positive;
+ (Str : String;
+ From, To : Integer)
+ return Positive;
+ with function Only_Decimal_Ghost
+ (Str : String;
+ From, To : Integer)
+ return Boolean;
+ with function Scan_Based_Number_Ghost
+ (Str : String;
+ From, To : Integer;
+ Base : Uns := 10;
+ Acc : Uns := 0)
+ return Uns_Option;
package System.Value_I is
pragma Preelaborate;
@@ -96,6 +108,13 @@ package System.Value_I is
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
+
procedure Scan_Integer
(Str : String;
Ptr : not null access Integer;
@@ -238,6 +257,22 @@ package System.Value_I is
-- 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
----------------
diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads
index 5c0f2a5d6bd..db1051b7e3f 100644
--- a/gcc/ada/libgnat/s-valuti.ads
+++ b/gcc/ada/libgnat/s-valuti.ads
@@ -376,6 +376,41 @@ 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
+ -- 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 <>;
+ type Uns_Option is private;
+
+ Unsigned_Width_Ghost : Natural;
+
+ with function Wrap_Option (Value : Uns) return Uns_Option;
+ with function Only_Decimal_Ghost
+ (Str : String;
+ From, To : Integer)
+ return Boolean;
+ with function Hexa_To_Unsigned_Ghost (X : Character) return Uns;
+ with function Scan_Based_Number_Ghost
+ (Str : String;
+ From, To : Integer;
+ Base : Uns := 10;
+ Acc : Uns := 0)
+ return Uns_Option;
+ with function Is_Integer_Ghost (Str : String) return Boolean;
+ with procedure Prove_Iter_Scan_Based_Number_Ghost
+ (Str1, Str2 : String;
+ From, To : Integer;
+ Base : Uns := 10;
+ Acc : Uns := 0);
+ with procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int);
+ with function Abs_Uns_Of_Int (Val : Int) return Uns;
+ with function Value_Integer (Str : String) return Int;
+
+ package Int_Params is
+ end Int_Params;
+
private
------------------------
diff --git a/gcc/ada/libgnat/s-widthu.ads b/gcc/ada/libgnat/s-widthu.ads
index 7bad3fd758e..2c583b31c6c 100644
--- a/gcc/ada/libgnat/s-widthu.ads
+++ b/gcc/ada/libgnat/s-widthu.ads
@@ -59,7 +59,7 @@ is
function Big (Arg : Uns) return Big_Integer renames
Unsigned_Conversion.To_Big_Integer;
- Big_10 : constant Big_Integer := Big (10) with Ghost;
+ Big_10 : constant Big_Integer := Big (Uns'(10)) with Ghost;
-- Maximum value of exponent for 10 that fits in Uns'Base
function Max_Log10 return Natural is
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-05-12 12:40 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-05-12 12:40 [gcc r13-352] [Ada] Proof of 'Image support for signed integers Pierre-Marie de Rodat
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).