From: Ed Schonberg <schonberg@adacore.com>
Date: Tue, 11 Dec 2018 11:11:17 +0000 (+0000)
Subject: [Ada] Missing predicate check on declaration with aggregate expression
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0a4578b6c6d1febbb569a473c1142135906cab18;p=gcc.git

[Ada] Missing predicate check on declaration with aggregate expression

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;

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.

From-SVN: r267002
---

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index b10768b354d..1f59c88303b 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,9 @@
+2018-12-11  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch3.adb (Analyze_Object_Declaration): Apply
+	Dynamic_Predicate check to an object of an array type
+	initialized with an aggregate.
+
 2018-12-11  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* freeze.adb (Add_To_Result): Move the ignored Ghost-specific
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 5195f8a267b..bbae46858f2 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/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