OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

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

Browse Source 
gcc/ada/

	* libgnat/a-strunb.ads: Mark package in SPARK with private part
	not in SPARK.
	(Free): Mark not in SPARK.
This commit is contained in:
Yannick Moy 2021-07-26 16:56:27 +02:00 committed by Pierre-Marie de Rodat
parent 9560e8430d
commit 490a987e05
1 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
gcc/ada/libgnat/a-strunb.ads
View File

@ -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;