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 <kirtc...@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 <kirtc...@adacore.com>
* gnat.dg/dflt_init_cond.adb, gnat.dg/dflt_init_cond_pkg.ads: New
testcase.
Index: exp_util.adb
===================================================================
--- exp_util.adb (revision 255683)
+++ exp_util.adb (working copy)
@@ -165,6 +165,10 @@
-- Force evaluation of bounds of a slice, which may be given by a range
-- or by a subtype indication with or without a constraint.
+ function Is_Verifiable_DIC_Pragma (Prag : Node_Id) return Boolean;
+ -- Determine whether pragma Default_Initial_Condition denoted by Prag has
+ -- an assertion expression that should be verified at run time.
+
function Make_CW_Equivalent_Type
(T : Entity_Id;
E : Node_Id) return Entity_Id;
@@ -1500,6 +1504,7 @@
-- Start of processing for Add_Own_DIC
begin
+ pragma Assert (Present (DIC_Expr));
Expr := New_Copy_Tree (DIC_Expr);
-- Perform the following substitution:
@@ -1733,8 +1738,6 @@
-- Produce an empty completing body in the following cases:
-- * Assertions are disabled
-- * The DIC Assertion_Policy is Ignore
- -- * Pragma DIC appears without an argument
- -- * Pragma DIC appears with argument "null"
if No (Stmts) then
Stmts := New_List (Make_Null_Statement (Loc));
@@ -8715,6 +8718,21 @@
and then Is_Itype (Full_Typ);
end Is_Untagged_Private_Derivation;
+ ------------------------------
+ -- Is_Verifiable_DIC_Pragma --
+ ------------------------------
+
+ function Is_Verifiable_DIC_Pragma (Prag : Node_Id) return Boolean is
+ Args : constant List_Id := Pragma_Argument_Associations (Prag);
+
+ begin
+ -- To qualify as verifiable, a DIC pragma must have a non-null argument
+
+ return
+ Present (Args)
+ and then Nkind (Get_Pragma_Arg (First (Args))) /= N_Null;
+ end Is_Verifiable_DIC_Pragma;
+
---------------------------
-- Is_Volatile_Reference --
---------------------------
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 255680)
+++ sem_util.adb (working copy)
@@ -10384,19 +10384,16 @@
function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean is
Comp : Entity_Id;
- Prag : Node_Id;
begin
- -- A type subject to pragma Default_Initial_Condition is fully default
- -- initialized when the pragma appears with a non-null argument. Since
- -- any type may act as the full view of a private type, this check must
- -- be performed prior to the specialized tests below.
+ -- A type subject to pragma Default_Initial_Condition may be fully
+ -- default initialized depending on inheritance and the argument of
+ -- the pragma. Since any type may act as the full view of a private
+ -- type, this check must be performed prior to the specialized tests
+ -- below.
- if Has_DIC (Typ) then
- Prag := Get_Pragma (Typ, Pragma_Default_Initial_Condition);
- pragma Assert (Present (Prag));
-
- return Is_Verifiable_DIC_Pragma (Prag);
+ if Has_Fully_Default_Initializing_DIC_Pragma (Typ) then
+ return True;
end if;
-- A scalar type is fully default initialized if it is subject to aspect
@@ -10463,6 +10460,47 @@
end if;
end Has_Full_Default_Initialization;
+ -----------------------------------------------
+ -- Has_Fully_Default_Initializing_DIC_Pragma --
+ -----------------------------------------------
+
+ function Has_Fully_Default_Initializing_DIC_Pragma
+ (Typ : Entity_Id) return Boolean
+ is
+ Args : List_Id;
+ Prag : Node_Id;
+
+ begin
+ -- A type that inherits pragma Default_Initial_Condition from a parent
+ -- type is automatically fully default initialized.
+
+ if Has_Inherited_DIC (Typ) then
+ return True;
+
+ -- Otherwise the type is fully default initialized only when the pragma
+ -- appears without an argument, or the argument is non-null.
+
+ elsif Has_Own_DIC (Typ) then
+ Prag := Get_Pragma (Typ, Pragma_Default_Initial_Condition);
+ pragma Assert (Present (Prag));
+ Args := Pragma_Argument_Associations (Prag);
+
+ -- The pragma appears without an argument in which case it defaults
+ -- to True.
+
+ if No (Args) then
+ return True;
+
+ -- The pragma appears with a non-null expression
+
+ elsif Nkind (Get_Pragma_Arg (First (Args))) /= N_Null then
+ return True;
+ end if;
+ end if;
+
+ return False;
+ end Has_Fully_Default_Initializing_DIC_Pragma;
+
--------------------
-- Has_Infinities --
--------------------
@@ -17018,21 +17056,6 @@
end if;
end Is_Variable;
- ------------------------------
- -- Is_Verifiable_DIC_Pragma --
- ------------------------------
-
- function Is_Verifiable_DIC_Pragma (Prag : Node_Id) return Boolean is
- Args : constant List_Id := Pragma_Argument_Associations (Prag);
-
- begin
- -- To qualify as verifiable, a DIC pragma must have a non-null argument
-
- return
- Present (Args)
- and then Nkind (Get_Pragma_Arg (First (Args))) /= N_Null;
- end Is_Verifiable_DIC_Pragma;
-
---------------------------
-- Is_Visibly_Controlled --
---------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 255680)
+++ sem_util.ads (working copy)
@@ -1238,9 +1238,15 @@
-- either include a default expression or have a type which defines
-- full default initialization. In the case of type extensions, the
-- parent type defines full default initialization.
- -- * A task type
- -- * A private type whose Default_Initial_Condition is non-null
+ -- * A task type
+ -- * A private type with pragma Default_Initial_Condition that provides
+ -- full default initialization.
+ function Has_Fully_Default_Initializing_DIC_Pragma
+ (Typ : Entity_Id) return Boolean;
+ -- Determine whether type Typ has a suitable Default_Initial_Condition
+ -- pragma which provides the full default initialization of the type.
+
function Has_Infinities (E : Entity_Id) return Boolean;
-- Determines if the range of the floating-point type E includes
-- infinities. Returns False if E is not a floating-point type.
@@ -1980,10 +1986,6 @@
-- default is True since this routine is commonly invoked as part of the
-- semantic analysis and it must not be disturbed by the rewriten nodes.
- function Is_Verifiable_DIC_Pragma (Prag : Node_Id) return Boolean;
- -- Determine whether pragma Default_Initial_Condition denoted by Prag has
- -- an assertion expression which should be verified at runtime.
-
function Is_Visibly_Controlled (T : Entity_Id) return Boolean;
-- Check whether T is derived from a visibly controlled type. This is true
-- if the root type is declared in Ada.Finalization. If T is derived
Index: sem_warn.adb
===================================================================
--- sem_warn.adb (revision 255678)
+++ sem_warn.adb (working copy)
@@ -1742,22 +1742,17 @@
-----------------------------
function Is_OK_Fully_Initialized return Boolean is
- Prag : Node_Id;
-
begin
if Is_Access_Type (Typ) and then Is_Dereferenced (N) then
return False;
- -- A type subject to pragma Default_Initial_Condition is fully
- -- default initialized when the pragma appears with a non-null
- -- argument (SPARK RM 3.1 and SPARK RM 7.3.3).
+ -- A type subject to pragma Default_Initial_Condition may be fully
+ -- default initialized depending on inheritance and the argument of
+ -- the pragma (SPARK RM 3.1 and SPARK RM 7.3.3).
- elsif Has_DIC (Typ) then
- Prag := Get_Pragma (Typ, Pragma_Default_Initial_Condition);
- pragma Assert (Present (Prag));
+ elsif Has_Fully_Default_Initializing_DIC_Pragma (Typ) then
+ return True;
- return Is_Verifiable_DIC_Pragma (Prag);
-
else
return Is_Fully_Initialized_Type (Typ);
end if;
Index: ../testsuite/gnat.dg/dflt_init_cond.adb
===================================================================
--- ../testsuite/gnat.dg/dflt_init_cond.adb (revision 0)
+++ ../testsuite/gnat.dg/dflt_init_cond.adb (revision 0)
@@ -0,0 +1,12 @@
+-- { dg-do compile }
+
+with Dflt_Init_Cond_Pkg; use Dflt_Init_Cond_Pkg;
+
+procedure Dflt_Init_Cond is
+ E : Explicit;
+ I : Implicit;
+
+begin
+ Read (E);
+ Read (I);
+end Dflt_Init_Cond;
Index: ../testsuite/gnat.dg/dflt_init_cond_pkg.ads
===================================================================
--- ../testsuite/gnat.dg/dflt_init_cond_pkg.ads (revision 0)
+++ ../testsuite/gnat.dg/dflt_init_cond_pkg.ads (revision 0)
@@ -0,0 +1,11 @@
+package Dflt_Init_Cond_Pkg is
+ type Explicit is limited private with Default_Initial_Condition => True;
+ type Implicit is limited private with Default_Initial_Condition;
+
+ procedure Read (Obj : Explicit);
+ procedure Read (Obj : Implicit);
+
+private
+ type Implicit is access all Integer;
+ type Explicit is access all Integer;
+end Dflt_Init_Cond_Pkg;
