diff options
| author | Yannick Moy <moy@adacore.com> | 2021-07-26 16:56:27 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-09-22 15:01:49 +0000 |
| commit | 490a987e05da85710ca68f4f30948ec904d745e9 (patch) | |
| tree | 1eceff768bae55f7c45e7bb552a21ea73fac603c | |
| parent | 9560e8430de8a427504183c1b3dd7d781653fe25 (diff) | |
| download | gcc-490a987e05da85710ca68f4f30948ec904d745e9.zip gcc-490a987e05da85710ca68f4f30948ec904d745e9.tar.gz gcc-490a987e05da85710ca68f4f30948ec904d745e9.tar.bz2 | |
[Ada] Clarify parts of Ada.Strings.Unbounded in SPARK or not
gcc/ada/
* libgnat/a-strunb.ads: Mark package in SPARK with private part
not in SPARK.
(Free): Mark not in SPARK.
| -rw-r--r-- | gcc/ada/libgnat/a-strunb.ads | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/gcc/ada/libgnat/a-strunb.ads b/gcc/ada/libgnat/a-strunb.ads index 13c7612..77d8a59 100644 --- a/gcc/ada/libgnat/a-strunb.ads +++ b/gcc/ada/libgnat/a-strunb.ads @@ -53,6 +53,7 @@ private with Ada.Strings.Text_Buffers; -- and selector operations are provided. package Ada.Strings.Unbounded with + SPARK_Mode, Initial_Condition => Length (Null_Unbounded_String) = 0 is pragma Preelaborate; @@ -73,7 +74,7 @@ is -- Provides a (nonprivate) access type for explicit processing of -- unbounded-length strings. - procedure Free (X : in out String_Access); + procedure Free (X : in out String_Access) with SPARK_Mode => Off; -- Performs an unchecked deallocation of an object of type String_Access -------------------------------------------------------- @@ -732,6 +733,8 @@ is -- strings applied to the string represented by Source's original value. private + pragma SPARK_Mode (Off); -- Controlled types are not in SPARK + pragma Inline (Length); package AF renames Ada.Finalization; |