From patchwork Fri Aug 2 07:11:34 2024 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: =?utf-8?q?Marc_Poulhi=C3=A8s?= X-Patchwork-Id: 1968213 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@legolas.ozlabs.org Authentication-Results: legolas.ozlabs.org; dkim=pass (2048-bit key; secure) header.d=adacore.com header.i=@adacore.com header.a=rsa-sha256 header.s=google header.b=jm5VHqbj; dkim-atps=neutral Authentication-Results: legolas.ozlabs.org; spf=pass (sender SPF authorized) smtp.mailfrom=gcc.gnu.org (client-ip=8.43.85.97; helo=server2.sourceware.org; envelope-from=gcc-patches-bounces~incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=patchwork.ozlabs.org) Received: from server2.sourceware.org (server2.sourceware.org [8.43.85.97]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature ECDSA (secp384r1) server-digest SHA384) (No client certificate requested) by legolas.ozlabs.org (Postfix) with ESMTPS id 4WZy2w6tLjz1ybX for ; Fri, 2 Aug 2024 17:22:32 +1000 (AEST) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id E56AA385EC56 for ; Fri, 2 Aug 2024 07:22:30 +0000 (GMT) X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-lj1-x231.google.com (mail-lj1-x231.google.com [IPv6:2a00:1450:4864:20::231]) by sourceware.org (Postfix) with ESMTPS id 140A6385DDF3 for ; Fri, 2 Aug 2024 07:12:41 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 140A6385DDF3 Authentication-Results: sourceware.org; dmarc=pass (p=quarantine dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=adacore.com ARC-Filter: OpenARC Filter v1.0.0 sourceware.org 140A6385DDF3 Authentication-Results: server2.sourceware.org; arc=none smtp.remote-ip=2a00:1450:4864:20::231 ARC-Seal: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1722582769; cv=none; b=dlQBaxUn1D5b6QatXVhQF7kn1zORW/Ek79WVk8J9AkFjGKG6RtNG0ULjOiN1dikeLMih19Oy8byMKEfr50D+zMaILjdjKjm6ckfPzW9iaQ7A3bIOxxuue4RUJTCovVZHkvTCtbPOZmSUYlPoRiwzsk8bO19Ag9BGeuLZ0ITSahY= ARC-Message-Signature: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1722582769; c=relaxed/simple; bh=G5G1RgkslIEu2vv9ZxwgykhaFxC1FkASWgzPv9wx0Uw=; h=DKIM-Signature:From:To:Subject:Date:Message-ID:MIME-Version; b=Uyc9RIBS/AEkZtTLy4sRAtu6HTYLdsp465U3JQbLLZle/Gfl42WBL+/030g1DZtDmkYCYPLRDT018wYObDkIiO0DGGZ5K/YxQgdxJgy1w4W8TpQmHV1kK9/fky2cHvie/2+eHr78vNhUDhCdglis38AOS9FrJdv0wZqQVDqsTOI= ARC-Authentication-Results: i=1; server2.sourceware.org Received: by mail-lj1-x231.google.com with SMTP id 38308e7fff4ca-2ee920b0781so84030681fa.1 for ; Fri, 02 Aug 2024 00:12:40 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1722582759; x=1723187559; darn=gcc.gnu.org; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:from:to:cc:subject:date :message-id:reply-to; bh=HaKKrzmb1ylNVyLn4dsja04IhYO9oCoDbNqMfHbRuHg=; b=jm5VHqbjYygIooMnxNIORaXQbvOAgbLdtcB6UH0V/2oIWk8quNffHDORVJ0lzUWrun RfDM8/GrTgpYVHp8nf5lTI3y6W6XA25zNUTEkRW1DY9T86rQzUQ4eD9vVqPqviIU+F+6 t+WNKemf54i0LgCxg+IY5ymIlKWNdydeQTounUES3EkX4YPuzL+YAMMiQLnmmz1kbU3Y xYtGTin88+4uq7SzX4Lh0TBS/EBFScjaSvclU0xtt1zVg3pSC8a4/iLIDdi76dzpkCbX zRWx9APz/F5BKR+1hJcn0V9gwqiz8NfL6isrNwolbXZraB2rzEirRRmXZsr8pTqd0wUR 0OXg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1722582759; x=1723187559; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:x-gm-message-state:from:to:cc :subject:date:message-id:reply-to; bh=HaKKrzmb1ylNVyLn4dsja04IhYO9oCoDbNqMfHbRuHg=; b=FAkKLsWhZHhb4h438oxBxnQAg2Y5ji5h9ZwMoW7QRUQkR69FeW+0cRgeNK6CmGkTC2 4A6EW0jkkCsGJz2nQUXxGzq3JNg0nxpi5jHDk1dP+vZtjvR1Gj3hSIc7BPuL16ELitgm dLCaIzQuEI1ZsmcPY6rkq4JH1vD80XI1f8NQHJdTB6qx7xkBmGVjluVysw1Sx1ylN90Q ZznO0LlddD9RgJ0jLK8Vfwb76YS/pkbyC5rzhpdgBc+IOhmHM3KqcWoNYy91oVgUUuvM 5690X7fRdXQvaZvHyqdcaiM3rVPqcCS34okvq//8tMa9bZoGwLLgRVTBDJGEQFtEEJeO dgWg== X-Gm-Message-State: AOJu0YxbONrgYNceaWqlQblRpNxsDvyIAl9k0yVx/T2a7p48LV0bx7xA CGpjaPCOUVqWc8oEDrkv442PXYOlM4G/yR/d4qWW53a2e9+5MxtFCaBiMnG/WmLZhEObNhYGJUC 1AA== X-Google-Smtp-Source: AGHT+IHd+4UKTUHpa8CWf+pQ6zHBYwiClDHN6To+VGyUhnmId7ovFAOXe+Rmlgk+vkJZS/X7vramZg== X-Received: by 2002:a2e:9081:0:b0:2ef:2ed2:25b1 with SMTP id 38308e7fff4ca-2f15aaba811mr17464711fa.20.1722582756930; Fri, 02 Aug 2024 00:12:36 -0700 (PDT) Received: from localhost.localdomain ([2001:861:3382:1a90:b6aa:4751:9ea1:da1e]) by smtp.gmail.com with ESMTPSA id ffacd0b85a97d-36bbd059932sm1195770f8f.69.2024.08.02.00.12.35 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 02 Aug 2024 00:12:36 -0700 (PDT) From: =?utf-8?q?Marc_Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [COMMITTED 17/26] ada: Add contracts to Ada.Strings.Unbounded and adapt implementation Date: Fri, 2 Aug 2024 09:11:34 +0200 Message-ID: <20240802071210.413366-17-poulhies@adacore.com> X-Mailer: git-send-email 2.45.2 In-Reply-To: <20240802071210.413366-1-poulhies@adacore.com> References: <20240802071210.413366-1-poulhies@adacore.com> MIME-Version: 1.0 X-Spam-Status: No, score=-11.6 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, FILL_THIS_FORM_LOAN, GIT_PATCH_0, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.30 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: gcc-patches-bounces~incoming=patchwork.ozlabs.org@gcc.gnu.org From: Yannick Moy Add complete functional contracts to all subprograms in Ada.Strings.Unbounded, except Count, following the specification from Ada RM A.4.5. These contracts are similar to the contracts found in Ada.Strings.Fixed and Ada.Strings.Bounded. A difference is that type Unbounded_String is controlled, thus we avoid performing copies of a parameter Source with Source'Old, and instead apply 'Old attribute on the enclosing call, such as Length(Source)'Old. As Unbounded_String is controlled, the implementation is not in SPARK. Instead, we have separately proved a slightly different implementation for which Unbounded_String is not controlled, against the same specification. This ensures that the specification is consistent. To minimize differences between this test from the SPARK testsuite and the actual implementation (the one in a-strunb.adb), and to avoid overflows in the actual implementation, some code is slightly rewritten. Delete and Insert are modified to return the correct result in all cases allowed by the standard. The same contracts are added to the version in a-strunb__shared.ads and similar implementation patches are applied to the body a-strunb__shared.adb. In particular, tests are added to avoid overflows on strings for which the last index is Natural'Last, and the computations that involve Sum to guarantee that an exception is raised in case of overflow are rewritten to guarantee correct detection and no intermediate overflows (and such tests are applied consistently between the procedure and the function when both exist). gcc/ada/ * libgnat/a-strunb.adb (Sum, Saturated_Sum, Saturated_Mul): Adapt function signatures to more precise types that allow proof. (function "&"): Conditionally assign a slice to avoid possible overflow which only occurs when the assignment is a noop (because the slice is empty in that case). (Append): Same. (function "*"): Retype K to avoid a possible overflow. Add early return on null length for proof. (Delete): Fix implementation to return the correct result in all cases allowed by the Ada standard. (Insert): Same. Also avoid possible overflows. (Length): Rewrite as expression function for proof. (Overwrite): Avoid possible overflows. (Slice): Same. (To_String): Rewrite as expression function for proof. * libgnat/a-strunb.ads: Extend Assertion_Policy to new contracts used. Add complete functional contracts to all subprograms of the public API except Count. * libgnat/a-strunb__shared.adb (Sum): Adapt function signature to more precise types that allow proof. (function "&"): Conditionally assign a slice to avoid possible overflow. (function "*"): Retype K to avoid a possible overflow. (Delete): Fix implementation to return the correct result in all cases allowed by the Ada standard. (Insert): Avoid possible overflows. (Overwrite): Avoid possible overflows. (Replace_Slice): Same. (Slice): Same. (To_String): Rewrite as expression function for proof. * libgnat/a-strunb__shared.ads: Extend Assertion_Policy to new contracts used. Add complete functional contracts to all subprograms of the public API except Count. Mark public part of spec as in SPARK. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/libgnat/a-strunb.adb | 110 +-- gcc/ada/libgnat/a-strunb.ads | 1039 ++++++++++++++++++++++++-- gcc/ada/libgnat/a-strunb__shared.adb | 150 ++-- gcc/ada/libgnat/a-strunb__shared.ads | 1029 +++++++++++++++++++++++-- 4 files changed, 2068 insertions(+), 260 deletions(-) diff --git a/gcc/ada/libgnat/a-strunb.adb b/gcc/ada/libgnat/a-strunb.adb index c3d4c71271b..163906ed5cd 100644 --- a/gcc/ada/libgnat/a-strunb.adb +++ b/gcc/ada/libgnat/a-strunb.adb @@ -30,22 +30,21 @@ ------------------------------------------------------------------------------ with Ada.Strings.Fixed; -with Ada.Strings.Search; with Ada.Unchecked_Deallocation; package body Ada.Strings.Unbounded is - function Sum (Left : Natural; Right : Integer) return Natural with Inline; + function Sum (Left, Right : Natural) return Natural with Inline; -- Returns summary of Left and Right, raise Constraint_Error on overflow function Mul (Left, Right : Natural) return Natural with Inline; -- Returns multiplication of Left and Right, raise Constraint_Error on -- overflow. - function Saturated_Sum (Left : Natural; Right : Integer) return Natural; + function Saturated_Sum (Left, Right : Natural) return Natural; -- Returns summary of Left and Right or Natural'Last on overflow - function Saturated_Mul (Left, Right : Natural) return Natural; + function Saturated_Mul (Left, Right : Positive) return Positive; -- Returns multiplication of Left and Right or Natural'Last on overflow --------- @@ -67,8 +66,11 @@ package body Ada.Strings.Unbounded is Result.Reference (1 .. L_Length) := Left.Reference (1 .. Left.Last); - Result.Reference (L_Length + 1 .. Result.Last) := - Right.Reference (1 .. Right.Last); + + if L_Length < Natural'Last then + Result.Reference (L_Length + 1 .. Result.Last) := + Right.Reference (1 .. Right.Last); + end if; return Result; end "&"; @@ -86,7 +88,10 @@ package body Ada.Strings.Unbounded is Result.Reference := new String (1 .. Result.Last); Result.Reference (1 .. L_Length) := Left.Reference (1 .. Left.Last); - Result.Reference (L_Length + 1 .. Result.Last) := Right; + + if L_Length < Natural'Last then + Result.Reference (L_Length + 1 .. Result.Last) := Right; + end if; return Result; end "&"; @@ -104,8 +109,11 @@ package body Ada.Strings.Unbounded is Result.Reference := new String (1 .. Result.Last); Result.Reference (1 .. Left'Length) := Left; - Result.Reference (Left'Length + 1 .. Result.Last) := - Right.Reference (1 .. Right.Last); + + if Left'Length < Natural'Last then + Result.Reference (Left'Length + 1 .. Result.Last) := + Right.Reference (1 .. Right.Last); + end if; return Result; end "&"; @@ -170,17 +178,21 @@ package body Ada.Strings.Unbounded is Right : String) return Unbounded_String is Len : constant Natural := Right'Length; - K : Positive; + K : Natural; Result : Unbounded_String; begin + if Len = 0 then + return Null_Unbounded_String; + end if; + Result.Last := Mul (Left, Len); Result.Reference := new String (1 .. Result.Last); - K := 1; + K := 0; for J in 1 .. Left loop - Result.Reference (K .. K + Len - 1) := Right; + Result.Reference (K + 1 .. K + Len) := Right; K := K + Len; end loop; @@ -192,17 +204,21 @@ package body Ada.Strings.Unbounded is Right : Unbounded_String) return Unbounded_String is Len : constant Natural := Right.Last; - K : Positive; + K : Natural; Result : Unbounded_String; begin + if Len = 0 then + return Null_Unbounded_String; + end if; + Result.Last := Mul (Left, Len); Result.Reference := new String (1 .. Result.Last); - K := 1; + K := 0; for J in 1 .. Left loop - Result.Reference (K .. K + Len - 1) := + Result.Reference (K + 1 .. K + Len) := Right.Reference (1 .. Right.Last); K := K + Len; end loop; @@ -380,8 +396,12 @@ package body Ada.Strings.Unbounded is is begin Realloc_For_Chunk (Source, New_Item.Last); - Source.Reference (Source.Last + 1 .. Source.Last + New_Item.Last) := - New_Item.Reference (1 .. New_Item.Last); + + if Source.Last < Natural'Last then + Source.Reference (Source.Last + 1 .. Source.Last + New_Item.Last) := + New_Item.Reference (1 .. New_Item.Last); + end if; + Source.Last := Source.Last + New_Item.Last; end Append; @@ -391,8 +411,12 @@ package body Ada.Strings.Unbounded is is begin Realloc_For_Chunk (Source, New_Item'Length); - Source.Reference (Source.Last + 1 .. Source.Last + New_Item'Length) := - New_Item; + + if Source.Last < Natural'Last then + Source.Reference (Source.Last + 1 .. Source.Last + New_Item'Length) := + New_Item; + end if; + Source.Last := Source.Last + New_Item'Length; end Append; @@ -462,16 +486,20 @@ package body Ada.Strings.Unbounded is if From > Through then null; - elsif From < Source.Reference'First or else Through > Source.Last then + elsif From - 1 > Source.Last then raise Index_Error; else declare - Len : constant Natural := Through - From + 1; + Len : constant Natural := + Natural'Min (Source.Last, Through) - From + 1; begin - Source.Reference (From .. Source.Last - Len) := - Source.Reference (Through + 1 .. Source.Last); + if Through < Natural'Last then + Source.Reference (From .. Source.Last - Len) := + Source.Reference (Through + 1 .. Source.Last); + end if; + Source.Last := Source.Last - Len; end; end if; @@ -714,17 +742,19 @@ package body Ada.Strings.Unbounded is New_Item : String) is begin - if Before not in Source.Reference'First .. Source.Last + 1 then + if Before - 1 > Source.Last then raise Index_Error; end if; Realloc_For_Chunk (Source, New_Item'Length); - Source.Reference - (Before + New_Item'Length .. Source.Last + New_Item'Length) := - Source.Reference (Before .. Source.Last); + if Before <= Source.Last then + Source.Reference + (Before + New_Item'Length .. Source.Last + New_Item'Length) := + Source.Reference (Before .. Source.Last); + end if; - Source.Reference (Before .. Before + New_Item'Length - 1) := New_Item; + Source.Reference (Before .. Before - 1 + New_Item'Length) := New_Item; Source.Last := Source.Last + New_Item'Length; end Insert; @@ -733,9 +763,7 @@ package body Ada.Strings.Unbounded is ------------ function Length (Source : Unbounded_String) return Natural is - begin - return Source.Last; - end Length; + (Source.Last); --------- -- Mul -- @@ -769,8 +797,8 @@ package body Ada.Strings.Unbounded is is NL : constant Natural := New_Item'Length; begin - if Position <= Source.Last - NL + 1 then - Source.Reference (Position .. Position + NL - 1) := New_Item; + if Position - 1 <= Source.Last - NL then + Source.Reference (Position .. Position - 1 + NL) := New_Item; else declare Old : String_Access := Source.Reference; @@ -897,7 +925,7 @@ package body Ada.Strings.Unbounded is -- Saturated_Mul -- ------------------- - function Saturated_Mul (Left, Right : Natural) return Natural is + function Saturated_Mul (Left, Right : Positive) return Positive is begin return Mul (Left, Right); exception @@ -905,11 +933,11 @@ package body Ada.Strings.Unbounded is return Natural'Last; end Saturated_Mul; - ----------------- + ------------------- -- Saturated_Sum -- - ----------------- + ------------------- - function Saturated_Sum (Left : Natural; Right : Integer) return Natural is + function Saturated_Sum (Left, Right : Natural) return Natural is begin return Sum (Left, Right); exception @@ -945,7 +973,7 @@ package body Ada.Strings.Unbounded is begin -- Note: test of High > Length is in accordance with AI95-00128 - if Low > Source.Last + 1 or else High > Source.Last then + if Low - 1 > Source.Last or else High > Source.Last then raise Index_Error; else return Source.Reference (Low .. High); @@ -956,7 +984,7 @@ package body Ada.Strings.Unbounded is -- Sum -- --------- - function Sum (Left : Natural; Right : Integer) return Natural is + function Sum (Left, Right : Natural) return Natural is pragma Unsuppress (Overflow_Check); begin return Left + Right; @@ -993,9 +1021,7 @@ package body Ada.Strings.Unbounded is --------------- function To_String (Source : Unbounded_String) return String is - begin - return Source.Reference (1 .. Source.Last); - end To_String; + (Source.Reference (1 .. Source.Last)); ------------------------- -- To_Unbounded_String -- diff --git a/gcc/ada/libgnat/a-strunb.ads b/gcc/ada/libgnat/a-strunb.ads index 385544ecb57..981f406a767 100644 --- a/gcc/ada/libgnat/a-strunb.ads +++ b/gcc/ada/libgnat/a-strunb.ads @@ -35,12 +35,18 @@ -- Preconditions in this unit are meant for analysis only, not for run-time -- checking, so that the expected exceptions are raised. This is enforced by --- setting the corresponding assertion policy to Ignore. +-- setting the corresponding assertion policy to Ignore. Postconditions and +-- contract cases should not be executed at runtime as well, in order not to +-- slow down the execution of these functions. -pragma Assertion_Policy (Pre => Ignore); +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore); -with Ada.Strings.Maps; +with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; with Ada.Finalization; +with Ada.Strings.Search; private with Ada.Strings.Text_Buffers; -- The language-defined package Strings.Unbounded provides a private type @@ -59,6 +65,13 @@ package Ada.Strings.Unbounded with is pragma Preelaborate; + -- Contracts may call function Length in the prefix of attribute reference + -- to Old as in Length (Source)'Old. Allow this use. + + pragma Unevaluated_Use_Of_Old (Allow); + + subtype String_1 is String (1 .. <>) with Ghost; -- Type used in contracts + type Unbounded_String is private with Default_Initial_Condition => Length (Unbounded_String) = 0; pragma Preelaborable_Initialization (Unbounded_String); @@ -84,9 +97,10 @@ is -------------------------------------------------------- function To_Unbounded_String - (Source : String) return Unbounded_String + (Source : String) return Unbounded_String with - Post => To_String (To_Unbounded_String'Result) = Source, + Post => To_String (To_Unbounded_String'Result) = Source + and then Length (To_Unbounded_String'Result) = Source'Length, Global => null; -- Returns an Unbounded_String that represents Source @@ -126,7 +140,8 @@ is New_Item : Unbounded_String) with Pre => Length (New_Item) <= Natural'Last - Length (Source), - Post => Length (Source) = Length (Source)'Old + Length (New_Item), + Post => + To_String (Source) = To_String (Source)'Old & To_String (New_Item), Global => null; procedure Append @@ -134,7 +149,7 @@ is New_Item : String) with Pre => New_Item'Length <= Natural'Last - Length (Source), - Post => Length (Source) = Length (Source)'Old + New_Item'Length, + Post => To_String (Source) = To_String (Source)'Old & New_Item, Global => null; procedure Append @@ -142,7 +157,7 @@ is New_Item : Character) with Pre => Length (Source) < Natural'Last, - Post => Length (Source) = Length (Source)'Old + 1, + Post => To_String (Source) = To_String (Source)'Old & New_Item, Global => null; -- For each of the Append procedures, the resulting string represented by @@ -154,7 +169,7 @@ is Right : Unbounded_String) return Unbounded_String with Pre => Length (Right) <= Natural'Last - Length (Left), - Post => Length ("&"'Result) = Length (Left) + Length (Right), + Post => To_String ("&"'Result) = To_String (Left) & To_String (Right), Global => null; function "&" @@ -162,7 +177,7 @@ is Right : String) return Unbounded_String with Pre => Right'Length <= Natural'Last - Length (Left), - Post => Length ("&"'Result) = Length (Left) + Right'Length, + Post => To_String ("&"'Result) = To_String (Left) & Right, Global => null; function "&" @@ -170,7 +185,7 @@ is Right : Unbounded_String) return Unbounded_String with Pre => Left'Length <= Natural'Last - Length (Right), - Post => Length ("&"'Result) = Left'Length + Length (Right), + Post => To_String ("&"'Result) = String_1 (Left) & To_String (Right), Global => null; function "&" @@ -178,7 +193,7 @@ is Right : Character) return Unbounded_String with Pre => Length (Left) < Natural'Last, - Post => Length ("&"'Result) = Length (Left) + 1, + Post => To_String ("&"'Result) = To_String (Left) & Right, Global => null; function "&" @@ -186,7 +201,7 @@ is Right : Unbounded_String) return Unbounded_String with Pre => Length (Right) < Natural'Last, - Post => Length ("&"'Result) = Length (Right) + 1, + Post => To_String ("&"'Result) = Left & To_String (Right), Global => null; -- Each of the "&" functions returns an Unbounded_String obtained by @@ -211,7 +226,8 @@ is By : Character) with Pre => Index <= Length (Source), - Post => Length (Source) = Length (Source)'Old, + Post => + To_String (Source) = (To_String (Source)'Old with delta Index => By), Global => null; -- Updates Source such that the character at position Index in the string -- represented by Source is By; propagates Index_Error if @@ -223,7 +239,9 @@ is High : Natural) return String with Pre => Low - 1 <= Length (Source) and then High <= Length (Source), - Post => Slice'Result'Length = Natural'Max (0, High - Low + 1), + Post => Slice'Result'First = Low + and then Slice'Result'Last = High + and then Slice'Result = To_String (Source) (Low .. High), Global => null; -- Returns the slice at positions Low through High in the string -- represented by Source; propagates Index_Error if @@ -237,7 +255,7 @@ is with Pre => Low - 1 <= Length (Source) and then High <= Length (Source), Post => - Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1), + To_String (Unbounded_Slice'Result) = To_String (Source) (Low .. High), Global => null; pragma Ada_05 (Unbounded_Slice); -- Returns the slice at positions Low through High in the string @@ -251,7 +269,7 @@ is High : Natural) with Pre => Low - 1 <= Length (Source) and then High <= Length (Source), - Post => Length (Target) = Natural'Max (0, High - Low + 1), + Post => To_String (Target) = To_String (Source) (Low .. High), Global => null; pragma Ada_05 (Unbounded_Slice); -- Sets Target to the Unbounded_String representing the slice at positions @@ -283,72 +301,84 @@ is (Left : Unbounded_String; Right : Unbounded_String) return Boolean with + Post => "<"'Result = (To_String (Left) < To_String (Right)), Global => null; function "<" (Left : Unbounded_String; Right : String) return Boolean with + Post => "<"'Result = (To_String (Left) < Right), Global => null; function "<" (Left : String; Right : Unbounded_String) return Boolean with + Post => "<"'Result = (Left < To_String (Right)), Global => null; function "<=" (Left : Unbounded_String; Right : Unbounded_String) return Boolean with + Post => "<="'Result = (To_String (Left) <= To_String (Right)), Global => null; function "<=" (Left : Unbounded_String; Right : String) return Boolean with + Post => "<="'Result = (To_String (Left) <= Right), Global => null; function "<=" (Left : String; Right : Unbounded_String) return Boolean with + Post => "<="'Result = (Left <= To_String (Right)), Global => null; function ">" (Left : Unbounded_String; Right : Unbounded_String) return Boolean with + Post => ">"'Result = (To_String (Left) > To_String (Right)), Global => null; function ">" (Left : Unbounded_String; Right : String) return Boolean with + Post => ">"'Result = (To_String (Left) > Right), Global => null; function ">" (Left : String; Right : Unbounded_String) return Boolean with + Post => ">"'Result = (Left > To_String (Right)), Global => null; function ">=" (Left : Unbounded_String; Right : Unbounded_String) return Boolean with + Post => ">="'Result = (To_String (Left) >= To_String (Right)), Global => null; function ">=" (Left : Unbounded_String; Right : String) return Boolean with + Post => ">="'Result = (To_String (Left) >= Right), Global => null; function ">=" (Left : String; Right : Unbounded_String) return Boolean with + Post => ">="'Result = (Left >= To_String (Right)), Global => null; -- Each of the functions "=", "<", ">", "<=", and ">=" returns the same @@ -365,8 +395,52 @@ is Going : Direction := Forward; Mapping : Maps.Character_Mapping := Maps.Identity) return Natural with - Pre => Pattern'Length /= 0, - Global => null; + Pre => Pattern'Length > 0, + Post => Index'Result <= Length (Source), + Contract_Cases => + + -- If Source is the empty string, then 0 is returned + + (Length (Source) = 0 + => + Index'Result = 0, + + -- If some slice of Source matches Pattern, then a valid index is + -- returned. + + Length (Source) > 0 + and then + (for some J in 1 .. Length (Source) - (Pattern'Length - 1) => + Search.Match (To_String (Source), Pattern, Mapping, J)) + => + -- The result is in the considered range of Source + + Index'Result in 1 .. Length (Source) - (Pattern'Length - 1) + + -- The slice beginning at the returned index matches Pattern + + and then Search.Match + (To_String (Source), Pattern, Mapping, Index'Result) + + -- The result is the smallest or largest index which satisfies + -- the matching, respectively when Going = Forward and Going = + -- Backward. + + and then + (for all J in 1 .. Length (Source) => + (if (if Going = Forward + then J <= Index'Result - 1 + else J - 1 in Index'Result + .. Length (Source) - Pattern'Length) + then not (Search.Match + (To_String (Source), Pattern, Mapping, J)))), + + -- Otherwise, 0 is returned + + others + => + Index'Result = 0), + Global => null; function Index (Source : Unbounded_String; @@ -374,8 +448,52 @@ is Going : Direction := Forward; Mapping : Maps.Character_Mapping_Function) return Natural with - Pre => Pattern'Length /= 0, - Global => null; + Pre => Pattern'Length /= 0 and then Mapping /= null, + Post => Index'Result <= Length (Source), + Contract_Cases => + + -- If Source is the empty string, then 0 is returned + + (Length (Source) = 0 + => + Index'Result = 0, + + -- If some slice of Source matches Pattern, then a valid index is + -- returned. + + Length (Source) > 0 + and then + (for some J in 1 .. Length (Source) - (Pattern'Length - 1) => + Search.Match (To_String (Source), Pattern, Mapping, J)) + => + -- The result is in the considered range of Source + + Index'Result in 1 .. Length (Source) - (Pattern'Length - 1) + + -- The slice beginning at the returned index matches Pattern + + and then Search.Match + (To_String (Source), Pattern, Mapping, Index'Result) + + -- The result is the smallest or largest index which satisfies + -- the matching, respectively when Going = Forward and Going = + -- Backward. + + and then + (for all J in 1 .. Length (Source) => + (if (if Going = Forward + then J <= Index'Result - 1 + else J - 1 in Index'Result + .. Length (Source) - Pattern'Length) + then not (Search.Match + (To_String (Source), Pattern, Mapping, J)))), + + -- Otherwise, 0 is returned + + others + => + Index'Result = 0), + Global => null; function Index (Source : Unbounded_String; @@ -383,7 +501,43 @@ is Test : Membership := Inside; Going : Direction := Forward) return Natural with - Global => null; + Post => Index'Result <= Length (Source), + Contract_Cases => + + -- If no character of Source satisfies the property Test on Set, + -- then 0 is returned. + + ((for all C of To_String (Source) => + (Test = Inside) /= Maps.Is_In (C, Set)) + => + Index'Result = 0, + + -- Otherwise, an index in the range of Source is returned + + others + => + -- The result is in the range of Source + + Index'Result in 1 .. Length (Source) + + -- The character at the returned index satisfies the property + -- Test on Set. + + and then + (Test = Inside) = + Maps.Is_In (Element (Source, Index'Result), Set) + + -- The result is the smallest or largest index which satisfies + -- the property, respectively when Going = Forward and Going = + -- Backward. + + and then + (for all J in 1 .. Length (Source) => + (if J /= Index'Result + and then (J < Index'Result) = (Going = Forward) + then (Test = Inside) + /= Maps.Is_In (Element (Source, J), Set)))), + Global => null; function Index (Source : Unbounded_String; @@ -392,9 +546,60 @@ is Going : Direction := Forward; Mapping : Maps.Character_Mapping := Maps.Identity) return Natural with - Pre => (if Length (Source) /= 0 then From <= Length (Source)) - and then Pattern'Length /= 0, - Global => null; + Pre => + (if Length (Source) /= 0 then From <= Length (Source)) + and then Pattern'Length /= 0, + Post => Index'Result <= Length (Source), + Contract_Cases => + + -- If Source is the empty string, then 0 is returned + + (Length (Source) = 0 + => + Index'Result = 0, + + -- If some slice of Source matches Pattern, then a valid index is + -- returned. + + Length (Source) > 0 + and then + (for some J in + (if Going = Forward then From else 1) + .. (if Going = Forward then Length (Source) else From) + - (Pattern'Length - 1) => + Search.Match (To_String (Source), Pattern, Mapping, J)) + => + -- The result is in the considered range of Source + + Index'Result in + (if Going = Forward then From else 1) + .. (if Going = Forward then Length (Source) else From) + - (Pattern'Length - 1) + + -- The slice beginning at the returned index matches Pattern + + and then Search.Match + (To_String (Source), Pattern, Mapping, Index'Result) + + -- The result is the smallest or largest index which satisfies + -- the matching, respectively when Going = Forward and Going = + -- Backward. + + and then + (for all J in 1 .. Length (Source) => + (if (if Going = Forward + then J in From .. Index'Result - 1 + else J - 1 in Index'Result + .. From - Pattern'Length) + then not (Search.Match + (To_String (Source), Pattern, Mapping, J)))), + + -- Otherwise, 0 is returned + + others + => + Index'Result = 0), + Global => null; pragma Ada_05 (Index); function Index @@ -404,9 +609,61 @@ is Going : Direction := Forward; Mapping : Maps.Character_Mapping_Function) return Natural with - Pre => (if Length (Source) /= 0 then From <= Length (Source)) - and then Pattern'Length /= 0, - Global => null; + Pre => + (if Length (Source) /= 0 then From <= Length (Source)) + and then Pattern'Length /= 0 + and then Mapping /= null, + Post => Index'Result <= Length (Source), + Contract_Cases => + + -- If Source is the empty string, then 0 is returned + + (Length (Source) = 0 + => + Index'Result = 0, + + -- If some slice of Source matches Pattern, then a valid index is + -- returned. + + Length (Source) > 0 + and then + (for some J in + (if Going = Forward then From else 1) + .. (if Going = Forward then Length (Source) else From) + - (Pattern'Length - 1) => + Search.Match (To_String (Source), Pattern, Mapping, J)) + => + -- The result is in the considered range of Source + + Index'Result in + (if Going = Forward then From else 1) + .. (if Going = Forward then Length (Source) else From) + - (Pattern'Length - 1) + + -- The slice beginning at the returned index matches Pattern + + and then Search.Match + (To_String (Source), Pattern, Mapping, Index'Result) + + -- The result is the smallest or largest index which satisfies + -- the matching, respectively when Going = Forward and Going = + -- Backward. + + and then + (for all J in 1 .. Length (Source) => + (if (if Going = Forward + then J in From .. Index'Result - 1 + else J - 1 in Index'Result + .. From - Pattern'Length) + then not (Search.Match + (To_String (Source), Pattern, Mapping, J)))), + + -- Otherwise, 0 is returned + + others + => + Index'Result = 0), + Global => null; pragma Ada_05 (Index); function Index @@ -416,23 +673,147 @@ is Test : Membership := Inside; Going : Direction := Forward) return Natural with - Pre => (if Length (Source) /= 0 then From <= Length (Source)), - Global => null; + Pre => + (if Length (Source) /= 0 then From <= Length (Source)), + Post => Index'Result <= Length (Source), + Contract_Cases => + + -- If Source is the empty string, or no character of the considered + -- slice of Source satisfies the property Test on Set, then 0 is + -- returned. + + (Length (Source) = 0 + or else + (for all J in 1 .. Length (Source) => + (if J = From or else (J > From) = (Going = Forward) then + (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))) + => + Index'Result = 0, + + -- Otherwise, an index in the considered range of Source is + -- returned. + + others + => + -- The result is in the considered range of Source + + Index'Result in 1 .. Length (Source) + and then + (Index'Result = From + or else (Index'Result > From) = (Going = Forward)) + + -- The character at the returned index satisfies the property + -- Test on Set. + + and then + (Test = Inside) = + Maps.Is_In (Element (Source, Index'Result), Set) + + -- The result is the smallest or largest index which satisfies + -- the property, respectively when Going = Forward and Going = + -- Backward. + + and then + (for all J in 1 .. Length (Source) => + (if J /= Index'Result + and then (J < Index'Result) = (Going = Forward) + and then (J = From + or else (J > From) = (Going = Forward)) + then (Test = Inside) + /= Maps.Is_In (Element (Source, J), Set)))), + Global => null; pragma Ada_05 (Index); function Index_Non_Blank (Source : Unbounded_String; Going : Direction := Forward) return Natural with - Global => null; + Post => Index_Non_Blank'Result <= Length (Source), + Contract_Cases => + + -- If all characters of Source are Space characters, then 0 is + -- returned. + + ((for all C of To_String (Source) => C = ' ') + => + Index_Non_Blank'Result = 0, + + -- Otherwise, an index in the range of Source is returned + + others + => + -- The result is in the range of Source + + Index_Non_Blank'Result in 1 .. Length (Source) + + -- The character at the returned index is not a Space character + + and then Element (Source, Index_Non_Blank'Result) /= ' ' + + -- The result is the smallest or largest index which is not a + -- Space character, respectively when Going = Forward and Going + -- = Backward. + + and then + (for all J in 1 .. Length (Source) => + (if J /= Index_Non_Blank'Result + and then + (J < Index_Non_Blank'Result) = (Going = Forward) + then Element (Source, J) = ' '))), + Global => null; function Index_Non_Blank (Source : Unbounded_String; From : Positive; Going : Direction := Forward) return Natural with - Pre => (if Length (Source) /= 0 then From <= Length (Source)), - Global => null; + Pre => + (if Length (Source) /= 0 then From <= Length (Source)), + Post => Index_Non_Blank'Result <= Length (Source), + Contract_Cases => + + -- If Source is the empty string, or all characters of the + -- considered slice of Source are Space characters, then 0 + -- is returned. + + (Length (Source) = 0 + or else + (for all J in 1 .. Length (Source) => + (if J = From or else (J > From) = (Going = Forward) then + Element (Source, J) = ' ')) + => + Index_Non_Blank'Result = 0, + + -- Otherwise, an index in the considered range of Source is + -- returned. + + others + => + -- The result is in the considered range of Source + + Index_Non_Blank'Result in 1 .. Length (Source) + and then + (Index_Non_Blank'Result = From + or else + (Index_Non_Blank'Result > From) = (Going = Forward)) + + -- The character at the returned index is not a Space character + + and then Element (Source, Index_Non_Blank'Result) /= ' ' + + -- The result is the smallest or largest index which isn't a + -- Space character, respectively when Going = Forward and Going + -- = Backward. + + and then + (for all J in 1 .. Length (Source) => + (if J /= Index_Non_Blank'Result + and then + (J < Index_Non_Blank'Result) = (Going = Forward) + and then (J = From + or else (J > From) = (Going = Forward)) + then Element (Source, J) = ' '))), + Global => null; pragma Ada_05 (Index_Non_Blank); function Count @@ -448,7 +829,7 @@ is Pattern : String; Mapping : Maps.Character_Mapping_Function) return Natural with - Pre => Pattern'Length /= 0, + Pre => Pattern'Length /= 0 and then Mapping /= null, Global => null; function Count @@ -465,8 +846,53 @@ is First : out Positive; Last : out Natural) with - Pre => (if Length (Source) /= 0 then From <= Length (Source)), - Global => null; + Pre => + (if Length (Source) /= 0 then From <= Length (Source)), + Contract_Cases => + + -- If Source is the empty string, or if no character of the + -- considered slice of Source satisfies the property Test on + -- Set, then First is set to From and Last is set to 0. + + (Length (Source) = 0 + or else + (for all J in From .. Length (Source) => + (Test = Inside) /= Maps.Is_In (Element (Source, J), Set)) + => + First = From and then Last = 0, + + -- Otherwise, First and Last are set to valid indexes + + others + => + -- First and Last are in the considered range of Source + + First in From .. Length (Source) + and then Last in First .. Length (Source) + + -- No character between From and First satisfies the property + -- Test on Set. + + and then + (for all J in From .. First - 1 => + (Test = Inside) /= Maps.Is_In (Element (Source, J), Set)) + + -- All characters between First and Last satisfy the property + -- Test on Set. + + and then + (for all J in First .. Last => + (Test = Inside) = Maps.Is_In (Element (Source, J), Set)) + + -- If Last is not Source'Last, then the character at position + -- Last + 1 does not satify the property Test on Set. + + and then + (if Last < Length (Source) + then + (Test = Inside) + /= Maps.Is_In (Element (Source, Last + 1), Set))), + Global => null; pragma Ada_2012 (Find_Token); procedure Find_Token @@ -476,7 +902,51 @@ is First : out Positive; Last : out Natural) with - Global => null; + Contract_Cases => + + -- If Source is the empty string, or if no character of the + -- considered slice of Source satisfies the property Test on + -- Set, then First is set to 1 and Last is set to 0. + + (Length (Source) = 0 + or else + (for all J in 1 .. Length (Source) => + (Test = Inside) /= Maps.Is_In (Element (Source, J), Set)) + => + First = 1 and then Last = 0, + + -- Otherwise, First and Last are set to valid indexes + + others + => + -- First and Last are in the considered range of Source + + First in 1 .. Length (Source) + and then Last in First .. Length (Source) + + -- No character between 1 and First satisfies the property Test + -- on Set. + + and then + (for all J in 1 .. First - 1 => + (Test = Inside) /= Maps.Is_In (Element (Source, J), Set)) + + -- All characters between First and Last satisfy the property + -- Test on Set. + + and then + (for all J in First .. Last => + (Test = Inside) = Maps.Is_In (Element (Source, J), Set)) + + -- If Last is not Source'Last, then the character at position + -- Last + 1 does not satify the property Test on Set. + + and then + (if Last < Length (Source) + then + (Test = Inside) + /= Maps.Is_In (Element (Source, Last + 1), Set))), + Global => null; -- Each of the search subprograms (Index, Index_Non_Blank, Count, -- Find_Token) has the same effect as the corresponding subprogram in @@ -491,28 +961,44 @@ is (Source : Unbounded_String; Mapping : Maps.Character_Mapping) return Unbounded_String with - Post => Length (Translate'Result) = Length (Source), + Post => Length (Translate'Result) = Length (Source) + and then + (for all K in 1 .. Length (Source) => + Element (Translate'Result, K) = + Ada.Strings.Maps.Value (Mapping, Element (Source, K))), Global => null; procedure Translate (Source : in out Unbounded_String; Mapping : Maps.Character_Mapping) with - Post => Length (Source) = Length (Source)'Old, + Post => Length (Source) = Length (Source)'Old + and then + (for all K in 1 .. Length (Source) => + Element (Source, K) = + Ada.Strings.Maps.Value (Mapping, To_String (Source)'Old (K))), Global => null; function Translate (Source : Unbounded_String; Mapping : Maps.Character_Mapping_Function) return Unbounded_String with - Post => Length (Translate'Result) = Length (Source), + Pre => Mapping /= null, + Post => Length (Translate'Result) = Length (Source) + and then + (for all K in 1 .. Length (Source) => + Element (Translate'Result, K) = Mapping (Element (Source, K))), Global => null; procedure Translate (Source : in out Unbounded_String; Mapping : Maps.Character_Mapping_Function) with - Post => Length (Source) = Length (Source)'Old, + Pre => Mapping /= null, + Post => Length (Source) = Length (Source)'Old + and then + (for all K in 1 .. Length (Source) => + Element (Source, K) = Mapping (To_String (Source)'Old (K))), Global => null; -- The Translate function has an analogous effect to the corresponding @@ -535,15 +1021,76 @@ is and then (if High >= Low then Low - 1 <= Natural'Last - By'Length - - Natural'Max (Length (Source) - High, 0) + - Integer'Max (Length (Source) - High, 0) else Length (Source) <= Natural'Last - By'Length), Contract_Cases => + + -- If High >= Low, when considering the application of To_String to + -- convert an Unbounded_String into String, then the returned string + -- comprises Source (Source'First .. Low - 1) & By + -- & Source(High + 1 .. Source'Last). + (High >= Low => + + -- Length of the returned string + Length (Replace_Slice'Result) - = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0), + = Low - 1 + By'Length + Integer'Max (Length (Source) - High, 0) + + -- Elements starting at Low are replaced by elements of By + + and then + Slice (Replace_Slice'Result, 1, Low - 1) = + Slice (Source, 1, Low - 1) + and then + Slice (Replace_Slice'Result, Low, Low - 1 + By'Length) = By + + -- When there are remaining characters after the replaced slice, + -- they are appended to the result. + + and then + (if High < Length (Source) + then + Slice (Replace_Slice'Result, + Low + By'Length, Length (Replace_Slice'Result)) = + Slice (Source, High + 1, Length (Source))), + + -- If High < Low, then the returned string is + -- Insert (Source, Before => Low, New_Item => By). + others => - Length (Replace_Slice'Result) = Length (Source)'Old + By'Length), + + -- Length of the returned string + + Length (Replace_Slice'Result) = Length (Source) + By'Length + + -- Elements of By are inserted after the element at Low + + and then + Slice (Replace_Slice'Result, 1, Low - 1) = + Slice (Source, 1, Low - 1) + and then + Slice (Replace_Slice'Result, Low, Low - 1 + By'Length) = By + + -- When there are remaining characters after Low in Source, they + -- are appended to the result. + + and then + (if Low < Length (Source) + then + Slice (Replace_Slice'Result, + Low + By'Length, Length (Replace_Slice'Result)) = + Slice (Source, Low, Length (Source)))), Global => null; + -- If Low > Source'Last + 1, or High < Source'First - 1, then Index_Error + -- is propagated. Otherwise: + -- + -- * If High >= Low, then the returned string comprises + -- Source (Source'First .. Low - 1) + -- & By & Source(High + 1 .. Source'Last), but with lower bound 1. + -- + -- * If High < Low, then the returned string is + -- Insert (Source, Before => Low, New_Item => By). procedure Replace_Slice (Source : in out Unbounded_String; @@ -559,11 +1106,61 @@ is - Natural'Max (Length (Source) - High, 0) else Length (Source) <= Natural'Last - By'Length), Contract_Cases => + + -- If High >= Low, when considering the application of To_String to + -- convert an Unbounded_String into String, then the returned string + -- comprises Source (Source'First .. Low - 1) & By + -- & Source(High + 1 .. Source'Last). + (High >= Low => + + -- Length of the returned string + Length (Source) - = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0), + = Low - 1 + By'Length + Integer'Max (Length (Source)'Old - High, 0) + + -- Elements starting at Low are replaced by elements of By + + and then Slice (Source, 1, Low - 1) = + Slice (Source, 1, Low - 1)'Old + and then Slice (Source, Low, Low - 1 + By'Length) = By + + -- When there are remaining characters after the replaced slice, + -- they are appended to the result. + + and then + (if High < Length (Source)'Old + then Slice (Source, Low + By'Length, Length (Source)) = + Slice (Source, + -- Really "High + 1" but expressed with a conditional + -- repeating the above test so that the call to Slice + -- is valid on entry (under 'Old) even when the test + -- evaluates to False. + (if High < Length (Source) then High + 1 else 1), + Length (Source))'Old), + + -- If High < Low, then the returned string is + -- Insert (Source, Before => Low, New_Item => By). + others => - Length (Source) = Length (Source)'Old + By'Length), + + -- Length of the returned string + + Length (Source) = Length (Source)'Old + By'Length + + -- Elements of By are inserted after the element at Low + + and then Slice (Source, 1, Low - 1) = + Slice (Source, 1, Low - 1)'Old + and then Slice (Source, Low, Low - 1 + By'Length) = By + + -- When there are remaining characters after Low in Source, they + -- are appended to the result. + + and then + (if Low < Length (Source)'Old + then Slice (Source, Low + By'Length, Length (Source)) = + Slice (Source, Low, Length (Source))'Old)), Global => null; function Insert @@ -573,8 +1170,32 @@ is with Pre => Before - 1 <= Length (Source) and then New_Item'Length <= Natural'Last - Length (Source), - Post => Length (Insert'Result) = Length (Source) + New_Item'Length, + Post => + -- Length of the returned string + + Length (Insert'Result) = Length (Source) + New_Item'Length + + -- Elements of New_Item are inserted after element at Before + + and then + Slice (Insert'Result, 1, Before - 1) = Slice (Source, 1, Before - 1) + and then + Slice (Insert'Result, Before, Before - 1 + New_Item'Length) + = New_Item + + -- When there are remaining characters after Before in Source, they + -- are appended to the returned string. + + and then + (if Before <= Length (Source) then + Slice (Insert'Result, Before + New_Item'Length, + Length (Insert'Result)) = + Slice (Source, Before, Length (Source))), Global => null; + -- Propagates Index_Error if Before is not in + -- Source'First .. Source'Last + 1; otherwise, returns + -- Source (Source'First .. Before - 1) + -- & New_Item & Source(Before..Source'Last), but with lower bound 1. procedure Insert (Source : in out Unbounded_String; @@ -583,7 +1204,25 @@ is with Pre => Before - 1 <= Length (Source) and then New_Item'Length <= Natural'Last - Length (Source), - Post => Length (Source) = Length (Source)'Old + New_Item'Length, + Post => + -- Length of the returned string + + Length (Source) = Length (Source)'Old + New_Item'Length + + -- Elements of New_Item are inserted after element at Before + + and then + Slice (Source, 1, Before - 1) = Slice (Source, 1, Before - 1)'Old + and then + Slice (Source, Before, Before - 1 + New_Item'Length) = New_Item + + -- When there are remaining characters after Before in Source, they + -- are appended to the returned string. + + and then + (if Before <= Length (Source)'Old then + Slice (Source, Before + New_Item'Length, Length (Source)) = + Slice (Source, Before, Length (Source))'Old), Global => null; function Overwrite @@ -592,12 +1231,31 @@ is New_Item : String) return Unbounded_String with Pre => Position - 1 <= Length (Source) - and then (if New_Item'Length /= 0 - then - New_Item'Length <= Natural'Last - (Position - 1)), + and then New_Item'Length <= Natural'Last - (Position - 1), Post => - Length (Overwrite'Result) - = Natural'Max (Length (Source), Position - 1 + New_Item'Length), + -- Length of the returned string + + Length (Overwrite'Result) = + Integer'Max (Length (Source), Position - 1 + New_Item'Length) + + -- Elements after Position are replaced by elements of New_Item + + and then + Slice (Overwrite'Result, 1, Position - 1) = + Slice (Source, 1, Position - 1) + and then + Slice (Overwrite'Result, Position, Position - 1 + New_Item'Length) = + New_Item + and then + (if Position - 1 + New_Item'Length < Length (Source) then + + -- There are some unchanged characters of Source remaining + -- after New_Item. + + Slice (Overwrite'Result, + Position + New_Item'Length, Length (Source)) = + Slice (Source, + Position + New_Item'Length, Length (Source))), Global => null; procedure Overwrite @@ -606,13 +1264,36 @@ is New_Item : String) with Pre => Position - 1 <= Length (Source) - and then (if New_Item'Length /= 0 - then - New_Item'Length <= Natural'Last - (Position - 1)), + and then New_Item'Length <= Natural'Last - (Position - 1), Post => - Length (Source) - = Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length), + -- Length of the returned string + + Length (Source) = + Integer'Max (Length (Source)'Old, Position - 1 + New_Item'Length) + + -- Elements after Position are replaced by elements of New_Item + + and then + Slice (Source, 1, Position - 1) = Slice (Source, 1, Position - 1) + and then + Slice (Source, Position, Position - 1 + New_Item'Length) = New_Item + and then + (if Position - 1 + New_Item'Length < Length (Source)'Old then + + -- There are some unchanged characters of Source remaining + -- after New_Item. + Slice (Source, + Position + New_Item'Length, Length (Source)'Old) = + Slice (Source, + -- Really "Position + New_Item'Length" but expressed with + -- a conditional repeating the above test so that the + -- call to Slice is valid on entry (under 'Old) even + -- when the test evaluates to False. + (if Position - 1 + New_Item'Length < Length (Source) + then Position + New_Item'Length + else 1), + Length (Source))'Old), Global => null; function Delete @@ -620,12 +1301,19 @@ is From : Positive; Through : Natural) return Unbounded_String with - Pre => (if Through <= From then From - 1 <= Length (Source)), + Pre => (if Through >= From then From - 1 <= Length (Source)), Contract_Cases => (Through >= From => - Length (Delete'Result) = Length (Source) - (Through - From + 1), + Length (Delete'Result) = + From - 1 + Natural'Max (Length (Source) - Through, 0) + and then + Slice (Delete'Result, 1, From - 1) = Slice (Source, 1, From - 1) + and then + (if Through < Length (Source) then + Slice (Delete'Result, From, Length (Delete'Result)) = + Slice (Source, Through + 1, Length (Source))), others => - Length (Delete'Result) = Length (Source)), + Delete'Result = Source), Global => null; procedure Delete @@ -633,82 +1321,255 @@ is From : Positive; Through : Natural) with - Pre => (if Through <= From then From - 1 <= Length (Source)), + Pre => (if Through >= From then From - 1 <= Length (Source)), Contract_Cases => (Through >= From => - Length (Source) = Length (Source)'Old - (Through - From + 1), + Length (Source) = + From - 1 + Natural'Max (Length (Source)'Old - Through, 0) + and then + Slice (Source, 1, From - 1) = + To_String (Source)'Old (1 .. From - 1) + and then + (if Through < Length (Source) then + Slice (Source, From, Length (Source)) = + To_String (Source)'Old (Through + 1 .. Length (Source)'Old)), others => - Length (Source) = Length (Source)'Old), + To_String (Source) = To_String (Source)'Old), Global => null; function Trim (Source : Unbounded_String; Side : Trim_End) return Unbounded_String with - Post => Length (Trim'Result) <= Length (Source), - Global => null; + Contract_Cases => + -- If all characters in Source are Space, the returned string is + -- empty. + + ((for all C of To_String (Source) => C = ' ') + => + Length (Trim'Result) = 0, + + -- Otherwise, the returned string is a slice of Source + + others + => + (declare + Low : constant Positive := + (if Side = Right then 1 + else Index_Non_Blank (Source, Forward)); + High : constant Positive := + (if Side = Left then Length (Source) + else Index_Non_Blank (Source, Backward)); + begin + To_String (Trim'Result) = Slice (Source, Low, High))), + Global => null; procedure Trim (Source : in out Unbounded_String; Side : Trim_End) with - Post => Length (Source) <= Length (Source)'Old, - Global => null; + Contract_Cases => + -- If all characters in Source are Space, the returned string is + -- empty. + + ((for all C of To_String (Source) => C = ' ') + => + Length (Source) = 0, + + -- Otherwise, the returned string is a slice of Source + + others + => + (declare + Low : constant Positive := + (if Side = Right then 1 + else Index_Non_Blank (Source, Forward)'Old); + High : constant Positive := + (if Side = Left then Length (Source)'Old + else Index_Non_Blank (Source, Backward)'Old); + begin + To_String (Source) = To_String (Source)'Old (Low .. High))), + Global => null; function Trim (Source : Unbounded_String; Left : Maps.Character_Set; Right : Maps.Character_Set) return Unbounded_String with - Post => Length (Trim'Result) <= Length (Source), - Global => null; + Contract_Cases => + -- If all characters in Source are contained in one of the sets Left + -- or Right, then the returned string is empty. + + ((for all C of To_String (Source) => Maps.Is_In (C, Left)) + or else + (for all C of To_String (Source) => Maps.Is_In (C, Right)) + => + Length (Trim'Result) = 0, + + -- Otherwise, the returned string is a slice of Source + + others + => + (declare + Low : constant Positive := + Index (Source, Left, Outside, Forward); + High : constant Positive := + Index (Source, Right, Outside, Backward); + begin + To_String (Trim'Result) = Slice (Source, Low, High))), + Global => null; procedure Trim (Source : in out Unbounded_String; Left : Maps.Character_Set; Right : Maps.Character_Set) with - Post => Length (Source) <= Length (Source)'Old, - Global => null; + Contract_Cases => + -- If all characters in Source are contained in one of the sets Left + -- or Right, then the returned string is empty. + + ((for all C of To_String (Source) => Maps.Is_In (C, Left)) + or else + (for all C of To_String (Source) => Maps.Is_In (C, Right)) + => + Length (Source) = 0, + + -- Otherwise, the returned string is a slice of Source + + others + => + (declare + Low : constant Positive := + Index (Source, Left, Outside, Forward)'Old; + High : constant Positive := + Index (Source, Right, Outside, Backward)'Old; + begin + To_String (Source) = To_String (Source)'Old (Low .. High))), + Global => null; function Head (Source : Unbounded_String; Count : Natural; Pad : Character := Space) return Unbounded_String with - Post => Length (Head'Result) = Count, - Global => null; + Post => Length (Head'Result) = Count, + Contract_Cases => + (Count <= Length (Source) + => + -- Source is cut + + To_String (Head'Result) = Slice (Source, 1, Count), + + others + => + -- Source is followed by Pad characters + + Slice (Head'Result, 1, Length (Source)) = To_String (Source) + and then + Slice (Head'Result, Length (Source) + 1, Count) = + [1 .. Count - Length (Source) => Pad]), + Global => null; procedure Head (Source : in out Unbounded_String; Count : Natural; Pad : Character := Space) with - Post => Length (Source) = Count, - Global => null; + Post => Length (Source) = Count, + Contract_Cases => + (Count <= Length (Source) + => + -- Source is cut + + To_String (Source) = Slice (Source, 1, Count), + + others + => + -- Source is followed by Pad characters + + Slice (Source, 1, Length (Source)'Old) = To_String (Source)'Old + and then + Slice (Source, Length (Source)'Old + 1, Count) = + [1 .. Count - Length (Source)'Old => Pad]), + Global => null; function Tail (Source : Unbounded_String; Count : Natural; Pad : Character := Space) return Unbounded_String with - Post => Length (Tail'Result) = Count, - Global => null; + Post => Length (Tail'Result) = Count, + Contract_Cases => + (Count = 0 + => + True, + + (Count in 1 .. Length (Source)) + => + -- Source is cut + + To_String (Tail'Result) = + Slice (Source, Length (Source) - Count + 1, Length (Source)), + + others + => + -- Source is preceded by Pad characters + + (if Length (Source) = 0 then + To_String (Tail'Result) = [1 .. Count => Pad] + else + Slice (Tail'Result, 1, Count - Length (Source)) = + [1 .. Count - Length (Source) => Pad] + and then + Slice (Tail'Result, Count - Length (Source) + 1, Count) = + To_String (Source))), + Global => null; procedure Tail (Source : in out Unbounded_String; Count : Natural; Pad : Character := Space) with - Post => Length (Source) = Count, - Global => null; + Post => Length (Source) = Count, + Contract_Cases => + (Count = 0 + => + True, + + (Count in 1 .. Length (Source)) + => + -- Source is cut + + To_String (Source) = + Slice (Source, + -- Really "Length (Source) - Count + 1" but expressed with a + -- conditional repeating the above guard so that the call to + -- Slice is valid on entry (under 'Old) even when the test + -- evaluates to False. + (if Count <= Length (Source) then Length (Source) - Count + 1 + else 1), + Length (Source))'Old, + + others + => + -- Source is preceded by Pad characters + + (if Length (Source)'Old = 0 then + To_String (Source) = [1 .. Count => Pad] + else + Slice (Source, 1, Count - Length (Source)'Old) = + [1 .. Count - Length (Source)'Old => Pad] + and then + Slice (Source, Count - Length (Source)'Old + 1, Count) = + To_String (Source)'Old)), + Global => null; function "*" (Left : Natural; Right : Character) return Unbounded_String with Pre => Left <= Natural'Last, - Post => Length ("*"'Result) = Left, + Post => To_String ("*"'Result) = [1 .. Left => Right], Global => null; function "*" @@ -716,7 +1577,13 @@ is Right : String) return Unbounded_String with Pre => (if Left /= 0 then Right'Length <= Natural'Last / Left), - Post => Length ("*"'Result) = Left * Right'Length, + 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 => null; function "*" @@ -724,7 +1591,13 @@ is Right : Unbounded_String) return Unbounded_String with Pre => (if Left /= 0 then Length (Right) <= Natural'Last / Left), - Post => Length ("*"'Result) = Left * Length (Right), + 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 => null; -- Each of the transformation functions (Replace_Slice, Insert, Overwrite, diff --git a/gcc/ada/libgnat/a-strunb__shared.adb b/gcc/ada/libgnat/a-strunb__shared.adb index ecc0e4af117..ef4f8c93bdb 100644 --- a/gcc/ada/libgnat/a-strunb__shared.adb +++ b/gcc/ada/libgnat/a-strunb__shared.adb @@ -29,7 +29,6 @@ -- -- ------------------------------------------------------------------------------ -with Ada.Strings.Search; with Ada.Unchecked_Deallocation; package body Ada.Strings.Unbounded is @@ -58,7 +57,7 @@ package body Ada.Strings.Unbounded is -- Calculation takes into account alignment of the allocated memory -- segments to use memory effectively by Append/Insert/etc operations. - function Sum (Left : Natural; Right : Integer) return Natural with Inline; + function Sum (Left, Right : Natural) return Natural with Inline; -- Returns summary of Left and Right, raise Constraint_Error on overflow function Mul (Left, Right : Natural) return Natural with Inline; @@ -165,7 +164,11 @@ package body Ada.Strings.Unbounded is else DR := Allocate (DL); DR.Data (1 .. Left'Length) := Left; - DR.Data (Left'Length + 1 .. DL) := RR.Data (1 .. RR.Last); + + if Left'Length < Natural'Last then + DR.Data (Left'Length + 1 .. DL) := RR.Data (1 .. RR.Last); + end if; + DR.Last := DL; end if; @@ -243,7 +246,7 @@ package body Ada.Strings.Unbounded is is DL : constant Natural := Mul (Left, Right'Length); DR : Shared_String_Access; - K : Positive; + K : Natural; begin -- Result is an empty string, reuse shared empty string @@ -255,10 +258,10 @@ package body Ada.Strings.Unbounded is else DR := Allocate (DL); - K := 1; + K := 0; for J in 1 .. Left loop - DR.Data (K .. K + Right'Length - 1) := Right; + DR.Data (K + 1 .. K + Right'Length) := Right; K := K + Right'Length; end loop; @@ -275,7 +278,7 @@ package body Ada.Strings.Unbounded is RR : constant Shared_String_Access := Right.Reference; DL : constant Natural := Mul (Left, RR.Last); DR : Shared_String_Access; - K : Positive; + K : Natural; begin -- Result is an empty string, reuse shared empty string @@ -293,10 +296,10 @@ package body Ada.Strings.Unbounded is else DR := Allocate (DL); - K := 1; + K := 0; for J in 1 .. Left loop - DR.Data (K .. K + RR.Last - 1) := RR.Data (1 .. RR.Last); + DR.Data (K + 1 .. K + RR.Last) := RR.Data (1 .. RR.Last); K := K + RR.Last; end loop; @@ -703,15 +706,15 @@ package body Ada.Strings.Unbounded is Reference (SR); DR := SR; - -- Index is out of range + -- From is too large - elsif Through > SR.Last then + elsif From - 1 > SR.Last then raise Index_Error; -- Compute size of the result else - DL := SR.Last - (Through - From + 1); + DL := SR.Last - (Natural'Min (SR.Last, Through) - From + 1); -- Result is an empty string, reuse shared empty string @@ -723,7 +726,11 @@ package body Ada.Strings.Unbounded is else DR := Allocate (DL); DR.Data (1 .. From - 1) := SR.Data (1 .. From - 1); - DR.Data (From .. DL) := SR.Data (Through + 1 .. SR.Last); + + if Through < Natural'Last then + DR.Data (From .. DL) := SR.Data (Through + 1 .. SR.Last); + end if; + DR.Last := DL; end if; end if; @@ -746,13 +753,13 @@ package body Ada.Strings.Unbounded is if From > Through then null; - -- Through is outside of the range + -- From is too large - elsif Through > SR.Last then + elsif From - 1 > SR.Last then raise Index_Error; else - DL := SR.Last - (Through - From + 1); + DL := SR.Last - (Natural'Min (SR.Last, Through) - From + 1); -- Result is empty, reuse shared empty string @@ -763,7 +770,10 @@ package body Ada.Strings.Unbounded is -- Try to reuse existing shared string elsif Can_Be_Reused (SR, DL) then - SR.Data (From .. DL) := SR.Data (Through + 1 .. SR.Last); + if Through < Natural'Last then + SR.Data (From .. DL) := SR.Data (Through + 1 .. SR.Last); + end if; + SR.Last := DL; -- Otherwise, allocate new shared string @@ -771,7 +781,11 @@ package body Ada.Strings.Unbounded is else DR := Allocate (DL); DR.Data (1 .. From - 1) := SR.Data (1 .. From - 1); - DR.Data (From .. DL) := SR.Data (Through + 1 .. SR.Last); + + if Through < Natural'Last then + DR.Data (From .. DL) := SR.Data (Through + 1 .. SR.Last); + end if; + DR.Last := DL; Source.Reference := DR; Unreference (SR); @@ -1093,7 +1107,7 @@ package body Ada.Strings.Unbounded is begin -- Check index first - if Before > SR.Last + 1 then + if Before - 1 > SR.Last then raise Index_Error; end if; @@ -1113,9 +1127,13 @@ package body Ada.Strings.Unbounded is else DR := Allocate (DL, DL / Growth_Factor); DR.Data (1 .. Before - 1) := SR.Data (1 .. Before - 1); - DR.Data (Before .. Before + New_Item'Length - 1) := New_Item; - DR.Data (Before + New_Item'Length .. DL) := - SR.Data (Before .. SR.Last); + DR.Data (Before .. Before - 1 + New_Item'Length) := New_Item; + + if Before <= SR.Last then + DR.Data (Before + New_Item'Length .. DL) := + SR.Data (Before .. SR.Last); + end if; + DR.Last := DL; end if; @@ -1134,7 +1152,7 @@ package body Ada.Strings.Unbounded is begin -- Check bounds - if Before > SR.Last + 1 then + if Before - 1 > SR.Last then raise Index_Error; end if; @@ -1152,9 +1170,12 @@ package body Ada.Strings.Unbounded is -- Try to reuse existing shared string first elsif Can_Be_Reused (SR, DL) then - SR.Data (Before + New_Item'Length .. DL) := - SR.Data (Before .. SR.Last); - SR.Data (Before .. Before + New_Item'Length - 1) := New_Item; + if Before <= SR.Last then + SR.Data (Before + New_Item'Length .. DL) := + SR.Data (Before .. SR.Last); + end if; + + SR.Data (Before .. Before - 1 + New_Item'Length) := New_Item; SR.Last := DL; -- Otherwise, allocate new shared string and fill it @@ -1162,9 +1183,13 @@ package body Ada.Strings.Unbounded is else DR := Allocate (DL, DL / Growth_Factor); DR.Data (1 .. Before - 1) := SR.Data (1 .. Before - 1); - DR.Data (Before .. Before + New_Item'Length - 1) := New_Item; - DR.Data (Before + New_Item'Length .. DL) := - SR.Data (Before .. SR.Last); + DR.Data (Before .. Before - 1 + New_Item'Length) := New_Item; + + if Before <= SR.Last then + DR.Data (Before + New_Item'Length .. DL) := + SR.Data (Before .. SR.Last); + end if; + DR.Last := DL; Source.Reference := DR; Unreference (SR); @@ -1206,7 +1231,7 @@ package body Ada.Strings.Unbounded is begin -- Check bounds - if Position > SR.Last + 1 then + if Position - 1 > SR.Last then raise Index_Error; end if; @@ -1228,9 +1253,13 @@ package body Ada.Strings.Unbounded is else DR := Allocate (DL); DR.Data (1 .. Position - 1) := SR.Data (1 .. Position - 1); - DR.Data (Position .. Position + New_Item'Length - 1) := New_Item; - DR.Data (Position + New_Item'Length .. DL) := - SR.Data (Position + New_Item'Length .. SR.Last); + DR.Data (Position .. Position - 1 + New_Item'Length) := New_Item; + + if Position <= SR.Last - New_Item'Length then + DR.Data (Position + New_Item'Length .. DL) := + SR.Data (Position + New_Item'Length .. SR.Last); + end if; + DR.Last := DL; end if; @@ -1249,11 +1278,11 @@ package body Ada.Strings.Unbounded is begin -- Bounds check - if Position > SR.Last + 1 then + if Position - 1 > SR.Last then raise Index_Error; end if; - DL := Integer'Max (SR.Last, Position + New_Item'Length - 1); + DL := Integer'Max (SR.Last, Sum (Position - 1, New_Item'Length)); -- Result is empty string, reuse empty shared string @@ -1269,7 +1298,7 @@ package body Ada.Strings.Unbounded is -- Try to reuse existing shared string elsif Can_Be_Reused (SR, DL) then - SR.Data (Position .. Position + New_Item'Length - 1) := New_Item; + SR.Data (Position .. Position - 1 + New_Item'Length) := New_Item; SR.Last := DL; -- Otherwise allocate new shared string and fill it @@ -1277,9 +1306,13 @@ package body Ada.Strings.Unbounded is else DR := Allocate (DL); DR.Data (1 .. Position - 1) := SR.Data (1 .. Position - 1); - DR.Data (Position .. Position + New_Item'Length - 1) := New_Item; - DR.Data (Position + New_Item'Length .. DL) := - SR.Data (Position + New_Item'Length .. SR.Last); + DR.Data (Position .. Position - 1 + New_Item'Length) := New_Item; + + if Position <= SR.Last - New_Item'Length then + DR.Data (Position + New_Item'Length .. DL) := + SR.Data (Position + New_Item'Length .. SR.Last); + end if; + DR.Last := DL; Source.Reference := DR; Unreference (SR); @@ -1365,15 +1398,14 @@ package body Ada.Strings.Unbounded is begin -- Check bounds - if Low > SR.Last + 1 then + if Low - 1 > SR.Last then raise Index_Error; end if; -- Do replace operation when removed slice is not empty if High >= Low then - DL := Sum (SR.Last, - By'Length + Low - Integer'Min (High, SR.Last) - 1); + DL := Sum (Low - 1 + Integer'Max (SR.Last - High, 0), By'Length); -- This is the number of characters remaining in the string after -- replacing the slice. @@ -1387,8 +1419,13 @@ package body Ada.Strings.Unbounded is else DR := Allocate (DL); DR.Data (1 .. Low - 1) := SR.Data (1 .. Low - 1); - DR.Data (Low .. Low + By'Length - 1) := By; - DR.Data (Low + By'Length .. DL) := SR.Data (High + 1 .. SR.Last); + DR.Data (Low .. Low - 1 + By'Length) := By; + + if High < SR.Last then + DR.Data (Low + By'Length .. DL) := + SR.Data (High + 1 .. SR.Last); + end if; + DR.Last := DL; end if; @@ -1414,14 +1451,14 @@ package body Ada.Strings.Unbounded is begin -- Bounds check - if Low > SR.Last + 1 then + if Low - 1 > SR.Last then raise Index_Error; end if; -- Do replace operation only when replaced slice is not empty if High >= Low then - DL := By'Length + SR.Last + Low - Integer'Min (High, SR.Last) - 1; + DL := Sum (Low - 1 + Integer'Max (SR.Last - High, 0), By'Length); -- This is the number of characters remaining in the string after -- replacing the slice. @@ -1434,8 +1471,12 @@ package body Ada.Strings.Unbounded is -- Try to reuse existing shared string elsif Can_Be_Reused (SR, DL) then - SR.Data (Low + By'Length .. DL) := SR.Data (High + 1 .. SR.Last); - SR.Data (Low .. Low + By'Length - 1) := By; + if High < SR.Last then + SR.Data (Low + By'Length .. DL) := + SR.Data (High + 1 .. SR.Last); + end if; + + SR.Data (Low .. Low - 1 + By'Length) := By; SR.Last := DL; -- Otherwise allocate new shared string and fill it @@ -1443,8 +1484,13 @@ package body Ada.Strings.Unbounded is else DR := Allocate (DL); DR.Data (1 .. Low - 1) := SR.Data (1 .. Low - 1); - DR.Data (Low .. Low + By'Length - 1) := By; - DR.Data (Low + By'Length .. DL) := SR.Data (High + 1 .. SR.Last); + DR.Data (Low .. Low - 1 + By'Length) := By; + + if High < SR.Last then + DR.Data (Low + By'Length .. DL) := + SR.Data (High + 1 .. SR.Last); + end if; + DR.Last := DL; Source.Reference := DR; Unreference (SR); @@ -1509,7 +1555,7 @@ package body Ada.Strings.Unbounded is begin -- Note: test of High > Length is in accordance with AI95-00128 - if Low > SR.Last + 1 or else High > SR.Last then + if Low - 1 > SR.Last or else High > SR.Last then raise Index_Error; else @@ -1521,7 +1567,7 @@ package body Ada.Strings.Unbounded is -- Sum -- --------- - function Sum (Left : Natural; Right : Integer) return Natural is + function Sum (Left, Right : Natural) return Natural is pragma Unsuppress (Overflow_Check); begin return Left + Right; diff --git a/gcc/ada/libgnat/a-strunb__shared.ads b/gcc/ada/libgnat/a-strunb__shared.ads index 3a0411de5de..fa97680a7fa 100644 --- a/gcc/ada/libgnat/a-strunb__shared.ads +++ b/gcc/ada/libgnat/a-strunb__shared.ads @@ -35,9 +35,14 @@ -- Preconditions in this unit are meant for analysis only, not for run-time -- checking, so that the expected exceptions are raised. This is enforced by --- setting the corresponding assertion policy to Ignore. +-- setting the corresponding assertion policy to Ignore. Postconditions and +-- contract cases should not be executed at runtime as well, in order not to +-- slow down the execution of these functions. -pragma Assertion_Policy (Pre => Ignore); +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore); -- This package provides an implementation of Ada.Strings.Unbounded that uses -- reference counts to implement copy on modification (rather than copy on @@ -77,17 +82,26 @@ pragma Assertion_Policy (Pre => Ignore); -- make objects of Unbounded_String thread-safe: an instance cannot be -- accessed by several tasks simultaneously. -with Ada.Strings.Maps; +with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; private with Ada.Finalization; private with System.Atomic_Counters; +with Ada.Strings.Search; private with Ada.Strings.Text_Buffers; package Ada.Strings.Unbounded with + SPARK_Mode, Initial_Condition => Length (Null_Unbounded_String) = 0, Always_Terminates is pragma Preelaborate; + -- Contracts may call function Length in the prefix of attribute reference + -- to Old as in Length (Source)'Old. Allow this use. + + pragma Unevaluated_Use_Of_Old (Allow); + + subtype String_1 is String (1 .. <>) with Ghost; -- Type used in contracts + type Unbounded_String is private with Default_Initial_Condition => Length (Unbounded_String) = 0; pragma Preelaborable_Initialization (Unbounded_String); @@ -99,7 +113,7 @@ is type String_Access is access all String; - procedure Free (X : in out String_Access); + procedure Free (X : in out String_Access) with SPARK_Mode => Off; -------------------------------------------------------- -- Conversion, Concatenation, and Selection Functions -- @@ -108,7 +122,8 @@ is function To_Unbounded_String (Source : String) return Unbounded_String with - Post => To_String (To_Unbounded_String'Result) = Source, + Post => To_String (To_Unbounded_String'Result) = Source + and then Length (To_Unbounded_String'Result) = Source'Length, Global => null; function To_Unbounded_String @@ -136,7 +151,8 @@ is New_Item : Unbounded_String) with Pre => Length (New_Item) <= Natural'Last - Length (Source), - Post => Length (Source) = Length (Source)'Old + Length (New_Item), + Post => + To_String (Source) = To_String (Source)'Old & To_String (New_Item), Global => null; procedure Append @@ -144,7 +160,7 @@ is New_Item : String) with Pre => New_Item'Length <= Natural'Last - Length (Source), - Post => Length (Source) = Length (Source)'Old + New_Item'Length, + Post => To_String (Source) = To_String (Source)'Old & New_Item, Global => null; procedure Append @@ -152,7 +168,7 @@ is New_Item : Character) with Pre => Length (Source) < Natural'Last, - Post => Length (Source) = Length (Source)'Old + 1, + Post => To_String (Source) = To_String (Source)'Old & New_Item, Global => null; function "&" @@ -160,7 +176,7 @@ is Right : Unbounded_String) return Unbounded_String with Pre => Length (Right) <= Natural'Last - Length (Left), - Post => Length ("&"'Result) = Length (Left) + Length (Right), + Post => To_String ("&"'Result) = To_String (Left) & To_String (Right), Global => null; function "&" @@ -168,7 +184,7 @@ is Right : String) return Unbounded_String with Pre => Right'Length <= Natural'Last - Length (Left), - Post => Length ("&"'Result) = Length (Left) + Right'Length, + Post => To_String ("&"'Result) = To_String (Left) & Right, Global => null; function "&" @@ -176,7 +192,7 @@ is Right : Unbounded_String) return Unbounded_String with Pre => Left'Length <= Natural'Last - Length (Right), - Post => Length ("&"'Result) = Left'Length + Length (Right), + Post => To_String ("&"'Result) = String_1 (Left) & To_String (Right), Global => null; function "&" @@ -184,7 +200,7 @@ is Right : Character) return Unbounded_String with Pre => Length (Left) < Natural'Last, - Post => Length ("&"'Result) = Length (Left) + 1, + Post => To_String ("&"'Result) = To_String (Left) & Right, Global => null; function "&" @@ -192,7 +208,7 @@ is Right : Unbounded_String) return Unbounded_String with Pre => Length (Right) < Natural'Last, - Post => Length ("&"'Result) = Length (Right) + 1, + Post => To_String ("&"'Result) = Left & To_String (Right), Global => null; function Element @@ -209,7 +225,8 @@ is By : Character) with Pre => Index <= Length (Source), - Post => Length (Source) = Length (Source)'Old, + Post => + To_String (Source) = (To_String (Source)'Old with delta Index => By), Global => null; function Slice @@ -218,7 +235,9 @@ is High : Natural) return String with Pre => Low - 1 <= Length (Source) and then High <= Length (Source), - Post => Slice'Result'Length = Natural'Max (0, High - Low + 1), + Post => Slice'Result'First = Low + and then Slice'Result'Last = High + and then Slice'Result = To_String (Source) (Low .. High), Global => null; function Unbounded_Slice @@ -228,7 +247,7 @@ is with Pre => Low - 1 <= Length (Source) and then High <= Length (Source), Post => - Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1), + To_String (Unbounded_Slice'Result) = To_String (Source) (Low .. High), Global => null; pragma Ada_05 (Unbounded_Slice); @@ -239,7 +258,7 @@ is High : Natural) with Pre => Low - 1 <= Length (Source) and then High <= Length (Source), - Post => Length (Target) = Natural'Max (0, High - Low + 1), + Post => To_String (Target) = To_String (Source) (Low .. High), Global => null; pragma Ada_05 (Unbounded_Slice); @@ -268,72 +287,84 @@ is (Left : Unbounded_String; Right : Unbounded_String) return Boolean with + Post => "<"'Result = (To_String (Left) < To_String (Right)), Global => null; function "<" (Left : Unbounded_String; Right : String) return Boolean with + Post => "<"'Result = (To_String (Left) < Right), Global => null; function "<" (Left : String; Right : Unbounded_String) return Boolean with + Post => "<"'Result = (Left < To_String (Right)), Global => null; function "<=" (Left : Unbounded_String; Right : Unbounded_String) return Boolean with + Post => "<="'Result = (To_String (Left) <= To_String (Right)), Global => null; function "<=" (Left : Unbounded_String; Right : String) return Boolean with + Post => "<="'Result = (To_String (Left) <= Right), Global => null; function "<=" (Left : String; Right : Unbounded_String) return Boolean with + Post => "<="'Result = (Left <= To_String (Right)), Global => null; function ">" (Left : Unbounded_String; Right : Unbounded_String) return Boolean with + Post => ">"'Result = (To_String (Left) > To_String (Right)), Global => null; function ">" (Left : Unbounded_String; Right : String) return Boolean with + Post => ">"'Result = (To_String (Left) > Right), Global => null; function ">" (Left : String; Right : Unbounded_String) return Boolean with + Post => ">"'Result = (Left > To_String (Right)), Global => null; function ">=" (Left : Unbounded_String; Right : Unbounded_String) return Boolean with + Post => ">="'Result = (To_String (Left) >= To_String (Right)), Global => null; function ">=" (Left : Unbounded_String; Right : String) return Boolean with + Post => ">="'Result = (To_String (Left) >= Right), Global => null; function ">=" (Left : String; Right : Unbounded_String) return Boolean with + Post => ">="'Result = (Left >= To_String (Right)), Global => null; ------------------------ @@ -346,8 +377,52 @@ is Going : Direction := Forward; Mapping : Maps.Character_Mapping := Maps.Identity) return Natural with - Pre => Pattern'Length /= 0, - Global => null; + Pre => Pattern'Length > 0, + Post => Index'Result <= Length (Source), + Contract_Cases => + + -- If Source is the empty string, then 0 is returned + + (Length (Source) = 0 + => + Index'Result = 0, + + -- If some slice of Source matches Pattern, then a valid index is + -- returned. + + Length (Source) > 0 + and then + (for some J in 1 .. Length (Source) - (Pattern'Length - 1) => + Search.Match (To_String (Source), Pattern, Mapping, J)) + => + -- The result is in the considered range of Source + + Index'Result in 1 .. Length (Source) - (Pattern'Length - 1) + + -- The slice beginning at the returned index matches Pattern + + and then Search.Match + (To_String (Source), Pattern, Mapping, Index'Result) + + -- The result is the smallest or largest index which satisfies + -- the matching, respectively when Going = Forward and Going = + -- Backward. + + and then + (for all J in 1 .. Length (Source) => + (if (if Going = Forward + then J <= Index'Result - 1 + else J - 1 in Index'Result + .. Length (Source) - Pattern'Length) + then not (Search.Match + (To_String (Source), Pattern, Mapping, J)))), + + -- Otherwise, 0 is returned + + others + => + Index'Result = 0), + Global => null; function Index (Source : Unbounded_String; @@ -355,8 +430,52 @@ is Going : Direction := Forward; Mapping : Maps.Character_Mapping_Function) return Natural with - Pre => Pattern'Length /= 0, - Global => null; + Pre => Pattern'Length /= 0 and then Mapping /= null, + Post => Index'Result <= Length (Source), + Contract_Cases => + + -- If Source is the empty string, then 0 is returned + + (Length (Source) = 0 + => + Index'Result = 0, + + -- If some slice of Source matches Pattern, then a valid index is + -- returned. + + Length (Source) > 0 + and then + (for some J in 1 .. Length (Source) - (Pattern'Length - 1) => + Search.Match (To_String (Source), Pattern, Mapping, J)) + => + -- The result is in the considered range of Source + + Index'Result in 1 .. Length (Source) - (Pattern'Length - 1) + + -- The slice beginning at the returned index matches Pattern + + and then Search.Match + (To_String (Source), Pattern, Mapping, Index'Result) + + -- The result is the smallest or largest index which satisfies + -- the matching, respectively when Going = Forward and Going = + -- Backward. + + and then + (for all J in 1 .. Length (Source) => + (if (if Going = Forward + then J <= Index'Result - 1 + else J - 1 in Index'Result + .. Length (Source) - Pattern'Length) + then not (Search.Match + (To_String (Source), Pattern, Mapping, J)))), + + -- Otherwise, 0 is returned + + others + => + Index'Result = 0), + Global => null; function Index (Source : Unbounded_String; @@ -364,7 +483,43 @@ is Test : Membership := Inside; Going : Direction := Forward) return Natural with - Global => null; + Post => Index'Result <= Length (Source), + Contract_Cases => + + -- If no character of Source satisfies the property Test on Set, + -- then 0 is returned. + + ((for all C of To_String (Source) => + (Test = Inside) /= Maps.Is_In (C, Set)) + => + Index'Result = 0, + + -- Otherwise, an index in the range of Source is returned + + others + => + -- The result is in the range of Source + + Index'Result in 1 .. Length (Source) + + -- The character at the returned index satisfies the property + -- Test on Set. + + and then + (Test = Inside) = + Maps.Is_In (Element (Source, Index'Result), Set) + + -- The result is the smallest or largest index which satisfies + -- the property, respectively when Going = Forward and Going = + -- Backward. + + and then + (for all J in 1 .. Length (Source) => + (if J /= Index'Result + and then (J < Index'Result) = (Going = Forward) + then (Test = Inside) + /= Maps.Is_In (Element (Source, J), Set)))), + Global => null; function Index (Source : Unbounded_String; @@ -373,9 +528,60 @@ is Going : Direction := Forward; Mapping : Maps.Character_Mapping := Maps.Identity) return Natural with - Pre => (if Length (Source) /= 0 then From <= Length (Source)) - and then Pattern'Length /= 0, - Global => null; + Pre => + (if Length (Source) /= 0 then From <= Length (Source)) + and then Pattern'Length /= 0, + Post => Index'Result <= Length (Source), + Contract_Cases => + + -- If Source is the empty string, then 0 is returned + + (Length (Source) = 0 + => + Index'Result = 0, + + -- If some slice of Source matches Pattern, then a valid index is + -- returned. + + Length (Source) > 0 + and then + (for some J in + (if Going = Forward then From else 1) + .. (if Going = Forward then Length (Source) else From) + - (Pattern'Length - 1) => + Search.Match (To_String (Source), Pattern, Mapping, J)) + => + -- The result is in the considered range of Source + + Index'Result in + (if Going = Forward then From else 1) + .. (if Going = Forward then Length (Source) else From) + - (Pattern'Length - 1) + + -- The slice beginning at the returned index matches Pattern + + and then Search.Match + (To_String (Source), Pattern, Mapping, Index'Result) + + -- The result is the smallest or largest index which satisfies + -- the matching, respectively when Going = Forward and Going = + -- Backward. + + and then + (for all J in 1 .. Length (Source) => + (if (if Going = Forward + then J in From .. Index'Result - 1 + else J - 1 in Index'Result + .. From - Pattern'Length) + then not (Search.Match + (To_String (Source), Pattern, Mapping, J)))), + + -- Otherwise, 0 is returned + + others + => + Index'Result = 0), + Global => null; pragma Ada_05 (Index); function Index @@ -385,9 +591,61 @@ is Going : Direction := Forward; Mapping : Maps.Character_Mapping_Function) return Natural with - Pre => (if Length (Source) /= 0 then From <= Length (Source)) - and then Pattern'Length /= 0, - Global => null; + Pre => + (if Length (Source) /= 0 then From <= Length (Source)) + and then Pattern'Length /= 0 + and then Mapping /= null, + Post => Index'Result <= Length (Source), + Contract_Cases => + + -- If Source is the empty string, then 0 is returned + + (Length (Source) = 0 + => + Index'Result = 0, + + -- If some slice of Source matches Pattern, then a valid index is + -- returned. + + Length (Source) > 0 + and then + (for some J in + (if Going = Forward then From else 1) + .. (if Going = Forward then Length (Source) else From) + - (Pattern'Length - 1) => + Search.Match (To_String (Source), Pattern, Mapping, J)) + => + -- The result is in the considered range of Source + + Index'Result in + (if Going = Forward then From else 1) + .. (if Going = Forward then Length (Source) else From) + - (Pattern'Length - 1) + + -- The slice beginning at the returned index matches Pattern + + and then Search.Match + (To_String (Source), Pattern, Mapping, Index'Result) + + -- The result is the smallest or largest index which satisfies + -- the matching, respectively when Going = Forward and Going = + -- Backward. + + and then + (for all J in 1 .. Length (Source) => + (if (if Going = Forward + then J in From .. Index'Result - 1 + else J - 1 in Index'Result + .. From - Pattern'Length) + then not (Search.Match + (To_String (Source), Pattern, Mapping, J)))), + + -- Otherwise, 0 is returned + + others + => + Index'Result = 0), + Global => null; pragma Ada_05 (Index); function Index @@ -397,23 +655,147 @@ is Test : Membership := Inside; Going : Direction := Forward) return Natural with - Pre => (if Length (Source) /= 0 then From <= Length (Source)), - Global => null; + Pre => + (if Length (Source) /= 0 then From <= Length (Source)), + Post => Index'Result <= Length (Source), + Contract_Cases => + + -- If Source is the empty string, or no character of the considered + -- slice of Source satisfies the property Test on Set, then 0 is + -- returned. + + (Length (Source) = 0 + or else + (for all J in 1 .. Length (Source) => + (if J = From or else (J > From) = (Going = Forward) then + (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))) + => + Index'Result = 0, + + -- Otherwise, an index in the considered range of Source is + -- returned. + + others + => + -- The result is in the considered range of Source + + Index'Result in 1 .. Length (Source) + and then + (Index'Result = From + or else (Index'Result > From) = (Going = Forward)) + + -- The character at the returned index satisfies the property + -- Test on Set. + + and then + (Test = Inside) = + Maps.Is_In (Element (Source, Index'Result), Set) + + -- The result is the smallest or largest index which satisfies + -- the property, respectively when Going = Forward and Going = + -- Backward. + + and then + (for all J in 1 .. Length (Source) => + (if J /= Index'Result + and then (J < Index'Result) = (Going = Forward) + and then (J = From + or else (J > From) = (Going = Forward)) + then (Test = Inside) + /= Maps.Is_In (Element (Source, J), Set)))), + Global => null; pragma Ada_05 (Index); function Index_Non_Blank (Source : Unbounded_String; Going : Direction := Forward) return Natural with - Global => null; + Post => Index_Non_Blank'Result <= Length (Source), + Contract_Cases => + + -- If all characters of Source are Space characters, then 0 is + -- returned. + + ((for all C of To_String (Source) => C = ' ') + => + Index_Non_Blank'Result = 0, + + -- Otherwise, an index in the range of Source is returned + + others + => + -- The result is in the range of Source + + Index_Non_Blank'Result in 1 .. Length (Source) + + -- The character at the returned index is not a Space character + + and then Element (Source, Index_Non_Blank'Result) /= ' ' + + -- The result is the smallest or largest index which is not a + -- Space character, respectively when Going = Forward and Going + -- = Backward. + + and then + (for all J in 1 .. Length (Source) => + (if J /= Index_Non_Blank'Result + and then + (J < Index_Non_Blank'Result) = (Going = Forward) + then Element (Source, J) = ' '))), + Global => null; function Index_Non_Blank (Source : Unbounded_String; From : Positive; Going : Direction := Forward) return Natural with - Pre => (if Length (Source) /= 0 then From <= Length (Source)), - Global => null; + Pre => + (if Length (Source) /= 0 then From <= Length (Source)), + Post => Index_Non_Blank'Result <= Length (Source), + Contract_Cases => + + -- If Source is the empty string, or all characters of the + -- considered slice of Source are Space characters, then 0 + -- is returned. + + (Length (Source) = 0 + or else + (for all J in 1 .. Length (Source) => + (if J = From or else (J > From) = (Going = Forward) then + Element (Source, J) = ' ')) + => + Index_Non_Blank'Result = 0, + + -- Otherwise, an index in the considered range of Source is + -- returned. + + others + => + -- The result is in the considered range of Source + + Index_Non_Blank'Result in 1 .. Length (Source) + and then + (Index_Non_Blank'Result = From + or else + (Index_Non_Blank'Result > From) = (Going = Forward)) + + -- The character at the returned index is not a Space character + + and then Element (Source, Index_Non_Blank'Result) /= ' ' + + -- The result is the smallest or largest index which isn't a + -- Space character, respectively when Going = Forward and Going + -- = Backward. + + and then + (for all J in 1 .. Length (Source) => + (if J /= Index_Non_Blank'Result + and then + (J < Index_Non_Blank'Result) = (Going = Forward) + and then (J = From + or else (J > From) = (Going = Forward)) + then Element (Source, J) = ' '))), + Global => null; pragma Ada_05 (Index_Non_Blank); function Count @@ -429,7 +811,7 @@ is Pattern : String; Mapping : Maps.Character_Mapping_Function) return Natural with - Pre => Pattern'Length /= 0, + Pre => Pattern'Length /= 0 and then Mapping /= null, Global => null; function Count @@ -446,8 +828,53 @@ is First : out Positive; Last : out Natural) with - Pre => (if Length (Source) /= 0 then From <= Length (Source)), - Global => null; + Pre => + (if Length (Source) /= 0 then From <= Length (Source)), + Contract_Cases => + + -- If Source is the empty string, or if no character of the + -- considered slice of Source satisfies the property Test on + -- Set, then First is set to From and Last is set to 0. + + (Length (Source) = 0 + or else + (for all J in From .. Length (Source) => + (Test = Inside) /= Maps.Is_In (Element (Source, J), Set)) + => + First = From and then Last = 0, + + -- Otherwise, First and Last are set to valid indexes + + others + => + -- First and Last are in the considered range of Source + + First in From .. Length (Source) + and then Last in First .. Length (Source) + + -- No character between From and First satisfies the property + -- Test on Set. + + and then + (for all J in From .. First - 1 => + (Test = Inside) /= Maps.Is_In (Element (Source, J), Set)) + + -- All characters between First and Last satisfy the property + -- Test on Set. + + and then + (for all J in First .. Last => + (Test = Inside) = Maps.Is_In (Element (Source, J), Set)) + + -- If Last is not Source'Last, then the character at position + -- Last + 1 does not satify the property Test on Set. + + and then + (if Last < Length (Source) + then + (Test = Inside) + /= Maps.Is_In (Element (Source, Last + 1), Set))), + Global => null; pragma Ada_2012 (Find_Token); procedure Find_Token @@ -457,7 +884,51 @@ is First : out Positive; Last : out Natural) with - Global => null; + Contract_Cases => + + -- If Source is the empty string, or if no character of the + -- considered slice of Source satisfies the property Test on + -- Set, then First is set to 1 and Last is set to 0. + + (Length (Source) = 0 + or else + (for all J in 1 .. Length (Source) => + (Test = Inside) /= Maps.Is_In (Element (Source, J), Set)) + => + First = 1 and then Last = 0, + + -- Otherwise, First and Last are set to valid indexes + + others + => + -- First and Last are in the considered range of Source + + First in 1 .. Length (Source) + and then Last in First .. Length (Source) + + -- No character between 1 and First satisfies the property Test + -- on Set. + + and then + (for all J in 1 .. First - 1 => + (Test = Inside) /= Maps.Is_In (Element (Source, J), Set)) + + -- All characters between First and Last satisfy the property + -- Test on Set. + + and then + (for all J in First .. Last => + (Test = Inside) = Maps.Is_In (Element (Source, J), Set)) + + -- If Last is not Source'Last, then the character at position + -- Last + 1 does not satify the property Test on Set. + + and then + (if Last < Length (Source) + then + (Test = Inside) + /= Maps.Is_In (Element (Source, Last + 1), Set))), + Global => null; ------------------------------------ -- String Translation Subprograms -- @@ -467,28 +938,44 @@ is (Source : Unbounded_String; Mapping : Maps.Character_Mapping) return Unbounded_String with - Post => Length (Translate'Result) = Length (Source), + Post => Length (Translate'Result) = Length (Source) + and then + (for all K in 1 .. Length (Source) => + Element (Translate'Result, K) = + Ada.Strings.Maps.Value (Mapping, Element (Source, K))), Global => null; procedure Translate (Source : in out Unbounded_String; Mapping : Maps.Character_Mapping) with - Post => Length (Source) = Length (Source)'Old, + Post => Length (Source) = Length (Source)'Old + and then + (for all K in 1 .. Length (Source) => + Element (Source, K) = + Ada.Strings.Maps.Value (Mapping, To_String (Source)'Old (K))), Global => null; function Translate (Source : Unbounded_String; Mapping : Maps.Character_Mapping_Function) return Unbounded_String with - Post => Length (Translate'Result) = Length (Source), + Pre => Mapping /= null, + Post => Length (Translate'Result) = Length (Source) + and then + (for all K in 1 .. Length (Source) => + Element (Translate'Result, K) = Mapping (Element (Source, K))), Global => null; procedure Translate (Source : in out Unbounded_String; Mapping : Maps.Character_Mapping_Function) with - Post => Length (Source) = Length (Source)'Old, + Pre => Mapping /= null, + Post => Length (Source) = Length (Source)'Old + and then + (for all K in 1 .. Length (Source) => + Element (Source, K) = Mapping (To_String (Source)'Old (K))), Global => null; --------------------------------------- @@ -506,14 +993,66 @@ is and then (if High >= Low then Low - 1 <= Natural'Last - By'Length - - Natural'Max (Length (Source) - High, 0) + - Integer'Max (Length (Source) - High, 0) else Length (Source) <= Natural'Last - By'Length), Contract_Cases => + + -- If High >= Low, when considering the application of To_String to + -- convert an Unbounded_String into String, then the returned string + -- comprises Source (Source'First .. Low - 1) & By + -- & Source(High + 1 .. Source'Last). + (High >= Low => + + -- Length of the returned string + Length (Replace_Slice'Result) - = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0), + = Low - 1 + By'Length + Integer'Max (Length (Source) - High, 0) + + -- Elements starting at Low are replaced by elements of By + + and then + Slice (Replace_Slice'Result, 1, Low - 1) = + Slice (Source, 1, Low - 1) + and then + Slice (Replace_Slice'Result, Low, Low - 1 + By'Length) = By + + -- When there are remaining characters after the replaced slice, + -- they are appended to the result. + + and then + (if High < Length (Source) + then + Slice (Replace_Slice'Result, + Low + By'Length, Length (Replace_Slice'Result)) = + Slice (Source, High + 1, Length (Source))), + + -- If High < Low, then the returned string is + -- Insert (Source, Before => Low, New_Item => By). + others => - Length (Replace_Slice'Result) = Length (Source)'Old + By'Length), + + -- Length of the returned string + + Length (Replace_Slice'Result) = Length (Source) + By'Length + + -- Elements of By are inserted after the element at Low + + and then + Slice (Replace_Slice'Result, 1, Low - 1) = + Slice (Source, 1, Low - 1) + and then + Slice (Replace_Slice'Result, Low, Low - 1 + By'Length) = By + + -- When there are remaining characters after Low in Source, they + -- are appended to the result. + + and then + (if Low < Length (Source) + then + Slice (Replace_Slice'Result, + Low + By'Length, Length (Replace_Slice'Result)) = + Slice (Source, Low, Length (Source)))), Global => null; procedure Replace_Slice @@ -530,11 +1069,61 @@ is - Natural'Max (Length (Source) - High, 0) else Length (Source) <= Natural'Last - By'Length), Contract_Cases => + + -- If High >= Low, when considering the application of To_String to + -- convert an Unbounded_String into String, then the returned string + -- comprises Source (Source'First .. Low - 1) & By + -- & Source(High + 1 .. Source'Last). + (High >= Low => + + -- Length of the returned string + Length (Source) - = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0), + = Low - 1 + By'Length + Integer'Max (Length (Source)'Old - High, 0) + + -- Elements starting at Low are replaced by elements of By + + and then Slice (Source, 1, Low - 1) = + Slice (Source, 1, Low - 1)'Old + and then Slice (Source, Low, Low - 1 + By'Length) = By + + -- When there are remaining characters after the replaced slice, + -- they are appended to the result. + + and then + (if High < Length (Source)'Old + then Slice (Source, Low + By'Length, Length (Source)) = + Slice (Source, + -- Really "High + 1" but expressed with a conditional + -- repeating the above test so that the call to Slice + -- is valid on entry (under 'Old) even when the test + -- evaluates to False. + (if High < Length (Source) then High + 1 else 1), + Length (Source))'Old), + + -- If High < Low, then the returned string is + -- Insert (Source, Before => Low, New_Item => By). + others => - Length (Source) = Length (Source)'Old + By'Length), + + -- Length of the returned string + + Length (Source) = Length (Source)'Old + By'Length + + -- Elements of By are inserted after the element at Low + + and then Slice (Source, 1, Low - 1) = + Slice (Source, 1, Low - 1)'Old + and then Slice (Source, Low, Low - 1 + By'Length) = By + + -- When there are remaining characters after Low in Source, they + -- are appended to the result. + + and then + (if Low < Length (Source)'Old + then Slice (Source, Low + By'Length, Length (Source)) = + Slice (Source, Low, Length (Source))'Old)), Global => null; function Insert @@ -544,7 +1133,27 @@ is with Pre => Before - 1 <= Length (Source) and then New_Item'Length <= Natural'Last - Length (Source), - Post => Length (Insert'Result) = Length (Source) + New_Item'Length, + Post => + -- Length of the returned string + + Length (Insert'Result) = Length (Source) + New_Item'Length + + -- Elements of New_Item are inserted after element at Before + + and then + Slice (Insert'Result, 1, Before - 1) = Slice (Source, 1, Before - 1) + and then + Slice (Insert'Result, Before, Before - 1 + New_Item'Length) + = New_Item + + -- When there are remaining characters after Before in Source, they + -- are appended to the returned string. + + and then + (if Before <= Length (Source) then + Slice (Insert'Result, Before + New_Item'Length, + Length (Insert'Result)) = + Slice (Source, Before, Length (Source))), Global => null; procedure Insert @@ -554,7 +1163,25 @@ is with Pre => Before - 1 <= Length (Source) and then New_Item'Length <= Natural'Last - Length (Source), - Post => Length (Source) = Length (Source)'Old + New_Item'Length, + Post => + -- Length of the returned string + + Length (Source) = Length (Source)'Old + New_Item'Length + + -- Elements of New_Item are inserted after element at Before + + and then + Slice (Source, 1, Before - 1) = Slice (Source, 1, Before - 1)'Old + and then + Slice (Source, Before, Before - 1 + New_Item'Length) = New_Item + + -- When there are remaining characters after Before in Source, they + -- are appended to the returned string. + + and then + (if Before <= Length (Source)'Old then + Slice (Source, Before + New_Item'Length, Length (Source)) = + Slice (Source, Before, Length (Source))'Old), Global => null; function Overwrite @@ -563,12 +1190,31 @@ is New_Item : String) return Unbounded_String with Pre => Position - 1 <= Length (Source) - and then (if New_Item'Length /= 0 - then - New_Item'Length <= Natural'Last - (Position - 1)), + and then New_Item'Length <= Natural'Last - (Position - 1), Post => - Length (Overwrite'Result) - = Natural'Max (Length (Source), Position - 1 + New_Item'Length), + -- Length of the returned string + + Length (Overwrite'Result) = + Integer'Max (Length (Source), Position - 1 + New_Item'Length) + + -- Elements after Position are replaced by elements of New_Item + + and then + Slice (Overwrite'Result, 1, Position - 1) = + Slice (Source, 1, Position - 1) + and then + Slice (Overwrite'Result, Position, Position - 1 + New_Item'Length) = + New_Item + and then + (if Position - 1 + New_Item'Length < Length (Source) then + + -- There are some unchanged characters of Source remaining + -- after New_Item. + + Slice (Overwrite'Result, + Position + New_Item'Length, Length (Source)) = + Slice (Source, + Position + New_Item'Length, Length (Source))), Global => null; procedure Overwrite @@ -577,13 +1223,36 @@ is New_Item : String) with Pre => Position - 1 <= Length (Source) - and then (if New_Item'Length /= 0 - then - New_Item'Length <= Natural'Last - (Position - 1)), + and then New_Item'Length <= Natural'Last - (Position - 1), Post => - Length (Source) - = Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length), + -- Length of the returned string + + Length (Source) = + Integer'Max (Length (Source)'Old, Position - 1 + New_Item'Length) + + -- Elements after Position are replaced by elements of New_Item + and then + Slice (Source, 1, Position - 1) = Slice (Source, 1, Position - 1) + and then + Slice (Source, Position, Position - 1 + New_Item'Length) = New_Item + and then + (if Position - 1 + New_Item'Length < Length (Source)'Old then + + -- There are some unchanged characters of Source remaining + -- after New_Item. + + Slice (Source, + Position + New_Item'Length, Length (Source)'Old) = + Slice (Source, + -- Really "Position + New_Item'Length" but expressed with + -- a conditional repeating the above test so that the + -- call to Slice is valid on entry (under 'Old) even + -- when the test evaluates to False. + (if Position - 1 + New_Item'Length < Length (Source) + then Position + New_Item'Length + else 1), + Length (Source))'Old), Global => null; function Delete @@ -591,12 +1260,19 @@ is From : Positive; Through : Natural) return Unbounded_String with - Pre => (if Through <= From then From - 1 <= Length (Source)), + Pre => (if Through >= From then From - 1 <= Length (Source)), Contract_Cases => (Through >= From => - Length (Delete'Result) = Length (Source) - (Through - From + 1), + Length (Delete'Result) = + From - 1 + Natural'Max (Length (Source) - Through, 0) + and then + Slice (Delete'Result, 1, From - 1) = Slice (Source, 1, From - 1) + and then + (if Through < Length (Source) then + Slice (Delete'Result, From, Length (Delete'Result)) = + Slice (Source, Through + 1, Length (Source))), others => - Length (Delete'Result) = Length (Source)), + Delete'Result = Source), Global => null; procedure Delete @@ -604,82 +1280,255 @@ is From : Positive; Through : Natural) with - Pre => (if Through <= From then From - 1 <= Length (Source)), + Pre => (if Through >= From then From - 1 <= Length (Source)), Contract_Cases => (Through >= From => - Length (Source) = Length (Source)'Old - (Through - From + 1), + Length (Source) = + From - 1 + Natural'Max (Length (Source)'Old - Through, 0) + and then + Slice (Source, 1, From - 1) = + To_String (Source)'Old (1 .. From - 1) + and then + (if Through < Length (Source) then + Slice (Source, From, Length (Source)) = + To_String (Source)'Old (Through + 1 .. Length (Source)'Old)), others => - Length (Source) = Length (Source)'Old), + To_String (Source) = To_String (Source)'Old), Global => null; function Trim (Source : Unbounded_String; Side : Trim_End) return Unbounded_String with - Post => Length (Trim'Result) <= Length (Source), - Global => null; + Contract_Cases => + -- If all characters in Source are Space, the returned string is + -- empty. + + ((for all C of To_String (Source) => C = ' ') + => + Length (Trim'Result) = 0, + + -- Otherwise, the returned string is a slice of Source + + others + => + (declare + Low : constant Positive := + (if Side = Right then 1 + else Index_Non_Blank (Source, Forward)); + High : constant Positive := + (if Side = Left then Length (Source) + else Index_Non_Blank (Source, Backward)); + begin + To_String (Trim'Result) = Slice (Source, Low, High))), + Global => null; procedure Trim (Source : in out Unbounded_String; Side : Trim_End) with - Post => Length (Source) <= Length (Source)'Old, - Global => null; + Contract_Cases => + -- If all characters in Source are Space, the returned string is + -- empty. + + ((for all C of To_String (Source) => C = ' ') + => + Length (Source) = 0, + + -- Otherwise, the returned string is a slice of Source + + others + => + (declare + Low : constant Positive := + (if Side = Right then 1 + else Index_Non_Blank (Source, Forward)'Old); + High : constant Positive := + (if Side = Left then Length (Source)'Old + else Index_Non_Blank (Source, Backward)'Old); + begin + To_String (Source) = To_String (Source)'Old (Low .. High))), + Global => null; function Trim (Source : Unbounded_String; Left : Maps.Character_Set; Right : Maps.Character_Set) return Unbounded_String with - Post => Length (Trim'Result) <= Length (Source), - Global => null; + Contract_Cases => + -- If all characters in Source are contained in one of the sets Left + -- or Right, then the returned string is empty. + + ((for all C of To_String (Source) => Maps.Is_In (C, Left)) + or else + (for all C of To_String (Source) => Maps.Is_In (C, Right)) + => + Length (Trim'Result) = 0, + + -- Otherwise, the returned string is a slice of Source + + others + => + (declare + Low : constant Positive := + Index (Source, Left, Outside, Forward); + High : constant Positive := + Index (Source, Right, Outside, Backward); + begin + To_String (Trim'Result) = Slice (Source, Low, High))), + Global => null; procedure Trim (Source : in out Unbounded_String; Left : Maps.Character_Set; Right : Maps.Character_Set) with - Post => Length (Source) <= Length (Source)'Old, - Global => null; + Contract_Cases => + -- If all characters in Source are contained in one of the sets Left + -- or Right, then the returned string is empty. + + ((for all C of To_String (Source) => Maps.Is_In (C, Left)) + or else + (for all C of To_String (Source) => Maps.Is_In (C, Right)) + => + Length (Source) = 0, + + -- Otherwise, the returned string is a slice of Source + + others + => + (declare + Low : constant Positive := + Index (Source, Left, Outside, Forward)'Old; + High : constant Positive := + Index (Source, Right, Outside, Backward)'Old; + begin + To_String (Source) = To_String (Source)'Old (Low .. High))), + Global => null; function Head (Source : Unbounded_String; Count : Natural; Pad : Character := Space) return Unbounded_String with - Post => Length (Head'Result) = Count, - Global => null; + Post => Length (Head'Result) = Count, + Contract_Cases => + (Count <= Length (Source) + => + -- Source is cut + + To_String (Head'Result) = Slice (Source, 1, Count), + + others + => + -- Source is followed by Pad characters + + Slice (Head'Result, 1, Length (Source)) = To_String (Source) + and then + Slice (Head'Result, Length (Source) + 1, Count) = + [1 .. Count - Length (Source) => Pad]), + Global => null; procedure Head (Source : in out Unbounded_String; Count : Natural; Pad : Character := Space) with - Post => Length (Source) = Count, - Global => null; + Post => Length (Source) = Count, + Contract_Cases => + (Count <= Length (Source) + => + -- Source is cut + + To_String (Source) = Slice (Source, 1, Count), + + others + => + -- Source is followed by Pad characters + + Slice (Source, 1, Length (Source)'Old) = To_String (Source)'Old + and then + Slice (Source, Length (Source)'Old + 1, Count) = + [1 .. Count - Length (Source)'Old => Pad]), + Global => null; function Tail (Source : Unbounded_String; Count : Natural; Pad : Character := Space) return Unbounded_String with - Post => Length (Tail'Result) = Count, - Global => null; + Post => Length (Tail'Result) = Count, + Contract_Cases => + (Count = 0 + => + True, + + (Count in 1 .. Length (Source)) + => + -- Source is cut + + To_String (Tail'Result) = + Slice (Source, Length (Source) - Count + 1, Length (Source)), + + others + => + -- Source is preceded by Pad characters + + (if Length (Source) = 0 then + To_String (Tail'Result) = [1 .. Count => Pad] + else + Slice (Tail'Result, 1, Count - Length (Source)) = + [1 .. Count - Length (Source) => Pad] + and then + Slice (Tail'Result, Count - Length (Source) + 1, Count) = + To_String (Source))), + Global => null; procedure Tail (Source : in out Unbounded_String; Count : Natural; Pad : Character := Space) with - Post => Length (Source) = Count, - Global => null; + Post => Length (Source) = Count, + Contract_Cases => + (Count = 0 + => + True, + + (Count in 1 .. Length (Source)) + => + -- Source is cut + + To_String (Source) = + Slice (Source, + -- Really "Length (Source) - Count + 1" but expressed with a + -- conditional repeating the above guard so that the call to + -- Slice is valid on entry (under 'Old) even when the test + -- evaluates to False. + (if Count <= Length (Source) then Length (Source) - Count + 1 + else 1), + Length (Source))'Old, + + others + => + -- Source is preceded by Pad characters + + (if Length (Source)'Old = 0 then + To_String (Source) = [1 .. Count => Pad] + else + Slice (Source, 1, Count - Length (Source)'Old) = + [1 .. Count - Length (Source)'Old => Pad] + and then + Slice (Source, Count - Length (Source)'Old + 1, Count) = + To_String (Source)'Old)), + Global => null; function "*" (Left : Natural; Right : Character) return Unbounded_String with Pre => Left <= Natural'Last, - Post => Length ("*"'Result) = Left, + Post => To_String ("*"'Result) = [1 .. Left => Right], Global => null; function "*" @@ -687,7 +1536,13 @@ is Right : String) return Unbounded_String with Pre => (if Left /= 0 then Right'Length <= Natural'Last / Left), - Post => Length ("*"'Result) = Left * Right'Length, + 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 => null; function "*" @@ -695,10 +1550,18 @@ is Right : Unbounded_String) return Unbounded_String with Pre => (if Left /= 0 then Length (Right) <= Natural'Last / Left), - Post => Length ("*"'Result) = Left * Length (Right), + 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 => null; private + pragma SPARK_Mode (Off); -- Controlled types are not in SPARK + pragma Inline (Length); package AF renames Ada.Finalization;