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 @@ -95,8 +95,7 @@ package Ada.Strings.Bounded with SPARK_Mode is others -- Drop = Right => To_String (To_Bounded_String'Result) = - Source (Source'First .. Source'First - 1 + Max_Length)), - Global => Max_Length; + Source (Source'First .. Source'First - 1 + Max_Length)); function To_String (Source : Bounded_String) return String with Global => null; @@ -120,8 +119,7 @@ package Ada.Strings.Bounded with SPARK_Mode is others -- Drop = Right => To_String (Target) = - Source (Source'First .. Source'First - 1 + Max_Length)), - Global => (Proof_In => Max_Length); + Source (Source'First .. Source'First - 1 + Max_Length)); pragma Ada_05 (Set_Bounded_String); function Append @@ -167,8 +165,7 @@ package Ada.Strings.Bounded with SPARK_Mode is and then (if Length (Left) < Max_Length then Slice (Append'Result, Length (Left) + 1, Max_Length) = - Slice (Right, 1, Max_Length - Length (Left)))), - Global => (Proof_In => Max_Length); + Slice (Right, 1, Max_Length - Length (Left)))); function Append (Left : Bounded_String; @@ -222,9 +219,7 @@ package Ada.Strings.Bounded with SPARK_Mode is (if Length (Left) < Max_Length then Slice (Append'Result, Length (Left) + 1, Max_Length) = Right (Right'First - .. Max_Length - Length (Left) - 1 + Right'First))), - Global => (Proof_In => Max_Length); - + .. Max_Length - Length (Left) - 1 + Right'First))); function Append (Left : String; Right : Bounded_String; @@ -274,8 +269,7 @@ package Ada.Strings.Bounded with SPARK_Mode is -- The result is the first Max_Length characters of Left To_String (Append'Result) = - Left (Left'First .. Max_Length - 1 + Left'First))), - Global => (Proof_In => Max_Length); + Left (Left'First .. Max_Length - 1 + Left'First))); function Append (Left : Bounded_String; @@ -302,8 +296,7 @@ package Ada.Strings.Bounded with SPARK_Mode is and then Slice (Append'Result, 1, Max_Length - 1) = Slice (Left, 2, Max_Length) - and then Element (Append'Result, Max_Length) = Right), - Global => (Proof_In => Max_Length); + and then Element (Append'Result, Max_Length) = Right); function Append (Left : Character; @@ -331,8 +324,7 @@ package Ada.Strings.Bounded with SPARK_Mode is and then Slice (Append'Result, 2, Max_Length) = Slice (Right, 1, Max_Length - 1) - and then Element (Append'Result, 1) = Left), - Global => (Proof_In => Max_Length); + and then Element (Append'Result, 1) = Left); procedure Append (Source : in out Bounded_String; @@ -378,8 +370,7 @@ package Ada.Strings.Bounded with SPARK_Mode is and then (if Length (Source'Old) < Max_Length then Slice (Source, Length (Source'Old) + 1, Max_Length) = - Slice (New_Item, 1, Max_Length - Length (Source'Old)))), - Global => (Proof_In => Max_Length); + Slice (New_Item, 1, Max_Length - Length (Source'Old)))); procedure Append (Source : in out Bounded_String; @@ -436,8 +427,7 @@ package Ada.Strings.Bounded with SPARK_Mode is Slice (Source, Length (Source'Old) + 1, Max_Length) = New_Item (New_Item'First .. Max_Length - Length (Source'Old) - 1 - + New_Item'First))), - Global => (Proof_In => Max_Length); + + New_Item'First))); procedure Append (Source : in out Bounded_String; @@ -465,68 +455,62 @@ package Ada.Strings.Bounded with SPARK_Mode is and then Slice (Source, 1, Max_Length - 1) = Slice (Source'Old, 2, Max_Length) - and then Element (Source, Max_Length) = New_Item), - Global => (Proof_In => Max_Length); + and then Element (Source, Max_Length) = New_Item); function "&" (Left : Bounded_String; Right : Bounded_String) return Bounded_String with - Pre => Length (Left) <= Max_Length - Length (Right), - Post => Length ("&"'Result) = Length (Left) + Length (Right) + Pre => Length (Left) <= Max_Length - Length (Right), + Post => Length ("&"'Result) = Length (Left) + Length (Right) and then Slice ("&"'Result, 1, Length (Left)) = To_String (Left) and then (if Length (Right) > 0 then Slice ("&"'Result, Length (Left) + 1, Length ("&"'Result)) = - To_String (Right)), - Global => (Proof_In => Max_Length); + To_String (Right)); function "&" (Left : Bounded_String; Right : String) return Bounded_String with - Pre => Right'Length <= Max_Length - Length (Left), - Post => Length ("&"'Result) = Length (Left) + Right'Length + Pre => Right'Length <= Max_Length - Length (Left), + Post => Length ("&"'Result) = Length (Left) + Right'Length and then Slice ("&"'Result, 1, Length (Left)) = To_String (Left) and then (if Right'Length > 0 then Slice ("&"'Result, Length (Left) + 1, Length ("&"'Result)) = - Right), - Global => (Proof_In => Max_Length); + Right); function "&" (Left : String; Right : Bounded_String) return Bounded_String with - Pre => Left'Length <= Max_Length - Length (Right), - Post => Length ("&"'Result) = Left'Length + Length (Right) + Pre => Left'Length <= Max_Length - Length (Right), + Post => Length ("&"'Result) = Left'Length + Length (Right) and then Slice ("&"'Result, 1, Left'Length) = Left and then (if Length (Right) > 0 then Slice ("&"'Result, Left'Length + 1, Length ("&"'Result)) = - To_String (Right)), - Global => (Proof_In => Max_Length); + To_String (Right)); function "&" (Left : Bounded_String; Right : Character) return Bounded_String with - Pre => Length (Left) < Max_Length, - Post => Length ("&"'Result) = Length (Left) + 1 + Pre => Length (Left) < Max_Length, + Post => Length ("&"'Result) = Length (Left) + 1 and then Slice ("&"'Result, 1, Length (Left)) = To_String (Left) - and then Element ("&"'Result, Length (Left) + 1) = Right, - Global => (Proof_In => Max_Length); + and then Element ("&"'Result, Length (Left) + 1) = Right; function "&" (Left : Character; Right : Bounded_String) return Bounded_String with - Pre => Length (Right) < Max_Length, - Post => Length ("&"'Result) = 1 + Length (Right) + Pre => Length (Right) < Max_Length, + Post => Length ("&"'Result) = 1 + Length (Right) and then Element ("&"'Result, 1) = Left and then - Slice ("&"'Result, 2, Length ("&"'Result)) = To_String (Right), - Global => (Proof_In => Max_Length); + Slice ("&"'Result, 2, Length ("&"'Result)) = To_String (Right); function Element (Source : Bounded_String; @@ -1426,8 +1410,7 @@ package Ada.Strings.Bounded with SPARK_Mode is Low + By'Length, Max_Length) = Slice (Source, Integer'Max (High + 1, Low), Integer'Max (High + 1, Low) + - (Max_Length - Low - By'Length)))), - Global => (Proof_In => Max_Length); + (Max_Length - Low - By'Length)))); procedure Replace_Slice (Source : in out Bounded_String; @@ -1551,8 +1534,7 @@ package Ada.Strings.Bounded with SPARK_Mode is and then Slice (Source, Low + By'Length, Max_Length) = Slice (Source'Old, Integer'Max (High + 1, Low), Integer'Max (High + 1, Low) + - (Max_Length - Low - By'Length)))), - Global => (Proof_In => Max_Length); + (Max_Length - Low - By'Length)))); function Insert (Source : Bounded_String; @@ -1666,8 +1648,7 @@ package Ada.Strings.Bounded with SPARK_Mode is and then Slice (Insert'Result, Before + New_Item'Length, Max_Length) = Slice (Source, - Before, Max_Length - New_Item'Length))), - Global => (Proof_In => Max_Length); + Before, Max_Length - New_Item'Length))); procedure Insert (Source : in out Bounded_String; @@ -1780,8 +1761,7 @@ package Ada.Strings.Bounded with SPARK_Mode is and then Slice (Source, Before + New_Item'Length, Max_Length) = Slice (Source'Old, - Before, Max_Length - New_Item'Length))), - Global => (Proof_In => Max_Length); + Before, Max_Length - New_Item'Length))); function Overwrite (Source : Bounded_String; @@ -1867,8 +1847,7 @@ package Ada.Strings.Bounded with SPARK_Mode is and then Slice (Overwrite'Result, Position, Max_Length) = New_Item - (New_Item'First .. Max_Length - Position + New_Item'First)), - Global => (Proof_In => Max_Length); + (New_Item'First .. Max_Length - Position + New_Item'First)); procedure Overwrite (Source : in out Bounded_String; @@ -1953,8 +1932,7 @@ package Ada.Strings.Bounded with SPARK_Mode is and then Slice (Source, Position, Max_Length) = New_Item - (New_Item'First .. Max_Length - Position + New_Item'First)), - Global => (Proof_In => Max_Length); + (New_Item'First .. Max_Length - Position + New_Item'First)); function Delete (Source : Bounded_String; @@ -2166,8 +2144,7 @@ package Ada.Strings.Bounded with SPARK_Mode is and then Slice (Head'Result, Max_Length - Count + Length (Source) + 1, Max_Length) = - (1 .. Count - Length (Source) => Pad)), - Global => (Proof_In => Max_Length); + (1 .. Count - Length (Source) => Pad)); procedure Head (Source : in out Bounded_String; @@ -2225,8 +2202,7 @@ package Ada.Strings.Bounded with SPARK_Mode is and then Slice (Source, Max_Length - Count + Length (Source'Old) + 1, Max_Length) = - (1 .. Count - Length (Source'Old) => Pad)), - Global => (Proof_In => Max_Length); + (1 .. Count - Length (Source'Old) => Pad)); function Tail (Source : Bounded_String; @@ -2287,8 +2263,7 @@ package Ada.Strings.Bounded with SPARK_Mode is (1 .. Count - Length (Source) => Pad) and then Slice (Tail'Result, Count - Length (Source) + 1, Max_Length) = - Slice (Source, 1, Max_Length - Count + Length (Source))), - Global => (Proof_In => Max_Length); + Slice (Source, 1, Max_Length - Count + Length (Source))); procedure Tail (Source : in out Bounded_String; @@ -2351,8 +2326,7 @@ package Ada.Strings.Bounded with SPARK_Mode is and then Slice (Source, Count - Length (Source'Old) + 1, Max_Length) = Slice (Source'Old, - 1, Max_Length - Count + Length (Source'Old))), - Global => (Proof_In => Max_Length); + 1, Max_Length - Count + Length (Source'Old))); ------------------------------------ -- String Constructor Subprograms -- @@ -2362,48 +2336,44 @@ package Ada.Strings.Bounded with SPARK_Mode is (Left : Natural; Right : Character) return Bounded_String with - Pre => Left <= Max_Length, - Post => To_String ("*"'Result) = (1 .. Left => Right), - Global => Max_Length; + Pre => Left <= Max_Length, + Post => To_String ("*"'Result) = (1 .. Left => Right); function "*" (Left : Natural; Right : String) return Bounded_String with - Pre => (if Left /= 0 then Right'Length <= Max_Length / Left), - Post => + Pre => (if Left /= 0 then Right'Length <= Max_Length / Left), + Post => Length ("*"'Result) = Left * Right'Length and then (if Right'Length > 0 then (for all K in 1 .. Left * Right'Length => Element ("*"'Result, K) = - Right (Right'First + (K - 1) mod Right'Length))), - Global => Max_Length; + Right (Right'First + (K - 1) mod Right'Length))); function "*" (Left : Natural; Right : Bounded_String) return Bounded_String with - Pre => (if Left /= 0 then Length (Right) <= Max_Length / Left), - Post => + Pre => (if Left /= 0 then Length (Right) <= Max_Length / Left), + Post => Length ("*"'Result) = Left * Length (Right) and then (if Length (Right) > 0 then (for all K in 1 .. Left * Length (Right) => Element ("*"'Result, K) = - Element (Right, 1 + (K - 1) mod Length (Right)))), - Global => (Proof_In => Max_Length); + Element (Right, 1 + (K - 1) mod Length (Right)))); function Replicate (Count : Natural; Item : Character; Drop : Truncation := Error) return Bounded_String with - Pre => (if Count > Max_Length then Drop /= Error), - Post => + Pre => (if Count > Max_Length then Drop /= Error), + Post => To_String (Replicate'Result) = - (1 .. Natural'Min (Max_Length, Count) => Item), - Global => Max_Length; + (1 .. Natural'Min (Max_Length, Count) => Item); function Replicate (Count : Natural; @@ -2437,8 +2407,7 @@ package Ada.Strings.Bounded with SPARK_Mode is and then (for all K in 1 .. Max_Length => Element (Replicate'Result, K) = - Item (Item'Last - (Max_Length - K) mod Item'Length))), - Global => Max_Length; + Item (Item'Last - (Max_Length - K) mod Item'Length))); function Replicate (Count : Natural; @@ -2473,8 +2442,7 @@ package Ada.Strings.Bounded with SPARK_Mode is (for all K in 1 .. Max_Length => Element (Replicate'Result, K) = Element (Item, - Length (Item) - (Max_Length - K) mod Length (Item)))), - Global => (Proof_In => Max_Length); + Length (Item) - (Max_Length - K) mod Length (Item)))); private -- Most of the implementation is in the separate non generic package