Commit 0b8ff545 by Yannick Moy Committed by Pierre-Marie de Rodat

[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.

From-SVN: r266990
parent 5fc26697
2018-12-11 Yannick Moy <moy@adacore.com> 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 * gnat1drv.adb (Gnat1drv): Issue specific error message in
GNATprove mode when multiple file names on the command line. GNATprove mode when multiple file names on the command line.
* osint.adb, osint.ads (Dump_Command_Line_Source_File_Names): * osint.adb, osint.ads (Dump_Command_Line_Source_File_Names):
......
...@@ -10880,6 +10880,11 @@ package body Sem_Util is ...@@ -10880,6 +10880,11 @@ package body Sem_Util is
if Is_Scalar_Type (Typ) then if Is_Scalar_Type (Typ) then
return Has_Default_Aspect (Typ); 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 -- An array type is fully default initialized if its element type is
-- scalar and the array type carries aspect Default_Component_Value or -- scalar and the array type carries aspect Default_Component_Value or
-- the element type is fully default initialized. -- the element type is fully default initialized.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment