From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-wr1-x42e.google.com (mail-wr1-x42e.google.com [IPv6:2a00:1450:4864:20::42e]) by sourceware.org (Postfix) with ESMTPS id 1FCB83858D35 for ; Thu, 23 Sep 2021 13:12:32 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 1FCB83858D35 Received: by mail-wr1-x42e.google.com with SMTP id u18so17093926wrg.5 for ; Thu, 23 Sep 2021 06:12:32 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=StJ5lKthWqghVv//Riu1+g+2rK9jb763EWNMRi5Wkr0=; b=1zC5ZdI/k+Gn87P2o3z8tANH2wHIDkAOtpnbkxlrSnKkBgW/GBnuqhFN+bJWgaYNfy Jco3wmXsXxcZyvIxfUuUTY2bZYsw0dQx0MsB62MOpC3XIlgbK4ONC5BhCMfb/eiIgy5E ok++H2Jz4GctI/mhvwq9p8k41Hvhz4EVb1BsqTIpflYm9r2JnSPReVYGzDbncrXu7LS/ y6L2tkKfNoJ0k7ccSW1Q10LeyMEnlHocJdyiugpDsVCfFiKY74DObn3dsX4/zEYa+a01 WwIgl5v+vv37OdfiqsWEwbTeFQ8Ui2Z4a7DUhj2RqMqMNJjH5OH+v4KqP2TiQ1D991Tf 2XyQ== X-Gm-Message-State: AOAM530fofEEOgtlb8tZFz1dnjC15Knvilsd2QQErY030a1GrA99+Hdh wR/KzIRloSRXA/hQh6Eb7tyTF3lGhgRNcw== X-Google-Smtp-Source: ABdhPJw6DFa1VSGO81e6eFOrxzhj6sHjODABlWfO/UL7V+nwRRE0namMxHB1GusFkbY0RAKwVJplZA== X-Received: by 2002:a05:6000:2c6:: with SMTP id o6mr5150197wry.292.1632402751155; Thu, 23 Sep 2021 06:12:31 -0700 (PDT) Received: from adacore.com ([2a02:2ab8:224:2ce:72b5:e8ff:feef:ee60]) by smtp.gmail.com with ESMTPSA id o19sm5711531wrg.60.2021.09.23.06.12.30 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 23 Sep 2021 06:12:30 -0700 (PDT) Date: Thu, 23 Sep 2021 13:12:29 +0000 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Piotr Trojanek Subject: [Ada] Remove global parameter in Global contracts of Ada.Strings.Bounded Message-ID: <20210923131229.GA2726990@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="qDbXVdCdHGoSgWSk" Content-Disposition: inline X-Spam-Status: No, score=-13.0 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP autolearn=ham autolearn_force=no version=3.4.4 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Thu, 23 Sep 2021 13:12:34 -0000 --qDbXVdCdHGoSgWSk Content-Type: text/plain; charset=us-ascii Content-Disposition: inline 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. --qDbXVdCdHGoSgWSk Content-Type: text/x-diff; charset=us-ascii Content-Disposition: attachment; filename="patch.diff" 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 --qDbXVdCdHGoSgWSk--