diff mbox series

[Ada] Add Default_Initial_Condition to type Unbounded_String

Message ID 20211005082636.GA2693574@adacore.com
State New
Headers show
Series [Ada] Add Default_Initial_Condition to type Unbounded_String | expand

Commit Message

Pierre-Marie de Rodat Oct. 5, 2021, 8:26 a.m. UTC 
SPARK emitted spurious checks on Unbounded_String variables that were
not initialized. This patch adds a default initial condition to the type
Unbounded_String so that they disappear.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* libgnat/a-strunb.ads, libgnat/a-strunb__shared.ads: Add
	Default_Initial_Condition to Unbounded_String.
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
@@ -58,7 +58,8 @@  package Ada.Strings.Unbounded with
 is
    pragma Preelaborate;
 
-   type Unbounded_String is private;
+   type Unbounded_String is private with
+     Default_Initial_Condition => Length (Unbounded_String) = 0;
    pragma Preelaborable_Initialization (Unbounded_String);
 
    Null_Unbounded_String : constant Unbounded_String;


diff --git a/gcc/ada/libgnat/a-strunb__shared.ads b/gcc/ada/libgnat/a-strunb__shared.ads
--- a/gcc/ada/libgnat/a-strunb__shared.ads
+++ b/gcc/ada/libgnat/a-strunb__shared.ads
@@ -85,7 +85,8 @@  package Ada.Strings.Unbounded with
 is
    pragma Preelaborate;
 
-   type Unbounded_String is private;
+   type Unbounded_String is private with
+     Default_Initial_Condition => Length (Unbounded_String) = 0;
    pragma Preelaborable_Initialization (Unbounded_String);
 
    Null_Unbounded_String : constant Unbounded_String;