From patchwork Mon Oct 4 08:48:01 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 1536006 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: bilbo.ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.a=rsa-sha256 header.s=default header.b=EHhhRHmw; dkim-atps=neutral Authentication-Results: ozlabs.org; spf=pass (sender SPF authorized) smtp.mailfrom=gcc.gnu.org (client-ip=2620:52:3:1:0:246e:9693:128c; helo=sourceware.org; envelope-from=gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Received: from sourceware.org (server2.sourceware.org [IPv6:2620:52:3:1:0:246e:9693:128c]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256) (No client certificate requested) by bilbo.ozlabs.org (Postfix) with ESMTPS id 4HNFC15fTKz9t0k for ; Mon, 4 Oct 2021 20:04:12 +1100 (AEDT) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 932AC3858422 for ; Mon, 4 Oct 2021 09:04:10 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 932AC3858422 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1633338250; bh=CJCeHwq/6I0tHYue1QO+jke77Shw/K/jNZ/a/cnYIbs=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=EHhhRHmw5ZFW7LE6Vy2frDXAeyb2XiR/axlhNs1MArmdR6j3NSlREAKx4DlJfx9KH mQBVk4wTFJO196+36qSM2w9VPlF7UPLbomJidwrNnJnciGfXAmNQijq5HDxouhXJgn /dYHHrchovxhJvt6duwU1eDzDl9P3I5GrCWBlfjs= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-lf1-x134.google.com (mail-lf1-x134.google.com [IPv6:2a00:1450:4864:20::134]) by sourceware.org (Postfix) with ESMTPS id 119BF3858413 for ; Mon, 4 Oct 2021 08:48:05 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 119BF3858413 Received: by mail-lf1-x134.google.com with SMTP id e15so68453249lfr.10 for ; Mon, 04 Oct 2021 01:48:05 -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=CJCeHwq/6I0tHYue1QO+jke77Shw/K/jNZ/a/cnYIbs=; b=vsMj9OsWwoEIDXhDZq+g1EstPqo87HktyQwzPoom7Y/RJwY0KHtSCcoJfpGDpLQWzL 0OeX7CO2LQRpK92lcyGE3HQImjiGCC2qTMqDwEzaDn+CxxgYiFfiIf9DDV78npSem6ol t6UpUlsTATt2UyZARcMlmaCxj+kFHRaB6LLTqbAPVx52+DamhWArTSi+8qAv0SEF7cz9 Yrobv/GUraJ1oTHu8t66fA/kr0SuCTPX8mB/o0M1GK/95d0VZlxyZePDO6qwnhxNbl/+ iMOHXQT+dti/qREtDCPYbNtsPHprLf3U9ffk5fLjk7DM739nnkwt7N+/ZaZqYzpncfcf 1Rhw== X-Gm-Message-State: AOAM5310pQpicPKkLNAncFofuDAATVPSfcqX33MxOHvRsQWld5dBSJBn Qkc73xZKX4PXXMJHsqgGppmtOzeXstGXdw== X-Google-Smtp-Source: ABdhPJyFXJR1Xm3F2vNMd8psEvXFgPqiKFWE3dj6G9KW01qqo8hmPP7Gou1UM0v0bOLuxs9jihu38A== X-Received: by 2002:a05:6512:3699:: with SMTP id d25mr13029805lfs.380.1633337283848; Mon, 04 Oct 2021 01:48:03 -0700 (PDT) Received: from adacore.com ([2a02:2ab8:224:2ce:72b5:e8ff:feef:ee60]) by smtp.gmail.com with ESMTPSA id f16sm1370214lfp.199.2021.10.04.01.48.02 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 04 Oct 2021 01:48:03 -0700 (PDT) Date: Mon, 4 Oct 2021 08:48:01 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] Add Ada RM description of Ada.Strings.Bounded as comments in the spec Message-ID: <20211004084801.GA1536802@adacore.com> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-12.6 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, KAM_ASCII_DIVIDERS, 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-Patchwork-Original-From: Pierre-Marie de Rodat via Gcc-patches From: Pierre-Marie de Rodat Reply-To: Pierre-Marie de Rodat Cc: Yannick Moy Errors-To: gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org Sender: "Gcc-patches" To facilitate using the standard library, Ada RM description from section A.4.4 is added to the code as comments. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/a-strbou.ads: Add comments. 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 @@ -33,6 +33,16 @@ -- -- ------------------------------------------------------------------------------ +-- The language-defined package Strings.Bounded provides a generic package +-- each of whose instances yields a private type Bounded_String and a set +-- of operations. An object of a particular Bounded_String type represents +-- a String whose low bound is 1 and whose length can vary conceptually +-- between 0 and a maximum size established at the generic instantiation. The +-- subprograms for fixed-length string handling are either overloaded directly +-- for Bounded_String, or are modified as needed to reflect the variability in +-- length. Additionally, since the Bounded_String type is private, appropriate +-- constructor and selector operations are provided. + with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; with Ada.Strings.Superbounded; with Ada.Strings.Search; @@ -65,11 +75,16 @@ package Ada.Strings.Bounded with SPARK_Mode is pragma Preelaborable_Initialization (Bounded_String); Null_Bounded_String : constant Bounded_String; + -- Null_Bounded_String represents the null string. If an object of type + -- Bounded_String is not otherwise initialized, it will be initialized + -- to the same value as Null_Bounded_String. subtype Length_Range is Natural range 0 .. Max_Length; function Length (Source : Bounded_String) return Length_Range with Global => null; + -- The Length function returns the length of the string represented by + -- Source. -------------------------------------------------------- -- Conversion, Concatenation, and Selection Functions -- @@ -94,9 +109,24 @@ package Ada.Strings.Bounded with SPARK_Mode is => To_String (To_Bounded_String'Result) = Source (Source'First .. Source'First - 1 + Max_Length)); + -- If Source'Length <= Max_Length, then this function returns a + -- Bounded_String that represents Source. Otherwise, the effect + -- depends on the value of Drop: + -- + -- * If Drop=Left, then the result is a Bounded_String that represents + -- the string comprising the rightmost Max_Length characters of + -- Source. + -- + -- * If Drop=Right, then the result is a Bounded_String that represents + -- the string comprising the leftmost Max_Length characters of Source. + -- + -- * If Drop=Error, then Strings.Length_Error is propagated. function To_String (Source : Bounded_String) return String with Global => null; + -- To_String returns the String value with lower bound 1 + -- represented by Source. If B is a Bounded_String, then + -- B = To_Bounded_String(To_String(B)). procedure Set_Bounded_String (Target : out Bounded_String; @@ -119,6 +149,14 @@ package Ada.Strings.Bounded with SPARK_Mode is To_String (Target) = Source (Source'First .. Source'First - 1 + Max_Length)); pragma Ada_05 (Set_Bounded_String); + -- Equivalent to Target := To_Bounded_String (Source, Drop); + + -- Each of the Append functions returns a Bounded_String obtained by + -- concatenating the string or character given or represented by one + -- of the parameters, with the string or character given or represented + -- by the other parameter, and applying To_Bounded_String to the + -- concatenation result string, with Drop as provided to the Append + -- function. function Append (Left : Bounded_String; @@ -324,6 +362,10 @@ package Ada.Strings.Bounded with SPARK_Mode is Slice (Right, 1, Max_Length - 1) and then Element (Append'Result, 1) = Left); + -- Each of the procedures Append(Source, New_Item, Drop) has the same + -- effect as the corresponding assignment + -- Source := Append(Source, New_Item, Drop). + procedure Append (Source : in out Bounded_String; New_Item : Bounded_String; @@ -455,6 +497,9 @@ package Ada.Strings.Bounded with SPARK_Mode is Slice (Source'Old, 2, Max_Length) and then Element (Source, Max_Length) = New_Item); + -- Each of the "&" functions has the same effect as the corresponding + -- Append function, with Error as the Drop parameter. + function "&" (Left : Bounded_String; Right : Bounded_String) return Bounded_String @@ -516,6 +561,8 @@ package Ada.Strings.Bounded with SPARK_Mode is with Pre => Index <= Length (Source), Global => null; + -- Returns the character at position Index in the string represented by + -- Source; propagates Index_Error if Index > Length(Source). procedure Replace_Element (Source : in out Bounded_String; @@ -528,6 +575,9 @@ package Ada.Strings.Bounded with SPARK_Mode is Element (Source, K) = (if K = Index then By else Element (Source'Old, K))), Global => null; + -- Updates Source such that the character at position Index in the + -- string represented by Source is By; propagates Index_Error if + -- Index > Length(Source). function Slice (Source : Bounded_String; @@ -536,6 +586,10 @@ package Ada.Strings.Bounded with SPARK_Mode is with Pre => Low - 1 <= Length (Source) and then High <= Length (Source), Global => null; + -- Returns the slice at positions Low through High in the + -- string represented by Source; propagates Index_Error if + -- Low > Length(Source)+1 or High > Length(Source). + -- The bounds of the returned string are Low and High. function Bounded_Slice (Source : Bounded_String; @@ -546,6 +600,9 @@ package Ada.Strings.Bounded with SPARK_Mode is Post => To_String (Bounded_Slice'Result) = Slice (Source, Low, High), Global => null; pragma Ada_05 (Bounded_Slice); + -- Returns the slice at positions Low through High in the string + -- represented by Source as a bounded string; propagates Index_Error + -- if Low > Length(Source)+1 or High > Length(Source). procedure Bounded_Slice (Source : Bounded_String; @@ -557,6 +614,11 @@ package Ada.Strings.Bounded with SPARK_Mode is Post => To_String (Target) = Slice (Source, Low, High), Global => null; pragma Ada_05 (Bounded_Slice); + -- Equivalent to Target := Bounded_Slice (Source, Low, High); + + -- Each of the functions "=", "<", ">", "<=", and ">=" returns the same + -- result as the corresponding String operation applied to the String + -- values given or represented by the two parameters. function "=" (Left : Bounded_String; @@ -667,6 +729,11 @@ package Ada.Strings.Bounded with SPARK_Mode is -- Search Functions -- ---------------------- + -- Each of the search subprograms (Index, Index_Non_Blank, Count, + -- Find_Token) has the same effect as the corresponding subprogram in + -- Strings.Fixed applied to the string represented by the Bounded_String + -- parameter. + function Index (Source : Bounded_String; Pattern : String; @@ -1230,6 +1297,16 @@ package Ada.Strings.Bounded with SPARK_Mode is -- String Translation Subprograms -- ------------------------------------ + -- Each of the Translate subprograms, when applied to a Bounded_String, + -- has an analogous effect to the corresponding subprogram in + -- Strings.Fixed. For the Translate function, the translation is applied + -- to the string represented by the Bounded_String parameter, and the + -- result is converted (via To_Bounded_String) to a Bounded_String. For + -- the Translate procedure, the string represented by the Bounded_String + -- parameter after the translation is given by the Translate function + -- for fixed-length strings applied to the string represented by the + -- original value of the parameter. + function Translate (Source : Bounded_String; Mapping : Maps.Character_Mapping) return Bounded_String @@ -1278,6 +1355,19 @@ package Ada.Strings.Bounded with SPARK_Mode is -- String Transformation Subprograms -- --------------------------------------- + -- Each of the transformation subprograms (Replace_Slice, Insert, + -- Overwrite, Delete), selector subprograms (Trim, Head, Tail), and + -- constructor functions ("*") has an effect based on its corresponding + -- subprogram in Strings.Fixed, and Replicate is based on Fixed."*". + -- In the case of a function, the corresponding fixed-length string + -- subprogram is applied to the string represented by the Bounded_String + -- parameter. To_Bounded_String is applied the result string, with Drop + -- (or Error in the case of Generic_Bounded_Length."*") determining + -- the effect when the string length exceeds Max_Length. In + -- the case of a procedure, the corresponding function in + -- Strings.Bounded.Generic_Bounded_Length is applied, with the + -- result assigned into the Source parameter. + function Replace_Slice (Source : Bounded_String; Low : Positive;