diff options
Diffstat (limited to 'gcc/ada/libgnat/s-vallli.ads')
-rw-r--r-- | gcc/ada/libgnat/s-vallli.ads | 18 |
1 files changed, 1 insertions, 17 deletions
diff --git a/gcc/ada/libgnat/s-vallli.ads b/gcc/ada/libgnat/s-vallli.ads index 7672cc5..a3b48e3 100644 --- a/gcc/ada/libgnat/s-vallli.ads +++ b/gcc/ada/libgnat/s-vallli.ads @@ -32,23 +32,9 @@ -- This package contains routines for scanning signed Long_Long_Integer -- values for use in Text_IO.Integer_IO, and the Value attribute. --- Preconditions in this unit are meant for analysis only, not for run-time --- checking, so that the expected exceptions are raised. This is enforced by --- setting the corresponding assertion policy to Ignore. Postconditions and --- contract cases should not be executed at runtime as well, in order not to --- slow down the execution of these functions. - -pragma Assertion_Policy (Pre => Ignore, - Post => Ignore, - Contract_Cases => Ignore, - Ghost => Ignore, - Subprogram_Variant => Ignore); - with System.Unsigned_Types; with System.Val_LLU; with System.Value_I; -with System.Vs_LLI; -with System.Vs_LLU; package System.Val_LLI with SPARK_Mode is pragma Preelaborate; @@ -58,9 +44,7 @@ package System.Val_LLI with SPARK_Mode is package Impl is new Value_I (Int => Long_Long_Integer, Uns => Long_Long_Unsigned, - Scan_Raw_Unsigned => Val_LLU.Scan_Raw_Long_Long_Unsigned, - U_Spec => System.Vs_LLU.Spec, - Spec => System.Vs_LLI.Spec); + Scan_Raw_Unsigned => Val_LLU.Scan_Raw_Long_Long_Unsigned); procedure Scan_Long_Long_Integer (Str : String; |