[Ada] Spurious warning on default initialized object

[Pierre-Marie de Rodat <derodat at adacore dot com>]

This patch updates the implications that pragma Default_Initial_Condition has
on full default initialization of objects and types. According to the SPARK RM,
the pragma may appear without an expression

   7.3.3 The aspect_definition may be omitted; this is semantically equivalent
         to specifying a static Boolean_expression having the value True.

which also satisfies the notion of "full default initialization" in SPARK

   3.1   A type is said to define full default initialization if it is

            * a private type whose Default_Initial_Condition aspect is
              specified to be a Boolean_expression.

The end result is that an object is now considered fully default initialized
for warning purposes. Prior to this patch, the compiler would warn on a read
of an object when

   * The object has default initialization
   * The object type carries pragma Default_Initial_Condition without an
     expression
   * No value is provided in between the object declaration and read

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

gcc/ada/

2017-12-15  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_util.adb (Add_Own_DIC): Ensure that the expression of the pragma
	is available (Is_Verifiable_DIC_Pragma): Moved from Sem_Util.
	* sem_util.adb (Has_Full_Default_Initialization):
	Has_Fully_Default_Initializing_DIC_Pragma is now used to determine
	whether a type has full default initialization due to pragma
	Default_Initial_Condition.
	(Has_Fully_Default_Initializing_DIC_Pragma): New routine.
	(Is_Verifiable_DIC_Pragma): Moved to Exp_Util.
	* sem_util.ads (Has_Fully_Default_Initializing_DIC_Pragma): New
	routine.
	(Is_Verifiable_DIC_Pragma): Moved to Exp_Util.
	* sem_warn.adb (Is_OK_Fully_Initialized):
	Has_Fully_Default_Initializing_DIC_Pragma is now used to determine
	whether a type has full default initialization due to pragma
	Default_Initial_Condition.

gcc/testsuite/

2017-12-15  Hristian Kirtchev  <kirtchev@adacore.com>

	* gnat.dg/dflt_init_cond.adb, gnat.dg/dflt_init_cond_pkg.ads: New
	testcase.

Attachment: difs
Description: Text document