From 0a4578b6c6d1febbb569a473c1142135906cab18 Mon Sep 17 00:00:00 2001 From: Ed Schonberg Date: Tue, 11 Dec 2018 11:11:17 +0000 Subject: [PATCH] [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 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 --- gcc/ada/ChangeLog | 6 ++++++ gcc/ada/sem_ch3.adb | 7 ++++++- 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index b10768b..1f59c88 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,9 @@ +2018-12-11 Ed Schonberg + + * 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 * 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 5195f8a..bbae468 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 -- 2.7.4