SPARK rules regarding constants with variable inputs and generic actual
parameters are currently not flexible enough to allow an explicit
Initializes contract on Ada.Strings.Bounded.Generic_Bounded_Length.
This patch removes the explicit contract, so that GNATprove generates an
implicit one with or without the Max_Length, as necessary.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/a-strbou.ads (Generic_Bounded_Length): Remove explicit
Initializes contract.diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads
--- a/gcc/ada/libgnat/a-strbou.ads
+++ b/gcc/ada/libgnat/a-strbou.ads
@@ -45,8 +45,6 @@ package Ada.Strings.Bounded with SPARK_Mode is
-- Maximum length of a Bounded_String
package Generic_Bounded_Length with SPARK_Mode,
- Initializes => (Null_Bounded_String => Max,
- Max_Length => Max),
Initial_Condition => Length (Null_Bounded_String) = 0,
Abstract_State => null
is
