diff options
Diffstat (limited to 'gcc/ada/libgnat/s-exponu.adb')
| -rw-r--r-- | gcc/ada/libgnat/s-exponu.adb | 24 |
1 files changed, 1 insertions, 23 deletions
diff --git a/gcc/ada/libgnat/s-exponu.adb b/gcc/ada/libgnat/s-exponu.adb index abb1930..0c52833 100644 --- a/gcc/ada/libgnat/s-exponu.adb +++ b/gcc/ada/libgnat/s-exponu.adb @@ -29,20 +29,7 @@ -- -- ------------------------------------------------------------------------------ -function System.Exponu (Left : Int; Right : Natural) return Int - with SPARK_Mode -is - -- 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); - +function System.Exponu (Left : Int; Right : Natural) return Int is -- Note that negative exponents get a constraint error because the -- subtype of the Right argument (the exponent) is Natural. @@ -61,16 +48,7 @@ begin if Exp /= 0 then loop - pragma Loop_Invariant (Exp > 0); - pragma Loop_Invariant (Result * Factor ** Exp = Left ** Right); - pragma Loop_Variant (Decreases => Exp); - if Exp rem 2 /= 0 then - pragma Assert - (Result * (Factor * Factor ** (Exp - 1)) = Left ** Right); - pragma Assert - ((Result * Factor) * Factor ** (Exp - 1) = Left ** Right); - Result := Result * Factor; end if; |