From 7165704bfaae012cb28e5411619218da6fb8320d Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Mon, 26 Jul 2021 12:21:02 +0200 Subject: [PATCH] [Ada] Minimize parts of Ada.Strings.Fixed marked SPARK_Mode => Off gcc/ada/ * libgnat/a-strfix.adb (Delete, Insert, Overwrite, Replace_Slice): Remove SPARK_Mode Off. * libgnat/a-strfix.ads (Insert, Overwrite, Replace_Slice): Strengthen precondition. --- gcc/ada/libgnat/a-strfix.adb | 18 ++++++++++++------ gcc/ada/libgnat/a-strfix.ads | 20 +++++++++++++++++--- 2 files changed, 29 insertions(+), 9 deletions(-) diff --git a/gcc/ada/libgnat/a-strfix.adb b/gcc/ada/libgnat/a-strfix.adb index e6f882f..31dea6c 100644 --- a/gcc/ada/libgnat/a-strfix.adb +++ b/gcc/ada/libgnat/a-strfix.adb @@ -214,7 +214,8 @@ package body Ada.Strings.Fixed with SPARK_Mode is -- Lemma_Split -- ----------------- - procedure Lemma_Split (Result : String) is + procedure Lemma_Split (Result : String) + is begin for K in Ptr + 1 .. Ptr + Right'Length loop Lemma_Mod (K - 1); @@ -307,7 +308,8 @@ package body Ada.Strings.Fixed with SPARK_Mode is From : Positive; Through : Natural; Justify : Alignment := Left; - Pad : Character := Space) with SPARK_Mode => Off is + Pad : Character := Space) + is begin Move (Source => Delete (Source, From, Through), Target => Source, @@ -403,7 +405,8 @@ package body Ada.Strings.Fixed with SPARK_Mode is (Source : in out String; Before : Positive; New_Item : String; - Drop : Truncation := Error) with SPARK_Mode => Off is + Drop : Truncation := Error) + is begin Move (Source => Insert (Source, Before, New_Item), Target => Source, @@ -419,7 +422,8 @@ package body Ada.Strings.Fixed with SPARK_Mode is Target : out String; Drop : Truncation := Error; Justify : Alignment := Left; - Pad : Character := Space) with SPARK_Mode => Off + Pad : Character := Space) + with SPARK_Mode => Off is Sfirst : constant Integer := Source'First; Slast : constant Integer := Source'Last; @@ -571,7 +575,8 @@ package body Ada.Strings.Fixed with SPARK_Mode is (Source : in out String; Position : Positive; New_Item : String; - Drop : Truncation := Right) with SPARK_Mode => Off is + Drop : Truncation := Right) + is begin Move (Source => Overwrite (Source, Position, New_Item), Target => Source, @@ -648,7 +653,8 @@ package body Ada.Strings.Fixed with SPARK_Mode is By : String; Drop : Truncation := Error; Justify : Alignment := Left; - Pad : Character := Space) with SPARK_Mode => Off is + Pad : Character := Space) + is begin Move (Replace_Slice (Source, Low, High, By), Source, Drop, Justify, Pad); end Replace_Slice; diff --git a/gcc/ada/libgnat/a-strfix.ads b/gcc/ada/libgnat/a-strfix.ads index 3555c7d..1d9fd1b 100644 --- a/gcc/ada/libgnat/a-strfix.ads +++ b/gcc/ada/libgnat/a-strfix.ads @@ -904,7 +904,15 @@ package Ada.Strings.Fixed with SPARK_Mode is Justify : Alignment := Left; Pad : Character := Space) with - Pre => Low - 1 <= Source'Last, + Pre => + Low - 1 <= Source'Last + and then High >= Source'First - 1 + and then (if High >= Low + then Natural'Max (0, Low - Source'First) + <= Natural'Last + - By'Length + - Natural'Max (Source'Last - High, 0) + else Source'Length <= Natural'Last - By'Length), -- Incomplete contract @@ -966,7 +974,9 @@ package Ada.Strings.Fixed with SPARK_Mode is New_Item : String; Drop : Truncation := Error) with - Pre => Before - 1 in Source'First - 1 .. Source'Last, + Pre => + Before - 1 in Source'First - 1 .. Source'Last + and then Source'Length <= Natural'Last - New_Item'Length, -- Incomplete contract @@ -1033,7 +1043,11 @@ package Ada.Strings.Fixed with SPARK_Mode is New_Item : String; Drop : Truncation := Right) with - Pre => Position - 1 in Source'First - 1 .. Source'Last, + Pre => + Position - 1 in Source'First - 1 .. Source'Last + and then + (if Position - Source'First >= Source'Length - New_Item'Length + then Position - Source'First <= Natural'Last - New_Item'Length), -- Incomplete contract -- 2.7.4