ada/libgnat/a-except.o \
ada/libgnat/a-exctra.o \
ada/libgnat/a-ioexce.o \
+ ada/libgnat/a-nubinu.o \
+ ada/libgnat/a-numeri.o \
ada/libgnat/ada.o \
ada/libgnat/g-byorma.o \
ada/libgnat/g-heasor.o \
ada/libgnat/s-wchcnv.o \
ada/libgnat/s-wchcon.o \
ada/libgnat/s-wchjis.o \
- ada/libgnat/s-wchstw.o
+ ada/libgnat/s-wchstw.o \
+ ada/libgnat/s-widuns.o
endif
# Object files for gnat executables
ada/libgnat/a-assert.o \
ada/libgnat/a-elchha.o \
ada/libgnat/a-except.o \
+ ada/libgnat/a-nubinu.o \
+ ada/libgnat/a-numeri.o \
ada/libgnat/ada.o \
ada/libgnat/g-byorma.o \
ada/libgnat/g-hesora.o \
ada/libgnat/s-wchcon.o \
ada/libgnat/s-wchjis.o \
ada/libgnat/s-wchstw.o \
+ ada/libgnat/s-widuns.o \
ada/adaint.o \
ada/argv.o \
ada/cio.o \
type Int is range <>;
package System.Image_D is
- pragma Pure;
procedure Image_Decimal
(V : Int;
Round : Boolean);
package System.Image_F is
- pragma Pure;
procedure Image_Fixed
(V : Int;
P : in out Natural);
package System.Image_R is
- pragma Pure;
procedure Image_Fixed_Point
(V : Num;
-- --
------------------------------------------------------------------------------
+with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+
package body System.Image_U 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,
+ Subprogram_Variant => Ignore);
+
+ 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;
+
+ -- Maximum value of exponent for 10 that fits in Uns'Base
+ function Max_Log10 return Natural is
+ (case Uns'Base'Size is
+ when 8 => 2,
+ when 16 => 4,
+ when 32 => 9,
+ when 64 => 19,
+ when 128 => 38,
+ when others => raise Program_Error)
+ with Ghost;
+
+ ------------------
+ -- Local Lemmas --
+ ------------------
+
+ 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);
+
+ procedure Lemma_Unsigned_Width_Ghost
+ with
+ Ghost,
+ Post => Unsigned_Width_Ghost = Max_Log10 + 2;
+
+ ---------------------------
+ -- 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;
+
+ --------------------------------
+ -- Lemma_Unsigned_Width_Ghost --
+ --------------------------------
+
+ procedure Lemma_Unsigned_Width_Ghost is
+ begin
+ pragma Assert (Unsigned_Width_Ghost <= Max_Log10 + 2);
+ pragma Assert (Big (Uns'Last) > Big_10 ** Max_Log10);
+ pragma Assert (Big (Uns'Last) < Big_10 ** (Unsigned_Width_Ghost - 1));
+ pragma Assert (Unsigned_Width_Ghost >= Max_Log10 + 2);
+ end Lemma_Unsigned_Width_Ghost;
+
--------------------
-- Image_Unsigned --
--------------------
P : out Natural)
is
pragma Assert (S'First = 1);
+
+ procedure Prove_Value_Unsigned
+ with
+ Ghost,
+ Pre => S'First = 1
+ 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;
+ -- Ghost lemma to prove the value of Value_Unsigned from the value of
+ -- Scan_Based_Number_Ghost on a decimal string.
+
+ --------------------------
+ -- Prove_Value_Unsigned --
+ --------------------------
+
+ procedure Prove_Value_Unsigned 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);
+ end Prove_Value_Unsigned;
+
+ -- Start of processing for Image_Unsigned
+
begin
S (1) := ' ';
P := 1;
Set_Image_Unsigned (V, S, P);
+
+ Prove_Value_Unsigned;
end Image_Unsigned;
------------------------
is
Nb_Digits : Natural := 0;
Value : Uns := V;
+
+ -- Local ghost variables
+
+ 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;
+
+ -- Local ghost lemmas
+
+ procedure Prove_Character_Val (R : Uns)
+ with
+ Ghost,
+ Pre => R in 0 .. 9,
+ Post => Character'Val (48 + R) in '0' .. '9';
+ -- Ghost lemma to prove the value of a character corresponding to the
+ -- next figure.
+
+ procedure Prove_Hexa_To_Unsigned_Ghost (R : Uns)
+ with
+ Ghost,
+ Pre => R in 0 .. 9,
+ Post => 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.
+
+ -----------------------------
+ -- Local lemma null bodies --
+ -----------------------------
+
+ procedure Prove_Character_Val (R : Uns) is null;
+ procedure Prove_Hexa_To_Unsigned_Ghost (R : Uns) is null;
+ procedure Prove_Unchanged 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_Image_Unsigned
+
begin
pragma Assert (P >= S'First - 1 and then P < S'Last and then
P < Natural'Last);
-- No check is done since, as documented in the specification, the
-- caller guarantees that S is long enough to hold the result.
+ Lemma_Unsigned_Width_Ghost;
+
-- First we compute the number of characters needed for representing
-- the number.
loop
+ Lemma_Div_Commutation (Value, 10);
+ Lemma_Div_Twice (Big (V), Big_10 ** Nb_Digits, Big_10);
+
Value := Value / 10;
Nb_Digits := Nb_Digits + 1;
+ Pow := Pow * 10;
+
+ pragma Loop_Invariant (Nb_Digits in 1 .. Unsigned_Width_Ghost - 1);
+ pragma Loop_Invariant (Pow = Big_10 ** Nb_Digits);
+ pragma Loop_Invariant (Big (Value) = Big (V) / Pow);
+ pragma Loop_Variant (Decreases => Value);
+
exit when Value = 0;
+
+ Lemma_Non_Zero (Value);
+ pragma Assert (Pow <= Big (Uns'Last));
end loop;
Value := V;
+ Pow := 1;
+
+ pragma Assert (Value = From_Big (Big (V) / Big_10 ** 0));
-- We now populate digits from the end of the string to the beginning
- for J in reverse 1 .. Nb_Digits loop
+ 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_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
+ 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;
+
+ pragma Assert (Prev = Cur);
+ pragma Assert (Prev = Wrap_Option (V));
+
+ 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);
+ 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
+ (Str => S,
+ From => P + J,
+ To => P + Nb_Digits,
+ Base => 10,
+ Acc => Value)
+ = Wrap_Option (V));
end loop;
+ Prove_Unchanged;
+ pragma Assert
+ (Scan_Based_Number_Ghost
+ (Str => S,
+ From => P + 1,
+ To => P + Nb_Digits,
+ Base => 10,
+ Acc => Value)
+ = Wrap_Option (V));
+
P := P + Nb_Digits;
end Set_Image_Unsigned;
-- modular integer types, and also for conversion operations required in
-- Text_IO.Modular_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);
+
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 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_Unsigned_Ghost (Str : String) return Boolean;
+ 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 procedure Prove_Scan_Only_Decimal_Ghost
+ (Str : String;
+ Val : Uns);
package System.Image_U is
- pragma Pure;
procedure Image_Unsigned
(V : Uns;
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 >= Unsigned_Width_Ghost,
+ Post => P in S'Range
+ and then Value_Unsigned (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
procedure Set_Image_Unsigned
(V : Uns;
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 (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
with System.Image_D;
package System.Img_Decimal_128 is
- pragma Pure;
subtype Int128 is Interfaces.Integer_128;
with System.Image_D;
package System.Img_Decimal_32 is
- pragma Pure;
subtype Int32 is Interfaces.Integer_32;
with System.Image_D;
package System.Img_Decimal_64 is
- pragma Pure;
subtype Int64 is Interfaces.Integer_64;
with System.Image_F;
package System.Img_Fixed_128 is
- pragma Pure;
subtype Int128 is Interfaces.Integer_128;
with System.Image_F;
package System.Img_Fixed_32 is
- pragma Pure;
subtype Int32 is Interfaces.Integer_32;
with System.Image_F;
package System.Img_Fixed_64 is
- pragma Pure;
subtype Int64 is Interfaces.Integer_64;
with System.Unsigned_Types;
package System.Img_Flt is
- pragma Pure;
package Impl is new Image_R
(Float,
with System.Unsigned_Types;
package System.Img_LFlt is
- pragma Pure;
-- Note that the following instantiation is really for a 32-bit target,
-- where 128-bit integer types are not available. For a 64-bit targaet,
with System.Unsigned_Types;
package System.Img_LLF is
- pragma Pure;
-- Note that the following instantiation is really for a 32-bit target,
-- where 128-bit integer types are not available. For a 64-bit targaet,
-- modular integer types larger than Long_Long_Unsigned, and also for
-- conversion operations required in Text_IO.Modular_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_U;
with System.Unsigned_Types;
+with System.Val_LLLU;
+with System.Wid_LLLU;
-package System.Img_LLLU is
- pragma Pure;
-
+package System.Img_LLLU
+ with SPARK_Mode
+is
subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
- package Impl is new Image_U (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 =>
+ 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);
procedure Image_Long_Long_Long_Unsigned
(V : Long_Long_Long_Unsigned;
-- modular integer types larger than Unsigned, and also for conversion
-- operations required in Text_IO.Modular_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_U;
with System.Unsigned_Types;
+with System.Val_LLU;
+with System.Wid_LLU;
-package System.Img_LLU is
- pragma Pure;
-
+package System.Img_LLU
+ with SPARK_Mode
+is
subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
- package Impl is new Image_U (Long_Long_Unsigned);
+ package Impl is new Image_U
+ (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,
+ 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);
procedure Image_Long_Long_Unsigned
(V : Long_Long_Unsigned;
with System.Img_LLF;
package System.Img_Real is
- pragma Pure;
procedure Set_Image_Real
(V : Long_Long_Float;
-- modular integer types up to Unsigned, and also for conversion operations
-- required in Text_IO.Modular_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_U;
with System.Unsigned_Types;
+with System.Val_Uns;
+with System.Wid_Uns;
-package System.Img_Uns is
- pragma Pure;
-
+package System.Img_Uns
+ with SPARK_Mode
+is
subtype Unsigned is Unsigned_Types.Unsigned;
- package Impl is new Image_U (Unsigned);
+ package Impl is new Image_U
+ (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,
+ 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);
procedure Image_Unsigned
(V : Unsigned;
-- This package provides some common utilities used by the s-imgxxx files
package System.Img_Util is
- pragma Pure;
Max_Real_Image_Length : constant := 5200;
-- If Exp is set to zero and Aft is set to Text_IO.Field'Last (i.e., 255)
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 --
-----------------------
when False =>
Value : Uns := 0;
end case;
- end record with Ghost;
+ 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
-- 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
-----------------------------
is
subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
- function Width_Long_Long_Long_Unsigned is
- new Width_U (Long_Long_Long_Unsigned);
- pragma Pure_Function (Width_Long_Long_Long_Unsigned);
+ package Width_Uns is new Width_U (Long_Long_Long_Unsigned);
+
+ function Width_Long_Long_Long_Unsigned
+ (Lo, Hi : Long_Long_Long_Unsigned)
+ return Natural
+ renames Width_Uns.Width;
end System.Wid_LLLU;
is
subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
- function Width_Long_Long_Unsigned is new Width_U (Long_Long_Unsigned);
- pragma Pure_Function (Width_Long_Long_Unsigned);
+ package Width_Uns is new Width_U (Long_Long_Unsigned);
+
+ function Width_Long_Long_Unsigned
+ (Lo, Hi : Long_Long_Unsigned)
+ return Natural
+ renames Width_Uns.Width;
end System.Wid_LLU;
-- --
------------------------------------------------------------------------------
-with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
-use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
-
-function System.Width_U (Lo, Hi : Uns) return Natural is
+package body System.Width_U 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);
-
- -----------------------
- -- Local Subprograms --
- -----------------------
-
- package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns);
-
- function Big (Arg : Uns) return Big_Integer renames
- Unsigned_Conversion.To_Big_Integer;
-
- -- Maximum value of exponent for 10 that fits in Uns'Base
- function Max_Log10 return Natural is
- (case Uns'Base'Size is
- when 8 => 2,
- when 16 => 4,
- when 32 => 9,
- when 64 => 19,
- when 128 => 38,
- when others => raise Program_Error)
- with Ghost;
-
- ------------------
- -- Local Lemmas --
- ------------------
-
- procedure Lemma_Lower_Mult (A, B, C : Big_Natural)
- with
- Ghost,
- Pre => A <= B,
- Post => A * C <= B * C;
-
- 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_Lower_Mult --
- ----------------------
-
- procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is null;
-
- ---------------------------
- -- Lemma_Div_Commutation --
- ---------------------------
-
- 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;
-
- -- Local variables
-
- W : Natural;
- T : Uns;
-
- -- Local ghost variables
-
- Max_W : constant Natural := Max_Log10 with Ghost;
- Big_10 : constant Big_Integer := Big (10) with Ghost;
-
- Pow : Big_Integer := 1 with Ghost;
- T_Init : constant Uns := Uns'Max (Lo, Hi) with Ghost;
-
--- Start of processing for System.Width_U
-
-begin
- if Lo > Hi then
- return 0;
-
- else
- -- Minimum value is 2, one for space, one for digit
-
- W := 2;
-
- -- Get max of absolute values
+ pragma Assertion_Policy (Ghost => Ignore,
+ Loop_Invariant => Ignore,
+ Assert => Ignore,
+ Assert_And_Cut => Ignore,
+ Subprogram_Variant => Ignore);
+
+ function Width (Lo, Hi : Uns) return Natural 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);
+
+ ------------------
+ -- Local Lemmas --
+ ------------------
+
+ procedure Lemma_Lower_Mult (A, B, C : Big_Natural)
+ with
+ Ghost,
+ Pre => A <= B,
+ Post => A * C <= B * C;
+
+ 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_Lower_Mult --
+ ----------------------
+
+ procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is null;
+
+ ---------------------------
+ -- Lemma_Div_Commutation --
+ ---------------------------
+
+ 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;
- T := Uns'Max (Lo, Hi);
+ -- Local variables
- -- Increase value if more digits required
+ W : Natural;
+ T : Uns;
- while T >= 10 loop
- Lemma_Div_Commutation (T, 10);
- Lemma_Div_Twice (Big (T_Init), Big_10 ** (W - 2), Big_10);
+ -- Local ghost variables
- T := T / 10;
- W := W + 1;
- Pow := Pow * 10;
+ Max_W : constant Natural := Max_Log10 with Ghost;
+ Pow : Big_Integer := 1 with Ghost;
+ T_Init : constant Uns := Uns'Max (Lo, Hi) with Ghost;
- pragma Loop_Invariant (W in 3 .. Max_W + 3);
- pragma Loop_Invariant (Pow = Big_10 ** (W - 2));
- pragma Loop_Invariant (Big (T) = Big (T_Init) / Pow);
- pragma Loop_Variant (Decreases => T);
- end loop;
+ -- Start of processing for System.Width_U
- declare
- F : constant Big_Integer := Big_10 ** (W - 2) with Ghost;
- Q : constant Big_Integer := Big (T_Init) / F with Ghost;
- R : constant Big_Integer := Big (T_Init) rem F with Ghost;
- begin
- pragma Assert (Q < Big_10);
- pragma Assert (Big (T_Init) = Q * F + R);
- Lemma_Lower_Mult (Q, Big (9), F);
- pragma Assert (Big (T_Init) <= Big (9) * F + F - 1);
- pragma Assert (Big (T_Init) < Big_10 * F);
- pragma Assert (Big_10 * F = Big_10 ** (W - 1));
- end;
-
- -- This is an expression of the functional postcondition for Width_U,
- -- which cannot be expressed readily as a postcondition as this would
- -- require making the instantiation Unsigned_Conversion and function
- -- Big available from the spec.
-
- pragma Assert (Big (Lo) < Big_10 ** (W - 1));
- pragma Assert (Big (Hi) < Big_10 ** (W - 1));
-
- return W;
- end if;
+ begin
+ if Lo > Hi then
+ return 0;
+
+ else
+ -- Minimum value is 2, one for space, one for digit
+
+ W := 2;
+
+ -- Get max of absolute values
+
+ T := Uns'Max (Lo, Hi);
+
+ -- Increase value if more digits required
+
+ while T >= 10 loop
+ Lemma_Div_Commutation (T, 10);
+ Lemma_Div_Twice (Big (T_Init), Big_10 ** (W - 2), Big_10);
+
+ T := T / 10;
+ W := W + 1;
+ Pow := Pow * 10;
+
+ pragma Loop_Invariant (W in 3 .. Max_W + 2);
+ pragma Loop_Invariant (Pow = Big_10 ** (W - 2));
+ pragma Loop_Invariant (Big (T) = Big (T_Init) / Pow);
+ pragma Loop_Variant (Decreases => T);
+ end loop;
+
+ declare
+ F : constant Big_Integer := Big_10 ** (W - 2) with Ghost;
+ Q : constant Big_Integer := Big (T_Init) / F with Ghost;
+ R : constant Big_Integer := Big (T_Init) rem F with Ghost;
+ begin
+ pragma Assert (Q < Big_10);
+ pragma Assert (Big (T_Init) = Q * F + R);
+ Lemma_Lower_Mult (Q, Big (9), F);
+ pragma Assert (Big (T_Init) <= Big (9) * F + F - 1);
+ pragma Assert (Big (T_Init) < Big_10 * F);
+ pragma Assert (Big_10 * F = Big_10 ** (W - 1));
+ end;
+
+ return W;
+ end if;
+ end Width;
end System.Width_U;
-- --
------------------------------------------------------------------------------
+-- 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);
+
-- Compute Width attribute for non-static type derived from a modular integer
-- type. The arguments Lo, Hi are the bounds of the type.
+with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+
generic
type Uns is mod <>;
-function System.Width_U (Lo, Hi : Uns) return Natural
-with
- Post => (if Lo > Hi then
- System.Width_U'Result = 0
- else
- System.Width_U'Result > 0);
+package System.Width_U
+ with Pure
+is
+ package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns);
+
+ function Big (Arg : Uns) return Big_Integer renames
+ Unsigned_Conversion.To_Big_Integer;
+
+ Big_10 : constant Big_Integer := Big (10) with Ghost;
+
+ -- Maximum value of exponent for 10 that fits in Uns'Base
+ function Max_Log10 return Natural is
+ (case Uns'Base'Size is
+ when 8 => 2,
+ when 16 => 4,
+ when 32 => 9,
+ when 64 => 19,
+ when 128 => 38,
+ when others => raise Program_Error)
+ with Ghost;
+
+ function Width (Lo, Hi : Uns) return Natural
+ with
+ Post =>
+ (declare
+ W : constant Natural := System.Width_U.Width'Result;
+ begin
+ (if Lo > Hi then W = 0
+ else W > 0
+ and then W <= Max_Log10 + 2
+ and then Big (Lo) < Big_10 ** (W - 1)
+ and then Big (Hi) < Big_10 ** (W - 1)));
+
+end System.Width_U;
is
subtype Unsigned is Unsigned_Types.Unsigned;
- function Width_Unsigned is new Width_U (Unsigned);
- pragma Pure_Function (Width_Unsigned);
+ package Width_Uns is new Width_U (Unsigned);
+
+ function Width_Unsigned (Lo, Hi : Unsigned) return Natural
+ renames Width_Uns.Width;
end System.Wid_Uns;
projects / thirdparty / gcc.git / commitdiff
