* [Ada] Remove global parameter in Global contracts of Ada.Strings.Bounded
@ 2021-09-23 13:12 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2021-09-23 13:12 UTC (permalink / raw)
To: gcc-patches; +Cc: Piotr Trojanek
[-- Attachment #1: Type: text/plain, Size: 1144 bytes --]
The predefined Ada.Strings.Bounded unit has been annotated SPARK
contracts that reference a local constant:
generic
Max : Positive;
package Generic_Bounded_Length
Max_Length : constant Positive := Max;
function XXX return YYY with Global => Max_Length;
...
When this unit is instantiated with an plain integer as the Max
parameter, the Global contract will use a constant that has no variable
inputs, which is illegal in SPARK.
This patch removes Global contracts wich reference Max_Length, leaving
their generation to GNATprove. Alternatively, it would have been
possible to replace Max_Length in the Global contracts with Max,
which gets erased by the tool when the actual parameter of an instance
has no variable inputs. This is explained in SPARK RM 6.1.4(19) and
implemented in the flow analysis part of GNATprove. But this solution
forces the use of Max instead of Max_Length everywhere in the code
and functional contracts, so was considered less appealing.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/a-strbou.ads (Generic_Bounded_Length): Remove non-null
Global contracts.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 16277 bytes --]
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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2021-09-23 13:12 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-09-23 13:12 [Ada] Remove global parameter in Global contracts of Ada.Strings.Bounded Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).