--- a/gcc/ada/libgnat/a-strunb__shared.ads	Thu Oct 25 07:37:49 2018 +0900
+++ b/gcc/ada/libgnat/a-strunb__shared.ads	Thu Feb 13 11:34:05 2020 +0900
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2018, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2019, Free Software Foundation, Inc.         --
 --                                                                          --
 -- This specification is derived from the Ada Reference Manual for use with --
 -- GNAT. The copyright notice above, and the license provisions that follow --
@@ -33,6 +33,12 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
+--  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.
+
+pragma Assertion_Policy (Pre => Ignore);
+
 --  This package provides an implementation of Ada.Strings.Unbounded that uses
 --  reference counts to implement copy on modification (rather than copy on
 --  assignment). This is significantly more efficient on many targets.
@@ -73,7 +79,9 @@
 private with Ada.Finalization;
 private with System.Atomic_Counters;
 
-package Ada.Strings.Unbounded is
+package Ada.Strings.Unbounded with
+  Initial_Condition => Length (Null_Unbounded_String) = 0
+is
    pragma Preelaborate;
 
    type Unbounded_String is private;
@@ -81,7 +89,8 @@
 
    Null_Unbounded_String : constant Unbounded_String;
 
-   function Length (Source : Unbounded_String) return Natural;
+   function Length (Source : Unbounded_String) return Natural with
+     Global => null;
 
    type String_Access is access all String;
 
@@ -92,136 +101,229 @@
    --------------------------------------------------------
 
    function To_Unbounded_String
-     (Source : String)  return Unbounded_String;
+     (Source : String)  return Unbounded_String
+   with
+     Post   => Length (To_Unbounded_String'Result) = Source'Length,
+     Global => null;
 
    function To_Unbounded_String
-     (Length : Natural) return Unbounded_String;
+     (Length : Natural) return Unbounded_String
+   with
+     Post   =>
+       Ada.Strings.Unbounded.Length (To_Unbounded_String'Result) = Length,
+     Global => null;
 
-   function To_String (Source : Unbounded_String) return String;
+   function To_String (Source : Unbounded_String) return String with
+     Post   => To_String'Result'Length = Length (Source),
+     Global => null;
 
    procedure Set_Unbounded_String
      (Target : out Unbounded_String;
-      Source : String);
+      Source : String)
+   with
+     Global => null;
    pragma Ada_05 (Set_Unbounded_String);
 
    procedure Append
      (Source   : in out Unbounded_String;
-      New_Item : Unbounded_String);
+      New_Item : Unbounded_String)
+   with
+     Pre    => Length (New_Item) <= Natural'Last - Length (Source),
+     Post   => Length (Source) = Length (Source)'Old + Length (New_Item),
+     Global => null;
 
    procedure Append
      (Source   : in out Unbounded_String;
-      New_Item : String);
+      New_Item : String)
+   with
+     Pre    => New_Item'Length <= Natural'Last - Length (Source),
+     Post   => Length (Source) = Length (Source)'Old + New_Item'Length,
+     Global => null;
 
    procedure Append
      (Source   : in out Unbounded_String;
-      New_Item : Character);
+      New_Item : Character)
+   with
+     Pre    => Length (Source) < Natural'Last,
+     Post   => Length (Source) = Length (Source)'Old + 1,
+     Global => null;
 
    function "&"
      (Left  : Unbounded_String;
-      Right : Unbounded_String) return Unbounded_String;
+      Right : Unbounded_String) return Unbounded_String
+   with
+     Pre    => Length (Right) <= Natural'Last - Length (Left),
+     Post   => Length ("&"'Result) = Length (Left) + Length (Right),
+     Global => null;
 
    function "&"
      (Left  : Unbounded_String;
-      Right : String) return Unbounded_String;
+      Right : String) return Unbounded_String
+   with
+     Pre    => Right'Length <= Natural'Last - Length (Left),
+     Post   => Length ("&"'Result) = Length (Left) + Right'Length,
+     Global => null;
 
    function "&"
      (Left  : String;
-      Right : Unbounded_String) return Unbounded_String;
+      Right : Unbounded_String) return Unbounded_String
+   with
+     Pre    => Left'Length <= Natural'Last - Length (Right),
+     Post   => Length ("&"'Result) = Left'Length + Length (Right),
+     Global => null;
 
    function "&"
      (Left  : Unbounded_String;
-      Right : Character) return Unbounded_String;
+      Right : Character) return Unbounded_String
+   with
+     Pre    => Length (Left) < Natural'Last,
+     Post   => Length ("&"'Result) = Length (Left) + 1,
+     Global => null;
 
    function "&"
      (Left  : Character;
-      Right : Unbounded_String) return Unbounded_String;
+      Right : Unbounded_String) return Unbounded_String
+   with
+     Pre    => Length (Right) < Natural'Last,
+     Post   => Length ("&"'Result) = Length (Right) + 1,
+     Global => null;
 
    function Element
      (Source : Unbounded_String;
-      Index  : Positive) return Character;
+      Index  : Positive) return Character
+   with
+     Pre    => Index <= Length (Source),
+     Global => null;
 
    procedure Replace_Element
      (Source : in out Unbounded_String;
       Index  : Positive;
-      By     : Character);
+      By     : Character)
+   with
+     Pre    => Index <= Length (Source),
+     Post   => Length (Source) = Length (Source)'Old,
+     Global => null;
 
    function Slice
      (Source : Unbounded_String;
       Low    : Positive;
-      High   : Natural) return String;
+      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),
+     Global => null;
 
    function Unbounded_Slice
      (Source : Unbounded_String;
       Low    : Positive;
-      High   : Natural) return Unbounded_String;
+      High   : Natural) return Unbounded_String
+   with
+     Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
+     Post   =>
+       Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1),
+     Global => null;
    pragma Ada_05 (Unbounded_Slice);
 
    procedure Unbounded_Slice
      (Source : Unbounded_String;
       Target : out Unbounded_String;
       Low    : Positive;
-      High   : Natural);
+      High   : Natural)
+   with
+     Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
+     Post   => Length (Target) = Natural'Max (0, High - Low + 1),
+     Global => null;
    pragma Ada_05 (Unbounded_Slice);
 
    function "="
      (Left  : Unbounded_String;
-      Right : Unbounded_String) return Boolean;
+      Right : Unbounded_String) return Boolean
+   with
+     Global => null;
 
    function "="
      (Left  : Unbounded_String;
-      Right : String) return Boolean;
+      Right : String) return Boolean
+   with
+     Global => null;
 
    function "="
      (Left  : String;
-      Right : Unbounded_String) return Boolean;
+      Right : Unbounded_String) return Boolean
+   with
+     Global => null;
 
    function "<"
      (Left  : Unbounded_String;
-      Right : Unbounded_String) return Boolean;
+      Right : Unbounded_String) return Boolean
+   with
+     Global => null;
 
    function "<"
      (Left  : Unbounded_String;
-      Right : String) return Boolean;
+      Right : String) return Boolean
+   with
+     Global => null;
 
    function "<"
      (Left  : String;
-      Right : Unbounded_String) return Boolean;
+      Right : Unbounded_String) return Boolean
+   with
+     Global => null;
 
    function "<="
      (Left  : Unbounded_String;
-      Right : Unbounded_String) return Boolean;
+      Right : Unbounded_String) return Boolean
+   with
+     Global => null;
 
    function "<="
      (Left  : Unbounded_String;
-      Right : String) return Boolean;
+      Right : String) return Boolean
+   with
+     Global => null;
 
    function "<="
      (Left  : String;
-      Right : Unbounded_String) return Boolean;
+      Right : Unbounded_String) return Boolean
+   with
+     Global => null;
 
    function ">"
      (Left  : Unbounded_String;
-      Right : Unbounded_String) return Boolean;
+      Right : Unbounded_String) return Boolean
+   with
+     Global => null;
 
    function ">"
      (Left  : Unbounded_String;
-      Right : String) return Boolean;
+      Right : String) return Boolean
+   with
+     Global => null;
 
    function ">"
      (Left  : String;
-      Right : Unbounded_String) return Boolean;
+      Right : Unbounded_String) return Boolean
+   with
+     Global => null;
 
    function ">="
      (Left  : Unbounded_String;
-      Right : Unbounded_String) return Boolean;
+      Right : Unbounded_String) return Boolean
+   with
+     Global => null;
 
    function ">="
      (Left  : Unbounded_String;
-      Right : String) return Boolean;
+      Right : String) return Boolean
+   with
+     Global => null;
 
    function ">="
      (Left  : String;
-      Right : Unbounded_String) return Boolean;
+      Right : Unbounded_String) return Boolean
+   with
+     Global => null;
 
    ------------------------
    -- Search Subprograms --
@@ -231,26 +333,39 @@
      (Source  : Unbounded_String;
       Pattern : String;
       Going   : Direction := Forward;
-      Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+      Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+   with
+     Pre    => Pattern'Length /= 0,
+     Global => null;
 
    function Index
      (Source  : Unbounded_String;
       Pattern : String;
       Going   : Direction := Forward;
-      Mapping : Maps.Character_Mapping_Function) return Natural;
+      Mapping : Maps.Character_Mapping_Function) return Natural
+   with
+     Pre    => Pattern'Length /= 0,
+     Global => null;
 
    function Index
      (Source : Unbounded_String;
       Set    : Maps.Character_Set;
       Test   : Membership := Inside;
-      Going  : Direction  := Forward) return Natural;
+      Going  : Direction  := Forward) return Natural
+   with
+     Global => null;
 
    function Index
      (Source  : Unbounded_String;
       Pattern : String;
       From    : Positive;
       Going   : Direction := Forward;
-      Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+      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;
    pragma Ada_05 (Index);
 
    function Index
@@ -258,7 +373,13 @@
       Pattern : String;
       From    : Positive;
       Going   : Direction := Forward;
-      Mapping : Maps.Character_Mapping_Function) return Natural;
+      Mapping : Maps.Character_Mapping_Function) return Natural
+   with
+     Pre    => (if Length (Source) /= 0
+                then From <= Length (Source))
+                       and then Pattern'Length /= 0,
+     Global => null;
+
    pragma Ada_05 (Index);
 
    function Index
@@ -266,32 +387,48 @@
       Set     : Maps.Character_Set;
       From    : Positive;
       Test    : Membership := Inside;
-      Going   : Direction := Forward) return Natural;
+      Going   : Direction := Forward) return Natural
+   with
+     Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
+     Global => null;
    pragma Ada_05 (Index);
 
    function Index_Non_Blank
      (Source : Unbounded_String;
-      Going  : Direction := Forward) return Natural;
+      Going  : Direction := Forward) return Natural
+   with
+     Global => null;
 
    function Index_Non_Blank
      (Source : Unbounded_String;
       From   : Positive;
-      Going  : Direction := Forward) return Natural;
+      Going  : Direction := Forward) return Natural
+   with
+     Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
+     Global => null;
    pragma Ada_05 (Index_Non_Blank);
 
    function Count
      (Source  : Unbounded_String;
       Pattern : String;
-      Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+      Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+   with
+     Pre    => Pattern'Length /= 0,
+     Global => null;
 
    function Count
      (Source  : Unbounded_String;
       Pattern : String;
-      Mapping : Maps.Character_Mapping_Function) return Natural;
+      Mapping : Maps.Character_Mapping_Function) return Natural
+   with
+     Pre    => Pattern'Length /= 0,
+     Global => null;
 
    function Count
      (Source : Unbounded_String;
-      Set    : Maps.Character_Set) return Natural;
+      Set    : Maps.Character_Set) return Natural
+   with
+     Global => null;
 
    procedure Find_Token
      (Source : Unbounded_String;
@@ -299,7 +436,10 @@
       From   : Positive;
       Test   : Membership;
       First  : out Positive;
-      Last   : out Natural);
+      Last   : out Natural)
+   with
+     Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
+     Global => null;
    pragma Ada_2012 (Find_Token);
 
    procedure Find_Token
@@ -307,7 +447,9 @@
       Set    : Maps.Character_Set;
       Test   : Membership;
       First  : out Positive;
-      Last   : out Natural);
+      Last   : out Natural)
+   with
+     Global => null;
 
    ------------------------------------
    -- String Translation Subprograms --
@@ -315,19 +457,31 @@
 
    function Translate
      (Source  : Unbounded_String;
-      Mapping : Maps.Character_Mapping) return Unbounded_String;
+      Mapping : Maps.Character_Mapping) return Unbounded_String
+   with
+     Post   => Length (Translate'Result) = Length (Source),
+     Global => null;
 
    procedure Translate
      (Source  : in out Unbounded_String;
-      Mapping : Maps.Character_Mapping);
+      Mapping : Maps.Character_Mapping)
+   with
+     Post   => Length (Source) = Length (Source)'Old,
+     Global => null;
 
    function Translate
      (Source  : Unbounded_String;
-      Mapping : Maps.Character_Mapping_Function) return Unbounded_String;
+      Mapping : Maps.Character_Mapping_Function) return Unbounded_String
+   with
+     Post   => Length (Translate'Result) = Length (Source),
+     Global => null;
 
    procedure Translate
      (Source  : in out Unbounded_String;
-      Mapping : Maps.Character_Mapping_Function);
+      Mapping : Maps.Character_Mapping_Function)
+   with
+     Post   => Length (Source) = Length (Source)'Old,
+     Global => null;
 
    ---------------------------------------
    -- String Transformation Subprograms --
@@ -337,93 +491,204 @@
      (Source : Unbounded_String;
       Low    : Positive;
       High   : Natural;
-      By     : String) return Unbounded_String;
+      By     : String) return Unbounded_String
+   with
+     Pre            =>
+       Low - 1 <= Length (Source)
+         and then (if High >= Low
+                   then Low - 1
+                     <= Natural'Last - By'Length
+                      - Natural'Max (Length (Source) - High, 0)
+                   else Length (Source) <= Natural'Last - By'Length),
+     Contract_Cases =>
+       (High >= Low =>
+          Length (Replace_Slice'Result)
+        = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
+        others      =>
+          Length (Replace_Slice'Result) = Length (Source)'Old + By'Length),
+     Global         => null;
 
    procedure Replace_Slice
      (Source : in out Unbounded_String;
       Low    : Positive;
       High   : Natural;
-      By     : String);
+      By     : String)
+   with
+     Pre            =>
+       Low - 1 <= Length (Source)
+         and then (if High >= Low
+                   then Low - 1
+                     <= Natural'Last - By'Length
+                      - Natural'Max (Length (Source) - High, 0)
+                   else Length (Source) <= Natural'Last - By'Length),
+     Contract_Cases =>
+       (High >= Low =>
+          Length (Source)
+        = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
+        others      =>
+          Length (Source) = Length (Source)'Old + By'Length),
+     Global         => null;
 
    function Insert
      (Source   : Unbounded_String;
       Before   : Positive;
-      New_Item : String) return Unbounded_String;
+      New_Item : String) return Unbounded_String
+   with
+     Pre    => Before - 1 <= Length (Source)
+                 and then New_Item'Length <= Natural'Last - Length (Source),
+     Post   => Length (Insert'Result) = Length (Source) + New_Item'Length,
+     Global => null;
 
    procedure Insert
      (Source   : in out Unbounded_String;
       Before   : Positive;
-      New_Item : String);
+      New_Item : String)
+   with
+     Pre    => Before - 1 <= Length (Source)
+                 and then New_Item'Length <= Natural'Last - Length (Source),
+     Post   => Length (Source) = Length (Source)'Old + New_Item'Length,
+     Global => null;
 
    function Overwrite
      (Source   : Unbounded_String;
       Position : Positive;
-      New_Item : String) return Unbounded_String;
+      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)),
+     Post   =>
+       Length (Overwrite'Result)
+     = Natural'Max (Length (Source), Position - 1 + New_Item'Length),
+     Global => null;
 
    procedure Overwrite
      (Source   : in out Unbounded_String;
       Position : Positive;
-      New_Item : String);
+      New_Item : String)
+   with
+     Pre    => Position - 1 <= Length (Source)
+                 and then (if New_Item'Length /= 0
+                           then
+                             New_Item'Length <= Natural'Last - (Position - 1)),
+     Post   =>
+       Length (Source)
+     = Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length),
+
+     Global => null;
 
    function Delete
      (Source  : Unbounded_String;
       From    : Positive;
-      Through : Natural) return Unbounded_String;
+      Through : Natural) return Unbounded_String
+   with
+     Pre            => (if Through <= From then From - 1 <= Length (Source)),
+     Contract_Cases =>
+       (Through >= From =>
+          Length (Delete'Result) = Length (Source) - (Through - From + 1),
+        others          =>
+          Length (Delete'Result) = Length (Source)),
+     Global         => null;
 
    procedure Delete
      (Source  : in out Unbounded_String;
       From    : Positive;
-      Through : Natural);
+      Through : Natural)
+   with
+     Pre            => (if Through <= From then From - 1 <= Length (Source)),
+     Contract_Cases =>
+       (Through >= From =>
+          Length (Source) = Length (Source)'Old - (Through - From + 1),
+        others          =>
+          Length (Source) = Length (Source)'Old),
+     Global         => null;
 
    function Trim
      (Source : Unbounded_String;
-      Side   : Trim_End) return Unbounded_String;
+      Side   : Trim_End) return Unbounded_String
+   with
+     Post   => Length (Trim'Result) <= Length (Source),
+     Global => null;
 
    procedure Trim
      (Source : in out Unbounded_String;
-      Side   : Trim_End);
+      Side   : Trim_End)
+   with
+     Post   => Length (Source) <= Length (Source)'Old,
+     Global => null;
 
    function Trim
      (Source : Unbounded_String;
       Left   : Maps.Character_Set;
-      Right  : Maps.Character_Set) return Unbounded_String;
+      Right  : Maps.Character_Set) return Unbounded_String
+   with
+     Post   => Length (Trim'Result) <= Length (Source),
+     Global => null;
 
    procedure Trim
      (Source : in out Unbounded_String;
       Left   : Maps.Character_Set;
-      Right  : Maps.Character_Set);
+      Right  : Maps.Character_Set)
+   with
+     Post   => Length (Source) <= Length (Source)'Old,
+     Global => null;
 
    function Head
      (Source : Unbounded_String;
       Count  : Natural;
-      Pad    : Character := Space) return Unbounded_String;
+      Pad    : Character := Space) return Unbounded_String
+   with
+     Post   => Length (Head'Result) = Count,
+     Global => null;
 
    procedure Head
      (Source : in out Unbounded_String;
       Count  : Natural;
-      Pad    : Character := Space);
+      Pad    : Character := Space)
+   with
+     Post   => Length (Source) = Count,
+     Global => null;
 
    function Tail
      (Source : Unbounded_String;
       Count  : Natural;
-      Pad    : Character := Space) return Unbounded_String;
+      Pad    : Character := Space) return Unbounded_String
+   with
+     Post   => Length (Tail'Result) = Count,
+     Global => null;
 
    procedure Tail
      (Source : in out Unbounded_String;
       Count  : Natural;
-      Pad    : Character := Space);
+      Pad    : Character := Space)
+   with
+     Post   => Length (Source) = Count,
+     Global => null;
 
    function "*"
      (Left  : Natural;
-      Right : Character) return Unbounded_String;
+      Right : Character) return Unbounded_String
+   with
+     Pre    => Left <= Natural'Last,
+     Post   => Length ("*"'Result) = Left,
+     Global => null;
 
    function "*"
      (Left  : Natural;
-      Right : String) return Unbounded_String;
+      Right : String) return Unbounded_String
+   with
+     Pre    => (if Left /= 0 then Right'Length <= Natural'Last / Left),
+     Post   => Length ("*"'Result) = Left * Right'Length,
+     Global => null;
 
    function "*"
      (Left  : Natural;
-      Right : Unbounded_String) return Unbounded_String;
+      Right : Unbounded_String) return Unbounded_String
+   with
+     Pre    => (if Left /= 0 then Length (Right) <= Natural'Last / Left),
+     Post   => Length ("*"'Result) = Left * Length (Right),
+     Global => null;
 
 private
    pragma Inline (Length);