[Ada] Aspect/pragma Default_Initial_Condition

[Arnaud Charlet <charlet at adacore dot com>]

This patch implements aspect/pragma Default_Initial_Condition. The construct
has the following semantics and runtime behavior:

The Default_Initial_Condition aspect is introduced by an aspect_specification
where the aspect_mark is Default_Initial_Condition. The aspect may be specified
only as part the aspect_specification of a private_type_declaration. The
aspect_definition, if any, of such an aspect specification shall be either a
null literal or a Boolean_expression.

The aspect_definition may be omitted; this is semantically equivalent to
specifying a static Boolean_expression having the value True. An aspect
specification of "null" indicates that the partial view of the type does not
define full default initialization.

Conversely, an aspect specification of a Boolean_expression indicates that the
partial view of the type does define full default initialization. In this case,
the completion of the private type shall define full default initialization.
Unlike the null literal case, this case has associated dynamic semantics. The
Boolean_expression (which might typically mention the current instance of the
type, although this is not required) is an assertion which is checked (at run
time) after any object of the given type (or of any descendant of the given
type for which the specified aspect is inherited and not overridden), is
?–?
8?ninitialized by default?–?
8?o (see Ada RM 3.3.1).

The Boolean_expression, if any, causes freezing in the same way as the
default_expression of a component_declaration.

Default_Initial_Condition assertion is an assertion aspect, which means that it
may be used in an Assertion_Policy pragma.

------------
-- Source --
------------

--  checker.ads

generic
   type Typ is private;
   Test : String;
procedure Checker;

--  checker.adb

with Ada.Assertions; use Ada.Assertions;
with Ada.Exceptions; use Ada.Exceptions;
with Ada.Text_IO;    use Ada.Text_IO;

procedure Checker is
begin
   declare
      Obj : Typ;
      pragma Unreferenced (Obj);
   begin
      Put_Line ("ERROR " & Test & ": Assertion_Error not raised");
   end;

exception
   when Ex : Assertion_Error =>
      Put_Line (Test & " OK");
      Put_Line (Exception_Information (Ex));

   when others =>
      Put_Line ("ERROR " & Test & ": unexpected exception");
end Checker;

--  derivations.ads

package Derivations is
   type T1 is tagged private
     with Default_Initial_Condition => Crash_1 (T1);
   type T2 is new T1 with private;      --  inherits Crash_1
   type T3 is new T1 with private       --  overrides with Crash_3
     with Default_Initial_Condition => Crash_3 (T3);
   type T4 is new T2 with private       --  overrides with Crash_4
     with Default_Initial_Condition => Crash_4 (T4);

   function Crash_1 (Obj : T1) return Boolean;
   function Crash_3 (Obj : T3) return Boolean;
   function Crash_4 (Obj : T4) return Boolean;
   procedure Force_Body;

private
   type T1 is tagged null record;
   function Crash_1 (Obj : T1) return Boolean is (False);
   type T2 is new T1 with null record;
   type T3 is new T1 with null record;
   function Crash_3 (Obj : T3) return Boolean is (False);
   type T4 is new T2 with null record;
   function Crash_4 (Obj : T4) return Boolean is (False);

   type T5 is new T1 with null record;  --  inherits Crash_1
   type T6 is new T2 with null record;  --  inherits Crash_2
   type T7 is new T3 with null record;  --  inherits Crash_3
   type T8 is new T4 with null record;  --  inherits Crash_4

   subtype T9  is T5;                   --  inherits Crash_1
   subtype T10 is T6;                   --  inherits Crash_2
   subtype T11 is T7;                   --  inherits Crash_3
   subtype T12 is T8;                   --  inherits Crash_4
end Derivations;

--  derivations.adb

with Checker;

package body Derivations is
   procedure Check_T1  is new Checker (T1,  "Test 1");
   procedure Check_T2  is new Checker (T2,  "Test 2");
   procedure Check_T3  is new Checker (T3,  "Test 3");
   procedure Check_T4  is new Checker (T4,  "Test 4");
   procedure Check_T5  is new Checker (T5,  "Test 5");
   procedure Check_T6  is new Checker (T6,  "Test 6");
   procedure Check_T7  is new Checker (T7,  "Test 7");
   procedure Check_T8  is new Checker (T8,  "Test 8");
   procedure Check_T9  is new Checker (T9,  "Test 9");
   procedure Check_T10 is new Checker (T10, "Test 10");
   procedure Check_T11 is new Checker (T11, "Test 11");
   procedure Check_T12 is new Checker (T12, "Test 12");
   procedure Force_Body is begin null; end Force_Body;

begin
   Check_T1;
   Check_T2;
   Check_T3;
   Check_T4;
   Check_T5;
   Check_T6;
   Check_T7;
   Check_T8;
   Check_T9;
   Check_T10;
   Check_T11;
   Check_T12;
end Derivations;

--  runtime_checks.adb

with Derivations;

procedure Runtime_Checks is begin null; end Runtime_Checks;

----------------------------
-- Compilation and output --
----------------------------

$ gnatmake -q -gnata runtime_checks.adb
$ ./runtime_checks
Test 1 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:3

Test 2 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:3

Test 3 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:6

Test 4 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:8

Test 5 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:3

Test 6 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:3

Test 7 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:6

Test 8 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:8

Test 9 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:3

Test 10 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:3

Test 11 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:6

Test 12 OK
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Default_Initial_Condition failed at derivations.ads:8

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

2014-08-04  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb Add an entry in table Canonical_Aspect for
	Default_Initial_Condition.
	* aspects.ads Add an entry in tables Aspect_Id, Aspect_Argument,
	Aspect_Names and Aspect_Delay for Default_Initial_Condition.
	* einfo.adb Flag3 is now Has_Default_Init_Cond. Flag132
	is now Is_Default_Init_Cond_ Procedure. Flag133 is now
	Has_Inherited_Default_Init_Cond.
	(Default_Init_Cond_Procedure): New routine.
	(Has_Default_Init_Cond): New routine.
	(Has_Inherited_Default_Init_Cond): New routine.
	(Is_Default_Init_Cond_Procedure): New routine.
	(Set_Default_Init_Cond_Procedure): New routine.
	(Set_Has_Default_Init_Cond): New routine.
	(Set_Has_Inherited_Default_Init_Cond): New routine.
	(Set_Is_Default_Init_Cond_Procedure): New routine.
	(Write_Entity_Flags): Output all the new flags.
	* einfo.ads New attributes Default_Init_Cond_Procedure,
	Has_Inherited_Default_Init_Cond and Is_Default_Init_Cond_Procedure
	along with usage in nodes.
	(Default_Init_Cond_Procedure): New routine.
	(Has_Default_Init_Cond): New routine and pragma Inline.
	(Has_Inherited_Default_Init_Cond): New routine and
	pragma Inline.
	(Is_Default_Init_Cond_Procedure): New routine and
	pragma Inline.
	(Set_Default_Init_Cond_Procedure): New routine.
	(Set_Has_Default_Init_Cond): New routine and pragma Inline.
	(Set_Has_Inherited_Default_Init_Cond): New routine and pragma Inline.
	(Set_Is_Default_Init_Cond_Procedure): New routine and pragma Inline.
	* exp_ch3.adb (Expand_N_Object_Declaration): New constant
	Next_N. Generate a call to the default initial condition procedure
	if the object's type is subject to the pragma.	(Freeze_Type):
	Generate the body of the default initial condition procedure or
	inherit the spec from a parent type.
	* exp_ch7.adb Add with and use clause for Exp_Prag.
	(Expand_Pragma_Initial_Condition): Removed.
	* exp_prag.ads, exp_prag.adb (Expand_Pragma_Initial_Condition): New
	routine.
	* par-prag.adb (Prag): Pragma Default_Initial_Condition does
	not need special treatment by the parser.
	* sem_ch3.adb (Build_Derived_Record_Type): Propagate the
	attributes related to pragma Default_Initial_Condition to the
	derived type.
	(Process_Full_View): Propagate the attributes
	related to pragma Default_Initial_Condition to the full view.
	* sem_ch7.adb (Analyze_Package_Specification): Build the
	declaration of the default initial condition procedure for all
	types that qualify or inherit the one from the parent type.
	* sem_ch13.adb (Analyze_Aspect_Specifications):
	Add processing for aspect Default_Initial_Condition.
	(Check_Aspect_At_Freeze_Point): Aspect
	Default_Initial_Condition does not require delayed analysis.
	(Replace_Type_References_Generic): Moved to spec.
	* sem_ch13.ads (Replace_Type_References_Generic): Moved from body.
	* sem_prag.adb Add an entry in table Sif_Glags for
	Default_Initial_Condition.
	(Analyze_Pragma): Pragma
	Default_Initial_Condition is now part of assertion
	policy. Add processing for pragma Default_Initial_Condition.
	(Is_Valid_Assertion_Kind): Pragma Default_Initial_Condition is
	now recognized as a proper assertion policy.
	* sem_util.ads, sem_util.adb (Build_Default_Init_Cond_Call): New
	routine.
	(Build_Default_Init_Cond_Procedure_Body): New routine.
	(Build_Default_Init_Cond_Procedure_Declaration): New routine.
	(Inherit_Default_Init_Cond_Procedure): New routine.
	* snames.ads-tmpl Add new predefined name and pragma id for
	Default_Initial_Condition.

Attachment: difs
Description: Text document