diff options
Diffstat (limited to 'gcc/ada/libgnat')
| -rw-r--r-- | gcc/ada/libgnat/a-nbnbig.adb (renamed from gcc/ada/libgnat/a-nbnbin__ghost.adb) | 11 | ||||
| -rw-r--r-- | gcc/ada/libgnat/a-nbnbig.ads (renamed from gcc/ada/libgnat/a-nbnbin__ghost.ads) | 20 | ||||
| -rw-r--r-- | gcc/ada/libgnat/s-widthu.adb | 4 |
3 files changed, 27 insertions, 8 deletions
diff --git a/gcc/ada/libgnat/a-nbnbin__ghost.adb b/gcc/ada/libgnat/a-nbnbig.adb index 7d22086..d04d2a4 100644 --- a/gcc/ada/libgnat/a-nbnbin__ghost.adb +++ b/gcc/ada/libgnat/a-nbnbig.adb @@ -2,7 +2,7 @@ -- -- -- GNAT RUN-TIME COMPONENTS -- -- -- --- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS -- +-- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS_GHOST -- -- -- -- B o d y -- -- -- @@ -33,7 +33,12 @@ -- currently does not compile instantiations of the spec with imported ghost -- generics for packages Signed_Conversions and Unsigned_Conversions. -package body Ada.Numerics.Big_Numbers.Big_Integers with +-- Ghost code in this unit is meant for analysis only, not for run-time +-- checking. This is enforced by setting the assertion policy to Ignore. + +pragma Assertion_Policy (Ghost => Ignore); + +package body Ada.Numerics.Big_Numbers.Big_Integers_Ghost with SPARK_Mode => Off is @@ -73,4 +78,4 @@ is end Unsigned_Conversions; -end Ada.Numerics.Big_Numbers.Big_Integers; +end Ada.Numerics.Big_Numbers.Big_Integers_Ghost; diff --git a/gcc/ada/libgnat/a-nbnbin__ghost.ads b/gcc/ada/libgnat/a-nbnbig.ads index 3663dd7..237bca1 100644 --- a/gcc/ada/libgnat/a-nbnbin__ghost.ads +++ b/gcc/ada/libgnat/a-nbnbig.ads @@ -2,7 +2,7 @@ -- -- -- GNAT RUN-TIME COMPONENTS -- -- -- --- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS -- +-- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS_GHOST -- -- -- -- S p e c -- -- -- @@ -13,7 +13,21 @@ -- -- ------------------------------------------------------------------------------ -package Ada.Numerics.Big_Numbers.Big_Integers with +-- This unit is provided as a replacement for the standard unit +-- Ada.Numerics.Big_Numbers.Big_Integers when only proof with SPARK is +-- intended. It cannot be used for execution, as all subprograms are marked +-- imported with no definition. + +-- Contrary to Ada.Numerics.Big_Numbers.Big_Integers, this unit does not +-- depend on System or Ada.Finalization, which makes it more convenient for +-- use in run-time units. + +-- Ghost code in this unit is meant for analysis only, not for run-time +-- checking. This is enforced by setting the assertion policy to Ignore. + +pragma Assertion_Policy (Ghost => Ignore); + +package Ada.Numerics.Big_Numbers.Big_Integers_Ghost with SPARK_Mode, Ghost, Preelaborate @@ -199,4 +213,4 @@ private type Big_Integer is null record; -end Ada.Numerics.Big_Numbers.Big_Integers; +end Ada.Numerics.Big_Numbers.Big_Integers_Ghost; diff --git a/gcc/ada/libgnat/s-widthu.adb b/gcc/ada/libgnat/s-widthu.adb index fce8c7a..79a0074 100644 --- a/gcc/ada/libgnat/s-widthu.adb +++ b/gcc/ada/libgnat/s-widthu.adb @@ -29,8 +29,8 @@ -- -- ------------------------------------------------------------------------------ -with Ada.Numerics.Big_Numbers.Big_Integers; -use Ada.Numerics.Big_Numbers.Big_Integers; +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 |