OSDN Git Service

* exp_disp.adb (Expand_Dispatching_Call): Propagate the convention on
[pf3gnuchains/gcc-fork.git] / gcc / ada / sem_prag.adb
index 4d6a55c..d7d5229 100644 (file)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2011, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2012, 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- --
@@ -29,6 +29,7 @@
 --  to complete the syntax checks. Certain pragmas are handled partially or
 --  completely by the parser (see Par.Prag for further details).
 
+with Aspects;  use Aspects;
 with Atree;    use Atree;
 with Casing;   use Casing;
 with Checks;   use Checks;
@@ -37,8 +38,9 @@ with Debug;    use Debug;
 with Einfo;    use Einfo;
 with Elists;   use Elists;
 with Errout;   use Errout;
-with Exp_Ch7;  use Exp_Ch7;
 with Exp_Dist; use Exp_Dist;
+with Exp_Util; use Exp_Util;
+with Freeze;   use Freeze;
 with Lib;      use Lib;
 with Lib.Writ; use Lib.Writ;
 with Lib.Xref; use Lib.Xref;
@@ -179,6 +181,11 @@ package body Sem_Prag is
    --  original one, following the renaming chain) is returned. Otherwise the
    --  entity is returned unchanged. Should be in Einfo???
 
+   procedure Preanalyze_TC_Args (N, Arg_Req, Arg_Ens : Node_Id);
+   --  Preanalyze the boolean expressions in the Requires and Ensures arguments
+   --  of a Test_Case pragma if present (possibly Empty). We treat these as
+   --  spec expressions (i.e. similar to a default expression).
+
    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
@@ -253,11 +260,129 @@ package body Sem_Prag is
       --  Preanalyze the boolean expression, we treat this as a spec expression
       --  (i.e. similar to a default expression).
 
-      pragma Assert (In_Pre_Post_Expression = False);
-      In_Pre_Post_Expression := True;
-      Preanalyze_Spec_Expression
-        (Get_Pragma_Arg (Arg1), Standard_Boolean);
-      In_Pre_Post_Expression := False;
+      Preanalyze_Spec_Expression (Get_Pragma_Arg (Arg1), Standard_Boolean);
+
+      --  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
+         Preanalyze_Spec_Expression
+           (Expression (Corresponding_Aspect (N)), Standard_Boolean);
+      end if;
+
+      --  For a class-wide condition, a reference to a controlling formal must
+      --  be interpreted as having the class-wide type (or an access to such)
+      --  so that the inherited condition can be properly applied to any
+      --  overriding operation (see ARM12 6.6.1 (7)).
+
+      if Class_Present (N) then
+         Class_Wide_Condition : declare
+            T   : constant Entity_Id := Find_Dispatching_Type (S);
+
+            ACW : Entity_Id := Empty;
+            --  Access to T'class, created if there is a controlling formal
+            --  that is an access parameter.
+
+            function Get_ACW return Entity_Id;
+            --  If the expression has a reference to an controlling access
+            --  parameter, create an access to T'class for the necessary
+            --  conversions if one does not exist.
+
+            function Process (N : Node_Id) return Traverse_Result;
+            --  ARM 6.1.1: Within the expression for a Pre'Class or Post'Class
+            --  aspect for a primitive subprogram of a tagged type T, a name
+            --  that denotes a formal parameter of type T is interpreted as
+            --  having type T'Class. Similarly, a name that denotes a formal
+            --  accessparameter of type access-to-T is interpreted as having
+            --  type access-to-T'Class. This ensures the expression is well-
+            --  defined for a primitive subprogram of a type descended from T.
+
+            -------------
+            -- Get_ACW --
+            -------------
+
+            function Get_ACW return Entity_Id is
+               Loc  : constant Source_Ptr := Sloc (N);
+               Decl : Node_Id;
+
+            begin
+               if No (ACW) then
+                  Decl := Make_Full_Type_Declaration (Loc,
+                    Defining_Identifier => Make_Temporary (Loc, 'T'),
+                    Type_Definition =>
+                       Make_Access_To_Object_Definition (Loc,
+                       Subtype_Indication =>
+                         New_Occurrence_Of (Class_Wide_Type (T), Loc),
+                       All_Present => True));
+
+                  Insert_Before (Unit_Declaration_Node (S), Decl);
+                  Analyze (Decl);
+                  ACW := Defining_Identifier (Decl);
+                  Freeze_Before (Unit_Declaration_Node (S), ACW);
+               end if;
+
+               return ACW;
+            end Get_ACW;
+
+            -------------
+            -- Process --
+            -------------
+
+            function Process (N : Node_Id) return Traverse_Result is
+               Loc : constant Source_Ptr := Sloc (N);
+               Typ : Entity_Id;
+
+            begin
+               if Is_Entity_Name (N)
+                 and then Is_Formal (Entity (N))
+                 and then Nkind (Parent (N)) /= N_Type_Conversion
+               then
+                  if Etype (Entity (N)) = T then
+                     Typ := Class_Wide_Type (T);
+
+                  elsif Is_Access_Type (Etype (Entity (N)))
+                    and then Designated_Type (Etype (Entity (N))) = T
+                  then
+                     Typ := Get_ACW;
+                  else
+                     Typ := Empty;
+                  end if;
+
+                  if Present (Typ) then
+                     Rewrite (N,
+                       Make_Type_Conversion (Loc,
+                         Subtype_Mark =>
+                           New_Occurrence_Of (Typ, Loc),
+                         Expression  => New_Occurrence_Of (Entity (N), Loc)));
+                     Set_Etype (N, Typ);
+                  end if;
+               end if;
+
+               return OK;
+            end Process;
+
+            procedure Replace_Type is new Traverse_Proc (Process);
+
+         --  Start of processing for Class_Wide_Condition
+
+         begin
+            if not Present (T) then
+               Error_Msg_Name_1 :=
+                 Chars (Identifier (Corresponding_Aspect (N)));
+
+               Error_Msg_Name_2 := Name_Class;
+
+               Error_Msg_N
+                 ("aspect `%''%` can only be specified for a primitive " &
+                  "operation of a tagged type",
+                  Corresponding_Aspect (N));
+            end if;
+
+            Replace_Type (Get_Pragma_Arg (Arg1));
+         end Class_Wide_Condition;
+      end if;
 
       --  Remove the subprogram from the scope stack now that the pre-analysis
       --  of the precondition/postcondition is done.
@@ -271,9 +396,13 @@ package body Sem_Prag is
 
    procedure Analyze_Pragma (N : Node_Id) is
       Loc     : constant Source_Ptr := Sloc (N);
-      Pname   : constant Name_Id    := Pragma_Name (N);
       Prag_Id : Pragma_Id;
 
+      Pname : Name_Id;
+      --  Name of the source pragma, or name of the corresponding aspect for
+      --  pragmas which originate in a source aspect. In the latter case, the
+      --  name may be different from the pragma name.
+
       Pragma_Exit : exception;
       --  This exception is used to exit pragma processing completely. It is
       --  used when an error is detected, and no further processing is
@@ -350,12 +479,21 @@ package body Sem_Prag is
       --  Check the specified argument Arg to make sure that it is a valid
       --  locking policy name. If not give error and raise Pragma_Exit.
 
-      procedure Check_Arg_Is_One_Of (Arg : Node_Id; N1, N2 : Name_Id);
-      procedure Check_Arg_Is_One_Of (Arg : Node_Id; N1, N2, N3 : Name_Id);
-      procedure Check_Arg_Is_One_Of (Arg : Node_Id; N1, N2, N3, N4 : Name_Id);
+      procedure Check_Arg_Is_One_Of
+        (Arg                : Node_Id;
+         N1, N2             : Name_Id);
+      procedure Check_Arg_Is_One_Of
+        (Arg                : Node_Id;
+         N1, N2, N3         : Name_Id);
+      procedure Check_Arg_Is_One_Of
+        (Arg                : Node_Id;
+         N1, N2, N3, N4     : Name_Id);
+      procedure Check_Arg_Is_One_Of
+        (Arg                : Node_Id;
+         N1, N2, N3, N4, N5 : Name_Id);
       --  Check the specified argument Arg to make sure that it is an
-      --  identifier whose name matches either N1 or N2 (or N3 if present).
-      --  If not then give error and raise Pragma_Exit.
+      --  identifier whose name matches either N1 or N2 (or N3, N4, N5 if
+      --  present). If not then give error and raise Pragma_Exit.
 
       procedure Check_Arg_Is_Queuing_Policy (Arg : Node_Id);
       --  Check the specified argument Arg to make sure that it is a valid
@@ -406,10 +544,31 @@ package body Sem_Prag is
       --  This procedure checks for possible duplications if this is the export
       --  case, and if found, issues an appropriate error message.
 
+      procedure Check_Expr_Is_Static_Expression
+        (Expr : Node_Id;
+         Typ  : Entity_Id := Empty);
+      --  Check the specified expression Expr to make sure that it is a static
+      --  expression of the given type (i.e. it will be analyzed and resolved
+      --  using this type, which can be any valid argument to Resolve, e.g.
+      --  Any_Integer is OK). If not, given error and raise Pragma_Exit. If
+      --  Typ is left Empty, then any static expression is allowed.
+
       procedure Check_First_Subtype (Arg : Node_Id);
       --  Checks that Arg, whose expression is an entity name, references a
       --  first subtype.
 
+      procedure Check_Identifier (Arg : Node_Id; Id : Name_Id);
+      --  Checks that the given argument has an identifier, and if so, requires
+      --  it to match the given identifier name. If there is no identifier, or
+      --  a non-matching identifier, then an error message is given and
+      --  Pragma_Exit is raised.
+
+      procedure Check_Identifier_Is_One_Of (Arg : Node_Id; N1, N2 : Name_Id);
+      --  Checks that the given argument has an identifier, and if so, requires
+      --  it to match one of the given identifier names. If there is no
+      --  identifier, or a non-matching identifier, then an error message is
+      --  given and Pragma_Exit is raised.
+
       procedure Check_In_Main_Program;
       --  Common checks for pragmas that appear within a main program
       --  (Priority, Main_Storage, Time_Slice, Relative_Deadline, CPU).
@@ -439,12 +598,12 @@ package body Sem_Prag is
       procedure Check_Optional_Identifier (Arg : Node_Id; Id : Name_Id);
       --  Checks if the given argument has an identifier, and if so, requires
       --  it to match the given identifier name. If there is a non-matching
-      --  identifier, then an error message is given and Error_Pragmas raised.
+      --  identifier, then an error message is given and Pragma_Exit is raised.
 
       procedure Check_Optional_Identifier (Arg : Node_Id; Id : String);
       --  Checks if the given argument has an identifier, and if so, requires
       --  it to match the given identifier name. If there is a non-matching
-      --  identifier, then an error message is given and Error_Pragmas raised.
+      --  identifier, then an error message is given and Pragma_Exit is raised.
       --  In this version of the procedure, the identifier name is given as
       --  a string with lower case letters.
 
@@ -478,6 +637,16 @@ package body Sem_Prag is
       --  that the constraint is static as required by the restrictions for
       --  Unchecked_Union.
 
+      procedure Check_Test_Case;
+      --  Called to process a test-case pragma. The treatment is similar to the
+      --  one for pre- and postcondition in Check_Precondition_Postcondition,
+      --  except the placement rules for the test-case pragma are stricter.
+      --  This pragma may only occur after a subprogram spec declared directly
+      --  in a package spec unit. In this case, the pragma is chained to the
+      --  subprogram in question (using Spec_TC_List and Next_Pragma) and
+      --  analysis of the pragma is delayed till the end of the spec. In
+      --  all other cases, an error message for bad placement is given.
+
       procedure Check_Valid_Configuration_Pragma;
       --  Legality checks for placement of a configuration pragma
 
@@ -555,7 +724,7 @@ package body Sem_Prag is
 
       procedure Fix_Error (Msg : in out String);
       --  This is called prior to issuing an error message. Msg is a string
-      --  which typically contains the substring pragma. If the current pragma
+      --  that typically contains the substring "pragma". If the current pragma
       --  comes from an aspect, each such "pragma" substring is replaced with
       --  the characters "aspect", and if Error_Msg_Name_1 is Name_Precondition
       --  (resp Name_Postcondition) it is changed to Name_Pre (resp Name_Post).
@@ -616,6 +785,10 @@ package body Sem_Prag is
       --  convention value in the specified entity or entities. On return
       --  C is the convention, Ent is the referenced entity.
 
+      procedure Process_Disable_Enable_Atomic_Sync (Nam : Name_Id);
+      --  Common processing for Disable/Enable_Atomic_Synchronization. Nam is
+      --  Name_Suppress for Disable and Name_Unsuppress for Enable.
+
       procedure Process_Extended_Import_Export_Exception_Pragma
         (Arg_Internal : Node_Id;
          Arg_External : Node_Id;
@@ -923,6 +1096,7 @@ package body Sem_Prag is
                if Is_Compilation_Unit (Ent) then
                   declare
                      Decl : constant Node_Id := Unit_Declaration_Node (Ent);
+
                   begin
                      --  Case of pragma placed immediately after spec
 
@@ -1020,8 +1194,8 @@ package body Sem_Prag is
       end Check_Arg_Is_One_Of;
 
       procedure Check_Arg_Is_One_Of
-        (Arg            : Node_Id;
-         N1, N2, N3, N4 : Name_Id)
+        (Arg                : Node_Id;
+         N1, N2, N3, N4     : Name_Id)
       is
          Argx : constant Node_Id := Get_Pragma_Arg (Arg);
 
@@ -1036,6 +1210,25 @@ package body Sem_Prag is
             Error_Pragma_Arg ("invalid argument for pragma%", Argx);
          end if;
       end Check_Arg_Is_One_Of;
+
+      procedure Check_Arg_Is_One_Of
+        (Arg                : Node_Id;
+         N1, N2, N3, N4, N5 : Name_Id)
+      is
+         Argx : constant Node_Id := Get_Pragma_Arg (Arg);
+
+      begin
+         Check_Arg_Is_Identifier (Argx);
+
+         if Chars (Argx) /= N1
+           and then Chars (Argx) /= N2
+           and then Chars (Argx) /= N3
+           and then Chars (Argx) /= N4
+           and then Chars (Argx) /= N5
+         then
+            Error_Pragma_Arg ("invalid argument for pragma%", Argx);
+         end if;
+      end Check_Arg_Is_One_Of;
       ---------------------------------
       -- Check_Arg_Is_Queuing_Policy --
       ---------------------------------
@@ -1059,53 +1252,8 @@ package body Sem_Prag is
         (Arg : Node_Id;
          Typ : Entity_Id := Empty)
       is
-         Argx : constant Node_Id := Get_Pragma_Arg (Arg);
-
       begin
-         if Present (Typ) then
-            Analyze_And_Resolve (Argx, Typ);
-         else
-            Analyze_And_Resolve (Argx);
-         end if;
-
-         if Is_OK_Static_Expression (Argx) then
-            return;
-
-         elsif Etype (Argx) = Any_Type then
-            raise Pragma_Exit;
-
-         --  An interesting special case, if we have a string literal and we
-         --  are in Ada 83 mode, then we allow it even though it will not be
-         --  flagged as static. This allows the use of Ada 95 pragmas like
-         --  Import in Ada 83 mode. They will of course be flagged with
-         --  warnings as usual, but will not cause errors.
-
-         elsif Ada_Version = Ada_83
-           and then Nkind (Argx) = N_String_Literal
-         then
-            return;
-
-         --  Static expression that raises Constraint_Error. This has already
-         --  been flagged, so just exit from pragma processing.
-
-         elsif Is_Static_Expression (Argx) then
-            raise Pragma_Exit;
-
-         --  Finally, we have a real error
-
-         else
-            Error_Msg_Name_1 := Pname;
-
-            declare
-               Msg : String :=
-                       "argument for pragma% must be a static expression!";
-            begin
-               Fix_Error (Msg);
-               Flag_Non_Static_Expr (Msg, Argx);
-            end;
-
-            raise Pragma_Exit;
-         end if;
+         Check_Expr_Is_Static_Expression (Get_Pragma_Arg (Arg), Typ);
       end Check_Arg_Is_Static_Expression;
 
       ------------------------------------------
@@ -1201,34 +1349,6 @@ package body Sem_Prag is
                      Subtype_Indication (Component_Definition (Comp));
          Typ     : constant Entity_Id := Etype (Comp_Id);
 
-         function Inside_Generic_Body (Id : Entity_Id) return Boolean;
-         --  Determine whether entity Id appears inside a generic body.
-         --  Shouldn't this be in a more general place ???
-
-         -------------------------
-         -- Inside_Generic_Body --
-         -------------------------
-
-         function Inside_Generic_Body (Id : Entity_Id) return Boolean is
-            S : Entity_Id;
-
-         begin
-            S := Id;
-            while Present (S) and then S /= Standard_Standard loop
-               if Ekind (S) = E_Generic_Package
-                 and then In_Package_Body (S)
-               then
-                  return True;
-               end if;
-
-               S := Scope (S);
-            end loop;
-
-            return False;
-         end Inside_Generic_Body;
-
-      --  Start of processing for Check_Component
-
       begin
          --  Ada 2005 (AI-216): If a component subtype is subject to a per-
          --  object constraint, then the component type shall be an Unchecked_
@@ -1250,7 +1370,7 @@ package body Sem_Prag is
          --  the formal part of the generic unit.
 
          elsif Ada_Version >= Ada_2012
-           and then Inside_Generic_Body (UU_Typ)
+           and then In_Generic_Body (UU_Typ)
            and then In_Variant_Part
            and then Is_Private_Type (Typ)
            and then Is_Generic_Type (Typ)
@@ -1338,6 +1458,61 @@ package body Sem_Prag is
          end if;
       end Check_Duplicated_Export_Name;
 
+      -------------------------------------
+      -- Check_Expr_Is_Static_Expression --
+      -------------------------------------
+
+      procedure Check_Expr_Is_Static_Expression
+        (Expr : Node_Id;
+         Typ  : Entity_Id := Empty)
+      is
+      begin
+         if Present (Typ) then
+            Analyze_And_Resolve (Expr, Typ);
+         else
+            Analyze_And_Resolve (Expr);
+         end if;
+
+         if Is_OK_Static_Expression (Expr) then
+            return;
+
+         elsif Etype (Expr) = Any_Type then
+            raise Pragma_Exit;
+
+         --  An interesting special case, if we have a string literal and we
+         --  are in Ada 83 mode, then we allow it even though it will not be
+         --  flagged as static. This allows the use of Ada 95 pragmas like
+         --  Import in Ada 83 mode. They will of course be flagged with
+         --  warnings as usual, but will not cause errors.
+
+         elsif Ada_Version = Ada_83
+           and then Nkind (Expr) = N_String_Literal
+         then
+            return;
+
+         --  Static expression that raises Constraint_Error. This has already
+         --  been flagged, so just exit from pragma processing.
+
+         elsif Is_Static_Expression (Expr) then
+            raise Pragma_Exit;
+
+         --  Finally, we have a real error
+
+         else
+            Error_Msg_Name_1 := Pname;
+
+            declare
+               Msg : String :=
+                       "argument for pragma% must be a static expression!";
+            begin
+               Fix_Error (Msg);
+               Flag_Non_Static_Expr (Msg, Expr);
+            end;
+
+            raise Pragma_Exit;
+         end if;
+      end Check_Expr_Is_Static_Expression;
+
       -------------------------
       -- Check_First_Subtype --
       -------------------------
@@ -1364,6 +1539,48 @@ package body Sem_Prag is
          end if;
       end Check_First_Subtype;
 
+      ----------------------
+      -- Check_Identifier --
+      ----------------------
+
+      procedure Check_Identifier (Arg : Node_Id; Id : Name_Id) is
+      begin
+         if Present (Arg)
+           and then Nkind (Arg) = N_Pragma_Argument_Association
+         then
+            if Chars (Arg) = No_Name or else Chars (Arg) /= Id then
+               Error_Msg_Name_1 := Pname;
+               Error_Msg_Name_2 := Id;
+               Error_Msg_N ("pragma% argument expects identifier%", Arg);
+               raise Pragma_Exit;
+            end if;
+         end if;
+      end Check_Identifier;
+
+      --------------------------------
+      -- Check_Identifier_Is_One_Of --
+      --------------------------------
+
+      procedure Check_Identifier_Is_One_Of (Arg : Node_Id; N1, N2 : Name_Id) is
+      begin
+         if Present (Arg)
+           and then Nkind (Arg) = N_Pragma_Argument_Association
+         then
+            if Chars (Arg) = No_Name then
+               Error_Msg_Name_1 := Pname;
+               Error_Msg_N ("pragma% argument expects an identifier", Arg);
+               raise Pragma_Exit;
+
+            elsif Chars (Arg) /= N1
+              and then Chars (Arg) /= N2
+            then
+               Error_Msg_Name_1 := Pname;
+               Error_Msg_N ("invalid identifier for pragma% argument", Arg);
+               raise Pragma_Exit;
+            end if;
+         end if;
+      end Check_Identifier_Is_One_Of;
+
       ---------------------------
       -- Check_In_Main_Program --
       ---------------------------
@@ -1571,10 +1788,10 @@ package body Sem_Prag is
          PO : Node_Id;
 
          procedure Chain_PPC (PO : Node_Id);
-         --  If PO is a subprogram declaration node (or a generic subprogram
-         --  declaration node), then the precondition/postcondition applies
-         --  to this subprogram and the processing for the pragma is completed.
-         --  Otherwise the pragma is misplaced.
+         --  If PO is an entry or a [generic] subprogram declaration node, then
+         --  the precondition/postcondition applies to this subprogram and the
+         --  processing for the pragma is completed. Otherwise the pragma is
+         --  misplaced.
 
          ---------------
          -- Chain_PPC --
@@ -1615,6 +1832,7 @@ package body Sem_Prag is
                  ("aspect % requires ''Class for null procedure");
 
             elsif not Nkind_In (PO, N_Subprogram_Declaration,
+                                    N_Expression_Function,
                                     N_Generic_Subprogram_Declaration,
                                     N_Entry_Declaration)
             then
@@ -1637,7 +1855,7 @@ package body Sem_Prag is
 
             if Pragma_Name (N) = Name_Precondition then
                if not From_Aspect_Specification (N) then
-                  P := Spec_PPC_List (S);
+                  P := Spec_PPC_List (Contract (S));
                   while Present (P) loop
                      if Pragma_Name (P) = Name_Precondition
                        and then From_Aspect_Specification (P)
@@ -1666,7 +1884,7 @@ package body Sem_Prag is
 
                begin
                   for J in Inherited'Range loop
-                     P := Spec_PPC_List (Inherited (J));
+                     P := Spec_PPC_List (Contract (Inherited (J)));
                      while Present (P) loop
                         if Pragma_Name (P) = Name_Precondition
                           and then Class_Present (P)
@@ -1691,8 +1909,8 @@ package body Sem_Prag is
 
             --  Chain spec PPC pragma to list for subprogram
 
-            Set_Next_Pragma (N, Spec_PPC_List (S));
-            Set_Spec_PPC_List (S, N);
+            Set_Next_Pragma (N, Spec_PPC_List (Contract (S)));
+            Set_Spec_PPC_List (Contract (S), N);
 
             --  Return indicating spec case
 
@@ -1700,7 +1918,7 @@ package body Sem_Prag is
             return;
          end Chain_PPC;
 
-         --  Start of processing for Check_Precondition_Postcondition
+      --  Start of processing for Check_Precondition_Postcondition
 
       begin
          if not Is_List_Member (N) then
@@ -1716,10 +1934,9 @@ package body Sem_Prag is
               (Get_Pragma_Arg (Arg2), Standard_String);
          end if;
 
-         --  Record if pragma is enabled
+         --  Record if pragma is disabled
 
          if Check_Enabled (Pname) then
-            Set_Pragma_Enabled (N);
             Set_SCO_Pragma_Enabled (Loc);
          end if;
 
@@ -1766,6 +1983,12 @@ package body Sem_Prag is
                   Chain_PPC (PO);
                   return;
 
+               elsif Nkind (PO) = N_Subprogram_Declaration
+                 and then In_Instance
+               then
+                  Chain_PPC (PO);
+                  return;
+
                --  For all other cases of non source code, do nothing
 
                else
@@ -1793,6 +2016,16 @@ package body Sem_Prag is
 
                Preanalyze_Spec_Expression
                  (Get_Pragma_Arg (Arg1), Standard_Boolean);
+
+               --  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
+                  Preanalyze_Spec_Expression
+                    (Expression (Corresponding_Aspect (N)), Standard_Boolean);
+               end if;
             end if;
 
             In_Body := True;
@@ -1801,6 +2034,15 @@ package body Sem_Prag is
          --  See if it is in the pragmas after a library level subprogram
 
          elsif Nkind (Parent (N)) = N_Compilation_Unit_Aux then
+
+            --  In formal verification mode, analyze pragma expression for
+            --  correctness, as it is not expanded later.
+
+            if Alfa_Mode then
+               Analyze_PPC_In_Decl_Part
+                 (N, Defining_Entity (Unit (Parent (Parent (N)))));
+            end if;
+
             Chain_PPC (Unit (Parent (Parent (N))));
             return;
          end if;
@@ -1871,6 +2113,161 @@ package body Sem_Prag is
          end case;
       end Check_Static_Constraint;
 
+      ---------------------
+      -- Check_Test_Case --
+      ---------------------
+
+      procedure Check_Test_Case is
+         P  : Node_Id;
+         PO : Node_Id;
+
+         procedure Chain_TC (PO : Node_Id);
+         --  If PO is a [generic] subprogram declaration node, then the
+         --  test-case applies to this subprogram and the processing for the
+         --  pragma is completed. Otherwise the pragma is misplaced.
+
+         --------------
+         -- Chain_TC --
+         --------------
+
+         procedure Chain_TC (PO : Node_Id) is
+            S   : Entity_Id;
+
+         begin
+            if Nkind (PO) = N_Abstract_Subprogram_Declaration then
+               if From_Aspect_Specification (N) then
+                  Error_Pragma
+                    ("aspect% cannot be applied to abstract subprogram");
+               else
+                  Error_Pragma
+                    ("pragma% cannot be applied to abstract subprogram");
+               end if;
+
+            elsif Nkind (PO) = N_Entry_Declaration then
+               if From_Aspect_Specification (N) then
+                  Error_Pragma ("aspect% cannot be applied to entry");
+               else
+                  Error_Pragma ("pragma% cannot be applied to entry");
+               end if;
+
+            elsif not Nkind_In (PO, N_Subprogram_Declaration,
+                                    N_Generic_Subprogram_Declaration)
+            then
+               Pragma_Misplaced;
+            end if;
+
+            --  Here if we have [generic] subprogram declaration
+
+            S := Defining_Unit_Name (Specification (PO));
+
+            --  Note: we do not analyze the pragma at this point. Instead we
+            --  delay this analysis until the end of the declarative part in
+            --  which the pragma appears. This implements the required delay
+            --  in this analysis, allowing forward references. The analysis
+            --  happens at the end of Analyze_Declarations.
+
+            --  There should not be another test case with the same name
+            --  associated to this subprogram.
+
+            declare
+               Name : constant String_Id := Get_Name_From_Test_Case_Pragma (N);
+               TC   : Node_Id;
+
+            begin
+               TC := Spec_TC_List (Contract (S));
+               while Present (TC) loop
+
+                  if String_Equal
+                    (Name, Get_Name_From_Test_Case_Pragma (TC))
+                  then
+                     Error_Msg_Sloc := Sloc (TC);
+
+                     if From_Aspect_Specification (N) then
+                        Error_Pragma ("name for aspect% is already used#");
+                     else
+                        Error_Pragma ("name for pragma% is already used#");
+                     end if;
+                  end if;
+
+                  TC := Next_Pragma (TC);
+               end loop;
+            end;
+
+            --  Chain spec TC pragma to list for subprogram
+
+            Set_Next_Pragma (N, Spec_TC_List (Contract (S)));
+            Set_Spec_TC_List (Contract (S), N);
+         end Chain_TC;
+
+      --  Start of processing for Check_Test_Case
+
+      begin
+         if not Is_List_Member (N) then
+            Pragma_Misplaced;
+         end if;
+
+         --  Test cases should only appear in package spec unit
+
+         if Get_Source_Unit (N) = No_Unit
+           or else not Nkind_In (Sinfo.Unit (Cunit (Get_Source_Unit (N))),
+                                 N_Package_Declaration,
+                                 N_Generic_Package_Declaration)
+         then
+            Pragma_Misplaced;
+         end if;
+
+         --  Search prior declarations
+
+         P := N;
+         while Present (Prev (P)) loop
+            P := Prev (P);
+
+            --  If the previous node is a generic subprogram, do not go to to
+            --  the original node, which is the unanalyzed tree: we need to
+            --  attach the test-case to the analyzed version at this point.
+            --  They get propagated to the original tree when analyzing the
+            --  corresponding body.
+
+            if Nkind (P) not in N_Generic_Declaration then
+               PO := Original_Node (P);
+            else
+               PO := P;
+            end if;
+
+            --  Skip past prior pragma
+
+            if Nkind (PO) = N_Pragma then
+               null;
+
+            --  Skip stuff not coming from source
+
+            elsif not Comes_From_Source (PO) then
+               null;
+
+            --  Only remaining possibility is subprogram declaration. First
+            --  check that it is declared directly in a package declaration.
+            --  This may be either the package declaration for the current unit
+            --  being defined or a local package declaration.
+
+            elsif not Present (Parent (Parent (PO)))
+              or else not Present (Parent (Parent (Parent (PO))))
+              or else not Nkind_In (Parent (Parent (PO)),
+                                    N_Package_Declaration,
+                                    N_Generic_Package_Declaration)
+            then
+               Pragma_Misplaced;
+
+            else
+               Chain_TC (PO);
+               return;
+            end if;
+         end loop;
+
+         --  If we fall through, pragma was misplaced
+
+         Pragma_Misplaced;
+      end Check_Test_Case;
+
       --------------------------------------
       -- Check_Valid_Configuration_Pragma --
       --------------------------------------
@@ -2348,7 +2745,14 @@ package body Sem_Prag is
 
       procedure GNAT_Pragma is
       begin
-         Check_Restriction (No_Implementation_Pragmas, N);
+         --  We need to check the No_Implementation_Pragmas restriction for
+         --  the case of a pragma from source. Note that the case of aspects
+         --  generating corresponding pragmas marks these pragmas as not being
+         --  from source, so this test also catches that case.
+
+         if Comes_From_Source (N) then
+            Check_Restriction (No_Implementation_Pragmas, N);
+         end if;
       end GNAT_Pragma;
 
       --------------------------
@@ -2568,16 +2972,29 @@ package body Sem_Prag is
                   Set_Has_Delayed_Freeze (E);
                end if;
 
-               --  An interesting improvement here. If an object of type X is
-               --  declared atomic, and the type X is not atomic, that's a
+               --  An interesting improvement here. If an object of composite
+               --  type X is declared atomic, and the type X isn't, that's a
                --  pity, since it may not have appropriate alignment etc. We
                --  can rescue this in the special case where the object and
                --  type are in the same unit by just setting the type as
                --  atomic, so that the back end will process it as atomic.
 
+               --  Note: we used to do this for elementary types as well,
+               --  but that turns out to be a bad idea and can have unwanted
+               --  effects, most notably if the type is elementary, the object
+               --  a simple component within a record, and both are in a spec:
+               --  every object of this type in the entire program will be
+               --  treated as atomic, thus incurring a potentially costly
+               --  synchronization operation for every access.
+
+               --  Of course it would be best if the back end could just adjust
+               --  the alignment etc for the specific object, but that's not
+               --  something we are capable of doing at this point.
+
                Utyp := Underlying_Type (Etype (E));
 
                if Present (Utyp)
+                 and then Is_Composite_Type (Utyp)
                  and then Sloc (E) > No_Location
                  and then Sloc (Utyp) > No_Location
                  and then
@@ -3012,7 +3429,39 @@ package body Sem_Prag is
 
          --  Set entity to return
 
-         Ent := E;
+         Ent := E;
+
+         --  Ada_Pass_By_Copy special checking
+
+         if C = Convention_Ada_Pass_By_Copy then
+            if not Is_First_Subtype (E) then
+               Error_Pragma_Arg
+                 ("convention `Ada_Pass_By_Copy` only "
+                  & "allowed for types", Arg2);
+            end if;
+
+            if Is_By_Reference_Type (E) then
+               Error_Pragma_Arg
+                 ("convention `Ada_Pass_By_Copy` not allowed for "
+                  & "by-reference type", Arg1);
+            end if;
+         end if;
+
+         --  Ada_Pass_By_Reference special checking
+
+         if C = Convention_Ada_Pass_By_Reference then
+            if not Is_First_Subtype (E) then
+               Error_Pragma_Arg
+                 ("convention `Ada_Pass_By_Reference` only "
+                  & "allowed for types", Arg2);
+            end if;
+
+            if Is_By_Copy_Type (E) then
+               Error_Pragma_Arg
+                 ("convention `Ada_Pass_By_Reference` not allowed for "
+                  & "by-copy type", Arg1);
+            end if;
+         end if;
 
          --  Go to renamed subprogram if present, since convention applies to
          --  the actual renamed entity, not to the renaming entity. If the
@@ -3103,19 +3552,39 @@ package body Sem_Prag is
               ("second argument of pragma% must be a subprogram", Arg2);
          end if;
 
-         --  For Stdcall, a subprogram, variable or subprogram type is required
+         --  Stdcall case
 
-         if C = Convention_Stdcall
-           and then not Is_Subprogram (E)
-           and then not Is_Generic_Subprogram (E)
-           and then Ekind (E) /= E_Variable
-           and then not
-             (Is_Access_Type (E)
-               and then Ekind (Designated_Type (E)) = E_Subprogram_Type)
-         then
-            Error_Pragma_Arg
-              ("second argument of pragma% must be subprogram (type)",
-               Arg2);
+         if C = Convention_Stdcall then
+
+            --  A dispatching call is not allowed. A dispatching subprogram
+            --  cannot be used to interface to the Win32 API, so in fact this
+            --  check does not impose any effective restriction.
+
+            if Is_Dispatching_Operation (E) then
+
+               Error_Pragma
+                 ("dispatching subprograms cannot use Stdcall convention");
+
+            --  Subprogram is allowed, but not a generic subprogram, and not a
+            --  dispatching operation.
+
+            elsif not Is_Subprogram (E)
+              and then not Is_Generic_Subprogram (E)
+
+              --  A variable is OK
+
+              and then Ekind (E) /= E_Variable
+
+              --  An access to subprogram is also allowed
+
+              and then not
+                (Is_Access_Type (E)
+                  and then Ekind (Designated_Type (E)) = E_Subprogram_Type)
+            then
+               Error_Pragma_Arg
+                 ("second argument of pragma% must be subprogram (type)",
+                  Arg2);
+            end if;
          end if;
 
          if not Is_Subprogram (E)
@@ -3187,6 +3656,35 @@ package body Sem_Prag is
          end if;
       end Process_Convention;
 
+      ----------------------------------------
+      -- Process_Disable_Enable_Atomic_Sync --
+      ----------------------------------------
+
+      procedure Process_Disable_Enable_Atomic_Sync (Nam : Name_Id) is
+      begin
+         GNAT_Pragma;
+         Check_No_Identifiers;
+         Check_At_Most_N_Arguments (1);
+
+         --  Modeled internally as
+         --    pragma Unsuppress (Atomic_Synchronization [,Entity])
+
+         Rewrite (N,
+           Make_Pragma (Loc,
+             Pragma_Identifier            =>
+               Make_Identifier (Loc, Nam),
+             Pragma_Argument_Associations => New_List (
+               Make_Pragma_Argument_Association (Loc,
+                 Expression =>
+                   Make_Identifier (Loc, Name_Atomic_Synchronization)))));
+
+         if Present (Arg1) then
+            Append_To (Pragma_Argument_Associations (N), New_Copy (Arg1));
+         end if;
+
+         Analyze (N);
+      end Process_Disable_Enable_Atomic_Sync;
+
       -----------------------------------------------------
       -- Process_Extended_Import_Export_Exception_Pragma --
       -----------------------------------------------------
@@ -4153,27 +4651,39 @@ package body Sem_Prag is
 
          --  Import a CPP class
 
-         elsif Is_Record_Type (Def_Id)
-           and then C = Convention_CPP
+         elsif C = Convention_CPP
+           and then (Is_Record_Type (Def_Id)
+                      or else Ekind (Def_Id) = E_Incomplete_Type)
          then
-            --  Types treated as CPP classes are treated as limited, but we
-            --  don't require them to be declared this way. A warning is issued
-            --  to encourage the user to declare them as limited. This is not
-            --  an error, for compatibility reasons, because these types have
-            --  been supported this way for some time.
+            if Ekind (Def_Id) = E_Incomplete_Type then
+               if Present (Full_View (Def_Id)) then
+                  Def_Id := Full_View (Def_Id);
+
+               else
+                  Error_Msg_N
+                    ("cannot import 'C'P'P type before full declaration seen",
+                     Get_Pragma_Arg (Arg2));
+
+                  --  Although we have reported the error we decorate it as
+                  --  CPP_Class to avoid reporting spurious errors
+
+                  Set_Is_CPP_Class (Def_Id);
+                  return;
+               end if;
+            end if;
+
+            --  Types treated as CPP classes must be declared limited (note:
+            --  this used to be a warning but there is no real benefit to it
+            --  since we did effectively intend to treat the type as limited
+            --  anyway).
 
             if not Is_Limited_Type (Def_Id) then
                Error_Msg_N
-                 ("imported 'C'P'P type should be " &
-                    "explicitly declared limited?",
-                  Get_Pragma_Arg (Arg2));
-               Error_Msg_N
-                 ("\type will be considered limited",
+                 ("imported 'C'P'P type must be limited",
                   Get_Pragma_Arg (Arg2));
             end if;
 
             Set_Is_CPP_Class (Def_Id);
-            Set_Is_Limited_Record (Def_Id);
 
             --  Imported CPP types must not have discriminants (because C++
             --  classes do not have discriminants).
@@ -4185,38 +4695,13 @@ package body Sem_Prag is
                           (Declaration_Node (Def_Id))));
             end if;
 
-            --  Components of imported CPP types must not have default
-            --  expressions because the constructor (if any) is on the
-            --  C++ side.
-
-            declare
-               Tdef  : constant Node_Id :=
-                         Type_Definition (Declaration_Node (Def_Id));
-               Clist : Node_Id;
-               Comp  : Node_Id;
-
-            begin
-               if Nkind (Tdef) = N_Record_Definition then
-                  Clist := Component_List (Tdef);
-
-               else
-                  pragma Assert (Nkind (Tdef) = N_Derived_Type_Definition);
-                  Clist := Component_List (Record_Extension_Part (Tdef));
-               end if;
-
-               if Present (Clist) then
-                  Comp := First (Component_Items (Clist));
-                  while Present (Comp) loop
-                     if Present (Expression (Comp)) then
-                        Error_Msg_N
-                          ("component of imported 'C'P'P type cannot have" &
-                           " default expression", Expression (Comp));
-                     end if;
+            --  Check that components of imported CPP types do not have default
+            --  expressions. For private types this check is performed when the
+            --  full view is analyzed (see Process_Full_View).
 
-                     Next (Comp);
-                  end loop;
-               end if;
-            end;
+            if not Is_Private_Type (Def_Id) then
+               Check_CPP_Type_Has_No_Defaults (Def_Id);
+            end if;
 
          elsif Nkind (Parent (Def_Id)) = N_Incomplete_Type_Declaration then
             Check_No_Link_Name;
@@ -4227,8 +4712,8 @@ package body Sem_Prag is
 
          else
             Error_Pragma_Arg
-              ("second argument of pragma% must be object, subprogram" &
-               or incomplete type",
+              ("second argument of pragma% must be object, subprogram "
+               & "or incomplete type",
                Arg2);
          end if;
 
@@ -4429,6 +4914,18 @@ package body Sem_Prag is
                      then
                         null;
                      end if;
+
+                  --  Inline is a program unit pragma (RM 10.1.5) and cannot
+                  --  appear in a formal part to apply to a formal subprogram.
+                  --  Do not apply check within an instance or a formal package
+                  --  the test will have been applied to the original generic.
+
+                  elsif Nkind (Decl) in N_Formal_Subprogram_Declaration
+                    and then List_Containing (Decl) = List_Containing (N)
+                    and then not In_Instance
+                  then
+                     Error_Msg_N
+                       ("Inline cannot apply to a formal subprogram", N);
                   end if;
                end if;
 
@@ -4506,7 +5003,8 @@ package body Sem_Prag is
 
                   --  For the pragma case, climb homonym chain. This is
                   --  what implements allowing the pragma in the renaming
-                  --  case, with the result applying to the ancestors.
+                  --  case, with the result applying to the ancestors, and
+                  --  also allows Inline to apply to all previous homonyms.
 
                   if not From_Aspect_Specification (N) then
                      while Present (Homonym (Subp))
@@ -4734,11 +5232,14 @@ package body Sem_Prag is
               (Get_Base_Subprogram (Subprogram_Def), Link_Nam);
          end if;
 
-         --  We allow duplicated export names in CIL, as they are always
+         --  We allow duplicated export names in CIL/Java, as they are always
          --  enclosed in a namespace that differentiates them, and overloaded
          --  entities are supported by the VM.
 
-         if Convention (Subprogram_Def) /= Convention_CIL then
+         if Convention (Subprogram_Def) /= Convention_CIL
+              and then
+            Convention (Subprogram_Def) /= Convention_Java
+         then
             Check_Duplicated_Export_Name (Link_Nam);
          end if;
       end Process_Interface_Name;
@@ -4877,6 +5378,46 @@ package body Sem_Prag is
                   Check_Restriction (No_Implementation_Restrictions, Arg);
                end if;
 
+               --  Special processing for No_Elaboration_Code restriction
+
+               if R_Id = No_Elaboration_Code then
+
+                  --  Restriction is only recognized within a configuration
+                  --  pragma file, or within a unit of the main extended
+                  --  program. Note: the test for Main_Unit is needed to
+                  --  properly include the case of configuration pragma files.
+
+                  if not (Current_Sem_Unit = Main_Unit
+                           or else In_Extended_Main_Source_Unit (N))
+                  then
+                     return;
+
+                  --  Don't allow in a subunit unless already specified in
+                  --  body or spec.
+
+                  elsif Nkind (Parent (N)) = N_Compilation_Unit
+                    and then Nkind (Unit (Parent (N))) = N_Subunit
+                    and then not Restriction_Active (No_Elaboration_Code)
+                  then
+                     Error_Msg_N
+                       ("invalid specification of ""No_Elaboration_Code""",
+                        N);
+                     Error_Msg_N
+                       ("\restriction cannot be specified in a subunit", N);
+                     Error_Msg_N
+                       ("\unless also specified in body or spec", N);
+                     return;
+
+                  --  If we have a No_Elaboration_Code pragma that we
+                  --  accept, then it needs to be added to the configuration
+                  --  restrcition set so that we get proper application to
+                  --  other units in the main extended source as required.
+
+                  else
+                     Add_To_Config_Boolean_Restrictions (No_Elaboration_Code);
+                  end if;
+               end if;
+
                --  If this is a warning, then set the warning unless we already
                --  have a real restriction active (we never want a warning to
                --  override a real restriction).
@@ -4916,8 +5457,15 @@ package body Sem_Prag is
                --  H.4(12). Restriction_Warnings never affects generated code
                --  so this is done only in the real restriction case.
 
+               --  Atomic_Synchronization is not a real check, so it is not
+               --  affected by this processing).
+
                if R_Id = No_Exceptions and then not Warn then
-                  Scope_Suppress := (others => True);
+                  for J in Scope_Suppress'Range loop
+                     if J /= Atomic_Synchronization then
+                        Scope_Suppress (J) := True;
+                     end if;
+                  end loop;
                end if;
 
             --  Case of No_Dependence => unit-name. Note that the parser
@@ -4926,6 +5474,26 @@ package body Sem_Prag is
             elsif Id = Name_No_Dependence then
                Check_Unit_Name (Expr);
 
+            --  Case of No_Specification_Of_Aspect => Identifier.
+
+            elsif Id = Name_No_Specification_Of_Aspect then
+               declare
+                  A_Id : Aspect_Id;
+
+               begin
+                  if Nkind (Expr) /= N_Identifier then
+                     A_Id := No_Aspect;
+                  else
+                     A_Id := Get_Aspect_Id (Chars (Expr));
+                  end if;
+
+                  if A_Id = No_Aspect then
+                     Error_Pragma_Arg ("invalid restriction name", Arg);
+                  else
+                     Set_Restriction_No_Specification_Of_Aspect (Expr, Warn);
+                  end if;
+               end;
+
             --  All other cases of restriction identifier present
 
             else
@@ -5009,6 +5577,17 @@ package body Sem_Prag is
 
          procedure Suppress_Unsuppress_Echeck (E : Entity_Id; C : Check_Id) is
          begin
+            --  Check for error of trying to set atomic synchronization for
+            --  a non-atomic variable.
+
+            if C = Atomic_Synchronization
+              and then not (Is_Atomic (E) or else Has_Atomic_Components (E))
+            then
+               Error_Msg_N
+                 ("pragma & requires atomic type or variable",
+                  Pragma_Identifier (Original_Node (N)));
+            end if;
+
             Set_Checks_May_Be_Suppressed (E);
 
             if In_Package_Spec then
@@ -5016,7 +5595,6 @@ package body Sem_Prag is
                  (Entity   => E,
                   Check    => C,
                   Suppress => Suppress_Case);
-
             else
                Push_Local_Suppress_Stack_Entry
                  (Entity   => E,
@@ -5037,10 +5615,13 @@ package body Sem_Prag is
       --  Start of processing for Process_Suppress_Unsuppress
 
       begin
-         --  Ignore pragma Suppress/Unsuppress in codepeer mode on user code:
-         --  we want to generate checks for analysis purposes, as set by -gnatC
+         --  Ignore pragma Suppress/Unsuppress in CodePeer and Alfa modes on
+         --  user code: we want to generate checks for analysis purposes, as
+         --  set respectively by -gnatC and -gnatd.F
 
-         if CodePeer_Mode and then Comes_From_Source (N) then
+         if (CodePeer_Mode or Alfa_Mode)
+           and then Comes_From_Source (N)
+         then
             return;
          end if;
 
@@ -5081,18 +5662,26 @@ package body Sem_Prag is
                --  the exception of Elaboration_Check, which is handled
                --  specially because of not wanting All_Checks to have the
                --  effect of deactivating static elaboration order processing.
+               --  Atomic_Synchronization is also not affected, since this is
+               --  not a real check.
 
                for J in Scope_Suppress'Range loop
-                  if J /= Elaboration_Check then
+                  if J /= Elaboration_Check
+                    and then J /= Atomic_Synchronization
+                  then
                      Scope_Suppress (J) := Suppress_Case;
                   end if;
                end loop;
 
             --  If not All_Checks, and predefined check, then set appropriate
             --  scope entry. Note that we will set Elaboration_Check if this
-            --  is explicitly specified.
+            --  is explicitly specified. Atomic_Synchronization is allowed
+            --  only if internally generated and entity is atomic.
 
-            elsif C in Predefined_Check_Id then
+            elsif C in Predefined_Check_Id
+              and then (not Comes_From_Source (N)
+                         or else C /= Atomic_Synchronization)
+            then
                Scope_Suppress (C) := Suppress_Case;
             end if;
 
@@ -5784,6 +6373,8 @@ package body Sem_Prag is
 
       --  Deal with unrecognized pragma
 
+      Pname := Pragma_Name (N);
+
       if not Is_Pragma_Name (Pname) then
          if Warn_On_Unrecognized_Pragma then
             Error_Msg_Name_1 := Pname;
@@ -5806,6 +6397,10 @@ package body Sem_Prag is
 
       Prag_Id := Get_Pragma_Id (Pname);
 
+      if Present (Corresponding_Aspect (N)) then
+         Pname := Chars (Identifier (Corresponding_Aspect (N)));
+      end if;
+
       --  Preset arguments
 
       Arg_Count := 0;
@@ -6062,56 +6657,63 @@ package body Sem_Prag is
          --  external tool and a tool-specific function. These arguments are
          --  not analyzed.
 
-         when Pragma_Annotate => Annotate : begin
+         when Pragma_Annotate => Annotate : declare
+            Arg : Node_Id;
+            Exp : Node_Id;
+
+         begin
             GNAT_Pragma;
             Check_At_Least_N_Arguments (1);
             Check_Arg_Is_Identifier (Arg1);
             Check_No_Identifiers;
             Store_Note (N);
 
-            declare
-               Arg : Node_Id;
-               Exp : Node_Id;
+            --  Second parameter is optional, it is never analyzed
 
-            begin
-               --  Second unanalyzed parameter is optional
+            if No (Arg2) then
+               null;
 
-               if No (Arg2) then
-                  null;
-               else
-                  Arg := Next (Arg2);
-                  while Present (Arg) loop
-                     Exp := Get_Pragma_Arg (Arg);
-                     Analyze (Exp);
+            --  Here if we have a second parameter
 
-                     if Is_Entity_Name (Exp) then
-                        null;
+            else
+               --  Second parameter must be identifier
 
-                     --  For string literals, we assume Standard_String as the
-                     --  type, unless the string contains wide or wide_wide
-                     --  characters.
+               Check_Arg_Is_Identifier (Arg2);
 
-                     elsif Nkind (Exp) = N_String_Literal then
-                        if Has_Wide_Wide_Character (Exp) then
-                           Resolve (Exp, Standard_Wide_Wide_String);
-                        elsif Has_Wide_Character (Exp) then
-                           Resolve (Exp, Standard_Wide_String);
-                        else
-                           Resolve (Exp, Standard_String);
-                        end if;
+               --  Process remaining parameters if any
 
-                     elsif Is_Overloaded (Exp) then
-                           Error_Pragma_Arg
-                             ("ambiguous argument for pragma%", Exp);
+               Arg := Next (Arg2);
+               while Present (Arg) loop
+                  Exp := Get_Pragma_Arg (Arg);
+                  Analyze (Exp);
+
+                  if Is_Entity_Name (Exp) then
+                     null;
+
+                  --  For string literals, we assume Standard_String as the
+                  --  type, unless the string contains wide or wide_wide
+                  --  characters.
 
+                  elsif Nkind (Exp) = N_String_Literal then
+                     if Has_Wide_Wide_Character (Exp) then
+                        Resolve (Exp, Standard_Wide_Wide_String);
+                     elsif Has_Wide_Character (Exp) then
+                        Resolve (Exp, Standard_Wide_String);
                      else
-                        Resolve (Exp);
+                        Resolve (Exp, Standard_String);
                      end if;
 
-                     Next (Arg);
-                  end loop;
-               end if;
-            end;
+                  elsif Is_Overloaded (Exp) then
+                        Error_Pragma_Arg
+                          ("ambiguous argument for pragma%", Exp);
+
+                  else
+                     Resolve (Exp);
+                  end if;
+
+                  Next (Arg);
+               end loop;
+            end if;
          end Annotate;
 
          ------------
@@ -6154,7 +6756,7 @@ package body Sem_Prag is
 
             Rewrite (N,
               Make_Pragma (Loc,
-                Chars => Name_Check,
+                Chars                        => Name_Check,
                 Pragma_Argument_Associations => Newa));
             Analyze (N);
          end Assert;
@@ -6163,7 +6765,7 @@ package body Sem_Prag is
          -- Assertion_Policy --
          ----------------------
 
-         --  pragma Assertion_Policy (Check | Ignore)
+         --  pragma Assertion_Policy (Check | Disable |Ignore)
 
          when Pragma_Assertion_Policy => Assertion_Policy : declare
             Policy : Node_Id;
@@ -6173,7 +6775,7 @@ package body Sem_Prag is
             Check_Valid_Configuration_Pragma;
             Check_Arg_Count (1);
             Check_No_Identifiers;
-            Check_Arg_Is_One_Of (Arg1, Name_Check, Name_Ignore);
+            Check_Arg_Is_One_Of (Arg1, Name_Check, Name_Disable, Name_Ignore);
 
             --  We treat pragma Assertion_Policy as equivalent to:
 
@@ -6493,7 +7095,6 @@ package body Sem_Prag is
                Error_Pragma_Arg ("inappropriate entity for pragma%", Arg1);
             end if;
          end Atomic_Components;
-
          --------------------
          -- Attach_Handler --
          --------------------
@@ -6511,7 +7112,7 @@ package body Sem_Prag is
                Check_Interrupt_Or_Attach_Handler;
 
                --  The expression that designates the attribute may depend on a
-               --  discriminant, and is therefore a per- object expression, to
+               --  discriminant, and is therefore a per-object expression, to
                --  be expanded in the init proc. If expansion is enabled, then
                --  perform semantic checks on a copy only.
 
@@ -6573,9 +7174,9 @@ package body Sem_Prag is
          -- Check --
          -----------
 
-         --  pragma Check ([Name    =>] Identifier,
-         --                [Check   =>] Boolean_Expression
-         --              [,[Message =>] String_Expression]);
+         --  pragma Check ([Name    =>] IDENTIFIER,
+         --                [Check   =>] Boolean_EXPRESSION
+         --              [,[Message =>] String_EXPRESSION]);
 
          when Pragma_Check => Check : declare
             Expr : Node_Id;
@@ -6598,14 +7199,20 @@ package body Sem_Prag is
 
             Check_Arg_Is_Identifier (Arg1);
 
+            --  Completely ignore if disabled
+
+            if Check_Disabled (Chars (Get_Pragma_Arg (Arg1))) then
+               Rewrite (N, Make_Null_Statement (Loc));
+               Analyze (N);
+               return;
+            end if;
+
             --  Indicate if pragma is enabled. The Original_Node reference here
             --  is to deal with pragma Assert rewritten as a Check pragma.
 
             Check_On := Check_Enabled (Chars (Get_Pragma_Arg (Arg1)));
 
             if Check_On then
-               Set_Pragma_Enabled (N);
-               Set_Pragma_Enabled (Original_Node (N));
                Set_SCO_Pragma_Enabled (Loc);
             end if;
 
@@ -6685,7 +7292,7 @@ package body Sem_Prag is
          --    [Name   =>] IDENTIFIER,
          --    [Policy =>] POLICY_IDENTIFIER);
 
-         --  POLICY_IDENTIFIER ::= ON | OFF | CHECK | IGNORE
+         --  POLICY_IDENTIFIER ::= ON | OFF | CHECK | DISABLE | IGNORE
 
          --  Note: this is a configuration pragma, but it is allowed to appear
          --  anywhere else.
@@ -6696,7 +7303,7 @@ package body Sem_Prag is
             Check_Optional_Identifier (Arg1, Name_Name);
             Check_Optional_Identifier (Arg2, Name_Policy);
             Check_Arg_Is_One_Of
-              (Arg2, Name_On, Name_Off, Name_Check, Name_Ignore);
+              (Arg2, Name_On, Name_Off, Name_Check, Name_Disable, Name_Ignore);
 
             --  A Check_Policy pragma can appear either as a configuration
             --  pragma, or in a declarative part or a package spec (see RM
@@ -7053,25 +7660,19 @@ package body Sem_Prag is
                Error_Pragma_Arg ("pragma% applicable to tagged types ", Arg1);
             end if;
 
-            --  Types treated as CPP classes are treated as limited, but we
-            --  don't require them to be declared this way. A warning is issued
-            --  to encourage the user to declare them as limited. This is not
-            --  an error, for compatibility reasons, because these types have
-            --  been supported this way for some time.
+            --  Types treated as CPP classes must be declared limited (note:
+            --  this used to be a warning but there is no real benefit to it
+            --  since we did effectively intend to treat the type as limited
+            --  anyway).
 
             if not Is_Limited_Type (Typ) then
                Error_Msg_N
-                 ("imported 'C'P'P type should be " &
-                    "explicitly declared limited?",
-                  Get_Pragma_Arg (Arg1));
-               Error_Msg_N
-                 ("\type will be considered limited",
+                 ("imported 'C'P'P type must be limited",
                   Get_Pragma_Arg (Arg1));
             end if;
 
-            Set_Is_CPP_Class      (Typ);
-            Set_Is_Limited_Record (Typ);
-            Set_Convention        (Typ, Convention_CPP);
+            Set_Is_CPP_Class (Typ);
+            Set_Convention (Typ, Convention_CPP);
 
             --  Imported CPP types must not have discriminants (because C++
             --  classes do not have discriminants).
@@ -7184,6 +7785,7 @@ package body Sem_Prag is
 
                Set_Has_Completion (Def_Id);
                Set_Is_Constructor (Def_Id);
+               Set_Convention (Def_Id, Convention_CPP);
 
                --  Imported C++ constructors are not dispatching primitives
                --  because in C++ they don't have a dispatch table slot.
@@ -7345,21 +7947,69 @@ package body Sem_Prag is
          --  pragma Debug ([boolean_EXPRESSION,] PROCEDURE_CALL_STATEMENT);
 
          when Pragma_Debug => Debug : declare
-               Cond : Node_Id;
+            Cond : Node_Id;
+            Call : Node_Id;
 
          begin
             GNAT_Pragma;
 
+            --  Skip analysis if disabled
+
+            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),
                  Loc);
 
+            if Debug_Pragmas_Enabled then
+               Set_SCO_Pragma_Enabled (Loc);
+            end if;
+
             if Arg_Count = 2 then
                Cond :=
                  Make_And_Then (Loc,
-                   Left_Opnd   => Relocate_Node (Cond),
-                   Right_Opnd  => Get_Pragma_Arg (Arg1));
+                   Left_Opnd  => Relocate_Node (Cond),
+                   Right_Opnd => Get_Pragma_Arg (Arg1));
+               Call := Get_Pragma_Arg (Arg2);
+            else
+               Call := Get_Pragma_Arg (Arg1);
+            end if;
+
+            if Nkind_In (Call,
+                 N_Indexed_Component,
+                 N_Function_Call,
+                 N_Identifier,
+                 N_Expanded_Name,
+                 N_Selected_Component)
+            then
+               --  If this pragma Debug comes from source, its argument was
+               --  parsed as a name form (which is syntactically identical).
+               --  In a generic context a parameterless call will be left as
+               --  an expanded name (if global) or selected_component if local.
+               --  Change it to a procedure call statement now.
+
+               Change_Name_To_Procedure_Call_Statement (Call);
+
+            elsif Nkind (Call) = N_Procedure_Call_Statement then
+
+               --  Already in the form of a procedure call statement: nothing
+               --  to do (could happen in case of an internally generated
+               --  pragma Debug).
+
+               null;
+
+            else
+               --  All other cases: diagnose error
+
+               Error_Msg
+                 ("argument of pragma ""Debug"" is not procedure call",
+                  Sloc (Call));
+               return;
             end if;
 
             --  Rewrite into a conditional with an appropriate condition. We
@@ -7367,14 +8017,27 @@ package body Sem_Prag is
             --  use of the secondary stack does not generate execution overhead
             --  for suppressed conditions.
 
+            --  Normally the analysis that follows will freeze the subprogram
+            --  being called. However, if the call is to a null procedure,
+            --  we want to freeze it before creating the block, because the
+            --  analysis that follows may be done with expansion disabled, in
+            --  which case the body will not be generated, leading to spurious
+            --  errors.
+
+            if Nkind (Call) = N_Procedure_Call_Statement
+              and then Is_Entity_Name (Name (Call))
+            then
+               Analyze (Name (Call));
+               Freeze_Before (N, Entity (Name (Call)));
+            end if;
+
             Rewrite (N, Make_Implicit_If_Statement (N,
               Condition => Cond,
                  Then_Statements => New_List (
                    Make_Block_Statement (Loc,
                      Handled_Statement_Sequence =>
                        Make_Handled_Sequence_Of_Statements (Loc,
-                         Statements => New_List (
-                           Relocate_Node (Debug_Statement (N))))))));
+                         Statements => New_List (Relocate_Node (Call)))))));
             Analyze (N);
          end Debug;
 
@@ -7387,9 +8050,11 @@ package body Sem_Prag is
          when Pragma_Debug_Policy =>
             GNAT_Pragma;
             Check_Arg_Count (1);
-            Check_Arg_Is_One_Of (Arg1, Name_Check, Name_Ignore);
+            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;
 
          ---------------------
          -- Detect_Blocking --
@@ -7454,23 +8119,14 @@ package body Sem_Prag is
 
             Default_Pool := Expression (Arg1);
 
-         ---------------
-         -- Dimension --
-         ---------------
-
-         when Pragma_Dimension =>
-            GNAT_Pragma;
-            Check_Arg_Count (4);
-            Check_No_Identifiers;
-            Check_Arg_Is_Local_Name (Arg1);
+         ------------------------------------
+         -- Disable_Atomic_Synchronization --
+         ------------------------------------
 
-            if not Is_Type (Arg1) then
-               Error_Pragma ("first argument for pragma% must be subtype");
-            end if;
+         --  pragma Disable_Atomic_Synchronization [(Entity)];
 
-            Check_Arg_Is_Static_Expression (Arg2, Standard_Integer);
-            Check_Arg_Is_Static_Expression (Arg3, Standard_Integer);
-            Check_Arg_Is_Static_Expression (Arg4, Standard_Integer);
+         when Pragma_Disable_Atomic_Synchronization =>
+            Process_Disable_Enable_Atomic_Sync (Name_Suppress);
 
          -------------------
          -- Discard_Names --
@@ -7534,6 +8190,54 @@ package body Sem_Prag is
             end if;
          end Discard_Names;
 
+         ------------------------
+         -- Dispatching_Domain --
+         ------------------------
+
+         --  pragma Dispatching_Domain (EXPRESSION);
+
+         when Pragma_Dispatching_Domain => Dispatching_Domain : declare
+            P   : constant Node_Id := Parent (N);
+            Arg : Node_Id;
+
+         begin
+            Ada_2012_Pragma;
+            Check_No_Identifiers;
+            Check_Arg_Count (1);
+
+            --  This pragma is born obsolete, but not the aspect
+
+            if not From_Aspect_Specification (N) then
+               Check_Restriction
+                 (No_Obsolescent_Features, Pragma_Identifier (N));
+            end if;
+
+            if Nkind (P) = N_Task_Definition then
+               Arg := Get_Pragma_Arg (Arg1);
+
+               --  The expression must be analyzed in the special manner
+               --  described in "Handling of Default and Per-Object
+               --  Expressions" in sem.ads.
+
+               Preanalyze_Spec_Expression (Arg, RTE (RE_Dispatching_Domain));
+
+            --  Anything else is incorrect
+
+            else
+               Pragma_Misplaced;
+            end if;
+
+            if Has_Pragma_Dispatching_Domain (P) then
+               Error_Pragma ("duplicate pragma% not allowed");
+            else
+               Set_Has_Pragma_Dispatching_Domain (P, True);
+
+               if Nkind (P) = N_Task_Definition then
+                  Record_Rep_Item (Defining_Identifier (Parent (P)), N);
+               end if;
+            end if;
+         end Dispatching_Domain;
+
          ---------------
          -- Elaborate --
          ---------------
@@ -7616,7 +8320,7 @@ package body Sem_Prag is
 
                if Citem = N then
                   Error_Pragma_Arg
-                    ("argument of pragma% is not with'ed unit", Arg);
+                    ("argument of pragma% is not withed unit", Arg);
                end if;
 
                Next (Arg);
@@ -7694,7 +8398,7 @@ package body Sem_Prag is
                if Citem = N then
                   Set_Error_Posted (N);
                   Error_Pragma_Arg
-                    ("argument of pragma% is not with'ed unit", Arg);
+                    ("argument of pragma% is not withed unit", Arg);
                end if;
 
                Next (Arg);
@@ -7846,6 +8550,15 @@ package body Sem_Prag is
                Source_Location);
          end Eliminate;
 
+         -----------------------------------
+         -- Enable_Atomic_Synchronization --
+         -----------------------------------
+
+         --  pragma Enable_Atomic_Synchronization [(Entity)];
+
+         when Pragma_Enable_Atomic_Synchronization =>
+            Process_Disable_Enable_Atomic_Sync (Name_Unsuppress);
+
          ------------
          -- Export --
          ------------
@@ -8635,12 +9348,52 @@ package body Sem_Prag is
             end;
          end Ident;
 
+         ----------------------------
+         -- Implementation_Defined --
+         ----------------------------
+
+         --  pragma Implementation_Defined (local_NAME);
+
+         --  Marks previously declared entity as implementation defined. For
+         --  an overloaded entity, applies to the most recent homonym.
+
+         --  pragma Implementation_Defined;
+
+         --  The form with no arguments appears anywhere within a scope, most
+         --  typically a package spec, and indicates that all entities that are
+         --  defined within the package spec are Implementation_Defined.
+
+         when Pragma_Implementation_Defined => Implementation_Defined : declare
+            Ent : Entity_Id;
+
+         begin
+            Check_No_Identifiers;
+
+            --  Form with no arguments
+
+            if Arg_Count = 0 then
+               Set_Is_Implementation_Defined (Current_Scope);
+
+            --  Form with one argument
+
+            else
+               Check_Arg_Count (1);
+               Check_Arg_Is_Local_Name (Arg1);
+               Ent := Entity (Get_Pragma_Arg (Arg1));
+               Set_Is_Implementation_Defined (Ent);
+            end if;
+         end Implementation_Defined;
+
          -----------------
          -- Implemented --
          -----------------
 
          --  pragma Implemented (procedure_LOCAL_NAME, implementation_kind);
-         --  implementation_kind ::= By_Entry | By_Protected_Procedure | By_Any
+         --  implementation_kind ::=
+         --    By_Entry | By_Protected_Procedure | By_Any | Optional
+
+         --  "By_Any" and "Optional" are treated as synonyms in order to
+         --  support Ada 2012 aspect Synchronization.
 
          when Pragma_Implemented => Implemented : declare
             Proc_Id : Entity_Id;
@@ -8652,8 +9405,11 @@ package body Sem_Prag is
             Check_No_Identifiers;
             Check_Arg_Is_Identifier (Arg1);
             Check_Arg_Is_Local_Name (Arg1);
-            Check_Arg_Is_One_Of
-              (Arg2, Name_By_Any, Name_By_Entry, Name_By_Protected_Procedure);
+            Check_Arg_Is_One_Of (Arg2,
+              Name_By_Any,
+              Name_By_Entry,
+              Name_By_Protected_Procedure,
+              Name_Optional);
 
             --  Extract the name of the local procedure
 
@@ -9168,11 +9924,12 @@ package body Sem_Prag is
             Check_Valid_Configuration_Pragma;
             Check_Restriction (No_Initialize_Scalars, N);
 
-            --  Initialize_Scalars creates false positives in CodePeer,
-            --  so ignore this pragma in this mode.
+            --  Initialize_Scalars creates false positives in CodePeer, and
+            --  incorrect negative results in Alfa mode, so ignore this pragma
+            --  in these modes.
 
             if not Restriction_Active (No_Initialize_Scalars)
-              and then not CodePeer_Mode
+              and then not (CodePeer_Mode or Alfa_Mode)
             then
                Init_Or_Norm_Scalars := True;
                Initialize_Scalars := True;
@@ -9199,10 +9956,10 @@ package body Sem_Prag is
          when Pragma_Inline_Always =>
             GNAT_Pragma;
 
-            --  Pragma always active unless in CodePeer mode, since this causes
-            --  walk order issues.
+            --  Pragma always active unless in CodePeer or Alfa mode, since
+            --  this causes walk order issues.
 
-            if not CodePeer_Mode then
+            if not (CodePeer_Mode or Alfa_Mode) then
                Process_Inline (True);
             end if;
 
@@ -9602,10 +10359,26 @@ package body Sem_Prag is
             if Typ = Any_Type then
                return;
 
-            elsif not Ekind_In (Typ, E_Private_Type,
-                                     E_Record_Type_With_Private,
-                                     E_Limited_Private_Type)
+            --  An invariant must apply to a private type, or appear in the
+            --  private part of a package spec and apply to a completion.
+
+            elsif Ekind_In (Typ, E_Private_Type,
+                                 E_Record_Type_With_Private,
+                                 E_Limited_Private_Type)
+            then
+               null;
+
+            elsif In_Private_Part (Current_Scope)
+              and then Has_Private_Declaration (Typ)
             then
+               null;
+
+            elsif In_Private_Part (Current_Scope) then
+               Error_Pragma_Arg
+                 ("pragma% only allowed for private type " &
+                  "declared in visible part", Arg1);
+
+            else
                Error_Pragma_Arg
                  ("pragma% only allowed for private type", Arg1);
             end if;
@@ -10263,16 +11036,23 @@ package body Sem_Prag is
          --  pragma Locking_Policy (policy_IDENTIFIER);
 
          when Pragma_Locking_Policy => declare
-            LP : Character;
-
+            subtype LP_Range is Name_Id
+              range First_Locking_Policy_Name .. Last_Locking_Policy_Name;
+            LP_Val : LP_Range;
+            LP     : Character;
          begin
             Check_Ada_83_Warning;
             Check_Arg_Count (1);
             Check_No_Identifiers;
             Check_Arg_Is_Locking_Policy (Arg1);
             Check_Valid_Configuration_Pragma;
-            Get_Name_String (Chars (Get_Pragma_Arg (Arg1)));
-            LP := Fold_Upper (Name_Buffer (1));
+            LP_Val := Chars (Get_Pragma_Arg (Arg1));
+
+            case LP_Val is
+               when Name_Ceiling_Locking            => LP := 'C';
+               when Name_Inheritance_Locking        => LP := 'I';
+               when Name_Concurrent_Readers_Locking => LP := 'R';
+            end case;
 
             if Locking_Policy /= ' '
               and then Locking_Policy /= LP
@@ -10298,7 +11078,8 @@ package body Sem_Prag is
 
          --  pragma Long_Float (D_Float | G_Float);
 
-         when Pragma_Long_Float =>
+         when Pragma_Long_Float => Long_Float : declare
+         begin
             GNAT_Pragma;
             Check_Valid_Configuration_Pragma;
             Check_Arg_Count (1);
@@ -10313,22 +11094,42 @@ package body Sem_Prag is
 
             if Chars (Get_Pragma_Arg (Arg1)) = Name_D_Float then
                if Opt.Float_Format_Long = 'G' then
-                  Error_Pragma ("G_Float previously specified");
-               end if;
+                  Error_Pragma_Arg
+                    ("G_Float previously specified", Arg1);
+
+               elsif Current_Sem_Unit /= Main_Unit
+                 and then Opt.Float_Format_Long /= 'D'
+               then
+                  Error_Pragma_Arg
+                    ("main unit not compiled with pragma Long_Float (D_Float)",
+                     "\pragma% must be used consistently for whole partition",
+                     Arg1);
 
-               Opt.Float_Format_Long := 'D';
+               else
+                  Opt.Float_Format_Long := 'D';
+               end if;
 
             --  G_Float case (this is the default, does not need overriding)
 
             else
                if Opt.Float_Format_Long = 'D' then
                   Error_Pragma ("D_Float previously specified");
-               end if;
 
-               Opt.Float_Format_Long := 'G';
+               elsif Current_Sem_Unit /= Main_Unit
+                 and then Opt.Float_Format_Long /= 'G'
+               then
+                  Error_Pragma_Arg
+                    ("main unit not compiled with pragma Long_Float (G_Float)",
+                     "\pragma% must be used consistently for whole partition",
+                     Arg1);
+
+               else
+                  Opt.Float_Format_Long := 'G';
+               end if;
             end if;
 
             Set_Standard_Fpt_Formats;
+         end Long_Float;
 
          -----------------------
          -- Machine_Attribute --
@@ -10641,10 +11442,11 @@ package body Sem_Prag is
             Check_Arg_Count (0);
             Check_Valid_Configuration_Pragma;
 
-            --  Normalize_Scalars creates false positives in CodePeer, so
-            --  ignore this pragma in this mode.
+            --  Normalize_Scalars creates false positives in CodePeer, and
+            --  incorrect negative results in Alfa mode, so ignore this pragma
+            --  in these modes.
 
-            if not CodePeer_Mode then
+            if not (CodePeer_Mode or Alfa_Mode) then
                Normalize_Scalars := True;
                Init_Or_Norm_Scalars := True;
             end if;
@@ -11011,9 +11813,9 @@ package body Sem_Prag is
 
                   --  In the context of static code analysis, we do not need
                   --  complex front-end expansions related to pragma Pack,
-                  --  so disable handling of pragma Pack in this case.
+                  --  so disable handling of pragma Pack in these cases.
 
-                  if CodePeer_Mode then
+                  if CodePeer_Mode or Alfa_Mode then
                      null;
 
                   --  Don't attempt any packing for VM targets. We possibly
@@ -11234,8 +12036,8 @@ package body Sem_Prag is
          -- Postcondition --
          -------------------
 
-         --  pragma Postcondition ([Check   =>] Boolean_Expression
-         --                      [,[Message =>] String_Expression]);
+         --  pragma Postcondition ([Check   =>] Boolean_EXPRESSION
+         --                      [,[Message =>] String_EXPRESSION]);
 
          when Pragma_Postcondition => Postcondition : declare
             In_Body : Boolean;
@@ -11257,8 +12059,8 @@ package body Sem_Prag is
          -- Precondition --
          ------------------
 
-         --  pragma Precondition ([Check   =>] Boolean_Expression
-         --                     [,[Message =>] String_Expression]);
+         --  pragma Precondition ([Check   =>] Boolean_EXPRESSION
+         --                     [,[Message =>] String_EXPRESSION]);
 
          when Pragma_Precondition => Precondition : declare
             In_Body : Boolean;
@@ -11662,12 +12464,21 @@ package body Sem_Prag is
 
             declare
                Argx : constant Node_Id := Get_Pragma_Arg (Arg1);
+
             begin
                if Chars (Argx) = Name_Ravenscar then
                   Set_Ravenscar_Profile (N);
+
                elsif Chars (Argx) = Name_Restricted then
                   Set_Profile_Restrictions
-                    (Restricted, N, Warn => Treat_Restrictions_As_Warnings);
+                    (Restricted,
+                     N, Warn => Treat_Restrictions_As_Warnings);
+
+               elsif Chars (Argx) = Name_No_Implementation_Extensions then
+                  Set_Profile_Restrictions
+                    (No_Implementation_Extensions,
+                     N, Warn => Treat_Restrictions_As_Warnings);
+
                else
                   Error_Pragma_Arg ("& is not a valid profile", Argx);
                end if;
@@ -11689,11 +12500,18 @@ package body Sem_Prag is
 
             declare
                Argx : constant Node_Id := Get_Pragma_Arg (Arg1);
+
             begin
                if Chars (Argx) = Name_Ravenscar then
                   Set_Profile_Restrictions (Ravenscar, N, Warn => True);
+
                elsif Chars (Argx) = Name_Restricted then
                   Set_Profile_Restrictions (Restricted, N, Warn => True);
+
+               elsif Chars (Argx) = Name_No_Implementation_Extensions then
+                  Set_Profile_Restrictions
+                    (No_Implementation_Extensions, N, Warn => True);
+
                else
                   Error_Pragma_Arg ("& is not a valid profile", Argx);
                end if;
@@ -11914,6 +12732,47 @@ package body Sem_Prag is
             end if;
          end Pure_05;
 
+         -------------
+         -- Pure_12 --
+         -------------
+
+         --  pragma Pure_12 [(library_unit_NAME)];
+
+         --  This pragma is useable only in GNAT_Mode, where it is used like
+         --  pragma Pure but it is only effective in Ada 2012 mode (otherwise
+         --  it is ignored). It may be used after a pragma Preelaborate, in
+         --  which case it overrides the effect of the pragma Preelaborate.
+         --  This is used to implement AI05-0212 which recategorizes some
+         --  run-time packages in Ada 2012 mode.
+
+         when Pragma_Pure_12 => Pure_12 : declare
+            Ent : Entity_Id;
+
+         begin
+            GNAT_Pragma;
+            Check_Valid_Library_Unit_Pragma;
+
+            if not GNAT_Mode then
+               Error_Pragma ("pragma% only available in GNAT mode");
+            end if;
+
+            if Nkind (N) = N_Null_Statement then
+               return;
+            end if;
+
+            --  This is one of the few cases where we need to test the value of
+            --  Ada_Version_Explicit rather than Ada_Version (which is always
+            --  set to Ada_2012 in a predefined unit), we need to know the
+            --  explicit version set to know if this pragma is active.
+
+            if Ada_Version_Explicit >= Ada_2012 then
+               Ent := Find_Lib_Unit_Name;
+               Set_Is_Preelaborated (Ent, False);
+               Set_Is_Pure (Ent);
+               Set_Suppress_Elaboration_Warnings (Ent);
+            end if;
+         end Pure_12;
+
          -------------------
          -- Pure_Function --
          -------------------
@@ -12060,6 +12919,40 @@ package body Sem_Prag is
             end if;
          end Relative_Deadline;
 
+         ------------------------
+         -- Remote_Access_Type --
+         ------------------------
+
+         --  pragma Remote_Access_Type ([Entity =>] formal_type_LOCAL_NAME);
+
+         when Pragma_Remote_Access_Type => Remote_Access_Type : declare
+            E : Entity_Id;
+
+         begin
+            GNAT_Pragma;
+            Check_Arg_Count (1);
+            Check_Optional_Identifier (Arg1, Name_Entity);
+            Check_Arg_Is_Local_Name (Arg1);
+
+            E := Entity (Get_Pragma_Arg (Arg1));
+
+            if Nkind (Parent (E)) = N_Formal_Type_Declaration
+              and then Ekind (E) = E_General_Access_Type
+              and then Is_Class_Wide_Type (Directly_Designated_Type (E))
+              and then Scope (Root_Type (Directly_Designated_Type (E)))
+                         = Scope (E)
+              and then Is_Valid_Remote_Object_Type
+                         (Root_Type (Directly_Designated_Type (E)))
+            then
+               Set_Is_Remote_Types (E);
+
+            else
+               Error_Pragma_Arg
+                 ("pragma% applies only to formal access to classwide types",
+                  Arg1);
+            end if;
+         end Remote_Access_Type;
+
          ---------------------------
          -- Remote_Call_Interface --
          ---------------------------
@@ -12286,6 +13179,66 @@ package body Sem_Prag is
             Check_Valid_Configuration_Pragma;
             Short_Descriptors := True;
 
+         ------------------------------
+         -- Simple_Storage_Pool_Type --
+         ------------------------------
+
+         --  pragma Simple_Storage_Pool_Type (type_LOCAL_NAME);
+
+         when Pragma_Simple_Storage_Pool_Type =>
+         Simple_Storage_Pool_Type : declare
+            Type_Id : Node_Id;
+            Typ     : Entity_Id;
+
+         begin
+            GNAT_Pragma;
+            Check_Arg_Count (1);
+            Check_Arg_Is_Library_Level_Local_Name (Arg1);
+
+            Type_Id := Get_Pragma_Arg (Arg1);
+            Find_Type (Type_Id);
+            Typ := Entity (Type_Id);
+
+            if Typ = Any_Type then
+               return;
+            end if;
+
+            --  We require the pragma to apply to a type declared in a package
+            --  declaration, but not (immediately) within a package body.
+
+            if Ekind (Current_Scope) /= E_Package
+              or else In_Package_Body (Current_Scope)
+            then
+               Error_Pragma
+                 ("pragma% can only apply to type declared immediately " &
+                  "within a package declaration");
+            end if;
+
+            --  A simple storage pool type must be an immutably limited record
+            --  or private type. If the pragma is given for a private type,
+            --  the full type is similarly restricted (which is checked later
+            --  in Freeze_Entity).
+
+            if Is_Record_Type (Typ)
+              and then not Is_Immutably_Limited_Type (Typ)
+            then
+               Error_Pragma
+                 ("pragma% can only apply to explicitly limited record type");
+
+            elsif Is_Private_Type (Typ) and then not Is_Limited_Type (Typ) then
+               Error_Pragma
+                 ("pragma% can only apply to a private type that is limited");
+
+            elsif not Is_Record_Type (Typ)
+              and then not Is_Private_Type (Typ)
+            then
+               Error_Pragma
+                 ("pragma% can only apply to limited record or private type");
+            end if;
+
+            Record_Rep_Item (Typ, N);
+         end Simple_Storage_Pool_Type;
+
          ----------------------
          -- Source_File_Name --
          ----------------------
@@ -12846,9 +13799,9 @@ package body Sem_Prag is
             end if;
          end;
 
-         --------------
+         ---------------
          -- Task_Info --
-         --------------
+         ---------------
 
          --  pragma Task_Info (EXPRESSION);
 
@@ -12965,6 +13918,52 @@ package body Sem_Prag is
             end if;
          end Task_Storage;
 
+         ---------------
+         -- Test_Case --
+         ---------------
+
+         --  pragma Test_Case ([Name     =>] Static_String_EXPRESSION
+         --                   ,[Mode     =>] MODE_TYPE
+         --                  [, Requires =>  Boolean_EXPRESSION]
+         --                  [, Ensures  =>  Boolean_EXPRESSION]);
+
+         --  MODE_TYPE ::= Nominal | Robustness
+
+         when Pragma_Test_Case => Test_Case : declare
+         begin
+            GNAT_Pragma;
+            Check_At_Least_N_Arguments (2);
+            Check_At_Most_N_Arguments (4);
+            Check_Arg_Order
+                 ((Name_Name, Name_Mode, Name_Requires, Name_Ensures));
+
+            Check_Optional_Identifier (Arg1, Name_Name);
+            Check_Arg_Is_Static_Expression (Arg1, Standard_String);
+
+            --  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
+               Check_Expr_Is_Static_Expression
+                 (Original_Node (Get_Pragma_Arg (Arg1)), Standard_String);
+            end if;
+
+            Check_Optional_Identifier (Arg2, Name_Mode);
+            Check_Arg_Is_One_Of (Arg2, Name_Nominal, Name_Robustness);
+
+            if Arg_Count = 4 then
+               Check_Identifier (Arg3, Name_Requires);
+               Check_Identifier (Arg4, Name_Ensures);
+
+            elsif Arg_Count = 3 then
+               Check_Identifier_Is_One_Of (Arg3, Name_Requires, Name_Ensures);
+            end if;
+
+            Check_Test_Case;
+         end Test_Case;
+
          --------------------------
          -- Thread_Local_Storage --
          --------------------------
@@ -13132,19 +14131,18 @@ package body Sem_Prag is
                Error_Msg_N ("Unchecked_Union must not be tagged", Typ);
                return;
 
-            elsif Is_Limited_Type (Typ) then
+            elsif not Has_Discriminants (Typ) then
                Error_Msg_N
-                 ("Unchecked_Union must not be limited record type", Typ);
-               Explain_Limited_Type (Typ, Typ);
+                ("Unchecked_Union must have one discriminant", Typ);
                return;
 
-            else
-               if not Has_Discriminants (Typ) then
-                  Error_Msg_N
-                    ("Unchecked_Union must have one discriminant", Typ);
-                  return;
-               end if;
+            --  Note: in previous versions of GNAT we used to check for limited
+            --  types and give an error, but in fact the standard does allow
+            --  Unchecked_Union on limited types, so this check was removed.
+
+            --  Proceed with basic error checks completed
 
+            else
                Discr := First_Discriminant (Typ);
                while Present (Discr) loop
                   if No (Discriminant_Default_Value (Discr)) then
@@ -13370,7 +14368,7 @@ package body Sem_Prag is
 
                   if Citem = N then
                      Error_Pragma_Arg
-                       ("argument of pragma% is not with'ed unit", Arg_Node);
+                       ("argument of pragma% is not withed unit", Arg_Node);
                   end if;
 
                   Next (Arg_Node);
@@ -13523,16 +14521,12 @@ package body Sem_Prag is
                end;
 
             elsif Nkind (A) = N_Identifier then
-
                if Chars (A) = Name_All_Checks then
                   Set_Validity_Check_Options ("a");
-
                elsif Chars (A) = Name_On then
                   Validity_Checks_On := True;
-
                elsif Chars (A) = Name_Off then
                   Validity_Checks_On := False;
-
                end if;
             end if;
          end Validity_Checks;
@@ -13653,7 +14647,7 @@ package body Sem_Prag is
                      end;
                   end if;
 
-                  --  Two or more arguments (must be two)
+               --  Two or more arguments (must be two)
 
                else
                   Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off);
@@ -13672,8 +14666,7 @@ package body Sem_Prag is
                      --  the formal may be wrapped in a conversion if the
                      --  actual is a conversion. Retrieve the real entity name.
 
-                     if (In_Instance_Body
-                         or else In_Inlined_Body)
+                     if (In_Instance_Body or In_Inlined_Body)
                        and then Nkind (E_Id) = N_Unchecked_Type_Conversion
                      then
                         E_Id := Expression (E_Id);
@@ -13737,10 +14730,21 @@ package body Sem_Prag is
                         --  In any other case, an error will be signalled (ON
                         --  with no matching OFF).
 
+                        --  Note: We set Used if we are inside a generic to
+                        --  disable the test that the non-config case actually
+                        --  cancels a warning. That's because we can't be sure
+                        --  there isn't an instantiation in some other unit
+                        --  where a warning is suppressed.
+
+                        --  We could do a little better here by checking if the
+                        --  generic unit we are inside is public, but for now
+                        --  we don't bother with that refinement.
+
                         if Chars (Argx) = Name_Off then
                            Set_Specific_Warning_Off
                              (Loc, Name_Buffer (1 .. Name_Len),
-                              Config => Is_Configuration_Pragma);
+                              Config => Is_Configuration_Pragma,
+                              Used   => Inside_A_Generic or else In_Instance);
 
                         elsif Chars (Argx) = Name_On then
                            Set_Specific_Warning_On
@@ -13829,6 +14833,65 @@ package body Sem_Prag is
       when Pragma_Exit => null;
    end Analyze_Pragma;
 
+   -----------------------------
+   -- Analyze_TC_In_Decl_Part --
+   -----------------------------
+
+   procedure Analyze_TC_In_Decl_Part (N : Node_Id; S : Entity_Id) is
+   begin
+      --  Install formals and push subprogram spec onto scope stack so that we
+      --  can see the formals from the pragma.
+
+      Install_Formals (S);
+      Push_Scope (S);
+
+      --  Preanalyze the boolean expressions, we treat these as spec
+      --  expressions (i.e. similar to a default expression).
+
+      Preanalyze_TC_Args (N,
+                          Get_Requires_From_Test_Case_Pragma (N),
+                          Get_Ensures_From_Test_Case_Pragma (N));
+
+      --  Remove the subprogram from the scope stack now that the pre-analysis
+      --  of the expressions in the test-case is done.
+
+      End_Scope;
+   end Analyze_TC_In_Decl_Part;
+
+   --------------------
+   -- Check_Disabled --
+   --------------------
+
+   function Check_Disabled (Nam : Name_Id) return Boolean is
+      PP : Node_Id;
+
+   begin
+      --  Loop through entries in check policy list
+
+      PP := Opt.Check_Policy_List;
+      loop
+         --  If there are no specific entries that matched, then nothing is
+         --  disabled, so return False.
+
+         if No (PP) then
+            return False;
+
+         --  Here we have an entry see if it matches
+
+         else
+            declare
+               PPA : constant List_Id := Pragma_Argument_Associations (PP);
+            begin
+               if Nam = Chars (Get_Pragma_Arg (First (PPA))) then
+                  return Chars (Get_Pragma_Arg (Last (PPA))) = Name_Disable;
+               else
+                  PP := Next_Pragma (PP);
+               end if;
+            end;
+         end if;
+      end loop;
+   end Check_Disabled;
+
    -------------------
    -- Check_Enabled --
    -------------------
@@ -13896,14 +14959,15 @@ package body Sem_Prag is
       --  Follow subprogram renaming chain
 
       Result := Def_Id;
-      while Is_Subprogram (Result)
+
+      if Is_Subprogram (Result)
         and then
           Nkind (Parent (Declaration_Node (Result))) =
                                          N_Subprogram_Renaming_Declaration
         and then Present (Alias (Result))
-      loop
+      then
          Result := Alias (Result);
-      end loop;
+      end if;
 
       return Result;
    end Get_Base_Subprogram;
@@ -13982,7 +15046,8 @@ package body Sem_Prag is
    -----------------------------------------
 
    --  This function makes use of the following static table which indicates
-   --  whether a given pragma is significant.
+   --  whether appearance of some name in a given pragma is to be considered
+   --  as a reference for the purposes of warnings about unreferenced objects.
 
    --  -1  indicates that references in any argument position are significant
    --  0   indicates that appearance in any argument is not significant
@@ -13991,191 +15056,198 @@ package body Sem_Prag is
    --  99  special processing required (e.g. for pragma Check)
 
    Sig_Flags : constant array (Pragma_Id) of Int :=
-     (Pragma_AST_Entry                     => -1,
-      Pragma_Abort_Defer                   => -1,
-      Pragma_Ada_83                        => -1,
-      Pragma_Ada_95                        => -1,
-      Pragma_Ada_05                        => -1,
-      Pragma_Ada_2005                      => -1,
-      Pragma_Ada_12                        => -1,
-      Pragma_Ada_2012                      => -1,
-      Pragma_All_Calls_Remote              => -1,
-      Pragma_Annotate                      => -1,
-      Pragma_Assert                        => -1,
-      Pragma_Assertion_Policy              =>  0,
-      Pragma_Assume_No_Invalid_Values      =>  0,
-      Pragma_Asynchronous                  => -1,
-      Pragma_Atomic                        =>  0,
-      Pragma_Atomic_Components             =>  0,
-      Pragma_Attach_Handler                => -1,
-      Pragma_Check                         => 99,
-      Pragma_Check_Name                    =>  0,
-      Pragma_Check_Policy                  =>  0,
-      Pragma_CIL_Constructor               => -1,
-      Pragma_CPP_Class                     =>  0,
-      Pragma_CPP_Constructor               =>  0,
-      Pragma_CPP_Virtual                   =>  0,
-      Pragma_CPP_Vtable                    =>  0,
-      Pragma_CPU                           => -1,
-      Pragma_C_Pass_By_Copy                =>  0,
-      Pragma_Comment                       =>  0,
-      Pragma_Common_Object                 => -1,
-      Pragma_Compile_Time_Error            => -1,
-      Pragma_Compile_Time_Warning          => -1,
-      Pragma_Compiler_Unit                 =>  0,
-      Pragma_Complete_Representation       =>  0,
-      Pragma_Complex_Representation        =>  0,
-      Pragma_Component_Alignment           => -1,
-      Pragma_Controlled                    =>  0,
-      Pragma_Convention                    =>  0,
-      Pragma_Convention_Identifier         =>  0,
-      Pragma_Debug                         => -1,
-      Pragma_Debug_Policy                  =>  0,
-      Pragma_Detect_Blocking               => -1,
-      Pragma_Default_Storage_Pool          => -1,
-      Pragma_Dimension                     => -1,
-      Pragma_Discard_Names                 =>  0,
-      Pragma_Elaborate                     => -1,
-      Pragma_Elaborate_All                 => -1,
-      Pragma_Elaborate_Body                => -1,
-      Pragma_Elaboration_Checks            => -1,
-      Pragma_Eliminate                     => -1,
-      Pragma_Export                        => -1,
-      Pragma_Export_Exception              => -1,
-      Pragma_Export_Function               => -1,
-      Pragma_Export_Object                 => -1,
-      Pragma_Export_Procedure              => -1,
-      Pragma_Export_Value                  => -1,
-      Pragma_Export_Valued_Procedure       => -1,
-      Pragma_Extend_System                 => -1,
-      Pragma_Extensions_Allowed            => -1,
-      Pragma_External                      => -1,
-      Pragma_Favor_Top_Level               => -1,
-      Pragma_External_Name_Casing          => -1,
-      Pragma_Fast_Math                     => -1,
-      Pragma_Finalize_Storage_Only         =>  0,
-      Pragma_Float_Representation          =>  0,
-      Pragma_Ident                         => -1,
-      Pragma_Implemented                   => -1,
-      Pragma_Implicit_Packing              =>  0,
-      Pragma_Import                        => +2,
-      Pragma_Import_Exception              =>  0,
-      Pragma_Import_Function               =>  0,
-      Pragma_Import_Object                 =>  0,
-      Pragma_Import_Procedure              =>  0,
-      Pragma_Import_Valued_Procedure       =>  0,
-      Pragma_Independent                   =>  0,
-      Pragma_Independent_Components        =>  0,
-      Pragma_Initialize_Scalars            => -1,
-      Pragma_Inline                        =>  0,
-      Pragma_Inline_Always                 =>  0,
-      Pragma_Inline_Generic                =>  0,
-      Pragma_Inspection_Point              => -1,
-      Pragma_Interface                     => +2,
-      Pragma_Interface_Name                => +2,
-      Pragma_Interrupt_Handler             => -1,
-      Pragma_Interrupt_Priority            => -1,
-      Pragma_Interrupt_State               => -1,
-      Pragma_Invariant                     => -1,
-      Pragma_Java_Constructor              => -1,
-      Pragma_Java_Interface                => -1,
-      Pragma_Keep_Names                    =>  0,
-      Pragma_License                       => -1,
-      Pragma_Link_With                     => -1,
-      Pragma_Linker_Alias                  => -1,
-      Pragma_Linker_Constructor            => -1,
-      Pragma_Linker_Destructor             => -1,
-      Pragma_Linker_Options                => -1,
-      Pragma_Linker_Section                => -1,
-      Pragma_List                          => -1,
-      Pragma_Locking_Policy                => -1,
-      Pragma_Long_Float                    => -1,
-      Pragma_Machine_Attribute             => -1,
-      Pragma_Main                          => -1,
-      Pragma_Main_Storage                  => -1,
-      Pragma_Memory_Size                   => -1,
-      Pragma_No_Return                     =>  0,
-      Pragma_No_Body                       =>  0,
-      Pragma_No_Run_Time                   => -1,
-      Pragma_No_Strict_Aliasing            => -1,
-      Pragma_Normalize_Scalars             => -1,
-      Pragma_Obsolescent                   =>  0,
-      Pragma_Optimize                      => -1,
-      Pragma_Optimize_Alignment            => -1,
-      Pragma_Ordered                       =>  0,
-      Pragma_Pack                          =>  0,
-      Pragma_Page                          => -1,
-      Pragma_Passive                       => -1,
-      Pragma_Preelaborable_Initialization  => -1,
-      Pragma_Polling                       => -1,
-      Pragma_Persistent_BSS                =>  0,
-      Pragma_Postcondition                 => -1,
-      Pragma_Precondition                  => -1,
-      Pragma_Predicate                     => -1,
-      Pragma_Preelaborate                  => -1,
-      Pragma_Preelaborate_05               => -1,
-      Pragma_Priority                      => -1,
-      Pragma_Priority_Specific_Dispatching => -1,
-      Pragma_Profile                       =>  0,
-      Pragma_Profile_Warnings              =>  0,
-      Pragma_Propagate_Exceptions          => -1,
-      Pragma_Psect_Object                  => -1,
-      Pragma_Pure                          => -1,
-      Pragma_Pure_05                       => -1,
-      Pragma_Pure_Function                 => -1,
-      Pragma_Queuing_Policy                => -1,
-      Pragma_Ravenscar                     => -1,
-      Pragma_Relative_Deadline             => -1,
-      Pragma_Remote_Call_Interface         => -1,
-      Pragma_Remote_Types                  => -1,
-      Pragma_Restricted_Run_Time           => -1,
-      Pragma_Restriction_Warnings          => -1,
-      Pragma_Restrictions                  => -1,
-      Pragma_Reviewable                    => -1,
-      Pragma_Short_Circuit_And_Or          => -1,
-      Pragma_Share_Generic                 => -1,
-      Pragma_Shared                        => -1,
-      Pragma_Shared_Passive                => -1,
-      Pragma_Short_Descriptors             =>  0,
-      Pragma_Source_File_Name              => -1,
-      Pragma_Source_File_Name_Project      => -1,
-      Pragma_Source_Reference              => -1,
-      Pragma_Storage_Size                  => -1,
-      Pragma_Storage_Unit                  => -1,
-      Pragma_Static_Elaboration_Desired    => -1,
-      Pragma_Stream_Convert                => -1,
-      Pragma_Style_Checks                  => -1,
-      Pragma_Subtitle                      => -1,
-      Pragma_Suppress                      =>  0,
-      Pragma_Suppress_Exception_Locations  =>  0,
-      Pragma_Suppress_All                  => -1,
-      Pragma_Suppress_Debug_Info           =>  0,
-      Pragma_Suppress_Initialization       =>  0,
-      Pragma_System_Name                   => -1,
-      Pragma_Task_Dispatching_Policy       => -1,
-      Pragma_Task_Info                     => -1,
-      Pragma_Task_Name                     => -1,
-      Pragma_Task_Storage                  =>  0,
-      Pragma_Thread_Local_Storage          =>  0,
-      Pragma_Time_Slice                    => -1,
-      Pragma_Title                         => -1,
-      Pragma_Unchecked_Union               =>  0,
-      Pragma_Unimplemented_Unit            => -1,
-      Pragma_Universal_Aliasing            => -1,
-      Pragma_Universal_Data                => -1,
-      Pragma_Unmodified                    => -1,
-      Pragma_Unreferenced                  => -1,
-      Pragma_Unreferenced_Objects          => -1,
-      Pragma_Unreserve_All_Interrupts      => -1,
-      Pragma_Unsuppress                    =>  0,
-      Pragma_Use_VADS_Size                 => -1,
-      Pragma_Validity_Checks               => -1,
-      Pragma_Volatile                      =>  0,
-      Pragma_Volatile_Components           =>  0,
-      Pragma_Warnings                      => -1,
-      Pragma_Weak_External                 => -1,
-      Pragma_Wide_Character_Encoding       =>  0,
-      Unknown_Pragma                       =>  0);
+     (Pragma_AST_Entry                      => -1,
+      Pragma_Abort_Defer                    => -1,
+      Pragma_Ada_83                         => -1,
+      Pragma_Ada_95                         => -1,
+      Pragma_Ada_05                         => -1,
+      Pragma_Ada_2005                       => -1,
+      Pragma_Ada_12                         => -1,
+      Pragma_Ada_2012                       => -1,
+      Pragma_All_Calls_Remote               => -1,
+      Pragma_Annotate                       => -1,
+      Pragma_Assert                         => -1,
+      Pragma_Assertion_Policy               =>  0,
+      Pragma_Assume_No_Invalid_Values       =>  0,
+      Pragma_Asynchronous                   => -1,
+      Pragma_Atomic                         =>  0,
+      Pragma_Atomic_Components              =>  0,
+      Pragma_Attach_Handler                 => -1,
+      Pragma_Check                          => 99,
+      Pragma_Check_Name                     =>  0,
+      Pragma_Check_Policy                   =>  0,
+      Pragma_CIL_Constructor                => -1,
+      Pragma_CPP_Class                      =>  0,
+      Pragma_CPP_Constructor                =>  0,
+      Pragma_CPP_Virtual                    =>  0,
+      Pragma_CPP_Vtable                     =>  0,
+      Pragma_CPU                            => -1,
+      Pragma_C_Pass_By_Copy                 =>  0,
+      Pragma_Comment                        =>  0,
+      Pragma_Common_Object                  => -1,
+      Pragma_Compile_Time_Error             => -1,
+      Pragma_Compile_Time_Warning           => -1,
+      Pragma_Compiler_Unit                  =>  0,
+      Pragma_Complete_Representation        =>  0,
+      Pragma_Complex_Representation         =>  0,
+      Pragma_Component_Alignment            => -1,
+      Pragma_Controlled                     =>  0,
+      Pragma_Convention                     =>  0,
+      Pragma_Convention_Identifier          =>  0,
+      Pragma_Debug                          => -1,
+      Pragma_Debug_Policy                   =>  0,
+      Pragma_Detect_Blocking                => -1,
+      Pragma_Default_Storage_Pool           => -1,
+      Pragma_Disable_Atomic_Synchronization => -1,
+      Pragma_Discard_Names                  =>  0,
+      Pragma_Dispatching_Domain             => -1,
+      Pragma_Elaborate                      => -1,
+      Pragma_Elaborate_All                  => -1,
+      Pragma_Elaborate_Body                 => -1,
+      Pragma_Elaboration_Checks             => -1,
+      Pragma_Eliminate                      => -1,
+      Pragma_Enable_Atomic_Synchronization  => -1,
+      Pragma_Export                         => -1,
+      Pragma_Export_Exception               => -1,
+      Pragma_Export_Function                => -1,
+      Pragma_Export_Object                  => -1,
+      Pragma_Export_Procedure               => -1,
+      Pragma_Export_Value                   => -1,
+      Pragma_Export_Valued_Procedure        => -1,
+      Pragma_Extend_System                  => -1,
+      Pragma_Extensions_Allowed             => -1,
+      Pragma_External                       => -1,
+      Pragma_Favor_Top_Level                => -1,
+      Pragma_External_Name_Casing           => -1,
+      Pragma_Fast_Math                      => -1,
+      Pragma_Finalize_Storage_Only          =>  0,
+      Pragma_Float_Representation           =>  0,
+      Pragma_Ident                          => -1,
+      Pragma_Implementation_Defined         => -1,
+      Pragma_Implemented                    => -1,
+      Pragma_Implicit_Packing               =>  0,
+      Pragma_Import                         => +2,
+      Pragma_Import_Exception               =>  0,
+      Pragma_Import_Function                =>  0,
+      Pragma_Import_Object                  =>  0,
+      Pragma_Import_Procedure               =>  0,
+      Pragma_Import_Valued_Procedure        =>  0,
+      Pragma_Independent                    =>  0,
+      Pragma_Independent_Components         =>  0,
+      Pragma_Initialize_Scalars             => -1,
+      Pragma_Inline                         =>  0,
+      Pragma_Inline_Always                  =>  0,
+      Pragma_Inline_Generic                 =>  0,
+      Pragma_Inspection_Point               => -1,
+      Pragma_Interface                      => +2,
+      Pragma_Interface_Name                 => +2,
+      Pragma_Interrupt_Handler              => -1,
+      Pragma_Interrupt_Priority             => -1,
+      Pragma_Interrupt_State                => -1,
+      Pragma_Invariant                      => -1,
+      Pragma_Java_Constructor               => -1,
+      Pragma_Java_Interface                 => -1,
+      Pragma_Keep_Names                     =>  0,
+      Pragma_License                        => -1,
+      Pragma_Link_With                      => -1,
+      Pragma_Linker_Alias                   => -1,
+      Pragma_Linker_Constructor             => -1,
+      Pragma_Linker_Destructor              => -1,
+      Pragma_Linker_Options                 => -1,
+      Pragma_Linker_Section                 => -1,
+      Pragma_List                           => -1,
+      Pragma_Locking_Policy                 => -1,
+      Pragma_Long_Float                     => -1,
+      Pragma_Machine_Attribute              => -1,
+      Pragma_Main                           => -1,
+      Pragma_Main_Storage                   => -1,
+      Pragma_Memory_Size                    => -1,
+      Pragma_No_Return                      =>  0,
+      Pragma_No_Body                        =>  0,
+      Pragma_No_Run_Time                    => -1,
+      Pragma_No_Strict_Aliasing             => -1,
+      Pragma_Normalize_Scalars              => -1,
+      Pragma_Obsolescent                    =>  0,
+      Pragma_Optimize                       => -1,
+      Pragma_Optimize_Alignment             => -1,
+      Pragma_Ordered                        =>  0,
+      Pragma_Pack                           =>  0,
+      Pragma_Page                           => -1,
+      Pragma_Passive                        => -1,
+      Pragma_Preelaborable_Initialization   => -1,
+      Pragma_Polling                        => -1,
+      Pragma_Persistent_BSS                 =>  0,
+      Pragma_Postcondition                  => -1,
+      Pragma_Precondition                   => -1,
+      Pragma_Predicate                      => -1,
+      Pragma_Preelaborate                   => -1,
+      Pragma_Preelaborate_05                => -1,
+      Pragma_Priority                       => -1,
+      Pragma_Priority_Specific_Dispatching  => -1,
+      Pragma_Profile                        =>  0,
+      Pragma_Profile_Warnings               =>  0,
+      Pragma_Propagate_Exceptions           => -1,
+      Pragma_Psect_Object                   => -1,
+      Pragma_Pure                           => -1,
+      Pragma_Pure_05                        => -1,
+      Pragma_Pure_12                        => -1,
+      Pragma_Pure_Function                  => -1,
+      Pragma_Queuing_Policy                 => -1,
+      Pragma_Ravenscar                      => -1,
+      Pragma_Relative_Deadline              => -1,
+      Pragma_Remote_Access_Type             => -1,
+      Pragma_Remote_Call_Interface          => -1,
+      Pragma_Remote_Types                   => -1,
+      Pragma_Restricted_Run_Time            => -1,
+      Pragma_Restriction_Warnings           => -1,
+      Pragma_Restrictions                   => -1,
+      Pragma_Reviewable                     => -1,
+      Pragma_Short_Circuit_And_Or           => -1,
+      Pragma_Share_Generic                  => -1,
+      Pragma_Shared                         => -1,
+      Pragma_Shared_Passive                 => -1,
+      Pragma_Short_Descriptors              =>  0,
+      Pragma_Simple_Storage_Pool_Type       =>  0,
+      Pragma_Source_File_Name               => -1,
+      Pragma_Source_File_Name_Project       => -1,
+      Pragma_Source_Reference               => -1,
+      Pragma_Storage_Size                   => -1,
+      Pragma_Storage_Unit                   => -1,
+      Pragma_Static_Elaboration_Desired     => -1,
+      Pragma_Stream_Convert                 => -1,
+      Pragma_Style_Checks                   => -1,
+      Pragma_Subtitle                       => -1,
+      Pragma_Suppress                       =>  0,
+      Pragma_Suppress_Exception_Locations   =>  0,
+      Pragma_Suppress_All                   => -1,
+      Pragma_Suppress_Debug_Info            =>  0,
+      Pragma_Suppress_Initialization        =>  0,
+      Pragma_System_Name                    => -1,
+      Pragma_Task_Dispatching_Policy        => -1,
+      Pragma_Task_Info                      => -1,
+      Pragma_Task_Name                      => -1,
+      Pragma_Task_Storage                   =>  0,
+      Pragma_Test_Case                      => -1,
+      Pragma_Thread_Local_Storage           =>  0,
+      Pragma_Time_Slice                     => -1,
+      Pragma_Title                          => -1,
+      Pragma_Unchecked_Union                =>  0,
+      Pragma_Unimplemented_Unit             => -1,
+      Pragma_Universal_Aliasing             => -1,
+      Pragma_Universal_Data                 => -1,
+      Pragma_Unmodified                     => -1,
+      Pragma_Unreferenced                   => -1,
+      Pragma_Unreferenced_Objects           => -1,
+      Pragma_Unreserve_All_Interrupts       => -1,
+      Pragma_Unsuppress                     =>  0,
+      Pragma_Use_VADS_Size                  => -1,
+      Pragma_Validity_Checks                => -1,
+      Pragma_Volatile                       =>  0,
+      Pragma_Volatile_Components            =>  0,
+      Pragma_Warnings                       => -1,
+      Pragma_Weak_External                  => -1,
+      Pragma_Wide_Character_Encoding        =>  0,
+      Unknown_Pragma                        =>  0);
 
    function Is_Non_Significant_Pragma_Reference (N : Node_Id) return Boolean is
       Id : Pragma_Id;
@@ -14297,6 +15369,118 @@ package body Sem_Prag is
       end if;
    end Is_Pragma_String_Literal;
 
+   -----------------------------------------
+   -- Make_Aspect_For_PPC_In_Gen_Sub_Decl --
+   -----------------------------------------
+
+   procedure Make_Aspect_For_PPC_In_Gen_Sub_Decl (Decl : Node_Id) is
+      Aspects : constant List_Id := New_List;
+      Loc     : constant Source_Ptr := Sloc (Decl);
+      Or_Decl : constant Node_Id := Original_Node (Decl);
+
+      Original_Aspects : List_Id;
+      --  To capture global references, a copy of the created aspects must be
+      --  inserted in the original tree.
+
+      Prag         : Node_Id;
+      Prag_Arg_Ass : Node_Id;
+      Prag_Id      : Pragma_Id;
+
+   begin
+      --  Check for any PPC pragmas that appear within Decl
+
+      Prag := Next (Decl);
+      while Nkind (Prag) = N_Pragma loop
+         Prag_Id := Get_Pragma_Id (Chars (Pragma_Identifier (Prag)));
+
+         case Prag_Id is
+            when Pragma_Postcondition | Pragma_Precondition =>
+               Prag_Arg_Ass := First (Pragma_Argument_Associations (Prag));
+
+               --  Make an aspect from any PPC pragma
+
+               Append_To (Aspects,
+                 Make_Aspect_Specification (Loc,
+                   Identifier =>
+                     Make_Identifier (Loc, Chars (Pragma_Identifier (Prag))),
+                   Expression =>
+                     Copy_Separate_Tree (Expression (Prag_Arg_Ass))));
+
+               --  Generate the analysis information in the pragma expression
+               --  and then set the pragma node analyzed to avoid any further
+               --  analysis.
+
+               Analyze (Expression (Prag_Arg_Ass));
+               Set_Analyzed (Prag, True);
+
+            when others => null;
+         end case;
+
+         Next (Prag);
+      end loop;
+
+      --  Set all new aspects into the generic declaration node
+
+      if Is_Non_Empty_List (Aspects) then
+
+         --  Create the list of aspects to be inserted in the original tree
+
+         Original_Aspects := Copy_Separate_List (Aspects);
+
+         --  Check if Decl already has aspects
+
+         --  Attach the new lists of aspects to both the generic copy and the
+         --  original tree.
+
+         if Has_Aspects (Decl) then
+            Append_List (Aspects, Aspect_Specifications (Decl));
+            Append_List (Original_Aspects, Aspect_Specifications (Or_Decl));
+
+         else
+            Set_Parent (Aspects, Decl);
+            Set_Aspect_Specifications (Decl, Aspects);
+            Set_Parent (Original_Aspects, Or_Decl);
+            Set_Aspect_Specifications (Or_Decl, Original_Aspects);
+         end if;
+      end if;
+   end Make_Aspect_For_PPC_In_Gen_Sub_Decl;
+
+   ------------------------
+   -- Preanalyze_TC_Args --
+   ------------------------
+
+   procedure Preanalyze_TC_Args (N, Arg_Req, Arg_Ens : Node_Id) is
+   begin
+      --  Preanalyze the boolean expressions, we treat these as spec
+      --  expressions (i.e. similar to a default expression).
+
+      if Present (Arg_Req) then
+         Preanalyze_Spec_Expression
+           (Get_Pragma_Arg (Arg_Req), Standard_Boolean);
+
+         --  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
+            Preanalyze_Spec_Expression
+              (Original_Node (Get_Pragma_Arg (Arg_Req)), Standard_Boolean);
+         end if;
+      end if;
+
+      if Present (Arg_Ens) then
+         Preanalyze_Spec_Expression
+           (Get_Pragma_Arg (Arg_Ens), Standard_Boolean);
+
+         --  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
+            Preanalyze_Spec_Expression
+              (Original_Node (Get_Pragma_Arg (Arg_Ens)), Standard_Boolean);
+         end if;
+      end if;
+   end Preanalyze_TC_Args;
+
    --------------------------------------
    -- Process_Compilation_Unit_Pragmas --
    --------------------------------------