This is the mail archive of the mailing list for the GCC project.

Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

[Ada] Require Elaborate_Body if non-null abstract state is specified

If a library level package declaration or generic package declaration
contains a non-null abstract state, and does not otherwise require a
body, then in accorance with SPARK (LRM 7.1.5(4)), the package must
contain a pragma Elaborate_Body. This implements this requirement,
as shown in the following compiled with -gnatj60 -gnatd.V.

     1. package Needs_Pragma_Elaborate_Body
     2.    with Abstract_State => State
        >>> package "Needs_Pragma_Elaborate_Body" specifies
            a non-null abstract state, but package does not
            otherwise require a body, pragma Elaborate_Body
            is required in this case

     3. is
     4.    --  package declarations with non-null
     5.    --  Abstract State shall have bodies.
     7.    --  There should be a pragma Elaborate_Body
     8. end Needs_Pragma_Elaborate_Body;

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

2013-10-15  Robert Dewar  <>

	* sem_ch7.adb (Unit_Requires_Body): Add flag
	Ignore_Abstract_State (Analyze_Package_Specification): Enforce
	rule requiring Elaborate_Body if a non-null abstract state is
	specified for a library-level package.
	* (Unit_Requires_Body): Add flag Ignore_Abstract_State.

Attachment: difs
Description: Text document

Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]