Except for the Free procedure which should not be called in SPARK code
(as it could be called on pointers to the stack), the rest of the public
API of Ada.Strings.Unbounded is valid in SPARK. Mark the private part
not in SPARK as it uses controlled types.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/a-strunb.ads: Mark package in SPARK with private part
not in SPARK.
(Free): Mark not in SPARK.diff --git a/gcc/ada/libgnat/a-strunb.ads b/gcc/ada/libgnat/a-strunb.ads
--- 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;
