[Ada] Missing predicate check on declaration with aggregate expression

[Ada] Missing predicate check on declaration with aggregate expression

[Pierre-Marie de Rodat]

[-- Attachment #1: Type: text/plain, Size: 1674 bytes --]

This patch adds a missing predicate check on the initial value of an
object whose declaration initializes the object with an aggregate. Such
a declaration is marked No_Initialization to prevent a call to a default
initialization procedure, but the check is needed on the value of the
aggregate.

Executing the following:

   gnatmake -q -gnata pred
   ./pred

must yield:

   raised SYSTEM.ASSERTIONS.ASSERT_FAILURE :
             Dynamic_Predicate failed at root.ads:30

----
with Root;

procedure Pred is
begin
   null;
end Pred;
----
package Root with SPARK_Mode is
   type Index_Type is range 1 .. Natural'Last;

   type Element_Type is private;
   Null_Element : constant Element_Type;

   type Foobar_Type is array (Index_Type range <>) of Element_Type
     with Dynamic_Predicate =>
            Foobar_Type'First > 0 and Foobar_Type'Length > 0;

   Null_Foobar : constant Foobar_Type;

private
   type Kind_Type is (Kind_Invalid, Kind_Valid);

   type Element_Type (Kind : Kind_Type := Kind_Invalid) is record
      Index1 : Index_Type;

      case Kind is
         when Kind_Valid =>
            Index2 : Index_Type;
         when Kind_Invalid =>
            null;
      end case;
   end record;

   Null_Element : constant Element_Type := (Kind   => Kind_Invalid,
                                            Index1 => Index_Type'First);

   Null_Foobar : constant Foobar_Type := (1 .. 0 => Null_Element);
end Root;

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

2018-12-11  Ed Schonberg  <schonberg@adacore.com>

gcc/ada/

	* sem_ch3.adb (Analyze_Object_Declaration): Apply
	Dynamic_Predicate check to an object of an array type
	initialized with an aggregate.

[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 900 bytes --]

--- gcc/ada/sem_ch3.adb
+++ gcc/ada/sem_ch3.adb
@@ -4454,11 +4454,16 @@ package body Sem_Ch3 is
       --  default initialization when we have at least one case of an explicit
       --  default initial value and then this is not an internal declaration
       --  whose initialization comes later (as for an aggregate expansion).
+      --  If expression is an aggregate it may be expanded into assignments
+      --  and the declaration itself is marked with No_Initialization, but
+      --  the predicate still applies.
 
       if not Suppress_Assignment_Checks (N)
         and then Present (Predicate_Function (T))
         and then not Predicates_Ignored (T)
-        and then not No_Initialization (N)
+        and then
+          (not No_Initialization (N)
+            or else (Present (E) and then Nkind (E) = N_Aggregate))
         and then
           (Present (E)
             or else