diff options
author | Joffrey Huguet <huguet@adacore.com> | 2023-01-16 16:44:14 +0100 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2023-05-22 10:44:08 +0200 |
commit | 561b239327842ca4f21bdbb6535e629b907355e4 (patch) | |
tree | 3ca867eb8d837cf5497a09bfc4a9b30821ec0b34 /gcc | |
parent | f23d4b88f5beffd8430b6b75088775614ed13980 (diff) | |
download | gcc-561b239327842ca4f21bdbb6535e629b907355e4.zip gcc-561b239327842ca4f21bdbb6535e629b907355e4.tar.gz gcc-561b239327842ca4f21bdbb6535e629b907355e4.tar.bz2 |
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.
Diffstat (limited to 'gcc')
-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 "<" |