diff options
Diffstat (limited to 'gcc/ada/libgnat/s-exponu.ads')
| -rw-r--r-- | gcc/ada/libgnat/s-exponu.ads | 17 |
1 files changed, 1 insertions, 16 deletions
diff --git a/gcc/ada/libgnat/s-exponu.ads b/gcc/ada/libgnat/s-exponu.ads index cfa6d78..7cc2f9c 100644 --- a/gcc/ada/libgnat/s-exponu.ads +++ b/gcc/ada/libgnat/s-exponu.ads @@ -31,25 +31,10 @@ -- This function implements unsigned integer exponentiation --- 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); - generic - type Int is mod <>; -function System.Exponu (Left : Int; Right : Natural) return Int -with - SPARK_Mode, - Post => System.Exponu'Result = Left ** Right; +function System.Exponu (Left : Int; Right : Natural) return Int; -- Calculate ``Left`` ** ``Right``. If ``Left`` is 0 then 0 is returned -- and if ``Right`` is 0 then 1 is returned. In all other cases the result -- is set to 1 and then computed in a loop as follows: |