This proves the generic unit System.Exponu instantiated for Unsigned,
Long_Long_Unsigned and Long_Long_Long_Unsigned. The proof is simpler
than the one for signed integers, as there are no possible overflows
here.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/s-explllu.ads: Mark in SPARK.
* libgnat/s-expllu.ads: Mark in SPARK.
* libgnat/s-exponu.adb: Add loop invariants and needed
assertions.
* libgnat/s-exponu.ads: Add functional contract.
* libgnat/s-expuns.ads: Mark in SPARK.diff --git a/gcc/ada/libgnat/s-explllu.ads b/gcc/ada/libgnat/s-explllu.ads
--- a/gcc/ada/libgnat/s-explllu.ads
+++ b/gcc/ada/libgnat/s-explllu.ads
@@ -34,10 +34,23 @@
-- The result is always full width, the caller must do a masking operation if
-- the modulus is less than 2 ** Long_Long_Long_Unsigned'Size.
+-- 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);
+
with System.Exponu;
with System.Unsigned_Types;
-package System.Exp_LLLU is
+package System.Exp_LLLU
+ with SPARK_Mode
+is
subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
diff --git a/gcc/ada/libgnat/s-expllu.ads b/gcc/ada/libgnat/s-expllu.ads
--- a/gcc/ada/libgnat/s-expllu.ads
+++ b/gcc/ada/libgnat/s-expllu.ads
@@ -34,10 +34,23 @@
-- The result is always full width, the caller must do a masking operation if
-- the modulus is less than 2 ** Long_Long_Unsigned'Size.
+-- 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);
+
with System.Exponu;
with System.Unsigned_Types;
-package System.Exp_LLU is
+package System.Exp_LLU
+ with SPARK_Mode
+is
subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
diff --git a/gcc/ada/libgnat/s-exponu.adb b/gcc/ada/libgnat/s-exponu.adb
--- a/gcc/ada/libgnat/s-exponu.adb
+++ b/gcc/ada/libgnat/s-exponu.adb
@@ -29,7 +29,19 @@
-- --
------------------------------------------------------------------------------
-function System.Exponu (Left : Int; Right : Natural) return Int is
+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);
-- Note that negative exponents get a constraint error because the
-- subtype of the Right argument (the exponent) is Natural.
@@ -49,7 +61,16 @@ 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;
diff --git a/gcc/ada/libgnat/s-exponu.ads b/gcc/ada/libgnat/s-exponu.ads
--- a/gcc/ada/libgnat/s-exponu.ads
+++ b/gcc/ada/libgnat/s-exponu.ads
@@ -31,8 +31,22 @@
-- Modular 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;
+function System.Exponu (Left : Int; Right : Natural) return Int
+with
+ SPARK_Mode,
+ Post => System.Exponu'Result = Left ** Right;
diff --git a/gcc/ada/libgnat/s-expuns.ads b/gcc/ada/libgnat/s-expuns.ads
--- a/gcc/ada/libgnat/s-expuns.ads
+++ b/gcc/ada/libgnat/s-expuns.ads
@@ -34,10 +34,23 @@
-- The result is always full width, the caller must do a masking operation if
-- the modulus is less than 2 ** Unsigned'Size.
+-- 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);
+
with System.Exponu;
with System.Unsigned_Types;
-package System.Exp_Uns is
+package System.Exp_Uns
+ with SPARK_Mode
+is
subtype Unsigned is Unsigned_Types.Unsigned;
