ada: Add contracts to Ada.Strings.Unbounded library

This patch adds contracts to the conversions between
Unbounded_String and String, the Element function and the
equality between two Unbounded_String, or between
Unbounded_String and String.
This patch also disallows the use of a function in SPARK, because
it returns an uninitialized Unbounded_String.

gcc/ada/

	* libgnat/a-strunb.ads, libgnat/a-strunb__shared.ads
	(To_Unbounded_String): Add postcondition. Add aspect SPARK_Mode
	Off on the version that takes a Natural as parameter.
	(To_String): Complete postcondition.
	(Set_Unbounded_String): Add postcondition.
	(Element): Likewise.
	("="): Likewise.

2 files changed, 22 insertions, 10 deletions

diff --git a/gcc/ada/libgnat/a-strunb.ads b/gcc/ada/libgnat/a-strunb.ads
index 0b0085a..d3e88d0 100644
--- a/gcc/ada/libgnat/a-strunb.ads
+++ b/gcc/ada/libgnat/a-strunb.ads
@@ -86,21 +86,22 @@ is
    function To_Unbounded_String
      (Source : String)  return Unbounded_String
    with
-     Post   => Length (To_Unbounded_String'Result) = Source'Length,
+     Post   => To_String (To_Unbounded_String'Result) = Source,
      Global => null;
    --  Returns an Unbounded_String that represents Source
 
    function To_Unbounded_String
      (Length : Natural) return Unbounded_String
    with
-     Post   =>
-       Ada.Strings.Unbounded.Length (To_Unbounded_String'Result) = Length,
-     Global => null;
+     SPARK_Mode => Off,
+     Global     => null;
    --  Returns an Unbounded_String that represents an uninitialized String
    --  whose length is Length.
 
    function To_String (Source : Unbounded_String) return String with
-     Post   => To_String'Result'Length = Length (Source),
+     Post   =>
+       To_String'Result'First = 1
+         and then To_String'Result'Length = Length (Source),
      Global => null;
    --  Returns the String with lower bound 1 represented by Source
 
@@ -115,6 +116,7 @@ is
      (Target : out Unbounded_String;
       Source : String)
    with
+     Post   => To_String (Target) = Source,
      Global => null;
    pragma Ada_05 (Set_Unbounded_String);
    --  Sets Target to an Unbounded_String that represents Source
@@ -198,6 +200,7 @@ is
       Index  : Positive) return Character
    with
      Pre    => Index <= Length (Source),
+     Post   => Element'Result = To_String (Source) (Index),
      Global => null;
    --  Returns the character at position Index in the string represented by
    --  Source; propagates Index_Error if Index > Length (Source).
@@ -259,18 +262,21 @@ 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 "<"
diff --git a/gcc/ada/libgnat/a-strunb__shared.ads b/gcc/ada/libgnat/a-strunb__shared.ads
index bb69056..3f5d56e 100644
--- a/gcc/ada/libgnat/a-strunb__shared.ads
+++ b/gcc/ada/libgnat/a-strunb__shared.ads
@@ -108,24 +108,26 @@ is
    function To_Unbounded_String
      (Source : String)  return Unbounded_String
    with
-     Post   => Length (To_Unbounded_String'Result) = Source'Length,
+     Post   => To_String (To_Unbounded_String'Result) = Source,
      Global => null;
 
    function To_Unbounded_String
      (Length : Natural) return Unbounded_String
    with
-     Post   =>
-       Ada.Strings.Unbounded.Length (To_Unbounded_String'Result) = Length,
-     Global => null;
+     SPARK_Mode => Off,
+     Global     => null;
 
    function To_String (Source : Unbounded_String) return String with
-     Post   => To_String'Result'Length = Length (Source),
+     Post   =>
+       To_String'Result'First = 1
+         and then To_String'Result'Length = Length (Source),
      Global => null;
 
    procedure Set_Unbounded_String
      (Target : out Unbounded_String;
       Source : String)
    with
+     Post   => To_String (Target) = Source,
      Global => null;
    pragma Ada_05 (Set_Unbounded_String);
 
@@ -198,6 +200,7 @@ is
       Index  : Positive) return Character
    with
      Pre    => Index <= Length (Source),
+     Post   => Element'Result = To_String (Source) (Index),
      Global => null;
 
    procedure Replace_Element
@@ -244,18 +247,21 @@ 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 "<"