diff options
Diffstat (limited to 'gcc/ada/libgnat/s-expint.ads')
| -rw-r--r-- | gcc/ada/libgnat/s-expint.ads | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/gcc/ada/libgnat/s-expint.ads b/gcc/ada/libgnat/s-expint.ads index a69c8d6..d349330 100644 --- a/gcc/ada/libgnat/s-expint.ads +++ b/gcc/ada/libgnat/s-expint.ads @@ -31,23 +31,11 @@ -- This package implements Integer exponentiation (checks on) --- Preconditions, postconditions, 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 (Pre => Ignore, - Post => Ignore, - Ghost => Ignore, - Loop_Invariant => Ignore, - Assert => Ignore); - with System.Expont; package System.Exp_Int with SPARK_Mode is - package Expont_Integer is new Expont (Integer); function Exp_Integer (Left : Integer; Right : Natural) return Integer |