Patchwork [Ada] Implement Ada 2012 Assertion_Policy pragma

login
register
mail settings
Submitter Arnaud Charlet
Date April 12, 2013, 1:38 p.m.
Message ID <20130412133809.GA11234@adacore.com>
Download mbox | patch
Permalink /patch/236095/
State New
Headers show

Comments

Arnaud Charlet - April 12, 2013, 1:38 p.m.
This implements pragma Assertion_Policy as described in AI 274. The
main improvements are that it can appear in any declarative part
with scope rules like pragma Suppress, and it can be applied to
individual assertion aspects. GNAT extensions allow it to also
apply to GNAT assertion aspects and pragmas. Check_Policy is
enhanced in a consistent manner. Finally Debug pragmas are
now controllable with Assertion_Policy.

The following program generates:

OK 1
OK 3
OK 4
OK 5
OK 6
OK 7

if compiled with out -gnata, and

OK 1
OK 2
OK 3
OK 4
OK 5
OK 6
OK 7

if compiled with -gnata

     1. pragma Ada_2012;
     2. with Text_IO; use Text_IO;
     3. with System.Assertions; use System.Assertions;
     4. procedure TestPolicy is
     5.    function Ident (M : Integer) return Integer is
     6.    begin return M; end;
     7. begin
     8.    begin
     9.       declare
    10.          pragma Check_Policy (Debug, Check);
    11.          pragma Debug (True, Put_Line ("OK 1"));
    12.          pragma Check_Policy (Debug, Ignore);
    13.          pragma Debug (True, Put_Line ("Not OK 1"));
    14.          pragma Check_Policy (Debug, Disable);
    15.          pragma Debug (True, 32);
    16.       begin
    17.          null;
    18.       end;
    19.
    20.       pragma Debug (True, Put_Line ("OK 2"));
    21.       null;
    22.    end;
    23.
    24.    declare
    25.       pragma Assertion_Policy (Pre => Disable);
    26.       procedure P1 with Pre => 32 is begin null; end;
    27.    begin
    28.       P1;
    29.    end;
    30.
    31.    declare
    32.       pragma Assertion_Policy (Pre => Check);
    33.       procedure P1 with Pre => False is begin null; end;
    34.    begin
    35.       P1;
    36.    exception
    37.       when Assert_Failure => Put_Line ("OK 3");
    38.    end;
    39.
    40.    declare
    41.       pragma Assertion_Policy (Pre => Ignore);
    42.       procedure P1 with Pre => False is begin null; end;
    43.    begin
    44.       P1;
    45.    exception
    46.       when Assert_Failure => Put_Line ("Not OK 2");
    47.    end;
    48.
    49.    begin
    50.       null;
    51.    end;
    52.
    53.    declare
    54.       pragma Assertion_Policy (Post => Check);
    55.       procedure P1 with Post => False is begin null; end;
    56.    begin
    57.       P1;
    58.    exception
    59.       when Assert_Failure => Put_Line ("OK 4");
    60.    end;
    61.
    62.    declare
    63.       pragma Assertion_Policy (Post => Ignore);
    64.       procedure P1 with Post => False is begin null; end;
    65.    begin
    66.       P1;
    67.    exception
    68.       when Assert_Failure => Put_Line ("Not OK 3");
    69.    end;
    70.
    71.    declare
    72.       pragma Assertion_Policy (Static_Predicate => Check);
    73.       subtype X is Integer with Static_Predicate => X > 0;
    74.       XX : X;
    75.    begin
    76.       XX := Ident (-4);
    77.    exception
    78.       when Assert_Failure => Put_Line ("OK 5");
    79.    end;
    80.
    81.    declare
    82.       pragma Check_Policy (Static_Predicate, Ignore);
    83.       subtype X is Integer with Static_Predicate => X > 0;
    84.       XX : X;
    85.    begin
    86.       XX := Ident (-4);
    87.    exception
    88.       when Assert_Failure => Put_Line ("Not OK 4");
    89.    end;
    90.
    91.    declare
    92.       pragma Assertion_Policy (Dynamic_Predicate => Check);
    93.       subtype X is Integer with Dynamic_Predicate => X > Ident (0);
    94.       XX : X;
    95.    begin
    96.       XX := Ident (-4);
    97.    exception
    98.       when Assert_Failure => Put_Line ("OK 6");
    99.    end;
   100.
   101.    declare
   102.       pragma Assertion_Policy (Dynamic_Predicate => Ignore);
   103.       subtype X is Integer with Dynamic_Predicate => X > Ident (0);
   104.       XX : X;
   105.    begin
   106.       XX := Ident (-4);
   107.    exception
   108.       when Assert_Failure => Put_Line ("Not OK 6");
   109.    end;
   110.
   111.    declare
   112.       pragma Check_Policy (Predicate, Check);
   113.       subtype X is Integer with Predicate => X > 0;
   114.       XX : X;
   115.    begin
   116.       XX := Ident (-4);
   117.    exception
   118.       when Assert_Failure => Put_Line ("OK 7");
   119.    end;
   120.
   121.    declare
   122.       pragma Assertion_Policy (Predicate => Ignore);
   123.       subtype X is Integer with Predicate => X > 0;
   124.       XX : X;
   125.    begin
   126.       XX := Ident (-4);
   127.    exception
   128.       when Assert_Failure => Put_Line ("Not OK 6");
   129.    end;
   130.
   131. end;

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

2013-04-12  Robert Dewar  <dewar@adacore.com>

	* einfo.adb (Has_Dynamic_Predicate_Aspect): New flag.
	(Has_Static_Predicate_Aspect): New flag.
	* einfo.ads (Has_Dynamic_Predicate_Aspect): New flag.
	(Has_Static_Predicate_Aspect): New flag.
	* exp_ch9.adb: Minor reformatting.
	* exp_util.adb (Make_Invariant_Call): Check_Enabled now handles
	synonyms.
	* gnat1drv.adb: Remove setting of Debug_Pragmas_Enabled,
	since this switch is gone and control of Debug is done with
	Assertions_Enabled.
	* gnat_rm.texi: Update documentation for Assertion_Policy and
	Check_Policy pragmas.
	* opt.adb (Debug_Pragmas_Disabled[_Config]): Removed
	(Debug_Pragmas_Enabled[_Config]): Removed Since debug now
	controlled by Assertion_Enabled.
	* opt.ads (Debug_Pragmas_Disabled[_Config]): Removed
	(Debug_Pragmas_Enabled[_Config]): Removed Since debug now
	controlled by Assertion_Enabled.
	* par-ch2.adb (Scan_Pragma_Argument_Association): Allow new
	'Class forms.
	* sem_attr.adb: Minor reformatting.
	* sem_ch13.adb (Analyze_Aspect_Specification): Disable aspect
	if DISABLE policy applies.
	* sem_ch6.adb (Grab_PPC): Check original name of aspect for
	aspect from pragma (Process_PPCs): Properly check assertion policy.
	* sem_prag.adb (Check_Enabled): Rewritten for new Assertion_Policy
	(Check_Appicable_Policy): New procedure.
	(Is_Valid_Assertion_Kind): New function.
	(Rewrite_Assertion_Kind): New procedure.
	(Analyze_Pragma): Handle case of disabled assertion pragma.
	(Analyze_Pragma, case Assertion_Policy): Rewritten for Ada 2012.
	(Analyze_Pragma, case Check): Deal with 'Class possibilities.
	(Analyze_Pragma, case Check_Policy): Deal with 'Class possibilities.
	(Analyze_Pragma, case Contract_Class): New handling of ignored pragma.
	(Analyze_Pragma, case Debug): New control with Assertion_Policy.
	(Analyze_Pragma, case Debug_Policy): Now consistent with
	Assertion_Policy.
	(Analyze_Pragma, case Loop_Invariant): New handling of ignored
	pragma.
	(Analyze_Pragma, case Loop_Variant): New handling of ignored pragma.
	(Analyze_Pragma, case Precondition): Use proper name for Check pragma.
	(Analyze_Pragma, case Check_Enabled): Rewritten for new policy stuff.
	* sem_prag.ads (Check_Enabled): Rewritten for new
	Assertion_Policy stuff.
	(Check_Appicable_Policy): New procedure.
	* sinfo.adb (Is_Disabled): New flag.
	(Is_Ignored): New flag.
	* sinfo.ads (Is_Disabled): New flag.
	(Is_Ignored): New flag.
	(N_Pragma_Argument_Association): New 'Class forms.
	* snames.ads-tmpl: New names Name_uPre, Name_uPost,
	Name_uType_Invariant, Name_uInvariant.
	* switch-c.adb: Remove setting of Debug_Pragmas_Enabled for -gnata.
	* tree_io.ads (ASIS_Version_Number): Updated (remove
	read write of obsolete flags Debug_Pragmas_Disabled and
	Debug_Pragmas_Enabled.

Patch

Index: gnat_rm.texi
===================================================================
--- gnat_rm.texi	(revision 197912)
+++ gnat_rm.texi	(working copy)
@@ -1229,47 +1229,69 @@ 
 
 @node Pragma Assertion_Policy
 @unnumberedsec Pragma Assertion_Policy
-@findex Debug_Policy
+@findex Assertion_Policy
 @noindent
 Syntax:
-
 @smallexample @c ada
 pragma Assertion_Policy (CHECK | DISABLE | IGNORE);
+
+Pragma Assertion_Policy (
+    ASSERTION_KIND => POLICY_IDENTIFIER
+ @{, ASSERTION_KIND => POLICY_IDENTIFIER@});
+
+ASSERTION_KIND ::= RM_ASSERTION_KIND | ID_ASSERTION_KIND
+
+RM_ASSERTION_KIND ::= Assert               |
+                      Static_Predicate     |
+                      Dynamic_Predicate    |
+                      Pre                  |
+                      Pre'Class            |
+                      Post                 |
+                      Post'Class           |
+                      Type_Invariant       |
+                      Type_Invariant'Class
+
+ID_ASSERTION_KIND ::= Assert_And_Cut       |
+                      Assume               |
+                      Contract_Cases       |
+                      Debug                |
+                      Invariant            |
+                      Invariant'Class      |
+                      Loop_Invariant       |
+                      Loop_Variant         |
+                      Postcondition        |
+                      Precondition         |
+                      Predicate
+
+POLICY_IDENTIFIER ::= Check | Disable | Ignore
 @end smallexample
 
 @noindent
-This is a standard Ada 2005 pragma that is available as an
+This is a standard Ada 2012 pragma that is available as an
 implementation-defined pragma in earlier versions of Ada.
+The assertion kinds @code{RM_ASSERTION_KIND} are those defined in
+the Ada standard. The assertion kinds @code{ID_ASSERTION_KIND}
+are implementation defined additions recognized by the GNAT compiler.
 
-If the argument is @code{CHECK}, then assertions are enabled.
-If the argument is @code{IGNORE}, then assertions are ignored.
+The pragma applies in both cases to pragmas and aspects with matching
+names, e.g. @code{Pre} applies to the Pre aspect, and @code{Precondition}
+applies to both the @code{Precondition} pragma
+and the aspect @code{Precondition}.
+
+If the policy is @code{CHECK}, then assertions are enabled, i.e.
+the corresponding pragma or aspect is activated.
+If the policy is @code{IGNORE}, then assertions are ignored, i.e.
+the corresponding pragma or aspect is deactivated.
 This pragma overrides the effect of the @option{-gnata} switch on the
 command line.
 
-Assertions are of three kinds:
-
-@itemize @bullet
-@item
-Pragma @code{Assert}.
-@item
-In Ada 2012, all assertions defined in the RM as aspects: preconditions,
-postconditions, type invariants and (sub)type predicates.
-@item
-Corresponding pragmas for type invariants and (sub)type predicates.
-@end itemize
-
 The implementation defined policy @code{DISABLE} is like
 @code{IGNORE} except that it completely disables semantic
-checking of the argument to @code{pragma Assert}. This may
-be useful when the pragma argument references subprograms
+checking of the corresponding pragma or aspect. This is
+useful when the pragma or aspect argument references subprograms
 in a with'ed package which is replaced by a dummy package
 for the final build.
 
-Note: this is a standard language-defined pragma in versions
-of Ada from 2005 on. In GNAT, it is implemented in all versions
-of Ada, and the DISABLE policy is an implementation-defined
-addition.
-
 @node Pragma Assume_No_Invalid_Values
 @unnumberedsec Pragma Assume_No_Invalid_Values
 @findex Assume_No_Invalid_Values
@@ -1416,9 +1438,12 @@ 
 Syntax:
 @smallexample @c ada
 pragma Check (
-     [Name    =>] Identifier,
+     [Name    =>] CHECK_KIND,
      [Check   =>] Boolean_EXPRESSION
   [, [Message =>] string_EXPRESSION] );
+
+CHECK_KIND ::= IDENTIFIER |
+               Pre'Class | Post'Class | Type_Invariant'Class
 @end smallexample
 
 @noindent
@@ -1426,10 +1451,7 @@ 
 extra identifier argument is present. In conjunction with pragma
 @code{Check_Policy}, this can be used to define groups of assertions that can
 be independently controlled. The identifier @code{Assertion} is special, it
-refers to the normal set of pragma @code{Assert} statements. The identifiers
-@code{Precondition} and @code{Postcondition} correspond to the pragmas of these
-names, so these three names would normally not be used directly in a pragma
-@code{Check}.
+refers to the normal set of pragma @code{Assert} statements.
 
 Checks introduced by this pragma are normally deactivated by default. They can
 be activated either by the command line option @option{-gnata}, which turns on
@@ -1532,61 +1554,61 @@ 
 Syntax:
 @smallexample @c ada
 pragma Check_Policy
- ([Name   =>] Identifier,
+ ([Name   =>] CHECK_KIND,
   [Policy =>] POLICY_IDENTIFIER);
 
+CHECK_KIND ::= IDENTIFIER |
+                   Pre'Class | Post'Class | Type_Invariant'Class
+
 POLICY_IDENTIFIER ::= ON | OFF | CHECK | DISABLE | IGNORE
 @end smallexample
 
 @noindent
-This pragma is similar to the predefined pragma @code{Assertion_Policy},
-except that it controls sets of named assertions introduced using the
-@code{Check} pragmas. It can be used as a configuration pragma or (unlike
-@code{Assertion_Policy}) can be used within a declarative part, in which case
-it controls the status to the end of the corresponding construct (in a manner
-identical to pragma @code{Suppress)}.
+This pragma is used to set the checking policy for assertions (specified
+by aspects of pragmas), the @code{Debug} pragma, or additional checks
+to be checked using the @code{Check} pragma. It may appear either as
+a configuration pragma, or within a declarative part of package. In the
+latter case, it applies from the point where it appears to the end of
+the declarative region (like pragma @code{Suppress}).
 
-The identifier given as the first argument corresponds to a name used in
-associated @code{Check} pragmas. For example, if the pragma:
+The @code{Check_Policy} pragma is similar to the
+predefined @code{Assertion_Policy} pragma,
+and if the first argument corresponds to one of the assertion kinds that
+are allowed by @code{Assertion_Policy}, then the effect is identical.
+The identifiers @code{Precondition} and @code{Postcondition} are allowed
+synonyms for @code{Pre} and @code{Post}.
 
+If the first argument is Debug, then the policy applies to Debug pragmas,
+disabling their effect if the policy is @code{Off}, @code{Disable}, or
+@code{Ignore}, and allowing them to execute with normal semantics if
+the policy is @code{On} or @code{Check}. In addition if the policy is
+@code{Disable}, then the procedure call in @code{Debug} pragmas will
+be totally ignored and not analyzed semanticslly.
+
+Finally the first argument may be some other identifier than the above
+posibilities, in which case it controls a set of named assertions
+that can be checked using pragma @code{Check}. For example, if the pragma:
+
 @smallexample @c ada
 pragma Check_Policy (Critical_Error, OFF);
 @end smallexample
 
 @noindent
 is given, then subsequent @code{Check} pragmas whose first argument is also
-@code{Critical_Error} will be disabled. The special identifier @code{Assertion}
-controls the behavior of normal assertions (thus a pragma
-@code{Check_Policy} with this identifier is similar to the normal
-@code{Assertion_Policy} pragma except that it can appear within a
-declarative part).
+@code{Critical_Error} will be disabled.
 
-The special identifiers @code{Precondition} and @code{Postcondition} control
-the status of preconditions and postconditions given as pragmas.
-If a @code{Precondition} pragma
-is encountered, it is ignored if turned off by a @code{Check_Policy} specifying
-that @code{Precondition} checks are @code{Off} or @code{Ignored}. Similarly use
-of the name @code{Postcondition} controls whether @code{Postcondition} pragmas
-are recognized. Note that preconditions and postconditions given as aspects
-are controlled differently, either by the @code{Assertion_Policy} pragma or
-by the @code{Check_Policy} pragma with identifier @code{Assertion}.
-
 The check policy is @code{OFF} to turn off corresponding checks, and @code{ON}
 to turn on corresponding checks. The default for a set of checks for which no
 @code{Check_Policy} is given is @code{OFF} unless the compiler switch
 @option{-gnata} is given, which turns on all checks by default.
 
-The check policy settings @code{CHECK} and @code{IGNORE} are also recognized
+The check policy settings @code{CHECK} and @code{IGNORE} are recognized
 as synonyms for @code{ON} and @code{OFF}. These synonyms are provided for
-compatibility with the standard @code{Assertion_Policy} pragma.
+compatibility with the standard @code{Assertion_Policy} pragma. The check
+policy setting @code{DISABLE} is also synonymous with @code{OFF} in this
+context, but does not have any other significance for check
+names other than assertion kinds.
 
-The implementation defined policy @code{DISABLE} is like
-@code{OFF} except that it completely disables semantic
-checking of the argument to the corresponding class of
-pragmas. This may be useful when the pragma arguments reference
-subprograms in a with'ed package which is replaced by a dummy package
-for the final build.
-
 @node Pragma Comment
 @unnumberedsec Pragma Comment
 @findex Comment
@@ -2113,7 +2135,8 @@ 
 permitted in sequences of declarations, so you can use pragma @code{Debug} to
 intersperse calls to debug procedures in the middle of declarations. Debug
 pragmas can be enabled either by use of the command line switch @option{-gnata}
-or by use of the configuration pragma @code{Debug_Policy}.
+or by use of the pragma @code{Check_Policy} with a first argument of
+@code{Debug}.
 
 @node Pragma Debug_Policy
 @unnumberedsec Pragma Debug_Policy
@@ -2122,22 +2145,14 @@ 
 Syntax:
 
 @smallexample @c ada
-pragma Debug_Policy (CHECK | DISABLE | IGNORE);
+pragma Debug_Policy (CHECK | DISABLE | IGNORE | ON | OFF);
 @end smallexample
 
 @noindent
-If the argument is @code{CHECK}, then pragma @code{DEBUG} is enabled.
-If the argument is @code{IGNORE}, then pragma @code{DEBUG} is ignored.
-This pragma overrides the effect of the @option{-gnata} switch on the
-command line.
+This pragma is equivalent to a corresponding @code{Check_Policy} pragma
+with a first argument of @code{Debug}. It is retained for historical
+compatibility reasons.
 
-The implementation defined policy @code{DISABLE} is like
-@code{IGNORE} except that it completely disables semantic
-checking of the argument to @code{pragma Debug}. This may
-be useful when the pragma argument references subprograms
-in a with'ed package which is replaced by a dummy package
-for the final build.
-
 @node Pragma Default_Storage_Pool
 @unnumberedsec Pragma Default_Storage_Pool
 @findex Default_Storage_Pool
Index: exp_util.adb
===================================================================
--- exp_util.adb	(revision 197911)
+++ exp_util.adb	(working copy)
@@ -5458,10 +5458,7 @@ 
       pragma Assert
         (Has_Invariants (Typ) and then Present (Invariant_Procedure (Typ)));
 
-      if Check_Enabled (Name_Invariant)
-           or else
-         Check_Enabled (Name_Assertion)
-      then
+      if Check_Enabled (Name_Invariant) then
          return
            Make_Procedure_Call_Statement (Loc,
              Name                   =>
@@ -5590,14 +5587,26 @@ 
       Expr : Node_Id) return Node_Id
    is
       Loc : constant Source_Ptr := Sloc (Expr);
+      Nam : Name_Id;
 
    begin
+      --  Compute proper name to use, we need to get this right so that the
+      --  right set of check policies apply to the CHeck pragma we are making.
+
+      if Has_Dynamic_Predicate_Aspect (Typ) then
+         Nam := Name_Dynamic_Predicate;
+      elsif Has_Static_Predicate_Aspect (Typ) then
+         Nam := Name_Static_Predicate;
+      else
+         Nam := Name_Predicate;
+      end if;
+
       return
         Make_Pragma (Loc,
           Pragma_Identifier            => Make_Identifier (Loc, Name_Check),
           Pragma_Argument_Associations => New_List (
             Make_Pragma_Argument_Association (Loc,
-              Expression => Make_Identifier (Loc, Name_Predicate)),
+              Expression => Make_Identifier (Loc, Nam)),
             Make_Pragma_Argument_Association (Loc,
               Expression => Make_Predicate_Call (Typ, Expr))));
    end Make_Predicate_Check;
Index: switch-c.adb
===================================================================
--- switch-c.adb	(revision 197902)
+++ switch-c.adb	(working copy)
@@ -283,7 +283,6 @@ 
             when 'a' =>
                Ptr := Ptr + 1;
                Assertions_Enabled := True;
-               Debug_Pragmas_Enabled := True;
 
             --  -gnatA (disregard gnat.adc)
 
Index: sinfo.adb
===================================================================
--- sinfo.adb	(revision 197909)
+++ sinfo.adb	(working copy)
@@ -1740,6 +1740,15 @@ 
       return Flag16 (N);
    end Is_Controlling_Actual;
 
+   function Is_Disabled
+      (N : Node_Id) return Boolean is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Aspect_Specification
+        or else NT (N).Nkind = N_Pragma);
+      return Flag15 (N);
+   end Is_Disabled;
+
    function Is_Delayed_Aspect
       (N : Node_Id) return Boolean is
    begin
@@ -1798,6 +1807,15 @@ 
       return Flag4 (N);
    end Is_Folded_In_Parser;
 
+   function Is_Ignored
+      (N : Node_Id) return Boolean is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Aspect_Specification
+        or else NT (N).Nkind = N_Pragma);
+      return Flag9 (N);
+   end Is_Ignored;
+
    function Is_In_Discriminant_Check
       (N : Node_Id) return Boolean is
    begin
@@ -4832,6 +4850,15 @@ 
       Set_Flag14 (N, Val);
    end Set_Is_Delayed_Aspect;
 
+   procedure Set_Is_Disabled
+      (N : Node_Id; Val : Boolean := True) is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Aspect_Specification
+        or else NT (N).Nkind = N_Pragma);
+      Set_Flag15 (N, Val);
+   end Set_Is_Disabled;
+
    procedure Set_Is_Dynamic_Coextension
       (N : Node_Id; Val : Boolean := True) is
    begin
@@ -4880,6 +4907,15 @@ 
       Set_Flag4 (N, Val);
    end Set_Is_Folded_In_Parser;
 
+   procedure Set_Is_Ignored
+      (N : Node_Id; Val : Boolean := True) is
+   begin
+      pragma Assert (False
+        or else NT (N).Nkind = N_Aspect_Specification
+        or else NT (N).Nkind = N_Pragma);
+      Set_Flag9 (N, Val);
+   end Set_Is_Ignored;
+
    procedure Set_Is_In_Discriminant_Check
       (N : Node_Id; Val : Boolean := True) is
    begin
Index: sinfo.ads
===================================================================
--- sinfo.ads	(revision 197909)
+++ sinfo.ads	(working copy)
@@ -1286,6 +1286,14 @@ 
    --    a dispatching call. It is off in all other cases. See Sem_Disp for
    --    details of its use.
 
+   --  Is_Disabled (Flag15-Sem)
+   --    A flag set in an N_Aspect_Specification or N_Pragma node if there was
+   --    a Check_Policy or Assertion_Policy (or in the case of a Debug_Pragma)
+   --    a Debug_Policy pragma that resulted in totally disabling the flagged
+   --    aspect or policy as a result of using the GNAT-defined policy DISABLE.
+   --    If this flag is set, the aspect or policy is not analyzed for semantic
+   --    correctness, so any expressions etc will not be marked as analyzed.
+
    --  Is_Dynamic_Coextension (Flag18-Sem)
    --    Present in allocator nodes, to indicate that this is an allocator
    --    for an access discriminant of a dynamically allocated object. The
@@ -1308,6 +1316,20 @@ 
    --    objects. The wrapper prevents interference between exception handlers
    --    and At_End handlers.
 
+   --  Is_Ignored (Flag9-Sem)
+   --    A flag set in an N_Aspect_Specification or N_Pragma node if there was
+   --    a Check_Policy or Assertion_Policy (or in the case of a Debug_Pragma)
+   --    a Debug_Policy pragma that specified a policy of IGNORE, DISABLE, or
+   --    OFF, for the pragma/aspect. If there was a Policy pragma specifying
+   --    a Policy of ON or CHECK, then this flag is reset. If no Policy pragma
+   --    gives a policy for the aspect or pragma, then there are two cases. For
+   --    an assertion aspect or pragma (one of the assertion kinds allowed in
+   --    an Assertion_Policy pragma), then Is_Ignored is set if assertions are
+   --    ignored because of the use of a -gnata switch. For any other aspects
+   --    or pragmas, the flag is off. If this flag is set, the aspect/pragma
+   --    is fully analyzed and checked for other syntactic/semantic errors,
+   --    but it does not have any semantic effect.
+
    --  Is_In_Discriminant_Check (Flag11-Sem)
    --    This flag is present in a selected component, and is used to indicate
    --    that the reference occurs within a discriminant check. The
@@ -2085,11 +2107,13 @@ 
       --  Corresponding_Aspect (Node3-Sem) (set to Empty if not present)
       --  Pragma_Identifier (Node4)
       --  Next_Rep_Item (Node5-Sem)
+      --  Class_Present (Flag6) set if from Aspect with 'Class
       --  From_Aspect_Specification (Flag13-Sem)
       --  Is_Delayed_Aspect (Flag14-Sem)
+      --  Is_Disabled (Flag15-Sem)
+      --  Is_Ignored (Flag9-Sem)
       --  Import_Interface_Present (Flag16-Sem)
       --  Split_PPC (Flag17) set if corresponding aspect had Split_PPC set
-      --  Class_Present (Flag6) set if from Aspect with 'Class
 
       --  Note: we should have a section on what pragmas are passed on to
       --  the back end to be processed. This section should note that pragma
@@ -2112,6 +2136,27 @@ 
       --    [pragma_argument_IDENTIFIER =>] NAME
       --  | [pragma_argument_IDENTIFIER =>] EXPRESSION
 
+      --  In Ada 2012, there are two more possibilities:
+
+      --  PRAGMA_ARGUMENT_ASSOCIATION ::=
+      --    [pragma_argument_ASPECT_MARK =>] NAME
+      --  | [pragma_argument_ASPECT_MARK =>] EXPRESSION
+
+      --  where the interesting allowed cases (which do not fit the syntax of
+      --  the first alternative above) are
+
+      --  ASPECT_MARK => Pre'Class | Post'Class | Type_Invariant'Class
+
+      --  We allow this special usage in all Ada modes, but it would be a
+      --  pain to allow these aspects to pervade the pragma syntax, and the
+      --  representation of pragma nodes internally. So what we do is to
+      --  replace these ASPECT_MARK forms with identifiers whose name is one
+      --  of the special internal names _Pre, _Post or _Type_Invariant.
+
+      --  We do a similar replacement of these Aspect_Mark forms in the
+      --  Expression of a pragma argument association for the cases of
+      --  the first arguments of any Check pragmas and Check_Policy pragmas
+
       --  N_Pragma_Argument_Association
       --  Sloc points to first token in association
       --  Chars (Name1) (set to No_Name if no pragma argument identifier)
@@ -6712,6 +6757,8 @@ 
       --  Split_PPC (Flag17) Set if split pre/post attribute
       --  Is_Boolean_Aspect (Flag16-Sem)
       --  Is_Delayed_Aspect (Flag14-Sem)
+      --  Is_Disabled (Flag15-Sem)
+      --  Is_Ignored (Flag9-Sem)
 
       --  Note: Aspect_Specification is an Ada 2012 feature
 
@@ -8667,6 +8714,9 @@ 
    function Is_Delayed_Aspect
      (N : Node_Id) return Boolean;    -- Flag14
 
+   function Is_Disabled
+     (N : Node_Id) return Boolean;    -- Flag15
+
    function Is_Dynamic_Coextension
      (N : Node_Id) return Boolean;    -- Flag18
 
@@ -8685,6 +8735,9 @@ 
    function Is_Folded_In_Parser
      (N : Node_Id) return Boolean;    -- Flag4
 
+   function Is_Ignored
+     (N : Node_Id) return Boolean;    -- Flag9
+
    function Is_In_Discriminant_Check
      (N : Node_Id) return Boolean;    -- Flag11
 
@@ -9648,6 +9701,12 @@ 
    procedure Set_Is_Delayed_Aspect
      (N : Node_Id; Val : Boolean := True);    -- Flag14
 
+   procedure Set_Is_Disabled
+     (N : Node_Id; Val : Boolean := True);    -- Flag15
+
+   procedure Set_Is_Ignored
+     (N : Node_Id; Val : Boolean := True);    -- Flag9
+
    procedure Set_Is_Dynamic_Coextension
      (N : Node_Id; Val : Boolean := True);    -- Flag18
 
@@ -12020,12 +12079,14 @@ 
    pragma Inline (Is_Component_Right_Opnd);
    pragma Inline (Is_Controlling_Actual);
    pragma Inline (Is_Delayed_Aspect);
+   pragma Inline (Is_Disabled);
    pragma Inline (Is_Dynamic_Coextension);
    pragma Inline (Is_Elsif);
    pragma Inline (Is_Entry_Barrier_Function);
    pragma Inline (Is_Expanded_Build_In_Place_Call);
    pragma Inline (Is_Finalization_Wrapper);
    pragma Inline (Is_Folded_In_Parser);
+   pragma Inline (Is_Ignored);
    pragma Inline (Is_In_Discriminant_Check);
    pragma Inline (Is_Machine_Number);
    pragma Inline (Is_Null_Loop);
@@ -12186,20 +12247,20 @@ 
    pragma Inline (Set_All_Present);
    pragma Inline (Set_Alternatives);
    pragma Inline (Set_Ancestor_Part);
-   pragma Inline (Set_Atomic_Sync_Required);
    pragma Inline (Set_Array_Aggregate);
    pragma Inline (Set_Aspect_Rep_Item);
    pragma Inline (Set_Assignment_OK);
    pragma Inline (Set_Associated_Node);
    pragma Inline (Set_At_End_Proc);
+   pragma Inline (Set_Atomic_Sync_Required);
    pragma Inline (Set_Attribute_Name);
    pragma Inline (Set_Aux_Decls_Node);
    pragma Inline (Set_Backwards_OK);
    pragma Inline (Set_Bad_Is_Detected);
+   pragma Inline (Set_Body_Required);
    pragma Inline (Set_Body_To_Inline);
-   pragma Inline (Set_Body_Required);
+   pragma Inline (Set_Box_Present);
    pragma Inline (Set_By_Ref);
-   pragma Inline (Set_Box_Present);
    pragma Inline (Set_Char_Literal_Value);
    pragma Inline (Set_Chars);
    pragma Inline (Set_Check_Address_Alignment);
@@ -12225,8 +12286,8 @@ 
    pragma Inline (Set_Context_Items);
    pragma Inline (Set_Context_Pending);
    pragma Inline (Set_Controlling_Argument);
+   pragma Inline (Set_Conversion_OK);
    pragma Inline (Set_Convert_To_Return_False);
-   pragma Inline (Set_Conversion_OK);
    pragma Inline (Set_Corresponding_Aspect);
    pragma Inline (Set_Corresponding_Body);
    pragma Inline (Set_Corresponding_Formal_Spec);
@@ -12237,8 +12298,8 @@ 
    pragma Inline (Set_Dcheck_Function);
    pragma Inline (Set_Declarations);
    pragma Inline (Set_Default_Expression);
+   pragma Inline (Set_Default_Name);
    pragma Inline (Set_Default_Storage_Pool);
-   pragma Inline (Set_Default_Name);
    pragma Inline (Set_Defining_Identifier);
    pragma Inline (Set_Defining_Unit_Name);
    pragma Inline (Set_Delay_Alternative);
@@ -12254,16 +12315,16 @@ 
    pragma Inline (Set_Discriminant_Type);
    pragma Inline (Set_Do_Accessibility_Check);
    pragma Inline (Set_Do_Discriminant_Check);
+   pragma Inline (Set_Do_Division_Check);
    pragma Inline (Set_Do_Length_Check);
-   pragma Inline (Set_Do_Division_Check);
    pragma Inline (Set_Do_Overflow_Check);
    pragma Inline (Set_Do_Range_Check);
    pragma Inline (Set_Do_Storage_Check);
    pragma Inline (Set_Do_Tag_Check);
-   pragma Inline (Set_Elaborate_Present);
    pragma Inline (Set_Elaborate_All_Desirable);
    pragma Inline (Set_Elaborate_All_Present);
    pragma Inline (Set_Elaborate_Desirable);
+   pragma Inline (Set_Elaborate_Present);
    pragma Inline (Set_Elaboration_Boolean);
    pragma Inline (Set_Else_Actions);
    pragma Inline (Set_Else_Statements);
@@ -12310,13 +12371,14 @@ 
    pragma Inline (Set_Has_Created_Identifier);
    pragma Inline (Set_Has_Dereference_Action);
    pragma Inline (Set_Has_Dynamic_Length_Check);
+   pragma Inline (Set_Has_Dynamic_Range_Check);
    pragma Inline (Set_Has_Init_Expression);
    pragma Inline (Set_Has_Local_Raise);
-   pragma Inline (Set_Has_Dynamic_Range_Check);
    pragma Inline (Set_Has_No_Elaboration_Code);
    pragma Inline (Set_Has_Pragma_Suppress_All);
    pragma Inline (Set_Has_Private_View);
    pragma Inline (Set_Has_Relative_Deadline_Pragma);
+   pragma Inline (Set_Has_Self_Reference);
    pragma Inline (Set_Has_Storage_Size_Pragma);
    pragma Inline (Set_Has_Wide_Character);
    pragma Inline (Set_Has_Wide_Wide_Character);
@@ -12325,16 +12387,15 @@ 
    pragma Inline (Set_High_Bound);
    pragma Inline (Set_Identifier);
    pragma Inline (Set_Implicit_With);
-   pragma Inline (Set_Includes_Infinities);
-   pragma Inline (Set_Interface_List);
-   pragma Inline (Set_Interface_Present);
    pragma Inline (Set_Import_Interface_Present);
    pragma Inline (Set_In_Assertion_Expression);
    pragma Inline (Set_In_Present);
+   pragma Inline (Set_Includes_Infinities);
    pragma Inline (Set_Inherited_Discriminant);
    pragma Inline (Set_Instance_Spec);
+   pragma Inline (Set_Interface_List);
+   pragma Inline (Set_Interface_Present);
    pragma Inline (Set_Intval);
-   pragma Inline (Set_Iterator_Specification);
    pragma Inline (Set_Is_Accessibility_Actual);
    pragma Inline (Set_Is_Asynchronous_Call_Block);
    pragma Inline (Set_Is_Boolean_Aspect);
@@ -12342,12 +12403,14 @@ 
    pragma Inline (Set_Is_Component_Right_Opnd);
    pragma Inline (Set_Is_Controlling_Actual);
    pragma Inline (Set_Is_Delayed_Aspect);
+   pragma Inline (Set_Is_Disabled);
    pragma Inline (Set_Is_Dynamic_Coextension);
    pragma Inline (Set_Is_Elsif);
    pragma Inline (Set_Is_Entry_Barrier_Function);
    pragma Inline (Set_Is_Expanded_Build_In_Place_Call);
    pragma Inline (Set_Is_Finalization_Wrapper);
    pragma Inline (Set_Is_Folded_In_Parser);
+   pragma Inline (Set_Is_Ignored);
    pragma Inline (Set_Is_In_Discriminant_Check);
    pragma Inline (Set_Is_Machine_Number);
    pragma Inline (Set_Is_Null_Loop);
@@ -12355,22 +12418,22 @@ 
    pragma Inline (Set_Is_Power_Of_2_For_Shift);
    pragma Inline (Set_Is_Prefixed_Call);
    pragma Inline (Set_Is_Protected_Subprogram_Body);
-   pragma Inline (Set_Has_Self_Reference);
    pragma Inline (Set_Is_Static_Coextension);
    pragma Inline (Set_Is_Static_Expression);
    pragma Inline (Set_Is_Subprogram_Descriptor);
    pragma Inline (Set_Is_Task_Allocation_Block);
    pragma Inline (Set_Is_Task_Master);
    pragma Inline (Set_Iteration_Scheme);
+   pragma Inline (Set_Iterator_Specification);
    pragma Inline (Set_Itype);
    pragma Inline (Set_Kill_Range_Check);
+   pragma Inline (Set_Label_Construct);
    pragma Inline (Set_Last_Bit);
    pragma Inline (Set_Last_Name);
+   pragma Inline (Set_Left_Opnd);
    pragma Inline (Set_Library_Unit);
-   pragma Inline (Set_Label_Construct);
-   pragma Inline (Set_Left_Opnd);
+   pragma Inline (Set_Limited_Present);
    pragma Inline (Set_Limited_View_Installed);
-   pragma Inline (Set_Limited_Present);
    pragma Inline (Set_Literals);
    pragma Inline (Set_Local_Raise_Not_OK);
    pragma Inline (Set_Local_Raise_Statements);
@@ -12398,9 +12461,9 @@ 
    pragma Inline (Set_No_Initialization);
    pragma Inline (Set_No_Minimize_Eliminate);
    pragma Inline (Set_No_Truncation);
-   pragma Inline (Set_Null_Present);
    pragma Inline (Set_Null_Exclusion_Present);
    pragma Inline (Set_Null_Exclusion_In_Return_Present);
+   pragma Inline (Set_Null_Present);
    pragma Inline (Set_Null_Record_Present);
    pragma Inline (Set_Object_Definition);
    pragma Inline (Set_Of_Present);
@@ -12409,8 +12472,8 @@ 
    pragma Inline (Set_Others_Discrete_Choices);
    pragma Inline (Set_Out_Present);
    pragma Inline (Set_Parameter_Associations);
+   pragma Inline (Set_Parameter_List_Truncated);
    pragma Inline (Set_Parameter_Specifications);
-   pragma Inline (Set_Parameter_List_Truncated);
    pragma Inline (Set_Parameter_Type);
    pragma Inline (Set_Parent_Spec);
    pragma Inline (Set_Position);
@@ -12453,38 +12516,38 @@ 
    pragma Inline (Set_Selector_Names);
    pragma Inline (Set_Shift_Count_OK);
    pragma Inline (Set_Source_Type);
+   pragma Inline (Set_Spec_CTC_List);
    pragma Inline (Set_Spec_PPC_List);
-   pragma Inline (Set_Spec_CTC_List);
    pragma Inline (Set_Specification);
    pragma Inline (Set_Split_PPC);
    pragma Inline (Set_Statements);
    pragma Inline (Set_Storage_Pool);
+   pragma Inline (Set_Strval);
    pragma Inline (Set_Subpool_Handle_Name);
-   pragma Inline (Set_Strval);
    pragma Inline (Set_Subtype_Indication);
    pragma Inline (Set_Subtype_Mark);
    pragma Inline (Set_Subtype_Marks);
    pragma Inline (Set_Suppress_Assignment_Checks);
    pragma Inline (Set_Suppress_Loop_Warnings);
    pragma Inline (Set_Synchronized_Present);
+   pragma Inline (Set_TSS_Elist);
    pragma Inline (Set_Tagged_Present);
    pragma Inline (Set_Target_Type);
    pragma Inline (Set_Task_Definition);
    pragma Inline (Set_Task_Present);
    pragma Inline (Set_Then_Actions);
    pragma Inline (Set_Then_Statements);
+   pragma Inline (Set_Treat_Fixed_As_Integer);
    pragma Inline (Set_Triggering_Alternative);
    pragma Inline (Set_Triggering_Statement);
-   pragma Inline (Set_Treat_Fixed_As_Integer);
-   pragma Inline (Set_TSS_Elist);
    pragma Inline (Set_Type_Definition);
    pragma Inline (Set_Unit);
    pragma Inline (Set_Unknown_Discriminants_Present);
    pragma Inline (Set_Unreferenced_In_Spec);
+   pragma Inline (Set_Used_Operations);
    pragma Inline (Set_Variant_Part);
    pragma Inline (Set_Variants);
    pragma Inline (Set_Visible_Declarations);
-   pragma Inline (Set_Used_Operations);
    pragma Inline (Set_Was_Originally_Stub);
    pragma Inline (Set_Withed_Body);
 
Index: exp_ch9.adb
===================================================================
--- exp_ch9.adb	(revision 197899)
+++ exp_ch9.adb	(working copy)
@@ -1934,7 +1934,8 @@ 
 
          while Present (P) loop
             if Pragma_Name (P) = Name_Precondition
-              or else Pragma_Name (P) = Name_Postcondition
+                 or else
+               Pragma_Name (P) = Name_Postcondition
             then
                Append (Relocate_Node (P), Decls);
                Set_Analyzed (Last (Decls), False);
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 197909)
+++ einfo.adb	(working copy)
@@ -546,9 +546,9 @@ 
    --    Is_Predicate_Function           Flag255
    --    Is_Predicate_Function_M         Flag256
    --    Is_Invariant_Procedure          Flag257
+   --    Has_Dynamic_Predicate_Aspect    Flag258
+   --    Has_Static_Predicate_Aspect     Flag259
 
-   --    (unused)                        Flag258
-   --    (unused)                        Flag259
    --    (unused)                        Flag260
 
    --    (unused)                        Flag261
@@ -1395,6 +1395,12 @@ 
       return Flag220 (Id);
    end Has_Dispatch_Table;
 
+   function Has_Dynamic_Predicate_Aspect (Id : E) return B is
+   begin
+      pragma Assert (Is_Type (Id));
+      return Flag258 (Id);
+   end Has_Dynamic_Predicate_Aspect;
+
    function Has_Enumeration_Rep_Clause (Id : E) return B is
    begin
       pragma Assert (Is_Enumeration_Type (Id));
@@ -1670,6 +1676,12 @@ 
       return Flag211 (Id);
    end Has_Static_Discriminants;
 
+   function Has_Static_Predicate_Aspect (Id : E) return B is
+   begin
+      pragma Assert (Is_Type (Id));
+      return Flag259 (Id);
+   end Has_Static_Predicate_Aspect;
+
    function Has_Storage_Size_Clause (Id : E) return B is
    begin
       pragma Assert (Is_Access_Type (Id) or else Is_Task_Type (Id));
@@ -3967,6 +3979,12 @@ 
       Set_Flag220 (Id, V);
    end Set_Has_Dispatch_Table;
 
+   procedure Set_Has_Dynamic_Predicate_Aspect (Id : E; V : B := True) is
+   begin
+      pragma Assert (Is_Type (Id));
+      Set_Flag258 (Id, V);
+   end Set_Has_Dynamic_Predicate_Aspect;
+
    procedure Set_Has_Enumeration_Rep_Clause (Id : E; V : B := True) is
    begin
       pragma Assert (Is_Enumeration_Type (Id));
@@ -4251,6 +4269,12 @@ 
       Set_Flag211 (Id, V);
    end Set_Has_Static_Discriminants;
 
+   procedure Set_Has_Static_Predicate_Aspect (Id : E; V : B := True) is
+   begin
+      pragma Assert (Is_Type (Id));
+      Set_Flag259 (Id, V);
+   end Set_Has_Static_Predicate_Aspect;
+
    procedure Set_Has_Storage_Size_Clause (Id : E; V : B := True) is
    begin
       pragma Assert (Is_Access_Type (Id) or else Is_Task_Type (Id));
@@ -7759,6 +7783,8 @@ 
       W ("Has_Delayed_Aspects",             Flag200 (Id));
       W ("Has_Delayed_Freeze",              Flag18  (Id));
       W ("Has_Discriminants",               Flag5   (Id));
+      W ("Has_Dispatch_Table",              Flag220 (Id));
+      W ("Has_Dynamic_Predicate_Aspect",    Flag258 (Id));
       W ("Has_Enumeration_Rep_Clause",      Flag66  (Id));
       W ("Has_Exit",                        Flag47  (Id));
       W ("Has_External_Tag_Rep_Clause",     Flag110 (Id));
@@ -7808,6 +7834,7 @@ 
       W ("Has_Specified_Stream_Read",       Flag192 (Id));
       W ("Has_Specified_Stream_Write",      Flag193 (Id));
       W ("Has_Static_Discriminants",        Flag211 (Id));
+      W ("Has_Static_Predicate_Aspect",     Flag259 (Id));
       W ("Has_Storage_Size_Clause",         Flag23  (Id));
       W ("Has_Stream_Size_Clause",          Flag184 (Id));
       W ("Has_Task",                        Flag30  (Id));
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 197909)
+++ einfo.ads	(working copy)
@@ -1487,6 +1487,14 @@ 
 --       of the table); otherwise the code that builds the table is added at
 --       the end of the list of declarations of the package.
 
+--    Has_Dynamic_Predicate_Aspect (Flag258)
+--       Defined in all types and subtypes. Set if a Dynamic_Predicate aspect
+--       applies to the type. Note that we can tell if a dynamic predicate is
+--       present by looking at Has_Predicates and Static_Predicate, but that
+--       could have come from a Predicate aspect or pragma, and we need to
+--       record the difference so that we can use the right set of check
+--       policies to figure out if the predicate is active.
+
 --    Has_Entries (synthesized)
 --       Applies to concurrent types. True if any entries are declared
 --       within the task or protected definition for the type.
@@ -1817,6 +1825,14 @@ 
 --       case of a variant record, the component list can be trimmed down to
 --       include only the components corresponding to these discriminants.
 
+--    Has_Static_Predicate_Aspect (Flag259)
+--       Defined in all types and subtypes. Set if a Dynamic_Predicate aspect
+--       applies to the type. Note that we can tell if a static predicate is
+--       present by looking at Has_Predicates and Static_Predicate, but that
+--       could have come from a Predicate aspect or pragma, and we need to
+--       record the difference so that we can use the right set of check
+--       policies to figure out if the predicate is active.
+
 --    Has_Storage_Size_Clause (Flag23) [implementation base type only]
 --       Defined in task types and access types. It is set if a Storage_Size
 --       clause is present for the type. Used to prevent multiple clauses for
@@ -4980,6 +4996,7 @@ 
    --    Has_Controlled_Component            (Flag43)   (base type only)
    --    Has_Default_Aspect                  (Flag39)   (base type only)
    --    Has_Discriminants                   (Flag5)
+   --    Has_Dynamic_Predicate_Aspect        (Flag258)
    --    Has_Independent_Components          (Flag34)   (base type only)
    --    Has_Inheritable_Invariants          (Flag248)
    --    Has_Invariants                      (Flag232)
@@ -4995,6 +5012,7 @@ 
    --    Has_Specified_Stream_Output         (Flag191)
    --    Has_Specified_Stream_Read           (Flag192)
    --    Has_Specified_Stream_Write          (Flag193)
+   --    Has_Static_Predicate_Aspect         (Flag259)
    --    Has_Task                            (Flag30)   (base type only)
    --    Has_Unchecked_Union                 (Flag123)  (base type only)
    --    Has_Volatile_Components             (Flag87)   (base type only)
@@ -6247,6 +6265,7 @@ 
    function Has_Delayed_Freeze                  (Id : E) return B;
    function Has_Discriminants                   (Id : E) return B;
    function Has_Dispatch_Table                  (Id : E) return B;
+   function Has_Dynamic_Predicate_Aspect        (Id : E) return B;
    function Has_Enumeration_Rep_Clause          (Id : E) return B;
    function Has_Exit                            (Id : E) return B;
    function Has_External_Tag_Rep_Clause         (Id : E) return B;
@@ -6285,6 +6304,7 @@ 
    function Has_Predicates                      (Id : E) return B;
    function Has_Primitive_Operations            (Id : E) return B;
    function Has_Private_Ancestor                (Id : E) return B;
+   function Has_Private_Declaration             (Id : E) return B;
    function Has_Qualified_Name                  (Id : E) return B;
    function Has_RACW                            (Id : E) return B;
    function Has_Record_Rep_Clause               (Id : E) return B;
@@ -6297,6 +6317,7 @@ 
    function Has_Specified_Stream_Read           (Id : E) return B;
    function Has_Specified_Stream_Write          (Id : E) return B;
    function Has_Static_Discriminants            (Id : E) return B;
+   function Has_Static_Predicate_Aspect         (Id : E) return B;
    function Has_Storage_Size_Clause             (Id : E) return B;
    function Has_Stream_Size_Clause              (Id : E) return B;
    function Has_Task                            (Id : E) return B;
@@ -6608,7 +6629,6 @@ 
    function Has_Attach_Handler                  (Id : E) return B;
    function Has_Entries                         (Id : E) return B;
    function Has_Foreign_Convention              (Id : E) return B;
-   function Has_Private_Declaration             (Id : E) return B;
    function Implementation_Base_Type            (Id : E) return E;
    function Is_Base_Type                        (Id : E) return B;
    function Is_Boolean_Type                     (Id : E) return B;
@@ -6853,6 +6873,7 @@ 
    procedure Set_Has_Delayed_Freeze              (Id : E; V : B := True);
    procedure Set_Has_Discriminants               (Id : E; V : B := True);
    procedure Set_Has_Dispatch_Table              (Id : E; V : B := True);
+   procedure Set_Has_Dynamic_Predicate_Aspect    (Id : E; V : B := True);
    procedure Set_Has_Enumeration_Rep_Clause      (Id : E; V : B := True);
    procedure Set_Has_Exit                        (Id : E; V : B := True);
    procedure Set_Has_External_Tag_Rep_Clause     (Id : E; V : B := True);
@@ -6903,6 +6924,7 @@ 
    procedure Set_Has_Specified_Stream_Read       (Id : E; V : B := True);
    procedure Set_Has_Specified_Stream_Write      (Id : E; V : B := True);
    procedure Set_Has_Static_Discriminants        (Id : E; V : B := True);
+   procedure Set_Has_Static_Predicate_Aspect     (Id : E; V : B := True);
    procedure Set_Has_Storage_Size_Clause         (Id : E; V : B := True);
    procedure Set_Has_Stream_Size_Clause          (Id : E; V : B := True);
    procedure Set_Has_Task                        (Id : E; V : B := True);
@@ -7550,6 +7572,7 @@ 
    pragma Inline (Has_Delayed_Freeze);
    pragma Inline (Has_Discriminants);
    pragma Inline (Has_Dispatch_Table);
+   pragma Inline (Has_Dynamic_Predicate_Aspect);
    pragma Inline (Has_Enumeration_Rep_Clause);
    pragma Inline (Has_Exit);
    pragma Inline (Has_External_Tag_Rep_Clause);
@@ -7600,6 +7623,7 @@ 
    pragma Inline (Has_Specified_Stream_Read);
    pragma Inline (Has_Specified_Stream_Write);
    pragma Inline (Has_Static_Discriminants);
+   pragma Inline (Has_Static_Predicate_Aspect);
    pragma Inline (Has_Storage_Size_Clause);
    pragma Inline (Has_Stream_Size_Clause);
    pragma Inline (Has_Task);
@@ -8005,6 +8029,7 @@ 
    pragma Inline (Set_Has_Delayed_Freeze);
    pragma Inline (Set_Has_Discriminants);
    pragma Inline (Set_Has_Dispatch_Table);
+   pragma Inline (Set_Has_Dynamic_Predicate_Aspect);
    pragma Inline (Set_Has_Enumeration_Rep_Clause);
    pragma Inline (Set_Has_Exit);
    pragma Inline (Set_Has_External_Tag_Rep_Clause);
@@ -8055,6 +8080,7 @@ 
    pragma Inline (Set_Has_Specified_Stream_Read);
    pragma Inline (Set_Has_Specified_Stream_Write);
    pragma Inline (Set_Has_Static_Discriminants);
+   pragma Inline (Set_Has_Static_Predicate_Aspect);
    pragma Inline (Set_Has_Storage_Size_Clause);
    pragma Inline (Set_Has_Stream_Size_Clause);
    pragma Inline (Set_Has_Task);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 197912)
+++ sem_prag.adb	(working copy)
@@ -181,11 +181,24 @@ 
    --  original one, following the renaming chain) is returned. Otherwise the
    --  entity is returned unchanged. Should be in Einfo???
 
+   function Is_Valid_Assertion_Kind (Nam : Name_Id) return Boolean;
+   --  Returns True if Nam is one of the names recognized as a valid assertion
+   --  kind by the Assertion_Policy pragma. Note that the 'Class cases are
+   --  represented by the corresponding special names Name_uPre, Name_uPost,
+   --  Name_uInviarnat, and Name_uType_Invariant (_Pre, _Post, _Invariant,
+   --  and _Type_Invariant).
+
    procedure Preanalyze_CTC_Args (N, Arg_Req, Arg_Ens : Node_Id);
    --  Preanalyze the boolean expressions in the Requires and Ensures arguments
    --  of a Contract_Case or Test_Case pragma if present (possibly Empty). We
    --  treat these as spec expressions (i.e. similar to a default expression).
 
+   procedure Rewrite_Assertion_Kind (N : Node_Id);
+   --  If N is Pre'Class, Post'Class, Invariant'Class, or Type_Invariant'Class,
+   --  then it is rewritten as an identifier with the corresponding special
+   --  name _Pre, _Post, _Invariant, or _Type_Invariant. Used by pragmas
+   --  Check, Check_Policy.
+
    procedure rv;
    --  This is a dummy function called by the processing for pragma Reviewable.
    --  It is there for assisting front end debugging. By placing a Reviewable
@@ -294,7 +307,8 @@ 
       --  expressions (i.e. similar to a default expression).
 
       if Pragma_Name (N) = Name_Test_Case
-        or else Pragma_Name (N) = Name_Contract_Case
+           or else
+         Pragma_Name (N) = Name_Contract_Case
       then
          Preanalyze_CTC_Args
            (N,
@@ -308,9 +322,7 @@ 
          --  In ASIS mode, for a pragma generated from a source aspect, also
          --  analyze the original aspect expression.
 
-         if ASIS_Mode
-           and then Present (Corresponding_Aspect (N))
-         then
+         if ASIS_Mode and then Present (Corresponding_Aspect (N)) then
             Analyze_Contract_Cases (Expression (Corresponding_Aspect (N)));
          end if;
       end if;
@@ -1212,6 +1224,7 @@ 
                OK   : Boolean;
                Ent  : constant Entity_Id := Entity (Argx);
                Scop : constant Entity_Id := Scope (Ent);
+
             begin
                --  Case of a pragma applied to a compilation unit: pragma must
                --  occur immediately after the program unit in the compilation.
@@ -6768,6 +6781,12 @@ 
          Pname := Chars (Identifier (Corresponding_Aspect (N)));
       end if;
 
+      Check_Applicable_Policy (N);
+
+      if Is_Disabled (N) then
+         raise Pragma_Exit;
+      end if;
+
       --  Preset arguments
 
       Arg_Count := 0;
@@ -7446,41 +7465,174 @@ 
          -- Assertion_Policy --
          ----------------------
 
-         --  pragma Assertion_Policy (Check | Disable | Ignore)
+         --  pragma Assertion_Policy (POLICY_IDENTIFIER);
 
+         --  The following form is Ada 2012 only, but we allow it in all modes
+
+         --  Pragma Assertion_Policy (
+         --      ASSERTION_KIND => POLICY_IDENTIFIER
+         --   {, ASSERTION_KIND => POLICY_IDENTIFIER});
+
+         --  ASSERTION_KIND ::= RM_ASSERTION_KIND | ID_ASSERTION_KIND
+
+         --  RM_ASSERTION_KIND ::= Assert               |
+         --                        Static_Predicate     |
+         --                        Dynamic_Predicate    |
+         --                        Pre                  |
+         --                        Pre'Class            |
+         --                        Post                 |
+         --                        Post'Class           |
+         --                        Type_Invariant       |
+         --                        Type_Invariant'Class
+
+         --  ID_ASSERTION_KIND ::= Assert_And_Cut       }
+         --                        Assume               |
+         --                        Contract_Cases       |
+         --                        Debug                |
+         --                        Loop_Invariant       |
+         --                        Loop_Variant         |
+         --                        Postcondition        |
+         --                        Precondition         |
+         --                        Predicate
+         --
+         --  Note: The RM_ASSERTION_KIND list is language-defined, and the
+         --  ID_ASSERTION_KIND list contains implementation-defined additions
+         --  recognized by GNAT. The effect is to control the behavior of
+         --  identically named aspects and pragmas, depending on the specified
+         --  policy identifier:
+
+         --  POLICY_IDENTIFIER ::= Check | Disable | Ignore
+
+         --  Note: Check and Ignore are language-defined. Disable is a GNAT
+         --  implementation defined addition that results in totally ignoring
+         --  the corresponding assertion. If Disable is specified, then the
+         --  argument of the assertion is not even analyzed. This is useful
+         --  when the aspect/pragma argument references entities in a with'ed
+         --  packaqe that is replaced by a dummy package in the final build.
+
+         --  Note: the attribute forms Pre'Class, Post'Class, Invariant'Class,
+         --  and Type_Invariant'Class were recognized by the parser and
+         --  transformed into referencea to the special internal identifiers
+         --  _Pre, _Post, _Invariant, and _Type_Invariant, so no special
+         --  processing is required here.
+
          when Pragma_Assertion_Policy => Assertion_Policy : declare
+            LocP   : Source_Ptr;
             Policy : Node_Id;
+            Arg    : Node_Id;
+            Kind   : Name_Id;
+            Prag   : Node_Id;
 
          begin
             Ada_2005_Pragma;
-            Check_Valid_Configuration_Pragma;
-            Check_Arg_Count (1);
-            Check_No_Identifiers;
-            Check_Arg_Is_One_Of (Arg1, Name_Check, Name_Disable, Name_Ignore);
 
-            --  We treat pragma Assertion_Policy as equivalent to:
+            --  This can always appear as a configuration pragma
 
-            --    pragma Check_Policy (Assertion, policy)
+            if Is_Configuration_Pragma then
+               null;
 
-            --  So rewrite the pragma in that manner and link on to the chain
-            --  of Check_Policy pragmas, marking the pragma as analyzed.
+            --  It can also appear in a declaration or package spec in Ada
+            --  2012 mode. We allow this in other modes, but in that case
+            --  we consider that we have an Ada 2012 pragma on our hands.
 
-            Policy := Get_Pragma_Arg (Arg1);
+            else
+               Check_Is_In_Decl_Part_Or_Package_Spec;
+               Ada_2012_Pragma;
+            end if;
 
-            Rewrite (N,
-              Make_Pragma (Loc,
-                Chars                        => Name_Check_Policy,
-                Pragma_Argument_Associations => New_List (
-                  Make_Pragma_Argument_Association (Loc,
-                    Expression => Make_Identifier (Loc, Name_Assertion)),
+            --  One argument case with no identifier (first form above)
 
-                  Make_Pragma_Argument_Association (Loc,
-                    Expression =>
-                      Make_Identifier (Sloc (Policy), Chars (Policy))))));
+            if Arg_Count = 1
+              and then (Nkind (Arg1) /= N_Pragma_Argument_Association
+                         or else Chars (Arg1) = No_Name)
+            then
+               Check_Arg_Is_One_Of
+                 (Arg1, Name_Check, Name_Disable, Name_Ignore);
 
-            Set_Analyzed (N);
-            Set_Next_Pragma (N, Opt.Check_Policy_List);
-            Opt.Check_Policy_List := N;
+               --  Treat one argument Assertion_Policy as equivalent to:
+
+               --    pragma Check_Policy (Assertion, policy)
+
+               --  So rewrite pragma in that manner and link on to the chain
+               --  of Check_Policy pragmas, marking the pragma as analyzed.
+
+               Policy := Get_Pragma_Arg (Arg1);
+
+               Rewrite (N,
+                 Make_Pragma (Loc,
+                   Chars                        => Name_Check_Policy,
+                   Pragma_Argument_Associations => New_List (
+                     Make_Pragma_Argument_Association (Loc,
+                       Expression => Make_Identifier (Loc, Name_Assertion)),
+
+                     Make_Pragma_Argument_Association (Loc,
+                       Expression =>
+                         Make_Identifier (Sloc (Policy), Chars (Policy))))));
+
+               Set_Analyzed (N);
+               Set_Next_Pragma (N, Opt.Check_Policy_List);
+               Opt.Check_Policy_List := N;
+
+            --  Here if we have two or more arguments
+
+            else
+               Check_At_Least_N_Arguments (1);
+               Ada_2012_Pragma;
+
+               --  Loop through arguments
+
+               Arg := Arg1;
+               while Present (Arg) loop
+                  LocP := Sloc (Arg);
+
+                  --  Kind must be specified
+
+                  if Nkind (Arg) /= N_Pragma_Argument_Association
+                    or else Chars (Arg) = No_Name
+                  then
+                     Error_Pragma_Arg
+                       ("missing assertion kind for pragma%", Arg);
+                  end if;
+
+                  --  Check Kind and Policy have allowed forms
+
+                  Kind := Chars (Arg);
+
+                  if not Is_Valid_Assertion_Kind (Kind) then
+                     Error_Pragma_Arg
+                       ("invalid assertion kind for pragma%", Arg);
+                  end if;
+
+                  Check_Arg_Is_One_Of
+                    (Arg, Name_Check, Name_Disable, Name_Ignore);
+
+                  --  We rewrite the Assertion_Policy pragma as a series of
+                  --  Check_Policy pragmas:
+
+                  --    Check_Policy (Kind, Policy);
+
+                  Prag :=
+                    Make_Pragma (LocP,
+                      Chars                        => Name_Check_Policy,
+                      Pragma_Argument_Associations => New_List (
+                         Make_Pragma_Argument_Association (LocP,
+                           Expression => Make_Identifier (LocP, Kind)),
+                         Make_Pragma_Argument_Association (LocP,
+                           Expression => Get_Pragma_Arg (Arg))));
+
+                  Set_Analyzed (Prag);
+                  Set_Next_Pragma (Prag, Opt.Check_Policy_List);
+                  Opt.Check_Policy_List := Prag;
+                  Insert_Action (N, Prag);
+
+                  Arg := Next (Arg);
+               end loop;
+
+               --  Rewrite the Assertion_Policy pragma as null since we have
+               --  now inserted all the equivalent Check pragmas.
+
+               Rewrite (N, Make_Null_Statement (Loc));
+            end if;
          end Assertion_Policy;
 
          ------------
@@ -7930,10 +8082,16 @@ 
          -- Check --
          -----------
 
-         --  pragma Check ([Name    =>] IDENTIFIER,
+         --  pragma Check ([Name    =>] CHECK_KIND,
          --                [Check   =>] Boolean_EXPRESSION
          --              [,[Message =>] String_EXPRESSION]);
 
+         --  CHECK_KIND ::= IDENTIFIER           |
+         --                 Pre'Class            |
+         --                 Post'Class           |
+         --                 Invariant'Class      |
+         --                 Type_Invariant'Class
+
          when Pragma_Check => Check : declare
             Expr  : Node_Id;
             Eloc  : Source_Ptr;
@@ -7955,6 +8113,7 @@ 
                Str := Get_Pragma_Arg (Arg3);
             end if;
 
+            Rewrite_Assertion_Kind (Get_Pragma_Arg (Arg1));
             Check_Arg_Is_Identifier (Arg1);
             Cname := Chars (Get_Pragma_Arg (Arg1));
             Check_On := Check_Enabled (Cname);
@@ -8094,19 +8253,21 @@ 
          -- Check_Policy --
          ------------------
 
-         --  pragma Check_Policy (
-         --    [Name   =>] IDENTIFIER,
-         --    [Policy =>] POLICY_IDENTIFIER);
+         --  pragma Check_Policy ([Name   =>] CHECK_KIND
+         --                       [Policy =>] POLICY_IDENTIFIER);
 
-         --  POLICY_IDENTIFIER ::= ON | OFF | CHECK | DISABLE | IGNORE
+         --  POLICY_IDENTIFIER ::= On | Off | Check | Disable | Ignore
 
-         --  Note: this is a configuration pragma, but it is allowed to appear
-         --  anywhere else.
+         --  CHECK_KIND ::= IDENTIFIER |
+         --                 Pre'Class | Post'Class | Identifier'Class
 
-         when Pragma_Check_Policy =>
+         when Pragma_Check_Policy => Check_Policy :
+         begin
             GNAT_Pragma;
             Check_Arg_Count (2);
             Check_Optional_Identifier (Arg1, Name_Name);
+            Rewrite_Assertion_Kind (Get_Pragma_Arg (Arg1));
+            Check_Arg_Is_Identifier (Arg1);
             Check_Optional_Identifier (Arg2, Name_Policy);
             Check_Arg_Is_One_Of
               (Arg2, Name_On, Name_Off, Name_Check, Name_Disable, Name_Ignore);
@@ -8122,6 +8283,7 @@ 
 
             Set_Next_Pragma (N, Opt.Check_Policy_List);
             Opt.Check_Policy_List := N;
+         end Check_Policy;
 
          ---------------------
          -- CIL_Constructor --
@@ -8438,9 +8600,9 @@ 
             S14_Pragma;
             Check_Arg_Count (1);
 
-            --  Completely ignore if disabled
+            --  Completely ignore if not enabled
 
-            if not Check_Enabled (Pname) then
+            if Is_Ignored (N) then
                Rewrite (N, Make_Null_Statement (Loc));
                Analyze (N);
                return;
@@ -8873,20 +9035,16 @@ 
          begin
             GNAT_Pragma;
 
-            --  Skip analysis if disabled
+            --  The condition for executing the call is that the expander
+            --  is active and that we are not ignoring this debug pragma.
 
-            if Debug_Pragmas_Disabled then
-               Rewrite (N, Make_Null_Statement (Loc));
-               Analyze (N);
-               return;
-            end if;
-
             Cond :=
               New_Occurrence_Of
-                (Boolean_Literals (Debug_Pragmas_Enabled and Expander_Active),
+                (Boolean_Literals
+                  (Expander_Active and then not Is_Ignored (N)),
                  Loc);
 
-            if Debug_Pragmas_Enabled then
+            if not Is_Ignored (N) then
                Set_SCO_Pragma_Enabled (Loc);
             end if;
 
@@ -8965,17 +9123,30 @@ 
          -- Debug_Policy --
          ------------------
 
-         --  pragma Debug_Policy (Check | Ignore)
+         --  pragma Debug_Policy (On | Off | Check | Disable | Ignore)
 
          when Pragma_Debug_Policy =>
             GNAT_Pragma;
             Check_Arg_Count (1);
-            Check_Arg_Is_One_Of (Arg1, Name_Check, Name_Disable, Name_Ignore);
-            Debug_Pragmas_Enabled :=
-              Chars (Get_Pragma_Arg (Arg1)) = Name_Check;
-            Debug_Pragmas_Disabled :=
-              Chars (Get_Pragma_Arg (Arg1)) = Name_Disable;
+            Check_No_Identifiers;
+            Check_Arg_Is_Identifier (Arg1);
 
+            --  Exactly equivalent to pragma Check_Policy (Debug, arg), so
+            --  rewrite it that way, and let the rest of the checking come
+            --  from analyzing the rewritten pragma.
+
+            Rewrite (N,
+              Make_Pragma (Loc,
+                Chars                        => Name_Check_Policy,
+                Pragma_Argument_Associations => New_List (
+                  Make_Pragma_Argument_Association (Loc,
+                    Expression => Make_Identifier (Loc, Name_Debug)),
+
+                  Make_Pragma_Argument_Association (Loc,
+                    Expression => Get_Pragma_Arg (Arg1)))));
+
+            Analyze (N);
+
          -------------
          -- Depends --
          -------------
@@ -12778,10 +12949,10 @@ 
             end if;
 
             --  Note that the type has at least one invariant, and also that
-            --  it has inheritable invariants if we have Invariant'Class.
-            --  Build the corresponding invariant procedure declaration, so
-            --  that calls to it can be generated before the body is built
-            --  (for example wihin an expression function).
+            --  it has inheritable invariants if we have Invariant'Class
+            --  or Type_Invariant'Class. Build the corresponding invariant
+            --  procedure declaration, so that calls to it can be generated
+            --  before the body is built (e.g. within an expression function).
 
             PDecl := Build_Invariant_Procedure_Declaration (Typ);
             Insert_After (N, PDecl);
@@ -13591,9 +13762,9 @@ 
             Check_Arg_Count (1);
             Check_Loop_Pragma_Placement;
 
-            --  Completely ignore if disabled
+            --  Completely ignore if not enabled
 
-            if not Check_Enabled (Pname) then
+            if Is_Ignored (N) then
                Rewrite (N, Make_Null_Statement (Loc));
                Analyze (N);
                return;
@@ -13662,9 +13833,9 @@ 
             Check_At_Least_N_Arguments (1);
             Check_Loop_Pragma_Placement;
 
-            --  Completely ignore if disabled
+            --  Completely ignore if not enabled
 
-            if not Check_Enabled (Pname) then
+            if Is_Ignored (N) then
                Rewrite (N, Make_Null_Statement (Loc));
                Analyze (N);
                return;
@@ -14762,7 +14933,7 @@ 
 
             Check_Precondition_Postcondition (In_Body);
 
-            --  When the pragma is a source contruct and appears inside a body,
+            --  When the pragma is a source construct appearing inside a body,
             --  preanalyze the boolean_expression to detect illegal forward
             --  references:
 
@@ -14793,18 +14964,28 @@ 
             Check_Precondition_Postcondition (In_Body);
 
             --  If in spec, nothing more to do. If in body, then we convert the
-            --  pragma to pragma Check (Precondition, cond [, msg]). Note we do
-            --  this whether or not precondition checks are enabled. That works
-            --  fine since pragma Check will do this check, and will also
-            --  analyze the condition itself in the proper context.
+            --  pragma to an equivalent pragam Check. Note we do this whether
+            --  or not precondition checks are enabled. That works fine since
+            --  pragma Check will do this check, and will also analyze the
+            --  condition itself in the proper context.
 
+            --  The form of the pragma Check is either:
+
+            --    pragma Check (Precondition, cond [, msg])
+            --       or
+            --    pragma Check (Pre, cond [, msg])
+
+            --  We use the Pre form if this pragma derived from a Pre aspect.
+            --  This is needed to make sure that the right set of Policy
+            --  pragmas are checked.
+
             if In_Body then
                Rewrite (N,
                  Make_Pragma (Loc,
                    Chars                        => Name_Check,
                    Pragma_Argument_Associations => New_List (
                      Make_Pragma_Argument_Association (Loc,
-                       Expression => Make_Identifier (Loc, Name_Precondition)),
+                       Expression => Make_Identifier (Loc, Pname)),
 
                      Make_Pragma_Argument_Association (Sloc (Arg1),
                        Expression => Relocate_Node (Get_Pragma_Arg (Arg1))))));
@@ -17591,40 +17772,124 @@ 
       --  Loop through entries in check policy list
 
       PP := Opt.Check_Policy_List;
-      loop
-         --  If there are no specific entries that matched, then we let the
-         --  setting of assertions govern. Note that this provides the needed
-         --  compatibility with the RM for the cases of assertion, invariant,
-         --  precondition, predicate, and postcondition.
+      while Present (PP) loop
+         declare
+            PPA : constant List_Id := Pragma_Argument_Associations (PP);
+            Pnm : constant Name_Id := Chars (Get_Pragma_Arg (First (PPA)));
 
-         if No (PP) then
-            return Assertions_Enabled;
+         begin
+            if Nam = Pnm
+              or else (Is_Valid_Assertion_Kind (Nam)
+                        and then Pnm = Name_Assertion)
+            then
+               case (Chars (Get_Pragma_Arg (Last (PPA)))) is
+                  when Name_On | Name_Check =>
+                     return True;
+                  when Name_Off | Name_Disable | Name_Ignore =>
+                     return False;
+                  when others =>
+                     raise Program_Error;
+               end case;
 
-         --  Here we have an entry see if it matches
+            else
+               PP := Next_Pragma (PP);
+            end if;
+         end;
+      end loop;
 
+      --  If there are no specific entries that matched, then we let the
+      --  setting of assertions govern. Note that this provides the needed
+      --  compatibility with the RM for the cases of assertion, invariant,
+      --  precondition, predicate, and postcondition.
+
+      return Assertions_Enabled;
+   end Check_Enabled;
+
+   -----------------------------
+   -- Check_Applicable_Policy --
+   -----------------------------
+
+   procedure Check_Applicable_Policy (N : Node_Id) is
+      PP     : Node_Id;
+      Policy : Name_Id;
+
+      Ename : Name_Id;
+      --  Effective name of aspect or pragma, this is simply the name of
+      --  the aspect or pragma, except in the case of a pragma derived from
+      --  an aspect, in which case it is the name of the aspect (which may be
+      --  different, e.g. Pre aspect generating Precondition pragma). It also
+      --  deals with the 'Class cases for an aspect.
+
+   begin
+      if Nkind (N) = N_Pragma then
+         if Present (Corresponding_Aspect (N)) then
+            Ename := Chars (Identifier (Corresponding_Aspect (N)));
          else
-            declare
-               PPA : constant List_Id := Pragma_Argument_Associations (PP);
+            Ename := Chars (Pragma_Identifier (N));
+         end if;
 
-            begin
-               if Nam = Chars (Get_Pragma_Arg (First (PPA))) then
-                  case (Chars (Get_Pragma_Arg (Last (PPA)))) is
-                     when Name_On | Name_Check =>
-                        return True;
-                     when Name_Off | Name_Disable | Name_Ignore =>
-                        return False;
-                     when others =>
-                        raise Program_Error;
-                  end case;
+      else
+         pragma Assert (Nkind (N) = N_Aspect_Specification);
+         Ename := Chars (Identifier (N));
 
-               else
-                  PP := Next_Pragma (PP);
-               end if;
-            end;
+         if Class_Present (N) then
+            case Ename is
+               when Name_Invariant      => Ename := Name_uInvariant;
+               when Name_Pre            => Ename := Name_uPre;
+               when Name_Post           => Ename := Name_uPost;
+               when Name_Type_Invariant => Ename := Name_uType_Invariant;
+               when others           => raise Program_Error;
+            end case;
          end if;
+      end if;
+
+      --  No effect if not valid assertion kind name
+
+      if not Is_Valid_Assertion_Kind (Ename) then
+         return;
+      end if;
+
+      --  Loop through entries in check policy list
+
+      PP := Opt.Check_Policy_List;
+      while Present (PP) loop
+         declare
+            PPA : constant List_Id := Pragma_Argument_Associations (PP);
+            Pnm : constant Name_Id := Chars (Get_Pragma_Arg (First (PPA)));
+
+         begin
+            if Ename = Pnm or else Pnm = Name_Assertion then
+               Policy := Chars (Get_Pragma_Arg (Last (PPA)));
+
+               case Policy is
+                  when Name_Off | Name_Ignore =>
+                     Set_Is_Ignored (N, True);
+
+                  when Name_Disable =>
+                     Set_Is_Ignored (N, True);
+                     Set_Is_Disabled (N, True);
+
+                  when others =>
+                     null;
+               end case;
+
+               return;
+            end if;
+
+            PP := Next_Pragma (PP);
+         end;
       end loop;
-   end Check_Enabled;
 
+      --  If there are no specific entries that matched, then we let the
+      --  setting of assertions govern. Note that this provides the needed
+      --  compatibility with the RM for the cases of assertion, invariant,
+      --  precondition, predicate, and postcondition.
+
+      if not Assertions_Enabled then
+         Set_Is_Ignored (N);
+      end if;
+   end Check_Applicable_Policy;
+
    ---------------------------------
    -- Delay_Config_Pragma_Analyze --
    ---------------------------------
@@ -18076,6 +18341,44 @@ 
       end if;
    end Is_Pragma_String_Literal;
 
+   -----------------------------
+   -- Is_Valid_Assertion_Kind --
+   -----------------------------
+
+   function Is_Valid_Assertion_Kind (Nam : Name_Id) return Boolean is
+   begin
+      case Nam is
+         when
+            --  RM defined
+
+            Name_Assert            |
+            Name_Static_Predicate  |
+            Name_Dynamic_Predicate |
+            Name_Pre               |
+            Name_uPre              |
+            Name_Post              |
+            Name_uPost             |
+            Name_Type_Invariant    |
+            Name_uType_Invariant   |
+
+            --  Impl defined
+
+            Name_Assert_And_Cut    |
+            Name_Assume            |
+            Name_Contract_Cases    |
+            Name_Debug             |
+            Name_Invariant         |
+            Name_uInvariant        |
+            Name_Loop_Invariant    |
+            Name_Loop_Variant      |
+            Name_Postcondition     |
+            Name_Precondition      |
+            Name_Predicate         => return True;
+
+         when others               => return False;
+      end case;
+   end Is_Valid_Assertion_Kind;
+
    -----------------------------------------
    -- Make_Aspect_For_PPC_In_Gen_Sub_Decl --
    -----------------------------------------
@@ -18215,6 +18518,35 @@ 
 
    end Process_Compilation_Unit_Pragmas;
 
+   ----------------------------
+   -- Rewrite_Assertion_Kind --
+   ----------------------------
+
+   procedure Rewrite_Assertion_Kind (N : Node_Id) is
+      Nam : Name_Id;
+
+   begin
+      if Nkind (N) = N_Attribute_Reference
+        and then Attribute_Name (N) = Name_Class
+        and then Nkind (Prefix (N)) = N_Identifier
+      then
+         case Chars (Prefix (N)) is
+            when Name_Pre =>
+               Nam := Name_uPre;
+            when Name_Post =>
+               Nam := Name_uPost;
+            when Name_Type_Invariant =>
+               Nam := Name_uType_Invariant;
+            when Name_Invariant =>
+               Nam := Name_uInvariant;
+            when others =>
+               return;
+         end case;
+
+         Rewrite (N, Make_Identifier (Sloc (N), Chars => Nam));
+      end if;
+   end Rewrite_Assertion_Kind;
+
    --------
    -- rv --
    --------
Index: sem_prag.ads
===================================================================
--- sem_prag.ads	(revision 197899)
+++ sem_prag.ads	(working copy)
@@ -56,14 +56,46 @@ 
 
    function Check_Enabled (Nam : Name_Id) return Boolean;
    --  This function is used in connection with pragmas Assertion, Check,
-   --  Precondition, and Postcondition, to determine if Check pragmas (or
-   --  corresponding Assert, Precondition, or Postcondition pragmas) are
-   --  currently active, as determined by the presence of -gnata on the
-   --  command line (which sets the default), and the appearance of pragmas
-   --  Check_Policy and Assertion_Policy as configuration pragmas either in
-   --  a configuration pragma file, or at the start of the current unit.
+   --  and assertion aspects and pragmas, to determine if Check pragmas
+   --  (or corresponding assertion aspects or pragmas) are currently active
+   --  as determined by the presence of -gnata on the command line (which
+   --  sets the default), and the appearance of pragmas Check_Policy and
+   --  Assertion_Policy as configuration pragmas either in a configuration
+   --  pragma file, or at the start of the current unit, or locally given
+   --  Check_Policy and Assertion_Policy pragmas that are currently active.
    --  True is returned if the specified check is enabled.
+   --
+   --  This function knows about all relevant synonyms (e.g. Precondition or
+   --  Pre can be used to refer to the Pre aspect or Precondition pragma, and
+   --  Predicate refers to both static and dynamic predicates, and Assertion
+   --  applies to all assertion aspects and pragmas).
+   --
+   --  Note: for assertion kinds Pre'Class, Post'Class, Type_Invariant'Class,
+   --  the name passed is Name_uPre, Name_uPost, Name_uType_Invariant, which
+   --  corresponds to _Pre, _Post, _Type_Invariant, which are special names
+   --  used in identifiers to represent these attribute references.
 
+   procedure Check_Applicable_Policy (N : Node_Id);
+   --  N is either an N_Aspect or an N_Pragma node. There are two cases. If
+   --  the name of the aspect or pragma is not one of those recognized as a
+   --  assertion kind by an Assertion_Kind pragma, then the call has no effect.
+   --  Note that in the case of a pragma derived from an aspect, the name
+   --  we use for the purpose of this procedure is the aspect name, which may
+   --  be different from the pragma name (e.g. Precondition for Pre aspect).
+   --  In addition, 'Class aspects are recognized (and the corresponding
+   --  special names used in the processing.
+   --
+   --  If the name is valid assertion_Kind name, then the Check_Policy pragma
+   --  chain is checked for a matching entry (or for an Assertion entry which
+   --  matches all possibilities). If a matching entry is found then the policy
+   --  is checked. If it is Off, Ignore, or Disable, then the Is_Ignored flag
+   --  is set in the aspect or pragma node. Additionally for policy Disable,
+   --  the Is_Disabled flag is set.
+   --
+   --  If no matching Check_Policy pragma is found then the effect depends on
+   --  whether -gnata was used, if so, then the call has no effect, otherwise
+   --  Is_Ignored (but not Is_Disabled) is set True.
+
    function Delay_Config_Pragma_Analyze (N : Node_Id) return Boolean;
    --  N is a pragma appearing in a configuration pragma file. Most such
    --  pragmas are analyzed when the file is read, before parsing and analyzing
Index: par-ch2.adb
===================================================================
--- par-ch2.adb	(revision 197899)
+++ par-ch2.adb	(working copy)
@@ -40,6 +40,12 @@ 
    --  the scanned association has an identifier (this is used to check the
    --  rule that no associations without identifiers can follow an association
    --  which has an identifier). The result is returned in Association.
+   --
+   --  Note: We allow attribute forms Pre'Class, Post'Class, Invariant'Class,
+   --  Type_Invariant'Class in place of a pragma argument identifier. Rather
+   --  than handle this case specially, we replace such references with
+   --  one of the special internal identifiers _Pre, _Post, _Invariant, or
+   --  _Type_Invariant, and this procedure is where this replacement occurs.
 
    ---------------------
    -- 2.3  Identifier --
@@ -448,6 +454,24 @@ 
    --    [pragma_argument_IDENTIFIER =>] NAME
    --  | [pragma_argument_IDENTIFIER =>] EXPRESSION
 
+   --  In Ada 2012, there are two more possibilities:
+
+   --  PRAGMA_ARGUMENT_ASSOCIATION ::=
+   --    [pragma_argument_ASPECT_MARK =>] NAME
+   --  | [pragma_argument_ASPECT_MARK =>] EXPRESSION
+
+   --  where the interesting allowed cases (which do not fit the syntax of the
+   --  first alternative above are
+
+   --  ASPECT_MARK ::=
+   --    Pre'Class | Post'Class | Invariant'Class | Type_Invariant'Class
+
+   --  We allow this special usage in all Ada modes, but it would be a pain to
+   --  allow these aspects to pervade the pragma syntax, and the representation
+   --  of pragma nodes internally. So what we do is to replace these
+   --  ASPECT_MARK forms with identifiers whose name is one of the special
+   --  internal names _Pre, _Post, _Invariant, or _Type_Invariant.
+
    --  Error recovery: cannot raise Error_Resync
 
    procedure Scan_Pragma_Argument_Association
@@ -461,6 +485,7 @@ 
    begin
       Association := New_Node (N_Pragma_Argument_Association, Token_Ptr);
       Set_Chars (Association, No_Name);
+      Id_Present := False;
 
       --  Argument starts with identifier
 
@@ -470,22 +495,69 @@ 
          Scan; -- past Identifier
 
          if Token = Tok_Arrow then
-            Identifier_Seen := True;
             Scan; -- past arrow
-            Set_Chars (Association, Chars (Identifier_Node));
             Id_Present := True;
 
-         --  Case of argument with no identifier
+         --  Case of one of the special aspect forms
 
+         elsif Token = Tok_Apostrophe then
+            Scan; -- past apostrophe
+
+            --  We have apostrophe, so check for identifier'Class
+
+            if Token /= Tok_Identifier or else Token_Name /= Name_Class then
+               null;
+
+            --  We have identifier'Class, check for arrow
+
+            else
+               Scan; -- Past Class
+
+               if Token /= Tok_Arrow then
+                  null;
+
+               --  Here we have scanned identifier'Class =>
+
+               else
+                  Id_Present := True;
+                  Scan; -- past arrow
+
+                  case Chars (Identifier_Node) is
+                     when Name_Pre =>
+                        Set_Chars (Identifier_Node, Name_uPre);
+
+                     when Name_Post =>
+                        Set_Chars (Identifier_Node, Name_uPost);
+
+                     when Name_Type_Invariant =>
+                        Set_Chars (Identifier_Node, Name_uType_Invariant);
+
+                     when Name_Invariant =>
+                        Set_Chars (Identifier_Node, Name_uInvariant);
+
+                     --  If it is X'Class => for some invalid X, we will give
+                     --  an error, and forget that 'Class was present, which
+                     --  will give better error recovery. We could do a spell
+                     --  check here, but it seems too much work.
+
+                     when others =>
+                        Error_Msg_SC ("invalid aspect id for pragma");
+                  end case;
+               end if;
+            end if;
+         end if;
+
+         --  Identifier was present
+
+         if Id_Present then
+            Set_Chars (Association, Chars (Identifier_Node));
+            Identifier_Seen := True;
+
+         --  Identifier not present after all
+
          else
             Restore_Scan_State (Scan_State); -- to Identifier
-            Id_Present := False;
          end if;
-
-      --  Argument does not start with identifier
-
-      else
-         Id_Present := False;
       end if;
 
       --  Diagnose error of "positional" argument for pragma appearing after
Index: sem_attr.adb
===================================================================
--- sem_attr.adb	(revision 197914)
+++ sem_attr.adb	(working copy)
@@ -4345,11 +4345,10 @@ 
             end if;
          end if;
 
-         --  Either the attribute reference is generated for a Requires
-         --  clause, in which case no expressions follow, or it is a
-         --  primary. In that case, if expressions follow, the attribute
-         --  reference is an indexable object, so rewrite the node
-         --  accordingly.
+         --  If the attribute reference is generated for a Requires clause,
+         --  then no expressions follow. Otherwise it is a primary, in which
+         --  case, if expressions follow, the attribute reference must be
+         --  an indexable object, so rewrite the node accordingly.
 
          if Present (E1) then
             Rewrite (N,
Index: gnat1drv.adb
===================================================================
--- gnat1drv.adb	(revision 197906)
+++ gnat1drv.adb	(working copy)
@@ -240,11 +240,9 @@ 
 
          Generate_SCIL := True;
 
-         --  Enable assertions and debug pragmas, since they give CodePeer
-         --  valuable extra information.
+         --  Enable assertions, since they give CodePeer valuable extra info
 
          Assertions_Enabled    := True;
-         Debug_Pragmas_Enabled := True;
 
          --  Disable all simple value propagation. This is an optimization
          --  which is valuable for code optimization, and also for generation
@@ -401,11 +399,10 @@ 
 
          Use_Expression_With_Actions := False;
 
-         --  Enable assertions and debug pragmas, since they give valuable
-         --  extra information for formal verification.
+         --  Enable assertions, since they give valuable extra information for
+         --  formal verification.
 
-         Assertions_Enabled    := True;
-         Debug_Pragmas_Enabled := True;
+         Assertions_Enabled := True;
 
          --  Turn off style check options since we are not interested in any
          --  front-end warnings when we are getting Alfa output.
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 197909)
+++ sem_ch6.adb	(working copy)
@@ -490,8 +490,6 @@ 
       Func_Nam : constant Node_Id := Name (N);
       Actual   : Node_Id;
 
-   --  Start of processing for Analyze_Function_Call
-
    begin
       Analyze (Func_Nam);
 
@@ -7217,10 +7215,9 @@ 
          Prag := Spec_CTC_List (Contract (Spec));
          loop
             if Pragma_Name (Prag) = Name_Contract_Cases then
+               Aggr :=
+                 Expression (First (Pragma_Argument_Associations (Prag)));
 
-               Aggr := Expression (First
-                         (Pragma_Argument_Associations (Prag)));
-
                Post_Case := First (Component_Associations (Aggr));
                while Present (Post_Case) loop
                   Conseq := Expression (Post_Case);
@@ -11885,6 +11882,12 @@ 
          Map : Elist_Id;
          CP  : Node_Id;
 
+         Ename : Name_Id;
+         --  Effective name of pragma (maybe Pre/Post rather than Precondition/
+         --  Postcodition if the pragma came from a Pre/Post aspect). We need
+         --  the name right when we generate the Check pragma, since we want
+         --  the right set of check policies to apply.
+
       begin
          --  Prepare map if this is the case where we have to map entities of
          --  arguments in the overridden subprogram to corresponding entities
@@ -11936,11 +11939,19 @@ 
             return CP;
          end if;
 
+         --  Get effective name of aspect
+
+         if Present (Corresponding_Aspect (Prag)) then
+            Ename := Chars (Identifier (Corresponding_Aspect (Prag)));
+         else
+            Ename := Nam;
+         end if;
+
          --  Change copy of pragma into corresponding pragma Check
 
          Prepend_To (Pragma_Argument_Associations (CP),
            Make_Pragma_Argument_Association (Sloc (Prag),
-             Expression => Make_Identifier (Loc, Nam)));
+             Expression => Make_Identifier (Loc, Ename)));
          Set_Pragma_Identifier (CP, Make_Identifier (Sloc (Prag), Name_Check));
 
          --  If this is inherited case and the current message starts with
@@ -12249,11 +12260,12 @@ 
          Prag := First (Declarations (N));
          while Present (Prag) loop
             if Nkind (Prag) = N_Pragma then
+               Check_Applicable_Policy (Prag);
 
                --  If pragma, capture if postconditions enabled, else ignore
 
                if Pragma_Name (Prag) = Name_Postcondition
-                 and then Check_Enabled (Name_Postcondition)
+                 and then not Is_Ignored (Prag)
                then
                   if Plist = No_List then
                      Plist := Empty_List;
Index: opt.adb
===================================================================
--- opt.adb	(revision 197899)
+++ opt.adb	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -59,8 +59,6 @@ 
       Assume_No_Invalid_Values_Config       := Assume_No_Invalid_Values;
       Check_Float_Overflow_Config           := Check_Float_Overflow;
       Check_Policy_List_Config              := Check_Policy_List;
-      Debug_Pragmas_Disabled_Config         := Debug_Pragmas_Disabled;
-      Debug_Pragmas_Enabled_Config          := Debug_Pragmas_Enabled;
       Default_Pool_Config                   := Default_Pool;
       Dynamic_Elaboration_Checks_Config     := Dynamic_Elaboration_Checks;
       Exception_Locations_Suppressed_Config := Exception_Locations_Suppressed;
@@ -94,8 +92,6 @@ 
       Assume_No_Invalid_Values       := Save.Assume_No_Invalid_Values;
       Check_Float_Overflow           := Save.Check_Float_Overflow;
       Check_Policy_List              := Save.Check_Policy_List;
-      Debug_Pragmas_Disabled         := Save.Debug_Pragmas_Disabled;
-      Debug_Pragmas_Enabled          := Save.Debug_Pragmas_Enabled;
       Default_Pool                   := Save.Default_Pool;
       Dynamic_Elaboration_Checks     := Save.Dynamic_Elaboration_Checks;
       Exception_Locations_Suppressed := Save.Exception_Locations_Suppressed;
@@ -131,8 +127,6 @@ 
       Save.Assume_No_Invalid_Values       := Assume_No_Invalid_Values;
       Save.Check_Float_Overflow           := Check_Float_Overflow;
       Save.Check_Policy_List              := Check_Policy_List;
-      Save.Debug_Pragmas_Disabled         := Debug_Pragmas_Disabled;
-      Save.Debug_Pragmas_Enabled          := Debug_Pragmas_Enabled;
       Save.Default_Pool                   := Default_Pool;
       Save.Dynamic_Elaboration_Checks     := Dynamic_Elaboration_Checks;
       Save.Exception_Locations_Suppressed := Exception_Locations_Suppressed;
@@ -183,14 +177,10 @@ 
          if Main_Unit then
             Assertions_Enabled       := Assertions_Enabled_Config;
             Assume_No_Invalid_Values := Assume_No_Invalid_Values_Config;
-            Debug_Pragmas_Disabled   := Debug_Pragmas_Disabled_Config;
-            Debug_Pragmas_Enabled    := Debug_Pragmas_Enabled_Config;
             Check_Policy_List        := Check_Policy_List_Config;
          else
             Assertions_Enabled       := False;
             Assume_No_Invalid_Values := False;
-            Debug_Pragmas_Disabled   := False;
-            Debug_Pragmas_Enabled    := False;
             Check_Policy_List        := Empty;
          end if;
 
@@ -203,8 +193,6 @@ 
          Assume_No_Invalid_Values    := Assume_No_Invalid_Values_Config;
          Check_Float_Overflow        := Check_Float_Overflow_Config;
          Check_Policy_List           := Check_Policy_List_Config;
-         Debug_Pragmas_Disabled      := Debug_Pragmas_Disabled_Config;
-         Debug_Pragmas_Enabled       := Debug_Pragmas_Enabled_Config;
          Dynamic_Elaboration_Checks  := Dynamic_Elaboration_Checks_Config;
          Extensions_Allowed          := Extensions_Allowed_Config;
          External_Name_Exp_Casing    := External_Name_Exp_Casing_Config;
@@ -261,8 +249,6 @@ 
       Tree_Read_Bool (Assertions_Enabled);
       Tree_Read_Bool (Check_Float_Overflow);
       Tree_Read_Int  (Int (Check_Policy_List));
-      Tree_Read_Bool (Debug_Pragmas_Disabled);
-      Tree_Read_Bool (Debug_Pragmas_Enabled);
       Tree_Read_Int  (Int (Default_Pool));
       Tree_Read_Bool (Full_List);
 
@@ -328,8 +314,6 @@ 
       Tree_Write_Bool (Assertions_Enabled);
       Tree_Write_Bool (Check_Float_Overflow);
       Tree_Write_Int  (Int (Check_Policy_List));
-      Tree_Write_Bool (Debug_Pragmas_Disabled);
-      Tree_Write_Bool (Debug_Pragmas_Enabled);
       Tree_Write_Int  (Int (Default_Pool));
       Tree_Write_Bool (Full_List);
       Tree_Write_Int  (Int (Version_String'Length));
Index: opt.ads
===================================================================
--- opt.ads	(revision 197904)
+++ opt.ads	(working copy)
@@ -341,7 +341,7 @@ 
    --  Modified by use of -gnatwu/U.
 
    CodePeer_Mode : Boolean := False;
-   --  GNAT, GNATBIND
+   --  GNAT, GNATBIND, GPRBUILD
    --  Enable full CodePeer mode (SCIL generation, disable switches that
    --  interact badly with it, etc...).
 
@@ -388,14 +388,6 @@ 
    --  Set to True (-C switch) to indicate that the compiler will be invoked
    --  with a mapping file (-gnatem compiler switch).
 
-   Debug_Pragmas_Enabled : Boolean := False;
-   --  GNAT
-   --  Enable debug statements from pragma Debug
-
-   Debug_Pragmas_Disabled : Boolean := False;
-   --  GNAT
-   --  Debug pragmas completely disabled (no semantic checking)
-
    subtype Debug_Level_Value is Nat range 0 .. 3;
    Debugger_Level : Debug_Level_Value := 0;
    --  GNATBIND
@@ -1785,17 +1777,6 @@ 
    --  terminated by Empty. The order is most recently processed first. This
    --  list includes only those pragmas in configuration pragma files.
 
-   Debug_Pragmas_Disabled_Config : Boolean;
-   --  GNAT
-   --  This is the value of the configuration switch for debug pragmas disabled
-   --  mode, as possibly set by use of the configuration pragma Debug_Policy.
-
-   Debug_Pragmas_Enabled_Config : Boolean;
-   --  GNAT
-   --  This is the value of the configuration switch for debug pragmas enabled
-   --  mode, as possibly set by the command line switch -gnata and possibly
-   --  modified by the use of the configuration pragma Debug_Policy.
-
    Default_Pool_Config : Node_Id := Empty;
    --  GNAT
    --  Same as Default_Pool above, except this is only for Default_Storage_Pool
@@ -2042,8 +2023,6 @@ 
       Assume_No_Invalid_Values       : Boolean;
       Check_Float_Overflow           : Boolean;
       Check_Policy_List              : Node_Id;
-      Debug_Pragmas_Disabled         : Boolean;
-      Debug_Pragmas_Enabled          : Boolean;
       Default_Pool                   : Node_Id;
       Dynamic_Elaboration_Checks     : Boolean;
       Exception_Locations_Suppressed : Boolean;
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 197911)
+++ sem_ch13.adb	(working copy)
@@ -51,6 +51,7 @@ 
 with Sem_Dim;  use Sem_Dim;
 with Sem_Disp; use Sem_Disp;
 with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
 with Sem_Res;  use Sem_Res;
 with Sem_Type; use Sem_Type;
 with Sem_Util; use Sem_Util;
@@ -947,11 +948,11 @@ 
       --  Some special cases don't require delay analysis, thus the aspect is
       --  analyzed right now.
 
-      --  Note that there is a special handling for
-      --  Pre/Post/Test_Case/Contract_Case aspects. In this case, we do not
-      --  have to worry about delay issues, since the pragmas themselves deal
-      --  with delay of visibility for the expression analysis. Thus, we just
-      --  insert the pragma after the node N.
+      --  Note that there is a special handling for Pre, Post, Test_Case,
+      --  Contract_Case aspects. In these cases, we do not have to worry
+      --  about delay issues, since the pragmas themselves deal with delay
+      --  of visibility for the expression analysis. Thus, we just insert
+      --  the pragma after the node N.
 
    begin
       pragma Assert (Present (L));
@@ -1007,7 +1008,7 @@ 
 
                   if No (A) then
                      Error_Msg_N
-                       ("Missing Import/Export for Link/External name",
+                       ("missing Import/Export for Link/External name",
                          Aspect);
                   end if;
                end;
@@ -1021,7 +1022,7 @@ 
             begin
                if not Is_Type (E) or else not Has_Discriminants (E) then
                   Error_Msg_N
-                    ("Aspect must apply to a type with discriminants", N);
+                    ("aspect must apply to a type with discriminants", N);
 
                else
                   declare
@@ -1057,6 +1058,15 @@ 
                goto Continue;
             end if;
 
+            --  Skip looking at aspect if it is totally disabled. Just mark
+            --  it as such for later reference in the tree.
+
+            Check_Applicable_Policy (Aspect);
+
+            if Is_Disabled (Aspect) then
+               goto Continue;
+            end if;
+
             --  Set the source location of expression, used in the case of
             --  a failed precondition/postcondition or invariant. Note that
             --  the source location of the expression is not usually the best
@@ -1080,7 +1090,7 @@ 
 
             Check_Restriction_No_Specification_Of_Aspect (Aspect);
 
-            --  Analyze this aspect
+            --  Analyze this aspect (actual analysis is delayed till later)
 
             Set_Analyzed (Aspect);
             Set_Entity (Aspect, E);
@@ -1202,7 +1212,7 @@ 
                       Chars      => Chars (Id),
                       Expression => Relocate_Node (Expr));
 
-               --  Case 2: Aspects cooresponding to pragmas
+               --  Case 2: Aspects corresponding to pragmas
 
                --  Case 2a: Aspects corresponding to pragmas with two
                --  arguments, where the first argument is a local name
@@ -1212,8 +1222,6 @@ 
                when Aspect_Suppress   |
                     Aspect_Unsuppress =>
 
-                  --  Construct the pragma
-
                   Aitem :=
                     Make_Pragma (Loc,
                       Pragma_Argument_Associations => New_List (
@@ -1264,7 +1272,8 @@ 
                     Aspect_Static_Predicate  =>
 
                   --  Construct the pragma (always a pragma Predicate, with
-                  --  flags recording whether it is static/dynamic).
+                  --  flags recording whether it is static/dynamic). We also
+                  --  set flags recording this in the type itself.
 
                   Aitem :=
                     Make_Pragma (Loc,
@@ -1277,16 +1286,33 @@ 
                       Pragma_Identifier            =>
                         Make_Identifier (Sloc (Id), Name_Predicate));
 
+                  --  Mark type has predicates, and remember what kind of
+                  --  aspect lead to this predicate (we need this to access
+                  --  the right set of check policies later on).
+
+                  Set_Has_Predicates (E);
+
+                  if A_Id = Aspect_Dynamic_Predicate then
+                     Set_Has_Dynamic_Predicate_Aspect (E);
+                  elsif A_Id = Aspect_Static_Predicate then
+                     Set_Has_Static_Predicate_Aspect (E);
+                  end if;
+
                   --  If the type is private, indicate that its completion
                   --  has a freeze node, because that is the one that will be
                   --  visible at freeze time.
 
-                  Set_Has_Predicates (E);
-
                   if Is_Private_Type (E)
                     and then Present (Full_View (E))
                   then
                      Set_Has_Predicates (Full_View (E));
+
+                     if A_Id = Aspect_Dynamic_Predicate then
+                        Set_Has_Dynamic_Predicate_Aspect (Full_View (E));
+                     elsif A_Id = Aspect_Static_Predicate then
+                        Set_Has_Static_Predicate_Aspect (Full_View (E));
+                     end if;
+
                      Set_Has_Delayed_Aspects (Full_View (E));
                      Ensure_Freeze_Node (Full_View (E));
                   end if;
@@ -1379,6 +1405,7 @@ 
                when Aspect_CPU                |
                     Aspect_Interrupt_Priority |
                     Aspect_Priority           =>
+
                   if Nkind (N) = N_Subprogram_Body then
                      Aitem :=
                        Make_Pragma (Loc,
@@ -1396,9 +1423,6 @@ 
                   end if;
 
                when Aspect_Warnings =>
-
-                  --  Construct the pragma
-
                   Aitem :=
                     Make_Pragma (Loc,
                       Pragma_Argument_Associations => New_List (
@@ -1429,8 +1453,6 @@ 
                   --  an invariant must apply to a private type, or appear in
                   --  the private part of a spec and apply to a completion.
 
-                  --  Construct the pragma
-
                   Aitem :=
                     Make_Pragma (Loc,
                       Pragma_Argument_Associations => New_List (
@@ -1440,7 +1462,7 @@ 
                           Expression => Relocate_Node (Expr))),
                       Class_Present                => Class_Present (Aspect),
                       Pragma_Identifier            =>
-                        Make_Identifier (Sloc (Id), Name_Invariant));
+                                 Make_Identifier (Sloc (Id), Name_Invariant));
 
                   --  Add message unless exception messages are suppressed
 
@@ -1572,6 +1594,7 @@ 
                   goto Continue;
 
                --  Case 4: Special handling for aspects
+
                --  Pre/Post/Test_Case/Contract_Case whose corresponding pragmas
                --  take care of the delay.
 
@@ -5716,7 +5739,7 @@ 
       --  predicate being considered dynamic even if it looks static
 
       Static_Predicate_Present : Node_Id := Empty;
-      --  Set to N_Pragma node for a static predicate if one is encountered.
+      --  Set to N_Pragma node for a static predicate if one is encountered
 
       --------------
       -- Add_Call --
Index: tree_io.ads
===================================================================
--- tree_io.ads	(revision 197899)
+++ tree_io.ads	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -47,7 +47,7 @@ 
    Tree_Format_Error : exception;
    --  Raised if a format error is detected in the input file
 
-   ASIS_Version_Number : constant := 30;
+   ASIS_Version_Number : constant := 31;
    --  ASIS Version. This is used to check for consistency between the compiler
    --  used to generate trees and an ASIS application that is reading the
    --  trees. It must be incremented whenever a change is made to the tree
@@ -59,6 +59,7 @@ 
    --  29  Changes in Sem_Ch3 (tree copying in case of discriminant constraint
    --      for concurrent types).
    --  30  Add Check_Float_Overflow boolean to tree file
+   --  31  Remove read/write of Debug_Pragmas_Disabled/Debug_Pragmas_Enabled
 
    procedure Tree_Read_Initialize (Desc : File_Descriptor);
    --  Called to initialize reading of a tree file. This call must be made
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 197909)
+++ snames.ads-tmpl	(working copy)
@@ -165,9 +165,12 @@ 
    Name_uFinalizer                     : constant Name_Id := N + $;
    Name_uIdepth                        : constant Name_Id := N + $;
    Name_uInit                          : constant Name_Id := N + $;
+   Name_uInvariant                     : constant Name_Id := N + $;
    Name_uMaster                        : constant Name_Id := N + $;
    Name_uObject                        : constant Name_Id := N + $;
+   Name_uPost                          : constant Name_Id := N + $;
    Name_uPostconditions                : constant Name_Id := N + $;
+   Name_uPre                           : constant Name_Id := N + $;
    Name_uPriority                      : constant Name_Id := N + $;
    Name_uProcess_ATSD                  : constant Name_Id := N + $;
    Name_uRelative_Deadline             : constant Name_Id := N + $;
@@ -182,6 +185,7 @@ 
    Name_uTask_Info                     : constant Name_Id := N + $;
    Name_uTask_Name                     : constant Name_Id := N + $;
    Name_uTrace_Sp                      : constant Name_Id := N + $;
+   Name_uType_Invariant                : constant Name_Id := N + $;
 
    --  Names of predefined primitives used in the expansion of dispatching
    --  requeue and select statements, Abort, 'Callable and 'Terminated.