[gcc r12-3846] [Ada] Minimize parts of Ada.Strings.Fixed marked SPARK_Mode => Off

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:7165704bfaae012cb28e5411619218da6fb8320d

commit r12-3846-g7165704bfaae012cb28e5411619218da6fb8320d
Author: Yannick Moy <moy@adacore.com>
Date:   Mon Jul 26 12:21:02 2021 +0200

    [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.

Diff:
---
 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 e6f882f2799..31dea6c04a1 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 3555c7d8e1b..1d9fd1b5303 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