diff mbox series

[Ada] Clarify parts of Ada.Strings.Unbounded in SPARK or not

Message ID 20210922151607.GA1908133@adacore.com
State New
Headers show
Series [Ada] Clarify parts of Ada.Strings.Unbounded in SPARK or not | expand

Commit Message

Pierre-Marie de Rodat Sept. 22, 2021, 3:16 p.m. UTC 
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 mbox series

Patch

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;