[Ada] Missing predicate check on declaration with aggregate expression

Pierre-Marie de Rodat derodat@adacore.com
Tue Dec 11 11:34:00 GMT 2018

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

Executing the following:

   gnatmake -q -gnata pred

must yield:

             Dynamic_Predicate failed at root.ads:30

with Root;

procedure Pred is
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;

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


	* sem_ch3.adb (Analyze_Object_Declaration): Apply
	Dynamic_Predicate check to an object of an array type
	initialized with an aggregate.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: patch.diff
Type: text/x-diff
Size: 900 bytes
Desc: not available
URL: <http://gcc.gnu.org/pipermail/gcc-patches/attachments/20181211/7878428e/attachment.bin>

More information about the Gcc-patches mailing list