diff gcc/ada/sem_prag.adb @ 131:84e7813d76e9

gcc-8.2
author mir3636
date Thu, 25 Oct 2018 07:37:49 +0900
parents 04ced10e8804
children 1830386684a0
line wrap: on
line diff
--- a/gcc/ada/sem_prag.adb	Fri Oct 27 22:46:09 2017 +0900
+++ b/gcc/ada/sem_prag.adb	Thu Oct 25 07:37:49 2018 +0900
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2017, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2018, 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- --
@@ -64,6 +64,7 @@
 with Sem_Ch13;  use Sem_Ch13;
 with Sem_Disp;  use Sem_Disp;
 with Sem_Dist;  use Sem_Dist;
+with Sem_Elab;  use Sem_Elab;
 with Sem_Elim;  use Sem_Elim;
 with Sem_Eval;  use Sem_Eval;
 with Sem_Intr;  use Sem_Intr;
@@ -217,7 +218,7 @@
       Freeze_Id   : Entity_Id);
    --  Subsidiary to the analysis of pragmas Contract_Cases, Part_Of, Post, and
    --  Pre. Emit a freezing-related error message where Freeze_Id is the entity
-   --  of a body which caused contract "freezing" and Contract_Id denotes the
+   --  of a body which caused contract freezing and Contract_Id denotes the
    --  entity of the affected contstruct.
 
    procedure Duplication_Error (Prag : Node_Id; Prev : Node_Id);
@@ -432,7 +433,7 @@
 
                --  Emit a clarification message when the case guard contains
                --  at least one undefined reference, possibly due to contract
-               --  "freezing".
+               --  freezing.
 
                if Errors /= Serious_Errors_Detected
                  and then Present (Freeze_Id)
@@ -447,7 +448,7 @@
 
             --  Emit a clarification message when the consequence contains
             --  at least one undefined reference, possibly due to contract
-            --  "freezing".
+            --  freezing.
 
             if Errors /= Serious_Errors_Detected
               and then Present (Freeze_Id)
@@ -467,8 +468,9 @@
 
       CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
 
-      Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
-      --  Save the Ghost mode to restore on exit
+      Saved_GM  : constant Ghost_Mode_Type := Ghost_Mode;
+      Saved_IGR : constant Node_Id         := Ignored_Ghost_Region;
+      --  Save the Ghost-related attributes to restore on exit
 
       CCase         : Node_Id;
       Restore_Scope : Boolean := False;
@@ -535,7 +537,7 @@
 
       Set_Is_Analyzed_Pragma (N);
 
-      Restore_Ghost_Mode (Saved_GM);
+      Restore_Ghost_Region (Saved_GM, Saved_IGR);
    end Analyze_Contract_Cases_In_Decl_Part;
 
    ----------------------------------
@@ -940,6 +942,17 @@
 
                     Ekind_In (Item_Id, E_Abstract_State, E_Variable)
                   then
+                     --  A [generic] function is not allowed to have Output
+                     --  items in its dependency relations. Note that "null"
+                     --  and attribute 'Result are still valid items.
+
+                     if Ekind_In (Spec_Id, E_Function, E_Generic_Function)
+                       and then not Is_Input
+                     then
+                        SPARK_Msg_N
+                          ("output item is not applicable to function", Item);
+                     end if;
+
                      --  The item denotes a concurrent type. Note that single
                      --  protected/task types are not considered here because
                      --  they behave as objects in the context of pragma
@@ -2009,8 +2022,9 @@
      (N        : Node_Id;
       Expr_Val : out Boolean)
    is
-      Arg1     : constant Node_Id := First (Pragma_Argument_Associations (N));
-      Obj_Decl : constant Node_Id := Find_Related_Context (N);
+      Arg1     : constant Node_Id   :=
+                   First (Pragma_Argument_Associations (N));
+      Obj_Decl : constant Node_Id   := Find_Related_Context (N);
       Obj_Id   : constant Entity_Id := Defining_Entity (Obj_Decl);
       Expr     : Node_Id;
 
@@ -2114,10 +2128,10 @@
          procedure Check_Mode_Restriction_In_Enclosing_Context
            (Item    : Node_Id;
             Item_Id : Entity_Id);
-         --  Verify that an item of mode In_Out or Output does not appear as an
-         --  input in the Global aspect of an enclosing subprogram. If this is
-         --  the case, emit an error. Item and Item_Id are respectively the
-         --  item and its entity.
+         --  Verify that an item of mode In_Out or Output does not appear as
+         --  an input in the Global aspect of an enclosing subprogram or task
+         --  unit. If this is the case, emit an error. Item and Item_Id are
+         --  respectively the item and its entity.
 
          procedure Check_Mode_Restriction_In_Function (Mode : Node_Id);
          --  Mode denotes either In_Out or Output. Depending on the kind of the
@@ -2469,16 +2483,28 @@
             Outputs : Elist_Id := No_Elist;
 
          begin
-            --  Traverse the scope stack looking for enclosing subprograms
-            --  subject to pragma [Refined_]Global.
+            --  Traverse the scope stack looking for enclosing subprograms or
+            --  tasks subject to pragma [Refined_]Global.
 
             Context := Scope (Subp_Id);
             while Present (Context) and then Context /= Standard_Standard loop
-               if Is_Subprogram (Context)
+
+               --  For a single task type, retrieve the corresponding object to
+               --  which pragma [Refined_]Global is attached.
+
+               if Ekind (Context) = E_Task_Type
+                 and then Is_Single_Concurrent_Type (Context)
+               then
+                  Context := Anonymous_Object (Context);
+               end if;
+
+               if (Is_Subprogram (Context)
+                     or else Ekind (Context) = E_Task_Type
+                     or else Is_Single_Task_Object (Context))
                  and then
-                   (Present (Get_Pragma (Context, Pragma_Global))
-                      or else
-                    Present (Get_Pragma (Context, Pragma_Refined_Global)))
+                  (Present (Get_Pragma (Context, Pragma_Global))
+                     or else
+                   Present (Get_Pragma (Context, Pragma_Refined_Global)))
                then
                   Collect_Subprogram_Inputs_Outputs
                     (Subp_Id      => Context,
@@ -2487,7 +2513,8 @@
                      Global_Seen  => Dummy);
 
                   --  The item is classified as In_Out or Output but appears as
-                  --  an Input in an enclosing subprogram (SPARK RM 6.1.4(12)).
+                  --  an Input in an enclosing subprogram or task unit (SPARK
+                  --  RM 6.1.4(12)).
 
                   if Appears_In (Inputs, Item_Id)
                     and then not Appears_In (Outputs, Item_Id)
@@ -2496,9 +2523,15 @@
                        ("global item & cannot have mode In_Out or Output",
                         Item, Item_Id);
 
-                     SPARK_Msg_NE
-                       (Fix_Msg (Subp_Id, "\item already appears as input of "
-                        & "subprogram &"), Item, Context);
+                     if Is_Subprogram (Context) then
+                        SPARK_Msg_NE
+                          (Fix_Msg (Subp_Id, "\item already appears as input "
+                           & "of subprogram &"), Item, Context);
+                     else
+                        SPARK_Msg_NE
+                          (Fix_Msg (Subp_Id, "\item already appears as input "
+                           & "of task &"), Item, Context);
+                     end if;
 
                      --  Stop the traversal once an error has been detected
 
@@ -2707,8 +2740,9 @@
       Pack_Id   : constant Entity_Id := Defining_Entity (Pack_Decl);
       Expr      : constant Node_Id   := Expression (Get_Argument (N, Pack_Id));
 
-      Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
-      --  Save the Ghost mode to restore on exit
+      Saved_GM  : constant Ghost_Mode_Type := Ghost_Mode;
+      Saved_IGR : constant Node_Id         := Ignored_Ghost_Region;
+      --  Save the Ghost-related attributes to restore on exit
 
    begin
       --  Do not analyze the pragma multiple times
@@ -2731,7 +2765,7 @@
       Preanalyze_Assert_Expression (Expr, Standard_Boolean);
       Set_Is_Analyzed_Pragma (N);
 
-      Restore_Ghost_Mode (Saved_GM);
+      Restore_Ghost_Region (Saved_GM, Saved_IGR);
    end Analyze_Initial_Condition_In_Decl_Part;
 
    --------------------------------------
@@ -2751,10 +2785,6 @@
       --  A list of all initialization items processed so far. This list is
       --  used to detect duplicate items.
 
-      Non_Null_Seen : Boolean := False;
-      Null_Seen     : Boolean := False;
-      --  Flags used to check the legality of a null initialization list
-
       States_And_Objs : Elist_Id := No_Elist;
       --  A list of all abstract states and objects declared in the visible
       --  declarations of the related package. This list is used to detect the
@@ -2784,91 +2814,67 @@
          Item_Id : Entity_Id;
 
       begin
-         --  Null initialization list
-
-         if Nkind (Item) = N_Null then
-            if Null_Seen then
-               SPARK_Msg_N ("multiple null initializations not allowed", Item);
-
-            elsif Non_Null_Seen then
-               SPARK_Msg_N
-                 ("cannot mix null and non-null initialization items", Item);
-            else
-               Null_Seen := True;
-            end if;
-
-         --  Initialization item
-
-         else
-            Non_Null_Seen := True;
-
-            if Null_Seen then
+         Analyze       (Item);
+         Resolve_State (Item);
+
+         if Is_Entity_Name (Item) then
+            Item_Id := Entity_Of (Item);
+
+            if Present (Item_Id)
+              and then Ekind_In (Item_Id, E_Abstract_State,
+                                          E_Constant,
+                                          E_Variable)
+            then
+               --  When the initialization item is undefined, it appears as
+               --  Any_Id. Do not continue with the analysis of the item.
+
+               if Item_Id = Any_Id then
+                  null;
+
+               --  The state or variable must be declared in the visible
+               --  declarations of the package (SPARK RM 7.1.5(7)).
+
+               elsif not Contains (States_And_Objs, Item_Id) then
+                  Error_Msg_Name_1 := Chars (Pack_Id);
+                  SPARK_Msg_NE
+                    ("initialization item & must appear in the visible "
+                     & "declarations of package %", Item, Item_Id);
+
+               --  Detect a duplicate use of the same initialization item
+               --  (SPARK RM 7.1.5(5)).
+
+               elsif Contains (Items_Seen, Item_Id) then
+                  SPARK_Msg_N ("duplicate initialization item", Item);
+
+               --  The item is legal, add it to the list of processed states
+               --  and variables.
+
+               else
+                  Append_New_Elmt (Item_Id, Items_Seen);
+
+                  if Ekind (Item_Id) = E_Abstract_State then
+                     Append_New_Elmt (Item_Id, States_Seen);
+                  end if;
+
+                  if Present (Encapsulating_State (Item_Id)) then
+                     Append_New_Elmt (Item_Id, Constits_Seen);
+                  end if;
+               end if;
+
+            --  The item references something that is not a state or object
+            --  (SPARK RM 7.1.5(3)).
+
+            else
                SPARK_Msg_N
-                 ("cannot mix null and non-null initialization items", Item);
-            end if;
-
-            Analyze       (Item);
-            Resolve_State (Item);
-
-            if Is_Entity_Name (Item) then
-               Item_Id := Entity_Of (Item);
-
-               if Present (Item_Id)
-                 and then Ekind_In (Item_Id, E_Abstract_State,
-                                             E_Constant,
-                                             E_Variable)
-               then
-                  --  When the initialization item is undefined, it appears as
-                  --  Any_Id. Do not continue with the analysis of the item.
-
-                  if Item_Id = Any_Id then
-                     null;
-
-                  --  The state or variable must be declared in the visible
-                  --  declarations of the package (SPARK RM 7.1.5(7)).
-
-                  elsif not Contains (States_And_Objs, Item_Id) then
-                     Error_Msg_Name_1 := Chars (Pack_Id);
-                     SPARK_Msg_NE
-                       ("initialization item & must appear in the visible "
-                        & "declarations of package %", Item, Item_Id);
-
-                  --  Detect a duplicate use of the same initialization item
-                  --  (SPARK RM 7.1.5(5)).
-
-                  elsif Contains (Items_Seen, Item_Id) then
-                     SPARK_Msg_N ("duplicate initialization item", Item);
-
-                  --  The item is legal, add it to the list of processed states
-                  --  and variables.
-
-                  else
-                     Append_New_Elmt (Item_Id, Items_Seen);
-
-                     if Ekind (Item_Id) = E_Abstract_State then
-                        Append_New_Elmt (Item_Id, States_Seen);
-                     end if;
-
-                     if Present (Encapsulating_State (Item_Id)) then
-                        Append_New_Elmt (Item_Id, Constits_Seen);
-                     end if;
-                  end if;
-
-               --  The item references something that is not a state or object
-               --  (SPARK RM 7.1.5(3)).
-
-               else
-                  SPARK_Msg_N
-                    ("initialization item must denote object or state", Item);
-               end if;
-
-            --  Some form of illegal construct masquerading as a name
-            --  (SPARK RM 7.1.5(3)). This is a syntax error, always report.
-
-            else
-               Error_Msg_N
                  ("initialization item must denote object or state", Item);
             end if;
+
+         --  Some form of illegal construct masquerading as a name
+         --  (SPARK RM 7.1.5(3)). This is a syntax error, always report.
+
+         else
+            Error_Msg_N
+              ("initialization item must denote object or state", Item);
          end if;
       end Analyze_Initialization_Item;
 
@@ -2894,7 +2900,6 @@
 
          procedure Analyze_Input_Item (Input : Node_Id) is
             Input_Id : Entity_Id;
-            Input_OK : Boolean := True;
 
          begin
             --  Null input list
@@ -2935,6 +2940,8 @@
                                                  E_In_Parameter,
                                                  E_In_Out_Parameter,
                                                  E_Out_Parameter,
+                                                 E_Protected_Type,
+                                                 E_Task_Type,
                                                  E_Variable)
                   then
                      --  The input cannot denote states or objects declared
@@ -2960,11 +2967,11 @@
                            null;
 
                         else
-                           Input_OK := False;
                            Error_Msg_Name_1 := Chars (Pack_Id);
                            SPARK_Msg_NE
                              ("input item & cannot denote a visible object or "
                               & "state of package %", Input, Input_Id);
+                           return;
                         end if;
                      end if;
 
@@ -2972,26 +2979,25 @@
                      --  (SPARK RM 7.1.5(5)).
 
                      if Contains (Inputs_Seen, Input_Id) then
-                        Input_OK := False;
                         SPARK_Msg_N ("duplicate input item", Input);
-                     end if;
-
-                     --  Input is legal, add it to the list of processed inputs
-
-                     if Input_OK then
-                        Append_New_Elmt (Input_Id, Inputs_Seen);
-
-                        if Ekind (Input_Id) = E_Abstract_State then
-                           Append_New_Elmt (Input_Id, States_Seen);
-                        end if;
-
-                        if Ekind_In (Input_Id, E_Abstract_State,
-                                               E_Constant,
-                                               E_Variable)
-                          and then Present (Encapsulating_State (Input_Id))
-                        then
-                           Append_New_Elmt (Input_Id, Constits_Seen);
-                        end if;
+                        return;
+                     end if;
+
+                     --  At this point it is known that the input is legal. Add
+                     --  it to the list of processed inputs.
+
+                     Append_New_Elmt (Input_Id, Inputs_Seen);
+
+                     if Ekind (Input_Id) = E_Abstract_State then
+                        Append_New_Elmt (Input_Id, States_Seen);
+                     end if;
+
+                     if Ekind_In (Input_Id, E_Abstract_State,
+                                            E_Constant,
+                                            E_Variable)
+                       and then Present (Encapsulating_State (Input_Id))
+                     then
+                        Append_New_Elmt (Input_Id, Constits_Seen);
                      end if;
 
                   --  The input references something that is not a state or an
@@ -3167,11 +3173,349 @@
       Encap_Id : out Entity_Id;
       Legal    : out Boolean)
    is
-      Encap_Typ   : Entity_Id;
-      Item_Decl   : Node_Id;
-      Pack_Id     : Entity_Id;
-      Placement   : State_Space_Kind;
-      Parent_Unit : Entity_Id;
+      procedure Check_Part_Of_Abstract_State;
+      pragma Inline (Check_Part_Of_Abstract_State);
+      --  Verify the legality of indicator Part_Of when the encapsulator is an
+      --  abstract state.
+
+      procedure Check_Part_Of_Concurrent_Type;
+      pragma Inline (Check_Part_Of_Concurrent_Type);
+      --  Verify the legality of indicator Part_Of when the encapsulator is a
+      --  single concurrent type.
+
+      ----------------------------------
+      -- Check_Part_Of_Abstract_State --
+      ----------------------------------
+
+      procedure Check_Part_Of_Abstract_State is
+         Pack_Id     : Entity_Id;
+         Placement   : State_Space_Kind;
+         Parent_Unit : Entity_Id;
+
+      begin
+         --  Determine where the object, package instantiation or state lives
+         --  with respect to the enclosing packages or package bodies.
+
+         Find_Placement_In_State_Space
+           (Item_Id   => Item_Id,
+            Placement => Placement,
+            Pack_Id   => Pack_Id);
+
+         --  The item appears in a non-package construct with a declarative
+         --  part (subprogram, block, etc). As such, the item is not allowed
+         --  to be a part of an encapsulating state because the item is not
+         --  visible.
+
+         if Placement = Not_In_Package then
+            SPARK_Msg_N
+              ("indicator Part_Of cannot appear in this context "
+               & "(SPARK RM 7.2.6(5))", Indic);
+
+            Error_Msg_Name_1 := Chars (Scope (Encap_Id));
+            SPARK_Msg_NE
+              ("\& is not part of the hidden state of package %",
+               Indic, Item_Id);
+            return;
+
+         --  The item appears in the visible state space of some package. In
+         --  general this scenario does not warrant Part_Of except when the
+         --  package is a nongeneric private child unit and the encapsulating
+         --  state is declared in a parent unit or a public descendant of that
+         --  parent unit.
+
+         elsif Placement = Visible_State_Space then
+            if Is_Child_Unit (Pack_Id)
+              and then not Is_Generic_Unit (Pack_Id)
+              and then Is_Private_Descendant (Pack_Id)
+            then
+               --  A variable or state abstraction which is part of the visible
+               --  state of a nongeneric private child unit or its public
+               --  descendants must have its Part_Of indicator specified. The
+               --  Part_Of indicator must denote a state declared by either the
+               --  parent unit of the private unit or by a public descendant of
+               --  that parent unit.
+
+               --  Find the nearest private ancestor (which can be the current
+               --  unit itself).
+
+               Parent_Unit := Pack_Id;
+               while Present (Parent_Unit) loop
+                  exit when
+                    Private_Present
+                      (Parent (Unit_Declaration_Node (Parent_Unit)));
+                  Parent_Unit := Scope (Parent_Unit);
+               end loop;
+
+               Parent_Unit := Scope (Parent_Unit);
+
+               if not Is_Child_Or_Sibling (Pack_Id, Scope (Encap_Id)) then
+                  SPARK_Msg_NE
+                    ("indicator Part_Of must denote abstract state of & or of "
+                     & "its public descendant (SPARK RM 7.2.6(3))",
+                     Indic, Parent_Unit);
+                  return;
+
+               elsif Scope (Encap_Id) = Parent_Unit
+                 or else
+                   (Is_Ancestor_Package (Parent_Unit, Scope (Encap_Id))
+                     and then not Is_Private_Descendant (Scope (Encap_Id)))
+               then
+                  null;
+
+               else
+                  SPARK_Msg_NE
+                    ("indicator Part_Of must denote abstract state of & or of "
+                     & "its public descendant (SPARK RM 7.2.6(3))",
+                     Indic, Parent_Unit);
+                  return;
+               end if;
+
+            --  Indicator Part_Of is not needed when the related package is
+            --  not a nongeneric private child unit or a public descendant
+            --  thereof.
+
+            else
+               SPARK_Msg_N
+                 ("indicator Part_Of cannot appear in this context "
+                  & "(SPARK RM 7.2.6(5))", Indic);
+
+               Error_Msg_Name_1 := Chars (Pack_Id);
+               SPARK_Msg_NE
+                 ("\& is declared in the visible part of package %",
+                  Indic, Item_Id);
+               return;
+            end if;
+
+         --  When the item appears in the private state space of a package, the
+         --  encapsulating state must be declared in the same package.
+
+         elsif Placement = Private_State_Space then
+            if Scope (Encap_Id) /= Pack_Id then
+               SPARK_Msg_NE
+                 ("indicator Part_Of must denote an abstract state of "
+                  & "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id);
+
+               Error_Msg_Name_1 := Chars (Pack_Id);
+               SPARK_Msg_NE
+                 ("\& is declared in the private part of package %",
+                  Indic, Item_Id);
+               return;
+            end if;
+
+         --  Items declared in the body state space of a package do not need
+         --  Part_Of indicators as the refinement has already been seen.
+
+         else
+            SPARK_Msg_N
+              ("indicator Part_Of cannot appear in this context "
+               & "(SPARK RM 7.2.6(5))", Indic);
+
+            if Scope (Encap_Id) = Pack_Id then
+               Error_Msg_Name_1 := Chars (Pack_Id);
+               SPARK_Msg_NE
+                 ("\& is declared in the body of package %", Indic, Item_Id);
+            end if;
+
+            return;
+         end if;
+
+         --  At this point it is known that the Part_Of indicator is legal
+
+         Legal := True;
+      end Check_Part_Of_Abstract_State;
+
+      -----------------------------------
+      -- Check_Part_Of_Concurrent_Type --
+      -----------------------------------
+
+      procedure Check_Part_Of_Concurrent_Type is
+         function In_Proper_Order
+           (First  : Node_Id;
+            Second : Node_Id) return Boolean;
+         pragma Inline (In_Proper_Order);
+         --  Determine whether node First precedes node Second
+
+         procedure Placement_Error;
+         pragma Inline (Placement_Error);
+         --  Emit an error concerning the illegal placement of the item with
+         --  respect to the single concurrent type.
+
+         ---------------------
+         -- In_Proper_Order --
+         ---------------------
+
+         function In_Proper_Order
+           (First  : Node_Id;
+            Second : Node_Id) return Boolean
+         is
+            N : Node_Id;
+
+         begin
+            if List_Containing (First) = List_Containing (Second) then
+               N := First;
+               while Present (N) loop
+                  if N = Second then
+                     return True;
+                  end if;
+
+                  Next (N);
+               end loop;
+            end if;
+
+            return False;
+         end In_Proper_Order;
+
+         ---------------------
+         -- Placement_Error --
+         ---------------------
+
+         procedure Placement_Error is
+         begin
+            SPARK_Msg_N
+              ("indicator Part_Of must denote a previously declared single "
+               & "protected type or single task type", Encap);
+         end Placement_Error;
+
+         --  Local variables
+
+         Conc_Typ      : constant Entity_Id := Etype (Encap_Id);
+         Encap_Decl    : constant Node_Id   := Declaration_Node (Encap_Id);
+         Encap_Context : constant Node_Id   := Parent (Encap_Decl);
+
+         Item_Context : Node_Id;
+         Item_Decl    : Node_Id;
+         Prv_Decls    : List_Id;
+         Vis_Decls    : List_Id;
+
+      --  Start of processing for Check_Part_Of_Concurrent_Type
+
+      begin
+         --  Only abstract states and variables can act as constituents of an
+         --  encapsulating single concurrent type.
+
+         if Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
+            null;
+
+         --  The constituent is a constant
+
+         elsif Ekind (Item_Id) = E_Constant then
+            Error_Msg_Name_1 := Chars (Encap_Id);
+            SPARK_Msg_NE
+              (Fix_Msg (Conc_Typ, "constant & cannot act as constituent of "
+               & "single protected type %"), Indic, Item_Id);
+            return;
+
+         --  The constituent is a package instantiation
+
+         else
+            Error_Msg_Name_1 := Chars (Encap_Id);
+            SPARK_Msg_NE
+              (Fix_Msg (Conc_Typ, "package instantiation & cannot act as "
+               & "constituent of single protected type %"), Indic, Item_Id);
+            return;
+         end if;
+
+         --  When the item denotes an abstract state of a nested package, use
+         --  the declaration of the package to detect proper placement.
+
+         --    package Pack is
+         --       task T;
+         --       package Nested
+         --         with Abstract_State => (State with Part_Of => T)
+
+         if Ekind (Item_Id) = E_Abstract_State then
+            Item_Decl := Unit_Declaration_Node (Scope (Item_Id));
+         else
+            Item_Decl := Declaration_Node (Item_Id);
+         end if;
+
+         Item_Context := Parent (Item_Decl);
+
+         --  The item and the single concurrent type must appear in the same
+         --  declarative region, with the item following the declaration of
+         --  the single concurrent type (SPARK RM 9(3)).
+
+         if Item_Context = Encap_Context then
+            if Nkind_In (Item_Context, N_Package_Specification,
+                                       N_Protected_Definition,
+                                       N_Task_Definition)
+            then
+               Prv_Decls := Private_Declarations (Item_Context);
+               Vis_Decls := Visible_Declarations (Item_Context);
+
+               --  The placement is OK when the single concurrent type appears
+               --  within the visible declarations and the item in the private
+               --  declarations.
+               --
+               --    package Pack is
+               --       protected PO ...
+               --    private
+               --       Constit : ... with Part_Of => PO;
+               --    end Pack;
+
+               if List_Containing (Encap_Decl) = Vis_Decls
+                 and then List_Containing (Item_Decl) = Prv_Decls
+               then
+                  null;
+
+               --  The placement is illegal when the item appears within the
+               --  visible declarations and the single concurrent type is in
+               --  the private declarations.
+               --
+               --    package Pack is
+               --       Constit : ... with Part_Of => PO;
+               --    private
+               --       protected PO ...
+               --    end Pack;
+
+               elsif List_Containing (Item_Decl) = Vis_Decls
+                 and then List_Containing (Encap_Decl) = Prv_Decls
+               then
+                  Placement_Error;
+                  return;
+
+               --  Otherwise both the item and the single concurrent type are
+               --  in the same list. Ensure that the declaration of the single
+               --  concurrent type precedes that of the item.
+
+               elsif not In_Proper_Order
+                           (First  => Encap_Decl,
+                            Second => Item_Decl)
+               then
+                  Placement_Error;
+                  return;
+               end if;
+
+            --  Otherwise both the item and the single concurrent type are
+            --  in the same list. Ensure that the declaration of the single
+            --  concurrent type precedes that of the item.
+
+            elsif not In_Proper_Order
+                        (First  => Encap_Decl,
+                         Second => Item_Decl)
+            then
+               Placement_Error;
+               return;
+            end if;
+
+         --  Otherwise the item and the single concurrent type reside within
+         --  unrelated regions.
+
+         else
+            Error_Msg_Name_1 := Chars (Encap_Id);
+            SPARK_Msg_NE
+              (Fix_Msg (Conc_Typ, "constituent & must be declared "
+               & "immediately within the same region as single protected "
+               & "type %"), Indic, Item_Id);
+            return;
+         end if;
+
+         --  At this point it is known that the Part_Of indicator is legal
+
+         Legal := True;
+      end Check_Part_Of_Concurrent_Type;
+
+   --  Start of processing for Analyze_Part_Of
 
    begin
       --  Assume that the indicator is illegal
@@ -3231,230 +3575,13 @@
       --  The encapsulator is an abstract state
 
       if Ekind (Encap_Id) = E_Abstract_State then
-
-         --  Determine where the object, package instantiation or state lives
-         --  with respect to the enclosing packages or package bodies.
-
-         Find_Placement_In_State_Space
-           (Item_Id   => Item_Id,
-            Placement => Placement,
-            Pack_Id   => Pack_Id);
-
-         --  The item appears in a non-package construct with a declarative
-         --  part (subprogram, block, etc). As such, the item is not allowed
-         --  to be a part of an encapsulating state because the item is not
-         --  visible.
-
-         if Placement = Not_In_Package then
-            SPARK_Msg_N
-              ("indicator Part_Of cannot appear in this context "
-               & "(SPARK RM 7.2.6(5))", Indic);
-            Error_Msg_Name_1 := Chars (Scope (Encap_Id));
-            SPARK_Msg_NE
-              ("\& is not part of the hidden state of package %",
-               Indic, Item_Id);
-            return;
-
-         --  The item appears in the visible state space of some package. In
-         --  general this scenario does not warrant Part_Of except when the
-         --  package is a private child unit and the encapsulating state is
-         --  declared in a parent unit or a public descendant of that parent
-         --  unit.
-
-         elsif Placement = Visible_State_Space then
-            if Is_Child_Unit (Pack_Id)
-              and then Is_Private_Descendant (Pack_Id)
-            then
-               --  A variable or state abstraction which is part of the visible
-               --  state of a private child unit (or one of its public
-               --  descendants) must have its Part_Of indicator specified. The
-               --  Part_Of indicator must denote a state abstraction declared
-               --  by either the parent unit of the private unit or by a public
-               --  descendant of that parent unit.
-
-               --  Find nearest private ancestor (which can be the current unit
-               --  itself).
-
-               Parent_Unit := Pack_Id;
-               while Present (Parent_Unit) loop
-                  exit when
-                    Private_Present
-                      (Parent (Unit_Declaration_Node (Parent_Unit)));
-                  Parent_Unit := Scope (Parent_Unit);
-               end loop;
-
-               Parent_Unit := Scope (Parent_Unit);
-
-               if not Is_Child_Or_Sibling (Pack_Id, Scope (Encap_Id)) then
-                  SPARK_Msg_NE
-                    ("indicator Part_Of must denote abstract state or public "
-                     & "descendant of & (SPARK RM 7.2.6(3))",
-                     Indic, Parent_Unit);
-                  return;
-
-               elsif Scope (Encap_Id) = Parent_Unit
-                 or else
-                   (Is_Ancestor_Package (Parent_Unit, Scope (Encap_Id))
-                     and then not Is_Private_Descendant (Scope (Encap_Id)))
-               then
-                  null;
-
-               else
-                  SPARK_Msg_NE
-                    ("indicator Part_Of must denote abstract state or public "
-                     & "descendant of & (SPARK RM 7.2.6(3))",
-                     Indic, Parent_Unit);
-                  return;
-               end if;
-
-            --  Indicator Part_Of is not needed when the related package is not
-            --  a private child unit or a public descendant thereof.
-
-            else
-               SPARK_Msg_N
-                 ("indicator Part_Of cannot appear in this context "
-                  & "(SPARK RM 7.2.6(5))", Indic);
-               Error_Msg_Name_1 := Chars (Pack_Id);
-               SPARK_Msg_NE
-                 ("\& is declared in the visible part of package %",
-                  Indic, Item_Id);
-               return;
-            end if;
-
-         --  When the item appears in the private state space of a package, the
-         --  encapsulating state must be declared in the same package.
-
-         elsif Placement = Private_State_Space then
-            if Scope (Encap_Id) /= Pack_Id then
-               SPARK_Msg_NE
-                 ("indicator Part_Of must designate an abstract state of "
-                  & "package & (SPARK RM 7.2.6(2))", Indic, Pack_Id);
-               Error_Msg_Name_1 := Chars (Pack_Id);
-               SPARK_Msg_NE
-                 ("\& is declared in the private part of package %",
-                  Indic, Item_Id);
-               return;
-            end if;
-
-         --  Items declared in the body state space of a package do not need
-         --  Part_Of indicators as the refinement has already been seen.
-
-         else
-            SPARK_Msg_N
-              ("indicator Part_Of cannot appear in this context "
-               & "(SPARK RM 7.2.6(5))", Indic);
-
-            if Scope (Encap_Id) = Pack_Id then
-               Error_Msg_Name_1 := Chars (Pack_Id);
-               SPARK_Msg_NE
-                 ("\& is declared in the body of package %", Indic, Item_Id);
-            end if;
-
-            return;
-         end if;
+         Check_Part_Of_Abstract_State;
 
       --  The encapsulator is a single concurrent type
 
       else
-         Encap_Typ := Etype (Encap_Id);
-
-         --  Only abstract states and variables can act as constituents of an
-         --  encapsulating single concurrent type.
-
-         if Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
-            null;
-
-         --  The constituent is a constant
-
-         elsif Ekind (Item_Id) = E_Constant then
-            Error_Msg_Name_1 := Chars (Encap_Id);
-            SPARK_Msg_NE
-              (Fix_Msg (Encap_Typ, "constant & cannot act as constituent of "
-               & "single protected type %"), Indic, Item_Id);
-            return;
-
-         --  The constituent is a package instantiation
-
-         else
-            Error_Msg_Name_1 := Chars (Encap_Id);
-            SPARK_Msg_NE
-              (Fix_Msg (Encap_Typ, "package instantiation & cannot act as "
-               & "constituent of single protected type %"), Indic, Item_Id);
-            return;
-         end if;
-
-         --  When the item denotes an abstract state of a nested package, use
-         --  the declaration of the package to detect proper placement.
-
-         --    package Pack is
-         --       task T;
-         --       package Nested
-         --         with Abstract_State => (State with Part_Of => T)
-
-         if Ekind (Item_Id) = E_Abstract_State then
-            Item_Decl := Unit_Declaration_Node (Scope (Item_Id));
-         else
-            Item_Decl := Declaration_Node (Item_Id);
-         end if;
-
-         --  Both the item and its encapsulating single concurrent type must
-         --  appear in the same declarative region (SPARK RM 9.3). Note that
-         --  privacy is ignored.
-
-         if Parent (Item_Decl) /= Parent (Declaration_Node (Encap_Id)) then
-            Error_Msg_Name_1 := Chars (Encap_Id);
-            SPARK_Msg_NE
-              (Fix_Msg (Encap_Typ, "constituent & must be declared "
-               & "immediately within the same region as single protected "
-               & "type %"), Indic, Item_Id);
-            return;
-         end if;
-
-         --  The declaration of the item should follow the declaration of its
-         --  encapsulating single concurrent type and must appear in the same
-         --  declarative region (SPARK RM 9.3).
-
-         declare
-            N : Node_Id;
-
-         begin
-            N := Next (Declaration_Node (Encap_Id));
-            while Present (N) loop
-               exit when N = Item_Decl;
-               Next (N);
-            end loop;
-
-            --  The single concurrent type might be in the visible part of a
-            --  package, and the declaration of the item in the private part
-            --  of the same package.
-
-            if No (N) then
-               declare
-                  Pack : constant Node_Id :=
-                           Parent (Declaration_Node (Encap_Id));
-               begin
-                  if Nkind (Pack) = N_Package_Specification
-                    and then not In_Private_Part (Encap_Id)
-                  then
-                     N := First (Private_Declarations (Pack));
-                     while Present (N) loop
-                        exit when N = Item_Decl;
-                        Next (N);
-                     end loop;
-                  end if;
-               end;
-            end if;
-
-            if No (N) then
-               SPARK_Msg_N
-                 ("indicator Part_Of must denote a previously declared "
-                  & "single protected type or single task type", Encap);
-               return;
-            end if;
-         end;
-      end if;
-
-      Legal := True;
+         Check_Part_Of_Concurrent_Type;
+      end if;
    end Analyze_Part_Of;
 
    ----------------------------------
@@ -3510,7 +3637,7 @@
       end if;
 
       --  Emit a clarification message when the encapsulator is undefined,
-      --  possibly due to contract "freezing".
+      --  possibly due to contract freezing.
 
       if Errors /= Serious_Errors_Detected
         and then Present (Freeze_Id)
@@ -3558,6 +3685,12 @@
       -- Local Subprograms --
       -----------------------
 
+      function Acc_First (N : Node_Id) return Node_Id;
+      --  Helper function to iterate over arguments given to OpenAcc pragmas
+
+      function Acc_Next (N : Node_Id) return Node_Id;
+      --  Helper function to iterate over arguments given to OpenAcc pragmas
+
       procedure Acquire_Warning_Match_String (Arg : Node_Id);
       --  Used by pragma Warnings (Off, string), and Warn_As_Error (string) to
       --  get the given string argument, and place it in Name_Buffer, adding
@@ -4107,6 +4240,89 @@
       --  which is used for error messages on any constructs violating the
       --  profile.
 
+      procedure Validate_Acc_Condition_Clause (Clause : Node_Id);
+      --  Make sure the argument of a given Acc_If clause is a Boolean
+
+      procedure Validate_Acc_Data_Clause (Clause : Node_Id);
+      --  Make sure the argument of an OpenAcc data clause (e.g. Copy, Copyin,
+      --  Copyout...) is an identifier or an aggregate of identifiers.
+
+      procedure Validate_Acc_Int_Expr_Clause (Clause : Node_Id);
+      --  Make sure the argument of an OpenAcc clause is an Integer expression
+
+      procedure Validate_Acc_Int_Expr_List_Clause (Clause : Node_Id);
+      --  Make sure the argument of an OpenAcc clause is an Integer expression
+      --  or a list of Integer expressions.
+
+      procedure Validate_Acc_Loop_Collapse (Clause : Node_Id);
+      --  Make sure that the parent loop of the Acc_Loop(Collapse => N) pragma
+      --  contains at least N-1 nested loops.
+
+      procedure Validate_Acc_Loop_Gang (Clause : Node_Id);
+      --  Make sure the argument of the Gang clause of a Loop directive is
+      --  either an integer expression or a (Static => integer expressions)
+      --  aggregate.
+
+      procedure Validate_Acc_Loop_Vector (Clause : Node_Id);
+      --  When this procedure is called in a construct offloaded by an
+      --  Acc_Kernels pragma, makes sure that a Vector_Length clause does
+      --  not exist on said pragma. In all cases, make sure the argument
+      --  is an Integer expression.
+
+      procedure Validate_Acc_Loop_Worker (Clause : Node_Id);
+      --  When this procedure is called in a construct offloaded by an
+      --  Acc_Parallel pragma, makes sure that no argument has been given.
+      --  When this procedure is called in a construct offloaded by an
+      --  Acc_Kernels pragma and if Loop_Worker was given an argument,
+      --  makes sure that the Num_Workers clause does not appear on the
+      --  Acc_Kernels pragma and that the argument is an integer.
+
+      procedure Validate_Acc_Name_Reduction (Clause : Node_Id);
+      --  Make sure the reduction clause is an aggregate made of a string
+      --  representing a supported reduction operation (i.e. "+", "*", "and",
+      --  "or", "min" or "max") and either an identifier or aggregate of
+      --  identifiers.
+
+      procedure Validate_Acc_Size_Expressions (Clause : Node_Id);
+      --  Makes sure that Clause is either an integer expression or an
+      --  association with a Static as name and a list of integer expressions
+      --  or "*" strings on the right hand side.
+
+      ---------------
+      -- Acc_First --
+      ---------------
+
+      function Acc_First (N : Node_Id) return Node_Id is
+      begin
+         if Nkind (N) = N_Aggregate then
+            if Present (Expressions (N)) then
+               return First (Expressions (N));
+
+            elsif Present (Component_Associations (N)) then
+               return Expression (First (Component_Associations (N)));
+            end if;
+         end if;
+
+         return N;
+      end Acc_First;
+
+      --------------
+      -- Acc_Next --
+      --------------
+
+      function Acc_Next (N : Node_Id) return Node_Id is
+      begin
+         if Nkind (Parent (N)) = N_Component_Association then
+            return Expression (Next (Parent (N)));
+
+         elsif Nkind (Parent (N)) = N_Aggregate then
+            return Next (N);
+
+         else
+            return Empty;
+         end if;
+      end Acc_Next;
+
       ----------------------------------
       -- Acquire_Warning_Match_String --
       ----------------------------------
@@ -4340,7 +4556,9 @@
                if Present (Cont) then
                   Prag := Pre_Post_Conditions (Cont);
                   while Present (Prag) loop
-                     if Class_Present (Prag) then
+                     if Pragma_Name (Prag) = Name_Precondition
+                       and then Class_Present (Prag)
+                     then
                         return True;
                      end if;
 
@@ -4617,27 +4835,12 @@
 
          Body_Decl := Find_Related_Declaration_Or_Body (N, Do_Checks => True);
 
-         --  Entry body
-
-         if Nkind (Body_Decl) = N_Entry_Body then
-            null;
-
-         --  Subprogram body
-
-         elsif Nkind (Body_Decl) = N_Subprogram_Body then
-            null;
-
-         --  Subprogram body stub
-
-         elsif Nkind (Body_Decl) = N_Subprogram_Body_Stub then
-            null;
-
-         --  Task body
-
-         elsif Nkind (Body_Decl) = N_Task_Body then
-            null;
-
-         else
+         if not Nkind_In (Body_Decl, N_Entry_Body,
+                                     N_Subprogram_Body,
+                                     N_Subprogram_Body_Stub,
+                                     N_Task_Body,
+                                     N_Task_Body_Stub)
+         then
             Pragma_Misplaced;
             return;
          end if;
@@ -4812,9 +5015,9 @@
          end loop;
       end Analyze_Unmodified_Or_Unused;
 
-      -----------------------------------
-      -- Analyze_Unreference_Or_Unused --
-      -----------------------------------
+      ------------------------------------
+      -- Analyze_Unreferenced_Or_Unused --
+      ------------------------------------
 
       procedure Analyze_Unreferenced_Or_Unused
         (Is_Unused : Boolean := False)
@@ -5817,8 +6020,8 @@
 
             procedure Check_Grouping (L : List_Id) is
                HSS  : Node_Id;
-               Prag : Node_Id;
                Stmt : Node_Id;
+               Prag : Node_Id := Empty; -- init to avoid warning
 
             begin
                --  Inspect the list of declarations or statements looking for
@@ -5838,23 +6041,9 @@
                Stmt := First (L);
                while Present (Stmt) loop
 
-                  --  Pragmas Loop_Invariant and Loop_Variant may only appear
-                  --  inside a loop or a block housed inside a loop. Inspect
-                  --  the declarations and statements of the block as they may
-                  --  contain the first grouping.
-
-                  if Nkind (Stmt) = N_Block_Statement then
-                     HSS := Handled_Statement_Sequence (Stmt);
-
-                     Check_Grouping (Declarations (Stmt));
-
-                     if Present (HSS) then
-                        Check_Grouping (Statements (HSS));
-                     end if;
-
                   --  First pragma of the first topmost grouping has been found
 
-                  elsif Is_Loop_Pragma (Stmt) then
+                  if Is_Loop_Pragma (Stmt) then
 
                      --  The group and the current pragma are not in the same
                      --  declarative or statement list.
@@ -5872,24 +6061,28 @@
 
                      else
                         while Present (Stmt) loop
-
                            --  The current pragma is either the first pragma
-                           --  of the group or is a member of the group. Stop
-                           --  the search as the placement is legal.
+                           --  of the group or is a member of the group.
+                           --  Stop the search as the placement is legal.
 
                            if Stmt = N then
                               raise Stop_Search;
 
-                           --  Skip group members, but keep track of the last
-                           --  pragma in the group.
+                           --  Skip group members, but keep track of the
+                           --  last pragma in the group.
 
                            elsif Is_Loop_Pragma (Stmt) then
                               Prag := Stmt;
 
                            --  Skip declarations and statements generated by
-                           --  the compiler during expansion.
-
-                           elsif not Comes_From_Source (Stmt) then
+                           --  the compiler during expansion. Note that some
+                           --  source statements (e.g. pragma Assert) may have
+                           --  been transformed so that they do not appear as
+                           --  coming from source anymore, so we instead look
+                           --  at their Original_Node.
+
+                           elsif not Comes_From_Source (Original_Node (Stmt))
+                           then
                               null;
 
                            --  A non-pragma is separating the group from the
@@ -5907,6 +6100,24 @@
 
                         raise Program_Error;
                      end if;
+
+                  --  Pragmas Loop_Invariant and Loop_Variant may only appear
+                  --  inside a loop or a block housed inside a loop. Inspect
+                  --  the declarations and statements of the block as they may
+                  --  contain the first grouping. This case follows the one for
+                  --  loop pragmas, as block statements which originate in a
+                  --  loop pragma (and so Is_Loop_Pragma will return True on
+                  --  that block statement) should be treated in the previous
+                  --  case.
+
+                  elsif Nkind (Stmt) = N_Block_Statement then
+                     HSS := Handled_Statement_Sequence (Stmt);
+
+                     Check_Grouping (Declarations (Stmt));
+
+                     if Present (HSS) then
+                        Check_Grouping (Statements (HSS));
+                     end if;
                   end if;
 
                   Next (Stmt);
@@ -7302,9 +7513,11 @@
 
          if SPARK_Mode = On
            and then Prag_Id = Pragma_Volatile
-           and then
-             not Nkind_In (Original_Node (Decl), N_Full_Type_Declaration,
-                                                 N_Object_Declaration)
+           and then not Nkind_In (Original_Node (Decl),
+                                  N_Full_Type_Declaration,
+                                  N_Object_Declaration,
+                                  N_Single_Protected_Declaration,
+                                  N_Single_Task_Declaration)
          then
             Error_Pragma_Arg
               ("argument of pragma % must denote a full type or object "
@@ -7357,6 +7570,17 @@
       --  Start of processing for Process_Compile_Time_Warning_Or_Error
 
       begin
+         --  In GNATprove mode, pragmas Compile_Time_Error and
+         --  Compile_Time_Warning are ignored, as the analyzer may not have the
+         --  same information as the compiler (in particular regarding size of
+         --  objects decided in gigi) so it makes no sense to issue an error or
+         --  warning in GNATprove.
+
+         if GNATprove_Mode then
+            Rewrite (N, Make_Null_Statement (Loc));
+            return;
+         end if;
+
          Check_Arg_Count (2);
          Check_No_Identifiers;
          Check_Arg_Is_OK_Static_Expression (Arg2, Standard_String);
@@ -10707,9 +10931,9 @@
          pragma No_Return (Bad_Mechanism);
          --  Signal bad mechanism name
 
-         -------------------------
-         -- Bad_Mechanism_Value --
-         -------------------------
+         -------------------
+         -- Bad_Mechanism --
+         -------------------
 
          procedure Bad_Mechanism is
          begin
@@ -10958,6 +11182,308 @@
          end if;
       end Set_Ravenscar_Profile;
 
+      -----------------------------------
+      -- Validate_Acc_Condition_Clause --
+      -----------------------------------
+
+      procedure Validate_Acc_Condition_Clause (Clause : Node_Id) is
+      begin
+         Analyze_And_Resolve (Clause);
+
+         if not Is_Boolean_Type (Etype (Clause)) then
+            Error_Pragma ("expected a boolean");
+         end if;
+      end Validate_Acc_Condition_Clause;
+
+      ------------------------------
+      -- Validate_Acc_Data_Clause --
+      ------------------------------
+
+      procedure Validate_Acc_Data_Clause (Clause : Node_Id) is
+         Expr : Node_Id;
+
+      begin
+         Expr := Acc_First (Clause);
+         while Present (Expr) loop
+            if Nkind (Expr) /= N_Identifier then
+               Error_Pragma ("expected an identifer");
+            end if;
+
+            Analyze_And_Resolve (Expr);
+
+            Expr := Acc_Next (Expr);
+         end loop;
+      end Validate_Acc_Data_Clause;
+
+      ----------------------------------
+      -- Validate_Acc_Int_Expr_Clause --
+      ----------------------------------
+
+      procedure Validate_Acc_Int_Expr_Clause (Clause : Node_Id) is
+      begin
+         Analyze_And_Resolve (Clause);
+
+         if not Is_Integer_Type (Etype (Clause)) then
+            Error_Pragma_Arg ("expected an integer", Clause);
+         end if;
+      end Validate_Acc_Int_Expr_Clause;
+
+      ---------------------------------------
+      -- Validate_Acc_Int_Expr_List_Clause --
+      ---------------------------------------
+
+      procedure Validate_Acc_Int_Expr_List_Clause (Clause : Node_Id) is
+         Expr : Node_Id;
+
+      begin
+         Expr := Acc_First (Clause);
+         while Present (Expr) loop
+            Analyze_And_Resolve (Expr);
+
+            if not Is_Integer_Type (Etype (Expr)) then
+               Error_Pragma ("expected an integer");
+            end if;
+
+            Expr := Acc_Next (Expr);
+         end loop;
+      end Validate_Acc_Int_Expr_List_Clause;
+
+      --------------------------------
+      -- Validate_Acc_Loop_Collapse --
+      --------------------------------
+
+      procedure Validate_Acc_Loop_Collapse (Clause : Node_Id) is
+         Count    : Uint;
+         Par_Loop : Node_Id;
+         Stmt     : Node_Id;
+
+      begin
+         --  Make sure the argument is a positive integer
+
+         Analyze_And_Resolve (Clause);
+
+         Count := Static_Integer (Clause);
+         if Count = No_Uint or else Count < 1 then
+            Error_Pragma_Arg ("expected a positive integer", Clause);
+         end if;
+
+         --  Then, make sure we have at least Count-1 tightly-nested loops
+         --  (i.e. loops with no statements in between).
+
+         Par_Loop := Parent (Parent (Parent (Clause)));
+         Stmt     := First (Statements (Par_Loop));
+
+         --  Skip first pragmas in the parent loop
+
+         while Present (Stmt) and then Nkind (Stmt) = N_Pragma loop
+            Next (Stmt);
+         end loop;
+
+         if not Present (Next (Stmt)) then
+            while Nkind (Stmt) = N_Loop_Statement and Count > 1 loop
+               Stmt := First (Statements (Stmt));
+               exit when Present (Next (Stmt));
+
+               Count := Count - 1;
+            end loop;
+         end if;
+
+         if Count > 1 then
+            Error_Pragma_Arg
+              ("Collapse argument too high or loops not tightly nested",
+               Clause);
+         end if;
+      end Validate_Acc_Loop_Collapse;
+
+      ----------------------------
+      -- Validate_Acc_Loop_Gang --
+      ----------------------------
+
+      procedure Validate_Acc_Loop_Gang (Clause : Node_Id) is
+      begin
+         Error_Pragma_Arg ("Loop_Gang not implemented", Clause);
+      end Validate_Acc_Loop_Gang;
+
+      ------------------------------
+      -- Validate_Acc_Loop_Vector --
+      ------------------------------
+
+      procedure Validate_Acc_Loop_Vector (Clause : Node_Id) is
+      begin
+         Error_Pragma_Arg ("Loop_Vector not implemented", Clause);
+      end Validate_Acc_Loop_Vector;
+
+      -------------------------------
+      --  Validate_Acc_Loop_Worker --
+      -------------------------------
+
+      procedure Validate_Acc_Loop_Worker (Clause : Node_Id) is
+      begin
+         Error_Pragma_Arg ("Loop_Worker not implemented", Clause);
+      end Validate_Acc_Loop_Worker;
+
+      ---------------------------------
+      -- Validate_Acc_Name_Reduction --
+      ---------------------------------
+
+      procedure Validate_Acc_Name_Reduction (Clause : Node_Id) is
+
+         --  ??? On top of the following operations, the OpenAcc spec adds the
+         --  "bitwise and", "bitwise or" and modulo for C and ".eqv" and
+         --  ".neqv" for Fortran. Can we, should we and how do we support them
+         --  in Ada?
+
+         type Reduction_Op is (Add_Op, Mul_Op, Max_Op, Min_Op, And_Op, Or_Op);
+
+         function To_Reduction_Op (Op : String) return Reduction_Op;
+         --  Convert operator Op described by a String into its corresponding
+         --  enumeration value.
+
+         ---------------------
+         -- To_Reduction_Op --
+         ---------------------
+
+         function To_Reduction_Op (Op : String) return Reduction_Op is
+         begin
+            if Op = "+" then
+               return Add_Op;
+
+            elsif Op = "*" then
+               return Mul_Op;
+
+            elsif Op = "max" then
+               return Max_Op;
+
+            elsif Op = "min" then
+               return Min_Op;
+
+            elsif Op = "and" then
+               return And_Op;
+
+            elsif Op = "or" then
+               return Or_Op;
+
+            else
+               Error_Pragma ("unsuported reduction operation");
+            end if;
+         end To_Reduction_Op;
+
+         --  Local variables
+
+         Seen : constant Elist_Id := New_Elmt_List;
+
+         Expr      : Node_Id;
+         Reduc_Op  : Node_Id;
+         Reduc_Var : Node_Id;
+
+      --  Start of processing for Validate_Acc_Name_Reduction
+
+      begin
+         --  Reduction operations appear in the following form:
+         --    ("+" => (a, b), "*" => c)
+
+         Expr := First (Component_Associations (Clause));
+         while Present (Expr) loop
+            Reduc_Op := First (Choices (Expr));
+            String_To_Name_Buffer (Strval (Reduc_Op));
+
+            case To_Reduction_Op (Name_Buffer (1 .. Name_Len)) is
+               when Add_Op
+                  | Mul_Op
+                  | Max_Op
+                  | Min_Op
+               =>
+                  Reduc_Var := Acc_First (Expression (Expr));
+                  while Present (Reduc_Var) loop
+                     Analyze_And_Resolve (Reduc_Var);
+
+                     if Contains (Seen, Entity (Reduc_Var)) then
+                        Error_Pragma ("variable used in multiple reductions");
+
+                     else
+                        if Nkind (Reduc_Var) /= N_Identifier
+                          or not Is_Numeric_Type (Etype (Reduc_Var))
+                        then
+                           Error_Pragma
+                             ("expected an identifier for a Numeric");
+                        end if;
+
+                        Append_Elmt (Entity (Reduc_Var), Seen);
+                     end if;
+
+                     Reduc_Var := Acc_Next (Reduc_Var);
+                  end loop;
+
+               when And_Op
+                  | Or_Op
+               =>
+                  Reduc_Var := Acc_First (Expression (Expr));
+                  while Present (Reduc_Var) loop
+                     Analyze_And_Resolve (Reduc_Var);
+
+                     if Contains (Seen, Entity (Reduc_Var)) then
+                        Error_Pragma ("variable used in multiple reductions");
+
+                     else
+                        if Nkind (Reduc_Var) /= N_Identifier
+                          or not Is_Boolean_Type (Etype (Reduc_Var))
+                        then
+                           Error_Pragma
+                             ("expected a variable of type boolean");
+                        end if;
+
+                        Append_Elmt (Entity (Reduc_Var), Seen);
+                     end if;
+
+                     Reduc_Var := Acc_Next (Reduc_Var);
+                  end loop;
+            end case;
+
+            Next (Expr);
+         end loop;
+      end Validate_Acc_Name_Reduction;
+
+      -----------------------------------
+      -- Validate_Acc_Size_Expressions --
+      -----------------------------------
+
+      procedure Validate_Acc_Size_Expressions (Clause : Node_Id) is
+         function Validate_Size_Expr (Expr : Node_Id) return Boolean;
+         --  A size expr is either an integer expression or "*"
+
+         ------------------------
+         -- Validate_Size_Expr --
+         ------------------------
+
+         function Validate_Size_Expr (Expr : Node_Id) return Boolean is
+         begin
+            if Nkind (Expr) = N_Operator_Symbol then
+               return Get_String_Char (Strval (Expr), 1) = Get_Char_Code ('*');
+            end if;
+
+            Analyze_And_Resolve (Expr);
+
+            return Is_Integer_Type (Etype (Expr));
+         end Validate_Size_Expr;
+
+         --  Local variables
+
+         Expr : Node_Id;
+
+      --  Start of processing for Validate_Acc_Size_Expressions
+
+      begin
+         Expr := Acc_First (Clause);
+         while Present (Expr) loop
+            if not Validate_Size_Expr (Expr) then
+               Error_Pragma
+                 ("Size expressions should be either integers or '*'");
+            end if;
+
+            Expr := Acc_Next (Expr);
+         end loop;
+      end Validate_Acc_Size_Expressions;
+
    --  Start of processing for Analyze_Pragma
 
    begin
@@ -11005,7 +11531,7 @@
 
       --  Here to start processing for recognized pragma
 
-      Pname   := Original_Aspect_Pragma_Name (N);
+      Pname := Original_Aspect_Pragma_Name (N);
 
       --  Capture setting of Opt.Uneval_Old
 
@@ -11036,7 +11562,6 @@
 
       elsif Is_Rewrite_Substitution (N)
         and then Nkind (Original_Node (N)) = N_Pragma
-        and then Original_Node (N) /= N
       then
          Set_Is_Ignored (N, Is_Ignored (Original_Node (N)));
          Set_Is_Checked (N, Is_Checked (Original_Node (N)));
@@ -11390,6 +11915,7 @@
                         SPARK_Msg_N
                           ("expression of external state property must be "
                            & "static", Expr);
+                        return;
                      end if;
 
                   --  The lack of expression defaults the property to True
@@ -11563,6 +12089,11 @@
                   Set_Etype               (State_Id, Standard_Void_Type);
                   Set_Encapsulating_State (State_Id, Empty);
 
+                  --  Set the SPARK mode from the current context
+
+                  Set_SPARK_Pragma           (State_Id, SPARK_Mode_Pragma);
+                  Set_SPARK_Pragma_Inherited (State_Id);
+
                   --  An abstract state declared within a Ghost region becomes
                   --  Ghost (SPARK RM 6.9(2)).
 
@@ -11832,17 +12363,9 @@
 
             Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True);
 
-            --  Ensure the proper placement of the pragma. Abstract states must
-            --  be associated with a package declaration.
-
-            if Nkind_In (Pack_Decl, N_Generic_Package_Declaration,
-                                    N_Package_Declaration)
-            then
-               null;
-
-            --  Otherwise the pragma is associated with an illegal construct
-
-            else
+            if not Nkind_In (Pack_Decl, N_Generic_Package_Declaration,
+                                        N_Package_Declaration)
+            then
                Pragma_Misplaced;
                return;
             end if;
@@ -11904,6 +12427,306 @@
             Analyze_If_Present (Pragma_Initial_Condition);
          end Abstract_State;
 
+         --------------
+         -- Acc_Data --
+         --------------
+
+         when Pragma_Acc_Data => Acc_Data : declare
+            Clause_Names : constant Name_List :=
+              (Name_Attach,
+               Name_Copy,
+               Name_Copy_In,
+               Name_Copy_Out,
+               Name_Create,
+               Name_Delete,
+               Name_Detach,
+               Name_Device_Ptr,
+               Name_No_Create,
+               Name_Present);
+
+            Clause  : Node_Id;
+            Clauses : Args_List (Clause_Names'Range);
+
+         begin
+            if not OpenAcc_Enabled then
+               return;
+            end if;
+
+            GNAT_Pragma;
+
+            if Nkind (Parent (N)) /= N_Loop_Statement then
+               Error_Pragma
+                 ("Acc_Data pragma should be placed in loop or block "
+                  & "statements");
+            end if;
+
+            Gather_Associations (Clause_Names, Clauses);
+
+            for Id in Clause_Names'First .. Clause_Names'Last loop
+               Clause := Clauses (Id);
+
+               if Present (Clause) then
+                  case Clause_Names (Id) is
+                     when Name_Copy
+                        | Name_Copy_In
+                        | Name_Copy_Out
+                        | Name_Create
+                        | Name_Device_Ptr
+                        | Name_Present
+                     =>
+                        Validate_Acc_Data_Clause (Clause);
+
+                     when Name_Attach
+                        | Name_Detach
+                        | Name_Delete
+                        | Name_No_Create
+                      =>
+                        Error_Pragma ("unsupported pragma clause");
+
+                     when others =>
+                        raise Program_Error;
+                  end case;
+               end if;
+            end loop;
+
+            Set_Is_OpenAcc_Environment (Parent (N));
+         end Acc_Data;
+
+         --------------
+         -- Acc_Loop --
+         --------------
+
+         when Pragma_Acc_Loop => Acc_Loop : declare
+            Clause_Names : constant Name_List :=
+              (Name_Auto,
+               Name_Collapse,
+               Name_Gang,
+               Name_Independent,
+               Name_Acc_Private,
+               Name_Reduction,
+               Name_Seq,
+               Name_Tile,
+               Name_Vector,
+               Name_Worker);
+
+            Clause  : Node_Id;
+            Clauses : Args_List (Clause_Names'Range);
+            Par     : Node_Id;
+
+         begin
+            if not OpenAcc_Enabled then
+               return;
+            end if;
+
+            GNAT_Pragma;
+
+            --  Make sure the pragma is in an openacc construct
+
+            Check_Loop_Pragma_Placement;
+
+            Par := Parent (N);
+            while Present (Par)
+              and then (Nkind (Par) /= N_Loop_Statement
+                         or else not Is_OpenAcc_Environment (Par))
+            loop
+               Par := Parent (Par);
+            end loop;
+
+            if not Is_OpenAcc_Environment (Par) then
+               Error_Pragma
+                 ("Acc_Loop directive must be associated with an OpenAcc "
+                  & "construct region");
+            end if;
+
+            Gather_Associations (Clause_Names, Clauses);
+
+            for Id in Clause_Names'First .. Clause_Names'Last loop
+               Clause := Clauses (Id);
+
+               if Present (Clause) then
+                  case Clause_Names (Id) is
+                     when Name_Auto
+                        | Name_Independent
+                        | Name_Seq
+                     =>
+                        null;
+
+                     when Name_Collapse =>
+                        Validate_Acc_Loop_Collapse (Clause);
+
+                     when Name_Gang =>
+                        Validate_Acc_Loop_Gang (Clause);
+
+                     when Name_Acc_Private =>
+                        Validate_Acc_Data_Clause (Clause);
+
+                     when Name_Reduction =>
+                        Validate_Acc_Name_Reduction (Clause);
+
+                     when Name_Tile =>
+                        Validate_Acc_Size_Expressions (Clause);
+
+                     when Name_Vector =>
+                        Validate_Acc_Loop_Vector (Clause);
+
+                     when Name_Worker =>
+                        Validate_Acc_Loop_Worker (Clause);
+
+                     when others =>
+                        raise Program_Error;
+                  end case;
+               end if;
+            end loop;
+
+            Set_Is_OpenAcc_Loop (Parent (N));
+         end Acc_Loop;
+
+         ----------------------------------
+         -- Acc_Parallel and Acc_Kernels --
+         ----------------------------------
+
+         when Pragma_Acc_Parallel
+            | Pragma_Acc_Kernels
+         =>
+         Acc_Kernels_Or_Parallel : declare
+            Clause_Names : constant Name_List :=
+              (Name_Acc_If,
+               Name_Async,
+               Name_Copy,
+               Name_Copy_In,
+               Name_Copy_Out,
+               Name_Create,
+               Name_Default,
+               Name_Device_Ptr,
+               Name_Device_Type,
+               Name_Num_Gangs,
+               Name_Num_Workers,
+               Name_Present,
+               Name_Vector_Length,
+               Name_Wait,
+
+               --  Parallel only
+
+               Name_Acc_Private,
+               Name_First_Private,
+               Name_Reduction,
+
+               --  Kernels only
+
+               Name_Attach,
+               Name_No_Create);
+
+            Clause  : Node_Id;
+            Clauses : Args_List (Clause_Names'Range);
+
+         begin
+            if not OpenAcc_Enabled then
+               return;
+            end if;
+
+            GNAT_Pragma;
+            Check_Loop_Pragma_Placement;
+
+            if Nkind (Parent (N)) /= N_Loop_Statement then
+               Error_Pragma
+                 ("pragma should be placed in loop or block statements");
+            end if;
+
+            Gather_Associations (Clause_Names, Clauses);
+
+            for Id in Clause_Names'First .. Clause_Names'Last loop
+               Clause := Clauses (Id);
+
+               if Present (Clause) then
+                  if Chars (Parent (Clause)) = No_Name then
+                     Error_Pragma ("all arguments should be associations");
+                  else
+                     case Clause_Names (Id) is
+
+                        --  Note: According to the OpenAcc Standard v2.6,
+                        --  Async's argument should be optional. Because this
+                        --  complicates parsing the clause, the argument is
+                        --  made mandatory. The standard defines two negative
+                        --  values, acc_async_noval and acc_async_sync. When
+                        --  given acc_async_noval as value, the clause should
+                        --  behave as if no argument was given. According to
+                        --  the standard, acc_async_noval is defined in header
+                        --  files for C and Fortran, thus this value should
+                        --  probably be defined in the OpenAcc Ada library once
+                        --  it is implemented.
+
+                        when Name_Async
+                           | Name_Num_Gangs
+                           | Name_Num_Workers
+                           | Name_Vector_Length
+                        =>
+                           Validate_Acc_Int_Expr_Clause (Clause);
+
+                        when Name_Acc_If =>
+                           Validate_Acc_Condition_Clause (Clause);
+
+                        --  Unsupported by GCC
+
+                        when Name_Attach
+                           | Name_No_Create
+                        =>
+                           Error_Pragma ("unsupported clause");
+
+                        when Name_Acc_Private
+                           | Name_First_Private
+                        =>
+                           if Prag_Id /= Pragma_Acc_Parallel then
+                              Error_Pragma
+                                ("argument is only available for 'Parallel' "
+                                 & "construct");
+                           else
+                              Validate_Acc_Data_Clause (Clause);
+                           end if;
+
+                        when Name_Copy
+                           | Name_Copy_In
+                           | Name_Copy_Out
+                           | Name_Create
+                           | Name_Device_Ptr
+                           | Name_Present
+                        =>
+                           Validate_Acc_Data_Clause (Clause);
+
+                        when Name_Reduction =>
+                           if Prag_Id /= Pragma_Acc_Parallel then
+                              Error_Pragma
+                                ("argument is only available for 'Parallel' "
+                                 & "construct");
+                           else
+                              Validate_Acc_Name_Reduction (Clause);
+                           end if;
+
+                        when Name_Default =>
+                           if Chars (Clause) /= Name_None then
+                              Error_Pragma ("expected none");
+                           end if;
+
+                        when Name_Device_Type =>
+                           Error_Pragma ("unsupported pragma clause");
+
+                        --  Similar to Name_Async, Name_Wait's arguments should
+                        --  be optional. However, this can be simulated using
+                        --  acc_async_noval, hence, we do not bother making the
+                        --  argument optional for now.
+
+                        when Name_Wait =>
+                           Validate_Acc_Int_Expr_List_Clause (Clause);
+
+                        when others =>
+                           raise Program_Error;
+                     end case;
+                  end if;
+               end if;
+            end loop;
+
+            Set_Is_OpenAcc_Environment (Parent (N));
+         end Acc_Kernels_Or_Parallel;
+
          ------------
          -- Ada_83 --
          ------------
@@ -12761,12 +13584,7 @@
 
             --  Object declaration
 
-            if Nkind (Obj_Decl) = N_Object_Declaration then
-               null;
-
-            --  Otherwise the pragma is associated with an illegal construact
-
-            else
+            if Nkind (Obj_Decl) /= N_Object_Declaration then
                Pragma_Misplaced;
                return;
             end if;
@@ -13141,8 +13959,9 @@
          --  restore the Ghost mode.
 
          when Pragma_Check => Check : declare
-            Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
-            --  Save the Ghost mode to restore on exit
+            Saved_GM  : constant Ghost_Mode_Type := Ghost_Mode;
+            Saved_IGR : constant Node_Id         := Ignored_Ghost_Region;
+            --  Save the Ghost-related attributes to restore on exit
 
             Cname : Name_Id;
             Eloc  : Source_Ptr;
@@ -13200,7 +14019,6 @@
 
             elsif Is_Rewrite_Substitution (N)
               and then Nkind (Original_Node (N)) = N_Pragma
-              and then Original_Node (N) /= N
             then
                Set_Is_Ignored (N, Is_Ignored (Original_Node (N)));
                Set_Is_Checked (N, Is_Checked (Original_Node (N)));
@@ -13337,7 +14155,7 @@
                In_Assertion_Expr := In_Assertion_Expr - 1;
             end if;
 
-            Restore_Ghost_Mode (Saved_GM);
+            Restore_Ghost_Region (Saved_GM, Saved_IGR);
          end Check;
 
          --------------------------
@@ -13806,14 +14624,7 @@
 
             Obj_Decl := Find_Related_Context (N, Do_Checks => True);
 
-            --  Object declaration
-
-            if Nkind (Obj_Decl) = N_Object_Declaration then
-               null;
-
-            --  Otherwise the pragma is associated with an illegal construct
-
-            else
+            if Nkind (Obj_Decl) /= N_Object_Declaration then
                Pragma_Misplaced;
                return;
             end if;
@@ -15002,6 +15813,25 @@
                      Set_Elaborate_Present (Citem, True);
                      Set_Elab_Unit_Name (Get_Pragma_Arg (Arg), Name (Citem));
 
+                     --  With the pragma present, elaboration calls on
+                     --  subprograms from the named unit need no further
+                     --  checks, as long as the pragma appears in the current
+                     --  compilation unit. If the pragma appears in some unit
+                     --  in the context, there might still be a need for an
+                     --  Elaborate_All_Desirable from the current compilation
+                     --  to the named unit, so we keep the check enabled. This
+                     --  does not apply in SPARK mode, where we allow pragma
+                     --  Elaborate, but we don't trust it to be right so we
+                     --  will still insist on the Elaborate_All.
+
+                     if Legacy_Elaboration_Checks
+                       and then In_Extended_Main_Source_Unit (N)
+                       and then SPARK_Mode /= On
+                     then
+                        Set_Suppress_Elaboration_Warnings
+                          (Entity (Name (Citem)));
+                     end if;
+
                      exit Inner;
                   end if;
 
@@ -15015,24 +15845,6 @@
 
                Next (Arg);
             end loop Outer;
-
-            --  Give a warning if operating in static mode with one of the
-            --  gnatwl/-gnatwE (elaboration warnings enabled) switches set.
-
-            if Elab_Warnings
-              and not Dynamic_Elaboration_Checks
-
-              --  pragma Elaborate not allowed in SPARK mode anyway. We
-              --  already complained about it, no point in generating any
-              --  further complaint.
-
-              and SPARK_Mode /= On
-            then
-               Error_Msg_N
-                 ("?l?use of pragma Elaborate may not be safe", N);
-               Error_Msg_N
-                 ("?l?use pragma Elaborate_All instead if possible", N);
-            end if;
          end Elaborate;
 
          -------------------
@@ -15079,6 +15891,17 @@
                      Set_Elaborate_All_Present (Citem, True);
                      Set_Elab_Unit_Name (Get_Pragma_Arg (Arg), Name (Citem));
 
+                     --  Suppress warnings and elaboration checks on the named
+                     --  unit if the pragma is in the current compilation, as
+                     --  for pragma Elaborate.
+
+                     if Legacy_Elaboration_Checks
+                       and then In_Extended_Main_Source_Unit (N)
+                     then
+                        Set_Suppress_Elaboration_Warnings
+                          (Entity (Name (Citem)));
+                     end if;
+
                      exit Innr;
                   end if;
 
@@ -15128,6 +15951,27 @@
             else
                Set_Body_Required (Cunit_Node);
                Set_Has_Pragma_Elaborate_Body (Cunit_Ent);
+
+               --  If we are in dynamic elaboration mode, then we suppress
+               --  elaboration warnings for the unit, since it is definitely
+               --  fine NOT to do dynamic checks at the first level (and such
+               --  checks will be suppressed because no elaboration boolean
+               --  is created for Elaborate_Body packages).
+               --
+               --  But in the static model of elaboration, Elaborate_Body is
+               --  definitely NOT good enough to ensure elaboration safety on
+               --  its own, since the body may WITH other units that are not
+               --  safe from an elaboration point of view, so a client must
+               --  still do an Elaborate_All on such units.
+               --
+               --  Debug flag -gnatdD restores the old behavior of 3.13, where
+               --  Elaborate_Body always suppressed elab warnings.
+
+               if Legacy_Elaboration_Checks
+                 and then (Dynamic_Elaboration_Checks or Debug_Flag_DD)
+               then
+                  Set_Suppress_Elaboration_Warnings (Cunit_Ent);
+               end if;
             end if;
          end Elaborate_Body;
 
@@ -15137,16 +15981,118 @@
 
          --  pragma Elaboration_Checks (Static | Dynamic);
 
-         when Pragma_Elaboration_Checks =>
+         when Pragma_Elaboration_Checks => Elaboration_Checks : declare
+            procedure Check_Duplicate_Elaboration_Checks_Pragma;
+            --  Emit an error if the current context list already contains
+            --  a previous Elaboration_Checks pragma. This routine raises
+            --  Pragma_Exit if a duplicate is found.
+
+            procedure Ignore_Elaboration_Checks_Pragma;
+            --  Warn that the effects of the pragma are ignored. This routine
+            --  raises Pragma_Exit.
+
+            -----------------------------------------------
+            -- Check_Duplicate_Elaboration_Checks_Pragma --
+            -----------------------------------------------
+
+            procedure Check_Duplicate_Elaboration_Checks_Pragma is
+               Item : Node_Id;
+
+            begin
+               Item := Prev (N);
+               while Present (Item) loop
+                  if Nkind (Item) = N_Pragma
+                    and then Pragma_Name (Item) = Name_Elaboration_Checks
+                  then
+                     Duplication_Error
+                       (Prag => N,
+                        Prev => Item);
+                     raise Pragma_Exit;
+                  end if;
+
+                  Prev (Item);
+               end loop;
+            end Check_Duplicate_Elaboration_Checks_Pragma;
+
+            --------------------------------------
+            -- Ignore_Elaboration_Checks_Pragma --
+            --------------------------------------
+
+            procedure Ignore_Elaboration_Checks_Pragma is
+            begin
+               Error_Msg_Name_1 := Pname;
+               Error_Msg_N ("??effects of pragma % are ignored", N);
+               Error_Msg_N
+                 ("\place pragma on initial declaration of library unit", N);
+
+               raise Pragma_Exit;
+            end Ignore_Elaboration_Checks_Pragma;
+
+            --  Local variables
+
+            Context : constant Node_Id := Parent (N);
+            Unt     : Node_Id;
+
+         --  Start of processing for Elaboration_Checks
+
+         begin
             GNAT_Pragma;
             Check_Arg_Count (1);
             Check_Arg_Is_One_Of (Arg1, Name_Static, Name_Dynamic);
 
-            --  Set flag accordingly (ignore attempt at dynamic elaboration
-            --  checks in SPARK mode).
+            --  The pragma appears in a configuration file
+
+            if No (Context) then
+               Check_Valid_Configuration_Pragma;
+               Check_Duplicate_Elaboration_Checks_Pragma;
+
+            --  The pragma acts as a configuration pragma in a compilation unit
+
+            --    pragma Elaboration_Checks (...);
+            --    package Pack is ...;
+
+            elsif Nkind (Context) = N_Compilation_Unit
+              and then List_Containing (N) = Context_Items (Context)
+            then
+               Check_Valid_Configuration_Pragma;
+               Check_Duplicate_Elaboration_Checks_Pragma;
+
+               Unt := Unit (Context);
+
+               --  The pragma must appear on the initial declaration of a unit.
+               --  If this is not the case, warn that the effects of the pragma
+               --  are ignored.
+
+               if Nkind (Unt) = N_Package_Body then
+                  Ignore_Elaboration_Checks_Pragma;
+
+               --  Check the Acts_As_Spec flag of the compilation units itself
+               --  to determine whether the subprogram body completes since it
+               --  has not been analyzed yet. This is safe because compilation
+               --  units are not overloadable.
+
+               elsif Nkind (Unt) = N_Subprogram_Body
+                 and then not Acts_As_Spec (Context)
+               then
+                  Ignore_Elaboration_Checks_Pragma;
+
+               elsif Nkind (Unt) = N_Subunit then
+                  Ignore_Elaboration_Checks_Pragma;
+               end if;
+
+            --  Otherwise the pragma does not appear at the configuration level
+            --  and is illegal.
+
+            else
+               Pragma_Misplaced;
+            end if;
+
+            --  At this point the pragma is not a duplicate, and appears in the
+            --  proper context. Set the elaboration model in effect.
 
             Dynamic_Elaboration_Checks :=
               Chars (Get_Pragma_Arg (Arg1)) = Name_Dynamic;
+         end Elaboration_Checks;
 
          ---------------
          -- Eliminate --
@@ -16474,6 +17420,20 @@
                   return;
                end if;
 
+               --  Ada 2012 (AI05-0030): Cannot apply the implementation_kind
+               --  By_Protected_Procedure to the primitive procedure of a task
+               --  interface.
+
+               if Chars (Arg2) = Name_By_Protected_Procedure
+                 and then Is_Interface (Typ)
+                 and then Is_Task_Interface (Typ)
+               then
+                  Error_Pragma_Arg
+                    ("implementation kind By_Protected_Procedure cannot be "
+                     & "applied to a task interface primitive", Arg2);
+                  return;
+               end if;
+
             --  Procedures declared inside a protected type must be accepted
 
             elsif Ekind (Proc_Id) = E_Procedure
@@ -16489,20 +17449,6 @@
                return;
             end if;
 
-            --  Ada 2012 (AI05-0030): Cannot apply the implementation_kind
-            --  By_Protected_Procedure to the primitive procedure of a task
-            --  interface.
-
-            if Chars (Arg2) = Name_By_Protected_Procedure
-              and then Is_Interface (Typ)
-              and then Is_Task_Interface (Typ)
-            then
-               Error_Pragma_Arg
-                 ("implementation kind By_Protected_Procedure cannot be "
-                  & "applied to a task interface primitive", Arg2);
-               return;
-            end if;
-
             Record_Rep_Item (Proc_Id, N);
          end Implemented;
 
@@ -16785,6 +17731,38 @@
 
             E := Entity (E_Id);
 
+            --  A record type with a self-referential component of anonymous
+            --  access type is given an incomplete view in order to handle the
+            --  self reference:
+            --
+            --    type Rec is record
+            --       Self : access Rec;
+            --    end record;
+            --
+            --  becomes
+            --
+            --    type Rec;
+            --    type Ptr is access Rec;
+            --    type Rec is record
+            --       Self : Ptr;
+            --    end record;
+            --
+            --  Since the incomplete view is now the initial view of the type,
+            --  the argument of the pragma will reference the incomplete view,
+            --  but this view is illegal according to the semantics of the
+            --  pragma.
+            --
+            --  Obtain the full view of an internally-generated incomplete type
+            --  only. This way an attempt to associate the pragma with a source
+            --  incomplete type is still caught.
+
+            if Ekind (E) = E_Incomplete_Type
+              and then not Comes_From_Source (E)
+              and then Present (Full_View (E))
+            then
+               E := Full_View (E);
+            end if;
+
             --  A pragma that applies to a Ghost entity becomes Ghost for the
             --  purposes of legality checks and removal of ignored Ghost code.
 
@@ -16877,17 +17855,9 @@
 
             Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True);
 
-            --  Ensure the proper placement of the pragma. Initial_Condition
-            --  must be associated with a package declaration.
-
-            if Nkind_In (Pack_Decl, N_Generic_Package_Declaration,
-                                    N_Package_Declaration)
-            then
-               null;
-
-            --  Otherwise the pragma is associated with an illegal context
-
-            else
+            if not Nkind_In (Pack_Decl, N_Generic_Package_Declaration,
+                                        N_Package_Declaration)
+            then
                Pragma_Misplaced;
                return;
             end if;
@@ -16923,24 +17893,190 @@
          -- Initialize_Scalars --
          ------------------------
 
-         --  pragma Initialize_Scalars;
-
-         when Pragma_Initialize_Scalars =>
-            GNAT_Pragma;
-            Check_Arg_Count (0);
+         --  pragma Initialize_Scalars
+         --    [ ( TYPE_VALUE_PAIR {, TYPE_VALUE_PAIR} ) ];
+
+         --  TYPE_VALUE_PAIR ::=
+         --    SCALAR_TYPE => static_EXPRESSION
+
+         --  SCALAR_TYPE :=
+         --    Short_Float
+         --  | Float
+         --  | Long_Float
+         --  | Long_Long_Flat
+         --  | Signed_8
+         --  | Signed_16
+         --  | Signed_32
+         --  | Signed_64
+         --  | Unsigned_8
+         --  | Unsigned_16
+         --  | Unsigned_32
+         --  | Unsigned_64
+
+         when Pragma_Initialize_Scalars => Do_Initialize_Scalars : declare
+            Seen : array (Scalar_Id) of Node_Id := (others => Empty);
+            --  This collection holds the individual pairs which specify the
+            --  invalid values of their respective scalar types.
+
+            procedure Analyze_Float_Value
+              (Scal_Typ : Float_Scalar_Id;
+               Val_Expr : Node_Id);
+            --  Analyze a type value pair associated with float type Scal_Typ
+            --  and expression Val_Expr.
+
+            procedure Analyze_Integer_Value
+              (Scal_Typ : Integer_Scalar_Id;
+               Val_Expr : Node_Id);
+            --  Analyze a type value pair associated with integer type Scal_Typ
+            --  and expression Val_Expr.
+
+            procedure Analyze_Type_Value_Pair (Pair : Node_Id);
+            --  Analyze type value pair Pair
+
+            -------------------------
+            -- Analyze_Float_Value --
+            -------------------------
+
+            procedure Analyze_Float_Value
+              (Scal_Typ : Float_Scalar_Id;
+               Val_Expr : Node_Id)
+            is
+            begin
+               Analyze_And_Resolve (Val_Expr, Any_Real);
+
+               if Is_OK_Static_Expression (Val_Expr) then
+                  Set_Invalid_Scalar_Value (Scal_Typ, Expr_Value_R (Val_Expr));
+
+               else
+                  Error_Msg_Name_1 := Scal_Typ;
+                  Error_Msg_N ("value for type % must be static", Val_Expr);
+               end if;
+            end Analyze_Float_Value;
+
+            ---------------------------
+            -- Analyze_Integer_Value --
+            ---------------------------
+
+            procedure Analyze_Integer_Value
+              (Scal_Typ : Integer_Scalar_Id;
+               Val_Expr : Node_Id)
+            is
+            begin
+               Analyze_And_Resolve (Val_Expr, Any_Integer);
+
+               if Is_OK_Static_Expression (Val_Expr) then
+                  Set_Invalid_Scalar_Value (Scal_Typ, Expr_Value (Val_Expr));
+
+               else
+                  Error_Msg_Name_1 := Scal_Typ;
+                  Error_Msg_N ("value for type % must be static", Val_Expr);
+               end if;
+            end Analyze_Integer_Value;
+
+            -----------------------------
+            -- Analyze_Type_Value_Pair --
+            -----------------------------
+
+            procedure Analyze_Type_Value_Pair (Pair : Node_Id) is
+               Scal_Typ  : constant Name_Id := Chars (Pair);
+               Val_Expr  : constant Node_Id := Expression (Pair);
+               Prev_Pair : Node_Id;
+
+            begin
+               if Scal_Typ in Scalar_Id then
+                  Prev_Pair := Seen (Scal_Typ);
+
+                  --  Prevent multiple attempts to set a value for a scalar
+                  --  type.
+
+                  if Present (Prev_Pair) then
+                     Error_Msg_Name_1 := Scal_Typ;
+                     Error_Msg_N
+                       ("cannot specify multiple invalid values for type %",
+                        Pair);
+
+                     Error_Msg_Sloc := Sloc (Prev_Pair);
+                     Error_Msg_N ("previous value set #", Pair);
+
+                     --  Ignore the effects of the pair, but do not halt the
+                     --  analysis of the pragma altogether.
+
+                     return;
+
+                  --  Otherwise capture the first pair for this scalar type
+
+                  else
+                     Seen (Scal_Typ) := Pair;
+                  end if;
+
+                  if Scal_Typ in Float_Scalar_Id then
+                     Analyze_Float_Value (Scal_Typ, Val_Expr);
+
+                  else pragma Assert (Scal_Typ in Integer_Scalar_Id);
+                     Analyze_Integer_Value (Scal_Typ, Val_Expr);
+                  end if;
+
+               --  Otherwise the scalar family is illegal
+
+               else
+                  Error_Msg_Name_1 := Pname;
+                  Error_Msg_N
+                    ("argument of pragma % must denote valid scalar family",
+                     Pair);
+               end if;
+            end Analyze_Type_Value_Pair;
+
+            --  Local variables
+
+            Pairs : constant List_Id := Pragma_Argument_Associations (N);
+            Pair  : Node_Id;
+
+         --  Start of processing for Do_Initialize_Scalars
+
+         begin
+            GNAT_Pragma;
             Check_Valid_Configuration_Pragma;
             Check_Restriction (No_Initialize_Scalars, N);
 
+            --  Ignore the effects of the pragma when No_Initialize_Scalars is
+            --  in effect.
+
+            if Restriction_Active (No_Initialize_Scalars) then
+               null;
+
             --  Initialize_Scalars creates false positives in CodePeer, and
             --  incorrect negative results in GNATprove mode, so ignore this
             --  pragma in these modes.
 
-            if not Restriction_Active (No_Initialize_Scalars)
-              and then not (CodePeer_Mode or GNATprove_Mode)
-            then
+            elsif CodePeer_Mode or GNATprove_Mode then
+               null;
+
+            --  Otherwise analyze the pragma
+
+            else
+               if Present (Pairs) then
+
+                  --  Install Standard in order to provide access to primitive
+                  --  types in case the expressions contain attributes such as
+                  --  Integer'Last.
+
+                  Push_Scope (Standard_Standard);
+
+                  Pair := First (Pairs);
+                  while Present (Pair) loop
+                     Analyze_Type_Value_Pair (Pair);
+                     Next (Pair);
+                  end loop;
+
+                  --  Remove Standard
+
+                  Pop_Scope;
+               end if;
+
                Init_Or_Norm_Scalars := True;
-               Initialize_Scalars := True;
-            end if;
+               Initialize_Scalars   := True;
+            end if;
+         end Do_Initialize_Scalars;
 
          -----------------
          -- Initializes --
@@ -16991,17 +18127,9 @@
 
             Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True);
 
-            --  Ensure the proper placement of the pragma. Initializes must be
-            --  associated with a package declaration.
-
-            if Nkind_In (Pack_Decl, N_Generic_Package_Declaration,
-                                    N_Package_Declaration)
-            then
-               null;
-
-            --  Otherwise the pragma is associated with an illegal construc
-
-            else
+            if not Nkind_In (Pack_Decl, N_Generic_Package_Declaration,
+                                        N_Package_Declaration)
+            then
                Pragma_Misplaced;
                return;
             end if;
@@ -18167,7 +19295,7 @@
             Variant := First (Pragma_Argument_Associations (N));
             while Present (Variant) loop
                if Chars (Variant) = No_Name then
-                  Error_Pragma_Arg ("expect name `Increases`", Variant);
+                  Error_Pragma_Arg_Ident ("expect name `Increases`", Variant);
 
                elsif not Nam_In (Chars (Variant), Name_Decreases,
                                                   Name_Increases)
@@ -18358,14 +19486,22 @@
 
          --  pragma Max_Queue_Length (static_integer_EXPRESSION);
 
-         when Pragma_Max_Queue_Length => Max_Queue_Length : declare
+         --  This processing is shared by Pragma_Max_Entry_Queue_Depth
+
+         when Pragma_Max_Queue_Length
+            | Pragma_Max_Entry_Queue_Depth
+         =>
+         Max_Queue_Length : declare
             Arg        : Node_Id;
             Entry_Decl : Node_Id;
             Entry_Id   : Entity_Id;
             Val        : Uint;
 
          begin
-            GNAT_Pragma;
+            if Prag_Id = Pragma_Max_Queue_Length then
+               GNAT_Pragma;
+            end if;
+
             Check_Arg_Count (1);
 
             Entry_Decl :=
@@ -18382,7 +19518,7 @@
                   return;
                end if;
 
-               Entry_Id := Unique_Defining_Entity (Entry_Decl);
+               Entry_Id := Defining_Entity (Entry_Decl);
 
             --  Otherwise the pragma is associated with an illegal construct
 
@@ -18420,6 +19556,7 @@
 
             if Nkind (Arg) /= N_Integer_Literal then
                Rewrite (Arg, Make_Integer_Literal (Sloc (Arg), Val));
+               Set_Etype (Arg, Etype (Original_Node (Arg)));
             end if;
 
             Record_Rep_Item (Entry_Id, N);
@@ -19547,8 +20684,18 @@
                      if not Comes_From_Source (Item_Id) then
                         null;
 
+                     --  Do not consider generic formals or their corresponding
+                     --  actuals because they are not part of a visible state.
+                     --  Note that both entities are marked as hidden.
+
+                     elsif Is_Hidden (Item_Id) then
+                        null;
+
                      --  The Part_Of indicator turns an abstract state or an
                      --  object into a constituent of the encapsulating state.
+                     --  Note that constants are considered here even though
+                     --  they may not depend on variable input. This check is
+                     --  left to the SPARK prover.
 
                      elsif Ekind_In (Item_Id, E_Abstract_State,
                                               E_Constant,
@@ -20114,6 +21261,13 @@
             --  general Assertion_Policy pragma) to preserve existing warnings.
 
             Set_Has_Predicates (Typ);
+
+            --  Indicate that the pragma must be processed at the point the
+            --  type is frozen, as is done for the corresponding aspect.
+
+            Set_Has_Delayed_Aspects (Typ);
+            Set_Has_Delayed_Freeze (Typ);
+
             Set_Predicates_Ignored (Typ,
               Present (Check_Policy_List)
                 and then
@@ -20205,6 +21359,10 @@
                else
                   if not Debug_Flag_U then
                      Set_Is_Preelaborated (Ent);
+
+                     if Legacy_Elaboration_Checks then
+                        Set_Suppress_Elaboration_Warnings (Ent);
+                     end if;
                   end if;
                end if;
             end if;
@@ -20832,6 +21990,10 @@
             if not Debug_Flag_U then
                Set_Is_Pure (Ent);
                Set_Has_Pragma_Pure (Ent);
+
+               if Legacy_Elaboration_Checks then
+                  Set_Suppress_Elaboration_Warnings (Ent);
+               end if;
             end if;
          end Pure;
 
@@ -20846,6 +22008,8 @@
             E         : Entity_Id;
             E_Id      : Node_Id;
             Effective : Boolean := False;
+            Orig_Def  : Entity_Id;
+            Same_Decl : Boolean := False;
 
          begin
             GNAT_Pragma;
@@ -20879,11 +22043,25 @@
                        ("pragma% requires a function name", Arg1);
                   end if;
 
-                  Set_Is_Pure (Def_Id);
-
-                  if not Has_Pragma_Pure_Function (Def_Id) then
-                     Set_Has_Pragma_Pure_Function (Def_Id);
-                     Effective := True;
+                  --  When we have a generic function we must jump up a level
+                  --  to the declaration of the wrapper package itself.
+
+                  Orig_Def := Def_Id;
+
+                  if Is_Generic_Instance (Def_Id) then
+                     while Nkind (Orig_Def) /= N_Package_Declaration loop
+                        Orig_Def := Parent (Orig_Def);
+                     end loop;
+                  end if;
+
+                  if In_Same_Declarative_Part (Parent (N), Orig_Def) then
+                     Same_Decl := True;
+                     Set_Is_Pure (Def_Id);
+
+                     if not Has_Pragma_Pure_Function (Def_Id) then
+                        Set_Has_Pragma_Pure_Function (Def_Id);
+                        Effective := True;
+                     end if;
                   end if;
 
                   exit when From_Aspect_Specification (N);
@@ -20897,6 +22075,11 @@
                   Error_Msg_NE
                     ("pragma Pure_Function on& is redundant?r?",
                      N, Entity (E_Id));
+
+               elsif not Same_Decl then
+                  Error_Pragma_Arg
+                    ("pragma% argument must be in same declarative part",
+                     Arg1);
                end if;
             end if;
          end Pure_Function;
@@ -21195,15 +22378,7 @@
 
             Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True);
 
-            --  Ensure the proper placement of the pragma. Refined states must
-            --  be associated with a package body.
-
-            if Nkind (Pack_Decl) = N_Package_Body then
-               null;
-
-            --  Otherwise the pragma is associated with an illegal construct
-
-            else
+            if Nkind (Pack_Decl) /= N_Package_Body then
                Pragma_Misplaced;
                return;
             end if;
@@ -24253,11 +25428,16 @@
                               else
                                  OK := Set_Warning_Switch (Chr);
                               end if;
-                           end if;
-
-                           if not OK then
+
+                              if not OK then
+                                 Error_Pragma_Arg
+                                   ("invalid warning switch character " & Chr,
+                                    Arg1);
+                              end if;
+
+                           else
                               Error_Pragma_Arg
-                                ("invalid warning switch character " & Chr,
+                                ("invalid wide character in warning switch ",
                                  Arg1);
                            end if;
 
@@ -24304,6 +25484,13 @@
                                 (E, (Chars (Get_Pragma_Arg (Arg1)) =
                                       Name_Off));
 
+                              --  Suppress elaboration warnings if the entity
+                              --  denotes an elaboration target.
+
+                              if Is_Elaboration_Target (E) then
+                                 Set_Is_Elaboration_Warnings_OK_Id (E, False);
+                              end if;
+
                               --  For OFF case, make entry in warnings off
                               --  pragma table for later processing. But we do
                               --  not do that within an instance, since these
@@ -24567,9 +25754,11 @@
 
       --  Local variables
 
-      Expr     : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
-      Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
-      --  Save the Ghost mode to restore on exit
+      Expr : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
+
+      Saved_GM  : constant Ghost_Mode_Type := Ghost_Mode;
+      Saved_IGR : constant Node_Id         := Ignored_Ghost_Region;
+      --  Save the Ghost-related attributes to restore on exit
 
       Errors        : Nat;
       Restore_Scope : Boolean := False;
@@ -24608,7 +25797,7 @@
       Preanalyze_Assert_Expression (Expr, Standard_Boolean);
 
       --  Emit a clarification message when the expression contains at least
-      --  one undefined reference, possibly due to contract "freezing".
+      --  one undefined reference, possibly due to contract freezing.
 
       if Errors /= Serious_Errors_Detected
         and then Present (Freeze_Id)
@@ -24668,7 +25857,7 @@
       Check_Postcondition_Use_In_Inlined_Subprogram (N, Spec_Id);
       Set_Is_Analyzed_Pragma (N);
 
-      Restore_Ghost_Mode (Saved_GM);
+      Restore_Ghost_Region (Saved_GM, Saved_IGR);
    end Analyze_Pre_Post_Condition_In_Decl_Part;
 
    ------------------------------------------
@@ -26552,7 +27741,10 @@
                --  it must be an extra (SPARK RM 7.2.4(3)).
 
                else
-                  SPARK_Msg_NE ("extra global item &", Item, Item_Id);
+                  pragma Assert (Present (Global));
+                  Error_Msg_Sloc := Sloc (Global);
+                  SPARK_Msg_NE ("extra global item & does not refine or " &
+                                "repeat any global item #", Item, Item_Id);
                end if;
             end if;
          end Check_Refined_Global_Item;
@@ -27275,25 +28467,14 @@
                      end loop;
                   end if;
 
-                  --  Constants are part of the hidden state of a package, but
-                  --  the compiler cannot determine whether they have variable
-                  --  input (SPARK RM 7.1.1(2)) and cannot classify them as a
-                  --  hidden state. Accept the constant quietly even if it is
-                  --  a visible state or lacks a Part_Of indicator.
-
-                  if Ekind (Constit_Id) = E_Constant then
-                     Collect_Constituent;
-
-                  --  If we get here, then the constituent is not a hidden
-                  --  state of the related package and may not be used in a
-                  --  refinement (SPARK RM 7.2.2(9)).
-
-                  else
-                     Error_Msg_Name_1 := Chars (Spec_Id);
-                     SPARK_Msg_NE
-                       ("cannot use & in refinement, constituent is not a "
-                        & "hidden state of package %", Constit, Constit_Id);
-                  end if;
+                  --  At this point it is known that the constituent is not
+                  --  part of the package hidden state and cannot be used in
+                  --  a refinement (SPARK RM 7.2.2(9)).
+
+                  Error_Msg_Name_1 := Chars (Spec_Id);
+                  SPARK_Msg_NE
+                    ("cannot use & in refinement, constituent is not a hidden "
+                     & "state of package %", Constit, Constit_Id);
                end if;
             end Match_Constituent;
 
@@ -27358,7 +28539,7 @@
                   Constit_Id := Entity_Of (Constit);
 
                   --  When a constituent is declared after a subprogram body
-                  --  that caused "freezing" of the related contract where
+                  --  that caused freezing of the related contract where
                   --  pragma Refined_State resides, the constituent appears
                   --  undefined and carries Any_Id as its entity.
 
@@ -27751,6 +28932,10 @@
          return;
       end if;
 
+      --  Save the scenario for examination by the ABE Processing phase
+
+      Record_Elaboration_Scenario (N);
+
       --  Replicate the abstract states declared by the package because the
       --  matching algorithm will consume states.
 
@@ -28106,8 +29291,20 @@
                   when Name_Ignore
                      | Name_Off
                   =>
-                     Set_Is_Ignored (N, True);
-                     Set_Is_Checked (N, False);
+                     --  In CodePeer mode and GNATprove mode, we need to
+                     --  consider all assertions, unless they are disabled.
+                     --  Force Is_Checked on ignored assertions, in particular
+                     --  because transformations of the AST may depend on
+                     --  assertions being checked (e.g. the translation of
+                     --  attribute 'Loop_Entry).
+
+                     if CodePeer_Mode or GNATprove_Mode then
+                        Set_Is_Checked (N, True);
+                        Set_Is_Ignored (N, False);
+                     else
+                        Set_Is_Checked (N, False);
+                        Set_Is_Ignored (N, True);
+                     end if;
 
                   when Name_Check
                      | Name_On
@@ -28137,7 +29334,8 @@
       --  If there are no specific entries that matched, then we let the
       --  setting of assertions govern. Note that this provides the needed
       --  compatibility with the RM for the cases of assertion, invariant,
-      --  precondition, predicate, and postcondition.
+      --  precondition, predicate, and postcondition. Note also that
+      --  Assertions_Enabled is forced in CodePeer mode and GNATprove mode.
 
       if Assertions_Enabled then
          Set_Is_Checked (N, True);
@@ -28292,7 +29490,17 @@
             if not Comes_From_Source (Item_Id) then
                null;
 
-            --  A visible state has been found
+            --  Do not consider generic formals or their corresponding actuals
+            --  because they are not part of a visible state. Note that both
+            --  entities are marked as hidden.
+
+            elsif Is_Hidden (Item_Id) then
+               null;
+
+            --  A visible state has been found. Note that constants are not
+            --  considered here because it is not possible to determine whether
+            --  they depend on variable input. This check is left to the SPARK
+            --  prover.
 
             elsif Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
                return True;
@@ -28369,11 +29577,13 @@
 
       --  In general an item declared in the visible state space of a package
       --  does not require a Part_Of indicator. The only exception is when the
-      --  related package is a private child unit in which case Part_Of must
-      --  denote a state in the parent unit or in one of its descendants.
+      --  related package is a nongeneric private child unit, in which case
+      --  Part_Of must denote a state in the parent unit or in one of its
+      --  descendants.
 
       elsif Placement = Visible_State_Space then
          if Is_Child_Unit (Pack_Id)
+           and then not Is_Generic_Unit (Pack_Id)
            and then Is_Private_Descendant (Pack_Id)
          then
             --  A package instantiation does not need a Part_Of indicator when
@@ -28398,8 +29608,8 @@
             end if;
          end if;
 
-      --  When the item appears in the private state space of a packge, it must
-      --  be a part of some state declared by the said package.
+      --  When the item appears in the private state space of a package, it
+      --  must be a part of some state declared by the said package.
 
       else pragma Assert (Placement = Private_State_Space);
 
@@ -28412,9 +29622,9 @@
          --  A package instantiation does not need a Part_Of indicator when the
          --  related generic template has no visible state.
 
-         elsif Ekind (Pack_Id) = E_Package
-           and then Is_Generic_Instance (Pack_Id)
-           and then not Has_Visible_State (Pack_Id)
+         elsif Ekind (Item_Id) = E_Package
+           and then Is_Generic_Instance (Item_Id)
+           and then not Has_Visible_State (Item_Id)
          then
             null;
 
@@ -28747,7 +29957,7 @@
       Depends   : Node_Id;
       Formal    : Entity_Id;
       Global    : Node_Id;
-      Spec_Id   : Entity_Id;
+      Spec_Id   : Entity_Id := Empty;
       Subp_Decl : Node_Id;
       Typ       : Entity_Id;
 
@@ -29138,6 +30348,16 @@
                if Nkind (Original_Node (Stmt)) = N_Expression_Function then
                   return Stmt;
 
+               --  The subprogram declaration is an internally generated spec
+               --  for a stand-alone subrogram body declared inside a protected
+               --  body.
+
+               elsif Present (Corresponding_Body (Stmt))
+                 and then Comes_From_Source (Corresponding_Body (Stmt))
+                 and then Is_Protected_Type (Current_Scope)
+               then
+                  return Stmt;
+
                --  The subprogram is actually an instance housed within an
                --  anonymous wrapper package.
 
@@ -29290,7 +30510,7 @@
       elsif Present (Corresponding_Aspect (Prag)) then
          return Parent (Corresponding_Aspect (Prag));
 
-      --  No candidate packge [body] found
+      --  No candidate package [body] found
 
       else
          return Empty;
@@ -29334,23 +30554,18 @@
    -------------------------
 
    function Get_Base_Subprogram (Def_Id : Entity_Id) return Entity_Id is
-      Result : Entity_Id;
-
    begin
       --  Follow subprogram renaming chain
 
-      Result := Def_Id;
-
-      if Is_Subprogram (Result)
-        and then
-          Nkind (Parent (Declaration_Node (Result))) =
-                                         N_Subprogram_Renaming_Declaration
-        and then Present (Alias (Result))
+      if Is_Subprogram (Def_Id)
+        and then Nkind (Parent (Declaration_Node (Def_Id))) =
+                   N_Subprogram_Renaming_Declaration
+        and then Present (Alias (Def_Id))
       then
-         Result := Alias (Result);
-      end if;
-
-      return Result;
+         return Alias (Def_Id);
+      else
+         return Def_Id;
+      end if;
    end Get_Base_Subprogram;
 
    -----------------------
@@ -29364,10 +30579,11 @@
       elsif N = Name_Off then
          return Off;
 
-      --  Any other argument is illegal
+      --  Any other argument is illegal. Assume that no SPARK mode applies to
+      --  avoid potential cascaded errors.
 
       else
-         raise Program_Error;
+         return None;
       end if;
    end Get_SPARK_Mode_Type;
 
@@ -29606,6 +30822,10 @@
    Sig_Flags : constant array (Pragma_Id) of Int :=
      (Pragma_Abort_Defer                    => -1,
       Pragma_Abstract_State                 => -1,
+      Pragma_Acc_Data                       =>  0,
+      Pragma_Acc_Kernels                    =>  0,
+      Pragma_Acc_Loop                       =>  0,
+      Pragma_Acc_Parallel                   =>  0,
       Pragma_Ada_83                         => -1,
       Pragma_Ada_95                         => -1,
       Pragma_Ada_05                         => -1,
@@ -29729,6 +30949,7 @@
       Pragma_Machine_Attribute              => -1,
       Pragma_Main                           => -1,
       Pragma_Main_Storage                   => -1,
+      Pragma_Max_Entry_Queue_Depth          =>  0,
       Pragma_Max_Queue_Length               =>  0,
       Pragma_Memory_Size                    =>  0,
       Pragma_No_Return                      =>  0,
@@ -30149,11 +31370,18 @@
 
       if Compile_Time_Known_Value (Arg1x) then
          if Is_True (Expr_Value (Arg1x)) then
+
+            --  We have already verified that the second argument is a static
+            --  string expression. Its string value must be retrieved
+            --  explicitly if it is a declared constant, otherwise it has
+            --  been constant-folded previously.
+
             declare
                Cent    : constant Entity_Id := Cunit_Entity (Current_Sem_Unit);
                Pname   : constant Name_Id   := Pragma_Name_Unmapped (N);
                Prag_Id : constant Pragma_Id := Get_Pragma_Id (Pname);
-               Str     : constant String_Id := Strval (Get_Pragma_Arg (Arg2));
+               Str     : constant String_Id :=
+                           Strval (Expr_Value_S (Get_Pragma_Arg (Arg2)));
                Str_Len : constant Nat       := String_Length (Str);
 
                Force : constant Boolean :=