diff mbox series

[Ada] Support access types in GNATprove

Message ID 20181211113237.GA105080@adacore.com
State New
Headers show
Series [Ada] Support access types in GNATprove | expand

Commit Message

Pierre-Marie de Rodat Dec. 11, 2018, 11:32 a.m. UTC 
SPARK RM has been updated to support access types in SPARK. Part of this
support is that now SPARK RM 3.1 lists access types as having full
default initialization. Now updated.

There is no impact on compilation.

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

2018-12-11  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_util.adb (Has_Full_Default_Initialization): Consider
	access types as having full default initialization.
diff mbox series

Patch

--- gcc/ada/sem_util.adb
+++ gcc/ada/sem_util.adb
@@ -10880,6 +10880,11 @@  package body Sem_Util is
       if Is_Scalar_Type (Typ) then
          return Has_Default_Aspect (Typ);
 
+      --  An access type is fully default initialized by default
+
+      elsif Is_Access_Type (Typ) then
+         return True;
+
       --  An array type is fully default initialized if its element type is
       --  scalar and the array type carries aspect Default_Component_Value or
       --  the element type is fully default initialized.