diff options
Diffstat (limited to 'gcc/ada/libgnat/s-vallllu.ads')
| -rw-r--r-- | gcc/ada/libgnat/s-vallllu.ads | 15 |
1 files changed, 1 insertions, 14 deletions
diff --git a/gcc/ada/libgnat/s-vallllu.ads b/gcc/ada/libgnat/s-vallllu.ads index 8e57e51..50a061b 100644 --- a/gcc/ada/libgnat/s-vallllu.ads +++ b/gcc/ada/libgnat/s-vallllu.ads @@ -32,28 +32,15 @@ -- This package contains routines for scanning modular Long_Long_Unsigned -- values for use in Text_IO.Modular_IO, and the Value attribute. --- Preconditions in this unit are meant for analysis only, not for run-time --- checking, so that the expected exceptions are raised. This is enforced by --- setting the corresponding assertion policy to Ignore. Postconditions and --- contract cases should not be executed at runtime as well, in order not to --- slow down the execution of these functions. - -pragma Assertion_Policy (Pre => Ignore, - Post => Ignore, - Contract_Cases => Ignore, - Ghost => Ignore, - Subprogram_Variant => Ignore); - with System.Unsigned_Types; with System.Value_U; -with System.Vs_LLLU; package System.Val_LLLU with SPARK_Mode is pragma Preelaborate; subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned; - package Impl is new Value_U (Long_Long_Long_Unsigned, System.Vs_LLLU.Spec); + package Impl is new Value_U (Long_Long_Long_Unsigned); procedure Scan_Raw_Long_Long_Long_Unsigned (Str : String; |