diff options
| -rw-r--r-- | gcc/ada/libgnat/a-strunb.ads | 16 | ||||
| -rw-r--r-- | 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 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 "<" |