From 0b8ff545ed09781fdbe20f1a6b9388db9b912a3c Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Tue, 11 Dec 2018 11:10:12 +0000 Subject: [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 gcc/ada/ * sem_util.adb (Has_Full_Default_Initialization): Consider access types as having full default initialization. From-SVN: r266990 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/sem_util.adb | 5 +++++ 2 files changed, 10 insertions(+) (limited to 'gcc') diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 003bea4..4713510 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,10 @@ 2018-12-11 Yannick Moy + * sem_util.adb (Has_Full_Default_Initialization): Consider + access types as having full default initialization. + +2018-12-11 Yannick Moy + * gnat1drv.adb (Gnat1drv): Issue specific error message in GNATprove mode when multiple file names on the command line. * osint.adb, osint.ads (Dump_Command_Line_Source_File_Names): diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index cf13c24..c5a1944 100644 --- 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. -- cgit v1.1