[COMMITTED] ada: Add contracts to Ada.Strings.Unbounded library

[Marc Poulhiès via Gcc-patches]

From: Joffrey Huguet <hug...@adacore.com>

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.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/libgnat/a-strunb.ads         | 16 +++++++++++-----
 gcc/ada/libgnat/a-strunb__shared.ads | 16 +++++++++++-----
 2 files changed, 22 insertions(+), 10 deletions(-)

diff --git a/gcc/ada/libgnat/a-strunb.ads b/gcc/ada/libgnat/a-strunb.ads
index 0b0085a41b1..d3e88d0b4b6 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 bb69056299f..3f5d56e0a8c 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 "<"
-- 
2.40.0