git
/
gcc
mirror of git://gcc.gnu.org/git/gcc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

[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
This commit is contained in:
Ed Schonberg 2018-12-11 11:11:17 +00:00 committed by Pierre-Marie de Rodat
parent 0617753f4a
commit 0a4578b6c6
2 changed files with 12 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
gcc/ada/ChangeLog
View File

@ -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

7
gcc/ada/sem_ch3.adb
View File

@ -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