[Ada] Support access types in GNATprove

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.

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.

git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@266990 138bc75d-0d04-0410-961f-82ee72b054a4

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 003bea4501d131e75e6668873213293df8f242ea..4713510d848db00cfa92e2a7a17509acfdd43470 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2018-12-11  Yannick Moy  <moy@adacore.com>
+
+       * sem_util.adb (Has_Full_Default_Initialization): Consider
+       access types as having full default initialization.
+
 2018-12-11  Yannick Moy  <moy@adacore.com>
 
        * gnat1drv.adb (Gnat1drv): Issue specific error message in

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index cf13c246d4b8e6cf753147de3306a0c85980a433..c5a194486bcec63d59e4934332557b590393b01b 100644 (file)
--- a/gcc/ada/sem_util.adb
+++ b/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.