[Ada] Spurious warning on default initialized object

Message ID 20171215111632.GA47477@adacore.com
State New
Headers show
Series
  • [Ada] Spurious warning on default initialized object
Related show

Commit Message

Pierre-Marie de Rodat Dec. 15, 2017, 11:16 a.m.
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.

Patch

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;