[Ada] Simplify prevention of cascaded errors for Refined_State
[gcc.git] / gcc / ada / sem_prag.adb
index 7b36f8e3923de5f4ca6ee35ab36acd391f761d2e..1ffe513e9a4c7010eb17caa53bda08141aab6be3 100644 (file)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2019, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2020, 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- --
@@ -44,6 +44,7 @@ with Exp_Util;  use Exp_Util;
 with Expander;  use Expander;
 with Freeze;    use Freeze;
 with Ghost;     use Ghost;
+with GNAT_CUDA; use GNAT_CUDA;
 with Gnatvsn;   use Gnatvsn;
 with Lib;       use Lib;
 with Lib.Writ;  use Lib.Writ;
@@ -543,12 +544,16 @@ package body Sem_Prag is
       Set_Ghost_Mode (N);
 
       --  Single and multiple contract cases must appear in aggregate form. If
-      --  this is not the case, then either the parser of the analysis of the
+      --  this is not the case, then either the parser or the analysis of the
       --  pragma failed to produce an aggregate.
 
       pragma Assert (Nkind (CCases) = N_Aggregate);
 
-      if Present (Component_Associations (CCases)) then
+      --  Only CASE_GUARD => CONSEQUENCE clauses are allowed
+
+      if Present (Component_Associations (CCases))
+        and then No (Expressions (CCases))
+      then
 
          --  Ensure that the formal parameters are visible when analyzing all
          --  clauses. This falls out of the general rule of aspects pertaining
@@ -583,7 +588,7 @@ package body Sem_Prag is
       --  Otherwise the pragma is illegal
 
       else
-         Error_Msg_N ("wrong syntax for constract cases", N);
+         Error_Msg_N ("wrong syntax for contract cases", N);
       end if;
 
       Set_Is_Analyzed_Pragma (N);
@@ -697,8 +702,8 @@ package body Sem_Prag is
          elsif Ekind (Item_Id) = E_Constant then
             Add_Str_To_Name_Buffer ("constant");
 
-         elsif Ekind_In (Item_Id, E_Generic_In_Out_Parameter,
-                                  E_Generic_In_Parameter)
+         elsif Ekind (Item_Id) in
+                 E_Generic_In_Out_Parameter | E_Generic_In_Parameter
          then
             Add_Str_To_Name_Buffer ("generic parameter");
 
@@ -972,32 +977,32 @@ package body Sem_Prag is
 
                   --  Constants
 
-                  if Ekind_In (Item_Id, E_Constant, E_Loop_Parameter)
+                  if Ekind (Item_Id) in E_Constant | E_Loop_Parameter
                       or else
 
                     --  Current instances of concurrent types
 
-                    Ekind_In (Item_Id, E_Protected_Type, E_Task_Type)
+                    Ekind (Item_Id) in E_Protected_Type | E_Task_Type
                       or else
 
                     --  Formal parameters
 
-                    Ekind_In (Item_Id, E_Generic_In_Out_Parameter,
-                                       E_Generic_In_Parameter,
-                                       E_In_Parameter,
-                                       E_In_Out_Parameter,
-                                       E_Out_Parameter)
+                    Ekind (Item_Id) in E_Generic_In_Out_Parameter
+                                     | E_Generic_In_Parameter
+                                     | E_In_Parameter
+                                     | E_In_Out_Parameter
+                                     | E_Out_Parameter
                       or else
 
                     --  States, variables
 
-                    Ekind_In (Item_Id, E_Abstract_State, E_Variable)
+                    Ekind (Item_Id) in 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)
+                     if Ekind (Spec_Id) in E_Function | E_Generic_Function
                        and then not Is_Input
                      then
                         SPARK_Msg_N
@@ -1009,7 +1014,7 @@ package body Sem_Prag is
                      --  they behave as objects in the context of pragma
                      --  [Refined_]Depends.
 
-                     if Ekind_In (Item_Id, E_Protected_Type, E_Task_Type) then
+                     if Ekind (Item_Id) in E_Protected_Type | E_Task_Type then
 
                         --  This use is legal as long as the concurrent type is
                         --  the current instance of an enclosing type.
@@ -1091,7 +1096,7 @@ package body Sem_Prag is
                         --  template is legal, do not perform this check in
                         --  the instance to circumvent this oddity.
 
-                        if Is_Generic_Instance (Spec_Id) then
+                        if In_Instance then
                            null;
 
                         --  An abstract state with visible refinement cannot
@@ -1144,9 +1149,9 @@ package body Sem_Prag is
                            Ref    => Item);
                      end if;
 
-                     if Ekind_In (Item_Id, E_Abstract_State,
-                                           E_Constant,
-                                           E_Variable)
+                     if Ekind (Item_Id) in E_Abstract_State
+                                         | E_Constant
+                                         | E_Variable
                        and then Present (Encapsulating_State (Item_Id))
                      then
                         Append_New_Elmt (Item_Id, Constits_Seen);
@@ -1222,7 +1227,7 @@ package body Sem_Prag is
 
       procedure Check_Function_Return is
       begin
-         if Ekind_In (Spec_Id, E_Function, E_Generic_Function)
+         if Ekind (Spec_Id) in E_Function | E_Generic_Function
            and then not Result_Seen
          then
             SPARK_Msg_NE
@@ -1262,17 +1267,17 @@ package body Sem_Prag is
            (Item_Is_Input  : out Boolean;
             Item_Is_Output : out Boolean)
          is
-            --  A constant or IN parameter of access type should be handled
-            --  like a variable, as the underlying memory pointed-to can be
-            --  modified. Use Adjusted_Kind to do this adjustment.
+            --  A constant or IN parameter of access-to-variable type should be
+            --  handled like a variable, as the underlying memory pointed-to
+            --  can be modified. Use Adjusted_Kind to do this adjustment.
 
             Adjusted_Kind : Entity_Kind := Ekind (Item_Id);
 
          begin
-            if Ekind_In (Item_Id, E_Constant,
-                                  E_Generic_In_Parameter,
-                                  E_In_Parameter)
-              and then Is_Access_Type (Etype (Item_Id))
+            if Ekind (Item_Id) in E_Constant
+                                | E_Generic_In_Parameter
+                                | E_In_Parameter
+              and then Is_Access_Variable (Etype (Item_Id))
             then
                Adjusted_Kind := E_Variable;
             end if;
@@ -1970,7 +1975,7 @@ package body Sem_Prag is
          --  clause as this will lead to misleading errors.
 
          if Has_Extra_Parentheses (Deps) then
-            return;
+            goto Leave;
          end if;
 
          if Present (Component_Associations (Deps)) then
@@ -2001,6 +2006,11 @@ package body Sem_Prag is
                Push_Scope (Spec_Id);
 
                if Ekind (Spec_Id) = E_Task_Type then
+
+                  --  Task discriminants cannot appear in the [Refined_]Depends
+                  --  contract, but must be present for the analysis so that we
+                  --  can reject them with an informative error message.
+
                   if Has_Discriminants (Spec_Id) then
                      Install_Discriminants (Spec_Id);
                   end if;
@@ -2031,11 +2041,9 @@ package body Sem_Prag is
 
                --  Do not normalize a clause if errors were detected (count
                --  of Serious_Errors has increased) because the inputs and/or
-               --  outputs may denote illegal items. Normalization is disabled
-               --  in ASIS mode as it alters the tree by introducing new nodes
-               --  similar to expansion.
+               --  outputs may denote illegal items.
 
-               if Serious_Errors_Detected = Errors and then not ASIS_Mode then
+               if Serious_Errors_Detected = Errors then
                   Normalize_Clause (Clause);
                end if;
 
@@ -2058,7 +2066,7 @@ package body Sem_Prag is
 
          else
             Error_Msg_N ("malformed dependency relation", Deps);
-            return;
+            goto Leave;
          end if;
 
       --  The top level dependency relation is malformed. This is a syntax
@@ -2097,12 +2105,11 @@ package body Sem_Prag is
       Expr     : Node_Id;
 
    begin
-      Expr_Val := False;
-
-      --  Do not analyze the pragma multiple times
+      --  Do not analyze the pragma multiple times, but set the output
+      --  parameter to the argument specified by the pragma.
 
       if Is_Analyzed_Pragma (N) then
-         return;
+         goto Leave;
       end if;
 
       Error_Msg_Name_1 := Pragma_Name (N);
@@ -2119,13 +2126,16 @@ package body Sem_Prag is
       if Prag_Id /= Pragma_No_Caching
         and then not Is_Effectively_Volatile (Obj_Id)
       then
-         if No_Caching_Enabled (Obj_Id) then
+         if Ekind (Obj_Id) = E_Variable
+           and then No_Caching_Enabled (Obj_Id)
+         then
             SPARK_Msg_N
               ("illegal combination of external property % and property "
                & """No_Caching"" (SPARK RM 7.1.2(6))", N);
          else
             SPARK_Msg_N
-              ("external property % must apply to a volatile object", N);
+              ("external property % must apply to a volatile type or object",
+               N);
          end if;
 
       --  Pragma No_Caching should only apply to volatile variables of
@@ -2140,6 +2150,10 @@ package body Sem_Prag is
          end if;
       end if;
 
+      Set_Is_Analyzed_Pragma (N);
+
+      <<Leave>>
+
       --  Ensure that the Boolean expression (if present) is static. A missing
       --  argument defaults the value to True (SPARK RM 7.1.2(5)).
 
@@ -2153,7 +2167,6 @@ package body Sem_Prag is
          end if;
       end if;
 
-      Set_Is_Analyzed_Pragma (N);
    end Analyze_External_Property_In_Decl_Part;
 
    ---------------------------------
@@ -2274,7 +2287,7 @@ package body Sem_Prag is
                --  the current instance of an enclosing protected or task type
                --  (SPARK RM 6.1.4).
 
-               elsif Ekind_In (Item_Id, E_Protected_Type, E_Task_Type) then
+               elsif Ekind (Item_Id) in E_Protected_Type | E_Task_Type then
                   if Is_CCT_Instance (Item_Id, Spec_Id) then
 
                      --  Pragma [Refined_]Global associated with a protected
@@ -2361,18 +2374,18 @@ package body Sem_Prag is
                --  The only legal references are those to abstract states,
                --  objects and various kinds of constants (SPARK RM 6.1.4(4)).
 
-               elsif not Ekind_In (Item_Id, E_Abstract_State,
-                                            E_Constant,
-                                            E_Loop_Parameter,
-                                            E_Variable)
+               elsif Ekind (Item_Id) not in E_Abstract_State
+                                          | E_Constant
+                                          | E_Loop_Parameter
+                                          | E_Variable
                then
                   SPARK_Msg_N
                     ("global item must denote object, state or current "
                      & "instance of concurrent type", Item);
 
-                  if Ekind (Item_Id) in Named_Kind then
+                  if Is_Named_Number (Item_Id) then
                      SPARK_Msg_NE
-                       ("\named number & is not an object", Item, Item);
+                       ("\named number & is not an object", Item, Item_Id);
                   end if;
 
                   return;
@@ -2390,7 +2403,7 @@ package body Sem_Prag is
                   --  do not perform this check in the instance to circumvent
                   --  this oddity.
 
-                  if Is_Generic_Instance (Spec_Id) then
+                  if In_Instance then
                      null;
 
                   --  An abstract state with visible refinement cannot appear
@@ -2408,7 +2421,7 @@ package body Sem_Prag is
                   --  nonvolatile function (SPARK RM 7.1.3(8)).
 
                   elsif Is_External_State (Item_Id)
-                    and then Ekind_In (Spec_Id, E_Function, E_Generic_Function)
+                    and then Ekind (Spec_Id) in E_Function | E_Generic_Function
                     and then not Is_Volatile_Function (Spec_Id)
                   then
                      SPARK_Msg_NE
@@ -2435,7 +2448,7 @@ package body Sem_Prag is
                   --  Unless it is of an access type, a constant is a read-only
                   --  item, therefore it cannot act as an output.
 
-                  if Nam_In (Global_Mode, Name_In_Out, Name_Output) then
+                  if Global_Mode in Name_In_Out | Name_Output then
                      SPARK_Msg_NE
                        ("constant & cannot act as output", Item, Item_Id);
                      return;
@@ -2448,7 +2461,7 @@ package body Sem_Prag is
                   --  A loop parameter is a read-only item, therefore it cannot
                   --  act as an output.
 
-                  if Nam_In (Global_Mode, Name_In_Out, Name_Output) then
+                  if Global_Mode in Name_In_Out | Name_Output then
                      SPARK_Msg_NE
                        ("loop parameter & cannot act as output",
                         Item, Item_Id);
@@ -2461,12 +2474,24 @@ package body Sem_Prag is
 
                elsif SPARK_Mode = On
                  and then Ekind (Item_Id) = E_Variable
-                 and then Is_Effectively_Volatile (Item_Id)
+                 and then Is_Effectively_Volatile_For_Reading (Item_Id)
                then
-                  --  An effectively volatile object cannot appear as a global
-                  --  item of a nonvolatile function (SPARK RM 7.1.3(8)).
+                  --  The current instance of a protected unit is not an
+                  --  effectively volatile object, unless the protected unit
+                  --  is already volatile for another reason (SPARK RM 7.1.2).
+
+                  if Is_Single_Protected_Object (Item_Id)
+                    and then Is_CCT_Instance (Etype (Item_Id), Spec_Id)
+                    and then not Is_Effectively_Volatile_For_Reading
+                      (Item_Id, Ignore_Protected => True)
+                  then
+                     null;
 
-                  if Ekind_In (Spec_Id, E_Function, E_Generic_Function)
+                  --  An effectively volatile object for reading cannot appear
+                  --  as a global item of a nonvolatile function (SPARK RM
+                  --  7.1.3(8)).
+
+                  elsif Ekind (Spec_Id) in E_Function | E_Generic_Function
                     and then not Is_Volatile_Function (Spec_Id)
                   then
                      Error_Msg_NE
@@ -2509,7 +2534,7 @@ package body Sem_Prag is
             --  Verify that an output does not appear as an input in an
             --  enclosing subprogram.
 
-            if Nam_In (Global_Mode, Name_In_Out, Name_Output) then
+            if Global_Mode in Name_In_Out | Name_Output then
                Check_Mode_Restriction_In_Enclosing_Context (Item, Item_Id);
             end if;
 
@@ -2540,7 +2565,7 @@ package body Sem_Prag is
                      Ref    => Item);
                end if;
 
-               if Ekind_In (Item_Id, E_Abstract_State, E_Constant, E_Variable)
+               if Ekind (Item_Id) in E_Abstract_State | E_Constant | E_Variable
                  and then Present (Encapsulating_State (Item_Id))
                then
                   Append_New_Elmt (Item_Id, Constits_Seen);
@@ -2644,7 +2669,7 @@ package body Sem_Prag is
 
          procedure Check_Mode_Restriction_In_Function (Mode : Node_Id) is
          begin
-            if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
+            if Ekind (Spec_Id) in E_Function | E_Generic_Function then
                SPARK_Msg_N
                  ("global mode & is not applicable to functions", Mode);
             end if;
@@ -2664,9 +2689,9 @@ package body Sem_Prag is
 
          --  Single global item declaration
 
-         elsif Nkind_In (List, N_Expanded_Name,
-                               N_Identifier,
-                               N_Selected_Component)
+         elsif Nkind (List) in N_Expanded_Name
+                             | N_Identifier
+                             | N_Selected_Component
          then
             Analyze_Global_Item (List, Global_Mode);
 
@@ -2792,6 +2817,11 @@ package body Sem_Prag is
             Push_Scope (Spec_Id);
 
             if Ekind (Spec_Id) = E_Task_Type then
+
+               --  Task discriminants cannot appear in the [Refined_]Global
+               --  contract, but must be present for the analysis so that we
+               --  can reject them with an informative error message.
+
                if Has_Discriminants (Spec_Id) then
                   Install_Discriminants (Spec_Id);
                end if;
@@ -2897,7 +2927,7 @@ package body Sem_Prag is
       --  Verify the legality of a single initialization item followed by a
       --  list of input items.
 
-      procedure Collect_States_And_Objects;
+      procedure Collect_States_And_Objects (Pack_Decl : Node_Id);
       --  Inspect the visible declarations of the related package and gather
       --  the entities of all abstract states and objects in States_And_Objs.
 
@@ -2916,9 +2946,8 @@ package body Sem_Prag is
             Item_Id := Entity_Of (Item);
 
             if Present (Item_Id)
-              and then Ekind_In (Item_Id, E_Abstract_State,
-                                          E_Constant,
-                                          E_Variable)
+              and then Ekind (Item_Id) in
+                         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.
@@ -3028,16 +3057,16 @@ package body Sem_Prag is
                   Input_Id := Entity_Of (Input);
 
                   if Present (Input_Id)
-                    and then Ekind_In (Input_Id, E_Abstract_State,
-                                                 E_Constant,
-                                                 E_Generic_In_Out_Parameter,
-                                                 E_Generic_In_Parameter,
-                                                 E_In_Parameter,
-                                                 E_In_Out_Parameter,
-                                                 E_Out_Parameter,
-                                                 E_Protected_Type,
-                                                 E_Task_Type,
-                                                 E_Variable)
+                    and then Ekind (Input_Id) in E_Abstract_State
+                                               | E_Constant
+                                               | E_Generic_In_Out_Parameter
+                                               | E_Generic_In_Parameter
+                                               | 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
                      --  within the related package (SPARK RM 7.1.5(4)).
@@ -3050,12 +3079,12 @@ package body Sem_Prag is
                         --  it is allowed for an initialization item to depend
                         --  on an input item.
 
-                        if Ekind_In (Input_Id, E_Generic_In_Out_Parameter,
-                                               E_Generic_In_Parameter)
+                        if Ekind (Input_Id) in E_Generic_In_Out_Parameter
+                                             | E_Generic_In_Parameter
                         then
                            null;
 
-                        elsif Ekind_In (Input_Id, E_Constant, E_Variable)
+                        elsif Ekind (Input_Id) in E_Constant | E_Variable
                           and then Present (Corresponding_Generic_Association
                                      (Declaration_Node (Input_Id)))
                         then
@@ -3087,9 +3116,9 @@ package body Sem_Prag is
                         Append_New_Elmt (Input_Id, States_Seen);
                      end if;
 
-                     if Ekind_In (Input_Id, E_Abstract_State,
-                                            E_Constant,
-                                            E_Variable)
+                     if Ekind (Input_Id) in E_Abstract_State
+                                          | E_Constant
+                                          | E_Variable
                        and then Present (Encapsulating_State (Input_Id))
                      then
                         Append_New_Elmt (Input_Id, Constits_Seen);
@@ -3166,15 +3195,21 @@ package body Sem_Prag is
       -- Collect_States_And_Objects --
       --------------------------------
 
-      procedure Collect_States_And_Objects is
-         Pack_Spec : constant Node_Id := Specification (Pack_Decl);
-         Decl      : Node_Id;
+      procedure Collect_States_And_Objects (Pack_Decl : Node_Id) is
+         Pack_Spec  : constant Node_Id := Specification (Pack_Decl);
+         Pack_Id    : constant Entity_Id := Defining_Entity (Pack_Decl);
+         Decl       : Node_Id;
+         State_Elmt : Elmt_Id;
 
       begin
          --  Collect the abstract states defined in the package (if any)
 
-         if Present (Abstract_States (Pack_Id)) then
-            States_And_Objs := New_Copy_Elist (Abstract_States (Pack_Id));
+         if Has_Non_Null_Abstract_State (Pack_Id) then
+            State_Elmt := First_Elmt (Abstract_States (Pack_Id));
+            while Present (State_Elmt) loop
+               Append_New_Elmt (Node (State_Elmt), States_And_Objs);
+               Next_Elmt (State_Elmt);
+            end loop;
          end if;
 
          --  Collect all objects that appear in the visible declarations of the
@@ -3184,11 +3219,14 @@ package body Sem_Prag is
             Decl := First (Visible_Declarations (Pack_Spec));
             while Present (Decl) loop
                if Comes_From_Source (Decl)
-                 and then Nkind_In (Decl, N_Object_Declaration,
-                                          N_Object_Renaming_Declaration)
+                 and then Nkind (Decl) in N_Object_Declaration
+                                        | N_Object_Renaming_Declaration
                then
                   Append_New_Elmt (Defining_Entity (Decl), States_And_Objs);
 
+               elsif Nkind (Decl) = N_Package_Declaration then
+                  Collect_States_And_Objects (Decl);
+
                elsif Is_Single_Concurrent_Type_Declaration (Decl) then
                   Append_New_Elmt
                     (Anonymous_Object (Defining_Entity (Decl)),
@@ -3228,7 +3266,7 @@ package body Sem_Prag is
 
       --  Initialize the various lists used during analysis
 
-      Collect_States_And_Objects;
+      Collect_States_And_Objects (Pack_Decl);
 
       if Present (Expressions (Inits)) then
          Init := First (Expressions (Inits));
@@ -3488,7 +3526,7 @@ package body Sem_Prag is
          --  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
+         if Ekind (Item_Id) in E_Abstract_State | E_Variable then
             null;
 
          --  The constituent is a constant
@@ -3531,9 +3569,9 @@ package body Sem_Prag is
          --  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)
+            if Nkind (Item_Context) in N_Package_Specification
+                                     | N_Protected_Definition
+                                     | N_Task_Definition
             then
                Prv_Decls := Private_Declarations (Item_Context);
                Vis_Decls := Visible_Declarations (Item_Context);
@@ -3618,9 +3656,8 @@ package body Sem_Prag is
       Encap_Id := Empty;
       Legal    := False;
 
-      if Nkind_In (Encap, N_Expanded_Name,
-                          N_Identifier,
-                          N_Selected_Component)
+      if Nkind (Encap) in
+           N_Expanded_Name | N_Identifier | N_Selected_Component
       then
          Analyze       (Encap);
          Resolve_State (Encap);
@@ -3769,7 +3806,8 @@ package body Sem_Prag is
       Arg2 : Node_Id;
       Arg3 : Node_Id;
       Arg4 : Node_Id;
-      --  First four pragma arguments (pragma argument association nodes, or
+      Arg5 : Node_Id;
+      --  First five pragma arguments (pragma argument association nodes, or
       --  Empty if the corresponding argument does not exist).
 
       type Name_List is array (Natural range <>) of Name_Id;
@@ -3780,12 +3818,6 @@ package body Sem_Prag is
       -- 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 Ada_2005_Pragma;
       --  Called for pragmas defined in Ada 2005, that are not in Ada 95. In
       --  Ada 95 mode, these are implementation defined pragmas, so should be
@@ -4041,7 +4073,8 @@ package body Sem_Prag is
       --  than library level instantiations these can appear in contexts which
       --  would normally be invalid (they only apply to the original template
       --  and to library level instantiations), and they are simply ignored,
-      --  which is implemented by rewriting them as null statements.
+      --  which is implemented by rewriting them as null statements and raising
+      --  exception to terminate analysis.
 
       procedure Check_Variant (Variant : Node_Id; UU_Typ : Entity_Id);
       --  Check an Unchecked_Union variant for lack of nested variants and
@@ -4051,10 +4084,10 @@ package body Sem_Prag is
       procedure Ensure_Aggregate_Form (Arg : Node_Id);
       --  Subsidiary routine to the processing of pragmas Abstract_State,
       --  Contract_Cases, Depends, Global, Initializes, Refined_Depends,
-      --  Refined_Global and Refined_State. Transform argument Arg into
-      --  an aggregate if not one already. N_Null is never transformed.
-      --  Arg may denote an aspect specification or a pragma argument
-      --  association.
+      --  Refined_Global, Refined_State and Subprogram_Variant. Transform
+      --  argument Arg into an aggregate if not one already. N_Null is never
+      --  transformed. Arg may denote an aspect specification or a pragma
+      --  argument association.
 
       procedure Error_Pragma (Msg : String);
       pragma No_Return (Error_Pragma);
@@ -4325,92 +4358,9 @@ package body Sem_Prag is
       procedure Set_Ravenscar_Profile (Profile : Profile_Name; N : Node_Id);
       --  Activate the set of configuration pragmas and restrictions that make
       --  up the Profile. Profile must be either GNAT_Extended_Ravenscar,
-      --  GNAT_Ravenscar_EDF, or Ravenscar. N is the corresponding pragma node,
-      --  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;
+      --  GNAT_Ravenscar_EDF, Jorvik, or Ravenscar. N is the corresponding
+      --  pragma node, which is used for error messages on any constructs
+      --  violating the profile.
 
       ---------------------
       -- Ada_2005_Pragma --
@@ -4499,7 +4449,17 @@ package body Sem_Prag is
          --  Subprogram declaration
 
          elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
-            null;
+
+            --  Pragmas Global and Depends are forbidden on null procedures
+            --  (SPARK RM 6.1.2(2)).
+
+            if Nkind (Specification (Subp_Decl)) = N_Procedure_Specification
+              and then Null_Present (Specification (Subp_Decl))
+            then
+               Error_Msg_N (Fix_Error
+                 ("pragma % cannot apply to null procedure"), N);
+               return;
+            end if;
 
          --  Task type
 
@@ -4694,12 +4654,12 @@ package body Sem_Prag is
          --  original pragma name by routine Original_Aspect_Pragma_Name.
 
          if Comes_From_Source (N) then
-            if Nam_In (Pname, Name_Pre, Name_Pre_Class) then
+            if Pname in Name_Pre | Name_Pre_Class then
                Is_Pre_Post := True;
                Set_Class_Present (N, Pname = Name_Pre_Class);
                Rewrite (Prag_Iden, Make_Identifier (Loc, Name_Precondition));
 
-            elsif Nam_In (Pname, Name_Post, Name_Post_Class) then
+            elsif Pname in Name_Post | Name_Post_Class then
                Is_Pre_Post := True;
                Set_Class_Present (N, Pname = Name_Post_Class);
                Rewrite (Prag_Iden, Make_Identifier (Loc, Name_Postcondition));
@@ -4710,7 +4670,7 @@ package body Sem_Prag is
          --  in a body. Pragmas Precondition and Postcondition were introduced
          --  before aspects and are not subject to the same aspect-like rules.
 
-         if Nam_In (Pname, Name_Precondition, Name_Postcondition) then
+         if Pname in Name_Precondition | Name_Postcondition then
             Duplicates_OK := True;
             In_Body_OK    := True;
          end if;
@@ -4834,7 +4794,18 @@ package body Sem_Prag is
          then
             null;
 
-         --  Otherwise the placement is illegal
+         --  For Ada 2020, pre/postconditions can appear on formal subprograms
+
+         elsif Nkind (Subp_Decl) = N_Formal_Concrete_Subprogram_Declaration
+            and then Ada_Version >= Ada_2020
+         then
+            null;
+
+         --  An access-to-subprogram type can have pre/postconditions, but
+         --  these are transferred to the generated subprogram wrapper and
+         --  analyzed there.
+
+         --  Otherwise the placement of the pragma is illegal
 
          else
             Pragma_Misplaced;
@@ -4851,14 +4822,14 @@ package body Sem_Prag is
          --  Chain the pragma on the contract for further processing by
          --  Analyze_Pre_Post_Condition_In_Decl_Part.
 
-         Add_Contract_Item (N, Defining_Entity (Subp_Decl));
+         Add_Contract_Item (N, Subp_Id);
 
          --  Fully analyze the pragma when it appears inside an entry or
          --  subprogram body because it cannot benefit from forward references.
 
-         if Nkind_In (Subp_Decl, N_Entry_Body,
-                                 N_Subprogram_Body,
-                                 N_Subprogram_Body_Stub)
+         if Nkind (Subp_Decl) in N_Entry_Body
+                               | N_Subprogram_Body
+                               | N_Subprogram_Body_Stub
          then
             --  The legality checks of pragmas Precondition and Postcondition
             --  are affected by the SPARK mode in effect and the volatility of
@@ -4898,11 +4869,9 @@ package body Sem_Prag is
 
          Body_Decl := Find_Related_Declaration_Or_Body (N, Do_Checks => True);
 
-         if not Nkind_In (Body_Decl, N_Entry_Body,
-                                     N_Subprogram_Body,
-                                     N_Subprogram_Body_Stub,
-                                     N_Task_Body,
-                                     N_Task_Body_Stub)
+         if Nkind (Body_Decl) not in
+              N_Entry_Body | N_Subprogram_Body | N_Subprogram_Body_Stub |
+              N_Task_Body  | N_Task_Body_Stub
          then
             Pragma_Misplaced;
             return;
@@ -4935,10 +4904,10 @@ package body Sem_Prag is
          --  When dealing with protected entries or protected subprograms, use
          --  the enclosing protected type as the proper context.
 
-         if Ekind_In (Spec_Id, E_Entry,
-                               E_Entry_Family,
-                               E_Function,
-                               E_Procedure)
+         if Ekind (Spec_Id) in E_Entry
+                             | E_Entry_Family
+                             | E_Function
+                             | E_Procedure
            and then Ekind (Scope (Spec_Id)) = E_Protected_Type
          then
             Spec_Decl := Declaration_Node (Scope (Spec_Id));
@@ -4960,7 +4929,7 @@ package body Sem_Prag is
 
          Mark_Ghost_Pragma (N, Spec_Id);
 
-         if Nam_In (Pname, Name_Refined_Depends, Name_Refined_Global) then
+         if Pname in Name_Refined_Depends | Name_Refined_Global then
             Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
          end if;
       end Analyze_Refined_Depends_Global_Post;
@@ -5525,7 +5494,7 @@ package body Sem_Prag is
       begin
          Check_Arg_Is_Identifier (Argx);
 
-         if not Nam_In (Chars (Argx), N1, N2) then
+         if Chars (Argx) not in N1 | N2 then
             Error_Msg_Name_2 := N1;
             Error_Msg_Name_3 := N2;
             Error_Pragma_Arg ("argument for pragma% must be% or%", Argx);
@@ -5541,7 +5510,7 @@ package body Sem_Prag is
       begin
          Check_Arg_Is_Identifier (Argx);
 
-         if not Nam_In (Chars (Argx), N1, N2, N3) then
+         if Chars (Argx) not in N1 | N2 | N3 then
             Error_Pragma_Arg ("invalid argument for pragma%", Argx);
          end if;
       end Check_Arg_Is_One_Of;
@@ -5555,7 +5524,7 @@ package body Sem_Prag is
       begin
          Check_Arg_Is_Identifier (Argx);
 
-         if not Nam_In (Chars (Argx), N1, N2, N3, N4) then
+         if Chars (Argx) not in N1 | N2 | N3 | N4 then
             Error_Pragma_Arg ("invalid argument for pragma%", Argx);
          end if;
       end Check_Arg_Is_One_Of;
@@ -5569,7 +5538,7 @@ package body Sem_Prag is
       begin
          Check_Arg_Is_Identifier (Argx);
 
-         if not Nam_In (Chars (Argx), N1, N2, N3, N4, N5) then
+         if Chars (Argx) not in N1 | N2 | N3 | N4 | N5 then
             Error_Pragma_Arg ("invalid argument for pragma%", Argx);
          end if;
       end Check_Arg_Is_One_Of;
@@ -5793,7 +5762,7 @@ package body Sem_Prag is
             --  For a single protected or a single task object, the error is
             --  issued on the original entity.
 
-            if Ekind_In (Id, E_Task_Type, E_Protected_Type) then
+            if Ekind (Id) in E_Task_Type | E_Protected_Type then
                Id := Defining_Identifier (Original_Node (Parent (Id)));
             end if;
 
@@ -5802,7 +5771,18 @@ package body Sem_Prag is
             then
                Error_Msg_NE ("aspect% for & previously given#", N, Id);
             else
-               Error_Msg_NE ("pragma% for & duplicates pragma#", N, Id);
+               --  If -gnatwr is set, warn in case of a duplicate pragma
+               --  [No_]Inline which is suspicious but not an error, generate
+               --  an error for other pragmas.
+
+               if Pragma_Name (N) in Name_Inline | Name_No_Inline then
+                  if Warn_On_Redundant_Constructs then
+                     Error_Msg_NE
+                       ("?r?pragma% for & duplicates pragma#", N, Id);
+                  end if;
+               else
+                  Error_Msg_NE ("pragma% for & duplicates pragma#", N, Id);
+               end if;
             end if;
 
             raise Pragma_Exit;
@@ -6111,7 +6091,7 @@ package body Sem_Prag is
                      --  The group and the current pragma are not in the same
                      --  declarative or statement list.
 
-                     if List_Containing (Stmt) /= List_Containing (N) then
+                     if not In_Same_List (Stmt, N) then
                         Grouping_Error (Stmt);
 
                      --  Try to reach the current pragma from the first pragma
@@ -6215,18 +6195,15 @@ package body Sem_Prag is
          --------------------
 
          function Is_Loop_Pragma (Stmt : Node_Id) return Boolean is
+            Original_Stmt : constant Node_Id := Original_Node (Stmt);
+
          begin
             --  Inspect the original node as Loop_Invariant and Loop_Variant
             --  pragmas are rewritten to null when assertions are disabled.
 
-            if Nkind (Original_Node (Stmt)) = N_Pragma then
-               return
-                 Nam_In (Pragma_Name_Unmapped (Original_Node (Stmt)),
-                         Name_Loop_Invariant,
-                         Name_Loop_Variant);
-            else
-               return False;
-            end if;
+            return Nkind (Original_Stmt) = N_Pragma
+             and then Pragma_Name_Unmapped (Original_Stmt)
+                   in Name_Loop_Invariant | Name_Loop_Variant;
          end Is_Loop_Pragma;
 
          ---------------------
@@ -6348,9 +6325,7 @@ package body Sem_Prag is
             elsif Nkind (P) = N_Handled_Sequence_Of_Statements then
                exit;
 
-            elsif Nkind_In (P, N_Package_Specification,
-                               N_Block_Statement)
-            then
+            elsif Nkind (P) in N_Package_Specification | N_Block_Statement then
                return;
 
             --  Note: the following tests seem a little peculiar, because
@@ -6359,10 +6334,8 @@ package body Sem_Prag is
             --  sequence, so the only way we get here is by being in the
             --  declarative part of the body.
 
-            elsif Nkind_In (P, N_Subprogram_Body,
-                               N_Package_Body,
-                               N_Task_Body,
-                               N_Entry_Body)
+            elsif Nkind (P) in
+              N_Subprogram_Body | N_Package_Body | N_Task_Body | N_Entry_Body
             then
                return;
             end if;
@@ -6614,7 +6587,7 @@ package body Sem_Prag is
 
                if Loc not in Source_First (Sindex) .. Source_Last (Sindex) then
                   Rewrite (N, Make_Null_Statement (Loc));
-                  return;
+                  raise Pragma_Exit;
 
                --  If before first declaration, the pragma applies to the
                --  enclosing unit, and the name if present must be this name.
@@ -6860,9 +6833,9 @@ package body Sem_Prag is
          if Nkind (P) = N_Compilation_Unit then
             Unit_Kind := Nkind (Unit (P));
 
-            if Nkind_In (Unit_Kind, N_Subprogram_Declaration,
-                                    N_Package_Declaration)
-              or else Unit_Kind in N_Generic_Declaration
+            if Unit_Kind in N_Subprogram_Declaration
+                          | N_Package_Declaration
+                          | N_Generic_Declaration
             then
                Unit_Name := Defining_Entity (Unit (P));
 
@@ -7259,14 +7232,18 @@ package body Sem_Prag is
       ------------------------------------------------
 
       procedure Process_Atomic_Independent_Shared_Volatile is
-         procedure Check_VFA_Conflicts (Ent : Entity_Id);
-         --  Apply additional checks for the GNAT pragma Volatile_Full_Access
+         procedure Check_Full_Access_Only (Ent : Entity_Id);
+         --  Apply legality checks to type or object Ent subject to the
+         --  Full_Access_Only aspect in Ada 2020 (RM C.6(8.2)).
 
          procedure Mark_Component_Or_Object (Ent : Entity_Id);
-         --  Appropriately set flags on the given entity (either an array or
+         --  Appropriately set flags on the given entityeither an array or
          --  record component, or an object declaration) according to the
          --  current pragma.
 
+         procedure Mark_Type (Ent : Entity_Id);
+         --  Appropriately set flags on the given entity, a type
+
          procedure Set_Atomic_VFA (Ent : Entity_Id);
          --  Set given type as Is_Atomic or Is_Volatile_Full_Access. Also, if
          --  no explicit alignment was given, set alignment to unknown, since
@@ -7274,118 +7251,106 @@ package body Sem_Prag is
          --  full access arrays. Note: this is necessary for derived types.
 
          -------------------------
-         -- Check_VFA_Conflicts --
+         -- Check_Full_Access_Only --
          -------------------------
 
-         procedure Check_VFA_Conflicts (Ent : Entity_Id) is
-            Comp : Entity_Id;
+         procedure Check_Full_Access_Only (Ent : Entity_Id) is
             Typ  : Entity_Id;
 
-            VFA_And_Atomic : Boolean := False;
-            --  Set True if atomic component present
+            Full_Access_Subcomponent : exception;
+            --  Exception raised if a full access subcomponent is found
 
-            VFA_And_Aliased : Boolean := False;
-            --  Set True if aliased component present
+            Generic_Type_Subcomponent : exception;
+            --  Exception raised if a subcomponent with generic type is found
 
-         begin
-            --  Fetch the type in case we are dealing with an object or
-            --  component.
+            procedure Check_Subcomponents (Typ : Entity_Id);
+            --  Apply checks to subcomponents recursively
 
-            if Is_Type (Ent) then
-               Typ := Ent;
-            else
-               pragma Assert (Is_Object (Ent)
-                 or else
-                   Nkind (Declaration_Node (Ent)) = N_Component_Declaration);
+            -------------------------
+            -- Check_Subcomponents --
+            -------------------------
 
-               Typ := Etype (Ent);
-            end if;
+            procedure Check_Subcomponents (Typ : Entity_Id) is
+               Comp : Entity_Id;
 
-            --  Check Atomic and VFA used together
+            begin
+               if Is_Array_Type (Typ) then
+                  Comp := Component_Type (Typ);
 
-            if Prag_Id = Pragma_Volatile_Full_Access
-              or else Is_Volatile_Full_Access (Ent)
-            then
-               if Prag_Id = Pragma_Atomic
-                 or else Prag_Id = Pragma_Shared
-                 or else Is_Atomic (Ent)
-               then
-                  VFA_And_Atomic := True;
+                  if Has_Atomic_Components (Typ)
+                    or else Is_Full_Access (Comp)
+                  then
+                     raise Full_Access_Subcomponent;
 
-               elsif Is_Array_Type (Typ) then
-                  VFA_And_Atomic := Has_Atomic_Components (Typ);
+                  elsif Is_Generic_Type (Comp) then
+                     raise Generic_Type_Subcomponent;
+                  end if;
 
-               --  Note: Has_Atomic_Components is not used below, as this flag
-               --  represents the pragma of the same name, Atomic_Components,
-               --  which only applies to arrays.
+                  --  Recurse on the component type
 
-               elsif Is_Record_Type (Typ) then
-                  --  Attributes cannot be applied to discriminants, only
-                  --  regular record components.
+                  Check_Subcomponents (Comp);
 
-                  Comp := First_Component (Typ);
+               elsif Is_Record_Type (Typ) then
+                  Comp := First_Component_Or_Discriminant (Typ);
                   while Present (Comp) loop
-                     if Is_Atomic (Comp)
-                       or else Is_Atomic (Typ)
+
+                     if Is_Full_Access (Comp)
+                       or else Is_Full_Access (Etype (Comp))
                      then
-                        VFA_And_Atomic := True;
+                        raise Full_Access_Subcomponent;
 
-                        exit;
+                     elsif Is_Generic_Type (Etype (Comp)) then
+                        raise Generic_Type_Subcomponent;
                      end if;
 
-                     Next_Component (Comp);
+                     --  Recurse on the component type
+
+                     Check_Subcomponents (Etype (Comp));
+
+                     Next_Component_Or_Discriminant (Comp);
                   end loop;
                end if;
+            end Check_Subcomponents;
 
-               if VFA_And_Atomic then
-                  Error_Pragma
-                    ("cannot have Volatile_Full_Access and Atomic for same "
-                     & "entity");
-               end if;
-            end if;
+         --  Start of processing for Check_Full_Access_Only
 
-            --  Check for the application of VFA to an entity that has aliased
-            --  components.
+         begin
+            --  Fetch the type in case we are dealing with an object or
+            --  component.
 
-            if Prag_Id = Pragma_Volatile_Full_Access then
-               if Is_Array_Type (Typ)
-                 and then Has_Aliased_Components (Typ)
-               then
-                  VFA_And_Aliased := True;
+            if Is_Type (Ent) then
+               Typ := Ent;
+            else
+               pragma Assert (Is_Object (Ent)
+                 or else
+                   Nkind (Declaration_Node (Ent)) = N_Component_Declaration);
 
-               --  Note: Has_Aliased_Components, like Has_Atomic_Components,
-               --  and Has_Independent_Components, applies only to arrays.
-               --  However, this flag does not have a corresponding pragma, so
-               --  perhaps it should be possible to apply it to record types as
-               --  well. Should this be done ???
+               Typ := Etype (Ent);
+            end if;
 
-               elsif Is_Record_Type (Typ) then
-                  --  It is possible to have an aliased discriminant, so they
-                  --  must be checked along with normal components.
+            if not Is_Volatile (Ent) and then not Is_Volatile (Typ) then
+               Error_Pragma
+                 ("cannot have Full_Access_Only without Volatile/Atomic "
+                  & "(RM C.6(8.2))");
+               return;
+            end if;
 
-                  Comp := First_Component_Or_Discriminant (Typ);
-                  while Present (Comp) loop
-                     if Is_Aliased (Comp)
-                       or else Is_Aliased (Etype (Comp))
-                     then
-                        VFA_And_Aliased := True;
-                        Check_SPARK_05_Restriction
-                          ("aliased is not allowed", Comp);
+            --  Check all the subcomponents of the type recursively, if any
 
-                        exit;
-                     end if;
+            Check_Subcomponents (Typ);
 
-                     Next_Component_Or_Discriminant (Comp);
-                  end loop;
-               end if;
+         exception
+            when Full_Access_Subcomponent =>
+               Error_Pragma
+                 ("cannot have Full_Access_Only with full access subcomponent "
+                  & "(RM C.6(8.2))");
 
-               if VFA_And_Aliased then
-                  Error_Pragma
-                    ("cannot apply Volatile_Full_Access (aliased component "
-                     & "present)");
-               end if;
-            end if;
-         end Check_VFA_Conflicts;
+            when Generic_Type_Subcomponent =>
+               Error_Pragma
+                 ("cannot have Full_Access_Only with subcomponent of generic "
+                  & "type (RM C.6(8.2))");
+
+         end Check_Full_Access_Only;
 
          ------------------------------
          -- Mark_Component_Or_Object --
@@ -7432,6 +7397,78 @@ package body Sem_Prag is
             end if;
          end Mark_Component_Or_Object;
 
+         ---------------
+         -- Mark_Type --
+         ---------------
+
+         procedure Mark_Type (Ent : Entity_Id) is
+         begin
+            --  Attribute belongs on the base type. If the view of the type is
+            --  currently private, it also belongs on the underlying type.
+
+            --  In Ada 2020, the pragma can apply to a formal type, for which
+            --  there may be no underlying type.
+
+            if Prag_Id = Pragma_Atomic
+              or else Prag_Id = Pragma_Shared
+              or else Prag_Id = Pragma_Volatile_Full_Access
+            then
+               Set_Atomic_VFA (Ent);
+               Set_Atomic_VFA (Base_Type (Ent));
+
+               if not Is_Generic_Type (Ent) then
+                  Set_Atomic_VFA (Underlying_Type (Ent));
+               end if;
+            end if;
+
+            --  Atomic/Shared/Volatile_Full_Access imply Independent
+
+            if Prag_Id /= Pragma_Volatile then
+               Set_Is_Independent (Ent);
+               Set_Is_Independent (Base_Type (Ent));
+
+               if not Is_Generic_Type (Ent) then
+                  Set_Is_Independent (Underlying_Type (Ent));
+
+                  if Prag_Id = Pragma_Independent then
+                     Record_Independence_Check (N, Base_Type (Ent));
+                  end if;
+               end if;
+            end if;
+
+            --  Atomic/Shared/Volatile_Full_Access imply Volatile
+
+            if Prag_Id /= Pragma_Independent then
+               Set_Is_Volatile (Ent);
+               Set_Is_Volatile (Base_Type (Ent));
+
+               if not Is_Generic_Type (Ent) then
+                  Set_Is_Volatile (Underlying_Type (Ent));
+                  Set_Treat_As_Volatile (Underlying_Type (Ent));
+               end if;
+
+               Set_Treat_As_Volatile (Ent);
+            end if;
+
+            --  Apply Volatile to the composite type's individual components,
+            --  (RM C.6(8/3)).
+
+            if Prag_Id = Pragma_Volatile
+              and then Is_Record_Type (Etype (Ent))
+            then
+               declare
+                  Comp : Entity_Id;
+               begin
+                  Comp := First_Component (Ent);
+                  while Present (Comp) loop
+                     Mark_Component_Or_Object (Comp);
+
+                     Next_Component (Comp);
+                  end loop;
+               end;
+            end if;
+         end Mark_Type;
+
          --------------------
          -- Set_Atomic_VFA --
          --------------------
@@ -7469,6 +7506,7 @@ package body Sem_Prag is
          end if;
 
          E := Entity (E_Arg);
+         Decl := Declaration_Node (E);
 
          --  A pragma that applies to a Ghost entity becomes Ghost for the
          --  purposes of legality checks and removal of ignored Ghost code.
@@ -7479,9 +7517,43 @@ package body Sem_Prag is
 
          Check_Duplicate_Pragma (E);
 
-         --  Check appropriateness of the entity
+         --  Check the constraints of Full_Access_Only in Ada 2020. Note that
+         --  they do not apply to GNAT's Volatile_Full_Access because 1) this
+         --  aspect subsumes the Volatile aspect and 2) nesting is supported
+         --  for this aspect and the outermost enclosing VFA object prevails.
 
-         Decl := Declaration_Node (E);
+         --  Note also that we used to forbid specifying both Atomic and VFA on
+         --  the same type or object, but the restriction has been lifted in
+         --  light of the semantics of Full_Access_Only and Atomic in Ada 2020.
+
+         if Prag_Id = Pragma_Volatile_Full_Access
+           and then From_Aspect_Specification (N)
+           and then
+             Get_Aspect_Id (Corresponding_Aspect (N)) = Aspect_Full_Access_Only
+         then
+            Check_Full_Access_Only (E);
+         end if;
+
+         --  The following check is only relevant when SPARK_Mode is on as
+         --  this is not a standard Ada legality rule. Pragma Volatile can
+         --  only apply to a full type declaration or an object declaration
+         --  (SPARK RM 7.1.3(2)). Original_Node is necessary to account for
+         --  untagged derived types that are rewritten as subtypes of their
+         --  respective root types.
+
+         if SPARK_Mode = On
+           and then Prag_Id = Pragma_Volatile
+           and then Nkind (Original_Node (Decl)) not in
+                      N_Full_Type_Declaration        |
+                      N_Formal_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 "
+               & "declaration", Arg1);
+         end if;
 
          --  Deal with the case where the pragma/attribute is applied to a type
 
@@ -7494,58 +7566,7 @@ package body Sem_Prag is
                Check_First_Subtype (Arg1);
             end if;
 
-            --  Attribute belongs on the base type. If the view of the type is
-            --  currently private, it also belongs on the underlying type.
-
-            if Prag_Id = Pragma_Atomic
-              or else Prag_Id = Pragma_Shared
-              or else Prag_Id = Pragma_Volatile_Full_Access
-            then
-               Set_Atomic_VFA (E);
-               Set_Atomic_VFA (Base_Type (E));
-               Set_Atomic_VFA (Underlying_Type (E));
-            end if;
-
-            --  Atomic/Shared/Volatile_Full_Access imply Independent
-
-            if Prag_Id /= Pragma_Volatile then
-               Set_Is_Independent (E);
-               Set_Is_Independent (Base_Type (E));
-               Set_Is_Independent (Underlying_Type (E));
-
-               if Prag_Id = Pragma_Independent then
-                  Record_Independence_Check (N, Base_Type (E));
-               end if;
-            end if;
-
-            --  Atomic/Shared/Volatile_Full_Access imply Volatile
-
-            if Prag_Id /= Pragma_Independent then
-               Set_Is_Volatile (E);
-               Set_Is_Volatile (Base_Type (E));
-               Set_Is_Volatile (Underlying_Type (E));
-
-               Set_Treat_As_Volatile (E);
-               Set_Treat_As_Volatile (Underlying_Type (E));
-            end if;
-
-            --  Apply Volatile to the composite type's individual components,
-            --  (RM C.6(8/3)).
-
-            if Prag_Id = Pragma_Volatile
-              and then Is_Record_Type (Etype (E))
-            then
-               declare
-                  Comp : Entity_Id;
-               begin
-                  Comp := First_Component (E);
-                  while Present (Comp) loop
-                     Mark_Component_Or_Object (Comp);
-
-                     Next_Component (Comp);
-                  end loop;
-               end;
-            end if;
+            Mark_Type (E);
 
          --  Deal with the case where the pragma/attribute applies to a
          --  component or object declaration.
@@ -7559,35 +7580,13 @@ package body Sem_Prag is
             end if;
 
             Mark_Component_Or_Object (E);
+
+         --  In other cases give an error
+
          else
             Error_Pragma_Arg ("inappropriate entity for pragma%", Arg1);
          end if;
-
-         --  Perform the checks needed to assure the proper use of the GNAT
-         --  pragma Volatile_Full_Access.
-
-         Check_VFA_Conflicts (E);
-
-         --  The following check is only relevant when SPARK_Mode is on as
-         --  this is not a standard Ada legality rule. Pragma Volatile can
-         --  only apply to a full type declaration or an object declaration
-         --  (SPARK RM 7.1.3(2)). Original_Node is necessary to account for
-         --  untagged derived types that are rewritten as subtypes of their
-         --  respective root types.
-
-         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,
-                                  N_Single_Protected_Declaration,
-                                  N_Single_Task_Declaration)
-         then
-            Error_Pragma_Arg
-              ("argument of pragma % must denote a full type or object "
-               & "declaration", Arg1);
-         end if;
-      end Process_Atomic_Independent_Shared_Volatile;
+      end Process_Atomic_Independent_Shared_Volatile;
 
       -------------------------------------------
       -- Process_Compile_Time_Warning_Or_Error --
@@ -7596,23 +7595,60 @@ package body Sem_Prag is
       procedure Process_Compile_Time_Warning_Or_Error is
          P : Node_Id := Parent (N);
          Arg1x : constant Node_Id := Get_Pragma_Arg (Arg1);
+
       begin
-         --  In GNATprove mode, pragmas Compile_Time_Error and
+         Check_Arg_Count (2);
+         Check_No_Identifiers;
+         Check_Arg_Is_OK_Static_Expression (Arg2, Standard_String);
+         Analyze_And_Resolve (Arg1x, Standard_Boolean);
+
+         --  In GNATprove mode, pragma Compile_Time_Error is translated as
+         --  a Check pragma in GNATprove mode, handled as an assumption in
+         --  GNATprove. This is correct as the compiler will issue an error
+         --  if the condition cannot be statically evaluated to False.
          --  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.
+         --  objects decided in gigi) so it makes no sense to issue a warning
+         --  in GNATprove.
 
          if GNATprove_Mode then
-            Rewrite (N, Make_Null_Statement (Loc));
+            if Prag_Id = Pragma_Compile_Time_Error then
+               declare
+                  New_Args : List_Id;
+               begin
+                  --  Implement Compile_Time_Error by generating
+                  --  a corresponding Check pragma:
+
+                  --    pragma Check (name, condition);
+
+                  --  where name is the identifier matching the pragma name. So
+                  --  rewrite pragma in this manner and analyze the result.
+
+                  New_Args := New_List
+                    (Make_Pragma_Argument_Association
+                       (Loc,
+                        Expression => Make_Identifier (Loc, Pname)),
+                     Make_Pragma_Argument_Association
+                       (Sloc (Arg1x),
+                        Expression => Arg1x));
+
+                  --  Rewrite as Check pragma
+
+                  Rewrite (N,
+                           Make_Pragma (Loc,
+                             Chars                        => Name_Check,
+                             Pragma_Argument_Associations => New_Args));
+
+                  Analyze (N);
+               end;
+
+            else
+               Rewrite (N, Make_Null_Statement (Loc));
+            end if;
+
             return;
          end if;
 
-         Check_Arg_Count (2);
-         Check_No_Identifiers;
-         Check_Arg_Is_OK_Static_Expression (Arg2, Standard_String);
-         Analyze_And_Resolve (Arg1x, Standard_Boolean);
-
          --  If the condition is known at compile time (now), validate it now.
          --  Otherwise, register the expression for validation after the back
          --  end has been called, because it might be known at compile time
@@ -7626,7 +7662,7 @@ package body Sem_Prag is
          else
             while Present (P) and then Nkind (P) not in N_Generic_Declaration
             loop
-               if Nkind_In (P, N_Package_Body, N_Subprogram_Body) then
+               if Nkind (P) in N_Package_Body | N_Subprogram_Body then
                   P := Corresponding_Spec (P);
                else
                   P := Parent (P);
@@ -7772,17 +7808,17 @@ package body Sem_Prag is
                   then
                      --  Give error if same as our pragma or Export/Convention
 
-                     if Nam_In (Pragma_Name_Unmapped (Decl),
-                                Name_Export,
-                                Name_Convention,
-                                Pragma_Name_Unmapped (N))
+                     if Pragma_Name_Unmapped (Decl)
+                          in Name_Export
+                           | Name_Convention
+                           | Pragma_Name_Unmapped (N)
                      then
                         exit;
 
                      --  Case of Import/Interface or the other way round
 
-                     elsif Nam_In (Pragma_Name_Unmapped (Decl),
-                                   Name_Interface, Name_Import)
+                     elsif Pragma_Name_Unmapped (Decl)
+                             in Name_Interface | Name_Import
                      then
                         --  Here we know that we have Import and Interface. It
                         --  doesn't matter which way round they are. See if
@@ -7841,59 +7877,24 @@ package body Sem_Prag is
                Error_Pragma_Arg
                  ("cannot change convention for overridden dispatching "
                   & "operation", Arg1);
-            end if;
-
-            --  Special checks for Convention_Stdcall
-
-            if C = Convention_Stdcall then
-
-               --  A dispatching call is not allowed. A dispatching subprogram
-               --  cannot be used to interface to the Win32 API, so in fact
-               --  this check does not impose any effective restriction.
 
-               if Is_Dispatching_Operation (E) then
-                  Error_Msg_Sloc := Sloc (E);
+            --  Special check for convention Stdcall: a dispatching call is not
+            --  allowed. A dispatching subprogram cannot be used to interface
+            --  to the Win32 API, so this check actually does not impose any
+            --  effective restriction.
 
-                  --  Note: make this unconditional so that if there is more
-                  --  than one call to which the pragma applies, we get a
-                  --  message for each call. Also don't use Error_Pragma,
-                  --  so that we get multiple messages.
-
-                  Error_Msg_N
-                    ("dispatching subprogram# cannot use Stdcall convention!",
-                     Arg1);
-
-               --  Several allowed cases
-
-               elsif Is_Subprogram_Or_Generic_Subprogram (E)
-
-                 --  A variable is OK
-
-                 or else Ekind (E) = E_Variable
-
-                 --  A component as well. The entity does not have its Ekind
-                 --  set until the enclosing record declaration is fully
-                 --  analyzed.
-
-                 or else Nkind (Parent (E)) = N_Component_Declaration
-
-                 --  An access to subprogram is also allowed
-
-                 or else
-                   (Is_Access_Type (E)
-                     and then Ekind (Designated_Type (E)) = E_Subprogram_Type)
-
-                 --  Allow internal call to set convention of subprogram type
-
-                 or else Ekind (E) = E_Subprogram_Type
-               then
-                  null;
+            elsif Is_Dispatching_Operation (E)
+              and then C = Convention_Stdcall
+            then
+               --  Note: make this unconditional so that if there is more
+               --  than one call to which the pragma applies, we get a
+               --  message for each call. Also don't use Error_Pragma,
+               --  so that we get multiple messages.
 
-               else
-                  Error_Pragma_Arg
-                    ("second argument of pragma% must be subprogram (type)",
-                     Arg2);
-               end if;
+               Error_Msg_Sloc := Sloc (E);
+               Error_Msg_N
+                 ("dispatching subprogram# cannot use Stdcall convention!",
+                  Get_Pragma_Arg (Arg1));
             end if;
 
             --  Set the convention
@@ -7904,26 +7905,38 @@ package body Sem_Prag is
             --  For the case of a record base type, also set the convention of
             --  any anonymous access types declared in the record which do not
             --  currently have a specified convention.
+            --  Similarly for an array base type and anonymous access types
+            --  components.
 
-            if Is_Record_Type (E) and then Is_Base_Type (E) then
-               declare
-                  Comp : Node_Id;
+            if Is_Base_Type (E) then
+               if Is_Record_Type (E) then
+                  declare
+                     Comp : Node_Id;
 
-               begin
-                  Comp := First_Component (E);
-                  while Present (Comp) loop
-                     if Present (Etype (Comp))
-                       and then Ekind_In (Etype (Comp),
-                                          E_Anonymous_Access_Type,
-                                          E_Anonymous_Access_Subprogram_Type)
-                       and then not Has_Convention_Pragma (Comp)
-                     then
-                        Set_Convention (Comp, C);
-                     end if;
+                  begin
+                     Comp := First_Component (E);
+                     while Present (Comp) loop
+                        if Present (Etype (Comp))
+                          and then
+                            Ekind (Etype (Comp)) in
+                              E_Anonymous_Access_Type |
+                              E_Anonymous_Access_Subprogram_Type
+                          and then not Has_Convention_Pragma (Comp)
+                        then
+                           Set_Convention (Comp, C);
+                        end if;
 
-                     Next_Component (Comp);
-                  end loop;
-               end;
+                        Next_Component (Comp);
+                     end loop;
+                  end;
+
+               elsif Is_Array_Type (E)
+                 and then Ekind (Component_Type (E)) in
+                            E_Anonymous_Access_Type |
+                            E_Anonymous_Access_Subprogram_Type
+               then
+                  Set_Convention (Designated_Type (Component_Type (E)), C);
+               end if;
             end if;
 
             --  Deal with incomplete/private type case, where underlying type
@@ -7985,6 +7998,7 @@ package body Sem_Prag is
          E         : Entity_Id;
          E1        : Entity_Id;
          Id        : Node_Id;
+         Subp      : Entity_Id;
 
       --  Start of processing for Process_Convention
 
@@ -8081,8 +8095,8 @@ package body Sem_Prag is
 
                E := Alias (E);
 
-            elsif Nkind_In (Parent (E), N_Full_Type_Declaration,
-                                        N_Private_Extension_Declaration)
+            elsif Nkind (Parent (E)) in
+                    N_Full_Type_Declaration | N_Private_Extension_Declaration
               and then Scope (E) = Scope (Alias (E))
             then
                E := Alias (E);
@@ -8106,7 +8120,7 @@ package body Sem_Prag is
 
          --  Check that we are not applying this to a named constant
 
-         if Ekind_In (E, E_Named_Integer, E_Named_Real) then
+         if Is_Named_Number (E) then
             Error_Msg_Name_1 := Pname;
             Error_Msg_N
               ("cannot apply pragma% to named constant!",
@@ -8153,16 +8167,123 @@ package body Sem_Prag is
             --  Accept Intrinsic Export on types if Relaxed_RM_Semantics
 
             if not (Is_Type (E) and then Relaxed_RM_Semantics) then
+               if From_Aspect_Specification (N) then
+                  Error_Pragma_Arg
+                     ("entity for aspect% must be a subprogram", Arg2);
+               else
+                  Error_Pragma_Arg
+                     ("second argument of pragma% must be a subprogram", Arg2);
+               end if;
+            end if;
+
+         --  Special checks for C_Variadic_n
+
+         elsif C in Convention_C_Variadic then
+
+            --  Several allowed cases
+
+            if Is_Subprogram_Or_Generic_Subprogram (E) then
+               Subp := E;
+
+            --  An access to subprogram is also allowed
+
+            elsif Is_Access_Type (E)
+              and then Ekind (Designated_Type (E)) = E_Subprogram_Type
+            then
+               Subp := Designated_Type (E);
+
+            --  Allow internal call to set convention of subprogram type
+
+            elsif Ekind (E) = E_Subprogram_Type then
+               Subp := E;
+
+            else
+               Error_Pragma_Arg
+                 ("argument of pragma% must be subprogram or access type",
+                  Arg2);
+               Subp := Empty;
+            end if;
+
+            --  ISO C requires a named parameter before the ellipsis, so a
+            --  variadic C function taking 0 fixed parameter cannot exist.
+
+            if C = Convention_C_Variadic_0 then
+
+               Error_Msg_N
+                 ("??C_Variadic_0 cannot be used for an 'I'S'O C function",
+                  Get_Pragma_Arg (Arg2));
+
+            --  Now check the number of parameters of the subprogram and give
+            --  an error if it is lower than n.
+
+            elsif Present (Subp) then
+               declare
+                  Minimum : constant Nat :=
+                    Convention_Id'Pos (C) -
+                      Convention_Id'Pos (Convention_C_Variadic_0);
+
+                  Count  : Nat;
+                  Formal : Entity_Id;
+
+               begin
+                  Count := 0;
+                  Formal := First_Formal (Subp);
+                  while Present (Formal) loop
+                     Count := Count + 1;
+                     Next_Formal (Formal);
+                  end loop;
+
+                  if Count < Minimum then
+                     Error_Msg_Uint_1 := UI_From_Int (Minimum);
+                     Error_Pragma_Arg
+                       ("argument of pragma% must have at least"
+                        & "^ parameters", Arg2);
+                  end if;
+               end;
+            end if;
+
+         --  Special checks for Stdcall
+
+         elsif C = Convention_Stdcall then
+
+            --  Several allowed cases
+
+            if Is_Subprogram_Or_Generic_Subprogram (E)
+
+              --  A variable is OK
+
+              or else Ekind (E) = E_Variable
+
+              --  A component as well. The entity does not have its Ekind
+              --  set until the enclosing record declaration is fully
+              --  analyzed.
+
+              or else Nkind (Parent (E)) = N_Component_Declaration
+
+              --  An access to subprogram is also allowed
+
+              or else
+                (Is_Access_Type (E)
+                  and then Ekind (Designated_Type (E)) = E_Subprogram_Type)
+
+              --  Allow internal call to set convention of subprogram type
+
+              or else Ekind (E) = E_Subprogram_Type
+            then
+               null;
+
+            else
                Error_Pragma_Arg
-                 ("second argument of pragma% must be a subprogram", Arg2);
+                 ("argument of pragma% must be subprogram or access type",
+                  Arg2);
             end if;
          end if;
 
+         Set_Convention_From_Pragma (E);
+
          --  Deal with non-subprogram cases
 
          if not Is_Subprogram_Or_Generic_Subprogram (E) then
-            Set_Convention_From_Pragma (E);
-
             if Is_Type (E) then
 
                --  The pragma must apply to a first subtype, but it can also
@@ -8190,9 +8311,6 @@ package body Sem_Prag is
          --  compilation unit.
 
          else
-            Comp_Unit := Get_Source_Unit (E);
-            Set_Convention_From_Pragma (E);
-
             --  Treat a pragma Import as an implicit body, and pragma import
             --  as implicit reference (for navigation in GNAT Studio).
 
@@ -8237,6 +8355,7 @@ package body Sem_Prag is
             --  Otherwise Loop through the homonyms of the pragma argument's
             --  entity, an apply convention to those in the current scope.
 
+            Comp_Unit := Get_Source_Unit (E);
             E1 := Ent;
 
             loop
@@ -8362,7 +8481,7 @@ package body Sem_Prag is
          Process_Extended_Import_Export_Internal_Arg (Arg_Internal);
          Def_Id := Entity (Arg_Internal);
 
-         if not Ekind_In (Def_Id, E_Constant, E_Variable) then
+         if Ekind (Def_Id) not in E_Constant | E_Variable then
             Error_Pragma_Arg
               ("pragma% must designate an object", Arg_Internal);
          end if;
@@ -8587,8 +8706,8 @@ package body Sem_Prag is
                   Match := False;
 
                elsif Etype (Def_Id) /= Standard_Void_Type
-                 and then Nam_In (Pname, Name_Export_Procedure,
-                                         Name_Import_Procedure)
+                 and then
+                   Pname in Name_Export_Procedure | Name_Import_Procedure
                then
                   Match := False;
 
@@ -8846,7 +8965,8 @@ package body Sem_Prag is
                               Set_Mechanism_Value
                                 (Formal, Expression (Massoc));
 
-                              --  Set entity on identifier (needed by ASIS)
+                              --  Set entity on identifier for proper tree
+                              --  structure.
 
                               Set_Entity (Choice, Formal);
 
@@ -8998,7 +9118,7 @@ package body Sem_Prag is
 
          --  Various error checks
 
-         if Ekind_In (Def_Id, E_Variable, E_Constant) then
+         if Ekind (Def_Id) in E_Variable | E_Constant then
 
             --  We do not permit Import to apply to a renaming declaration
 
@@ -9325,10 +9445,17 @@ package body Sem_Prag is
             Process_Import_Predefined_Type;
 
          else
-            Error_Pragma_Arg
-              ("second argument of pragma% must be object, subprogram "
-               & "or incomplete type",
-               Arg2);
+            if From_Aspect_Specification (N) then
+               Error_Pragma_Arg
+                  ("entity for aspect% must be object, subprogram "
+                     & "or incomplete type",
+                   Arg2);
+            else
+               Error_Pragma_Arg
+                  ("second argument of pragma% must be object, subprogram "
+                     & "or incomplete type",
+                   Arg2);
+            end if;
          end if;
 
          --  If this pragma applies to a compilation unit, then the unit, which
@@ -9497,9 +9624,9 @@ package body Sem_Prag is
                   --       pragma Inline_Always (Proc);
                   --    end Pack;
 
-                  elsif Nkind_In (Context, N_Package_Specification,
-                                           N_Protected_Definition,
-                                           N_Task_Definition)
+                  elsif Nkind (Context) in N_Package_Specification
+                                         | N_Protected_Definition
+                                         | N_Task_Definition
                     and then Init_List = Visible_Declarations (Context)
                     and then Prag_List = Private_Declarations (Context)
                   then
@@ -9759,20 +9886,11 @@ package body Sem_Prag is
                   --  the test will have been applied to the original generic.
 
                   elsif Nkind (Decl) in N_Formal_Subprogram_Declaration
-                    and then List_Containing (Decl) = List_Containing (N)
+                    and then In_Same_List (Decl, N)
                     and then not In_Instance
                   then
                      Error_Msg_N
                        ("Inline cannot apply to a formal subprogram", N);
-
-                  --  If Subp is a renaming, it is the renamed entity that
-                  --  will appear in any call, and be inlined. However, for
-                  --  ASIS uses it is convenient to indicate that the renaming
-                  --  itself is an inlined subprogram, so that some gnatcheck
-                  --  rules can be applied in the absence of expansion.
-
-                  elsif Nkind (Decl) = N_Subprogram_Renaming_Declaration then
-                     Set_Inline_Flags (Subp);
                   end if;
                end if;
 
@@ -9925,6 +10043,18 @@ package body Sem_Prag is
                   Applies := True;
 
                else
+                  --  Check for RM 13.1(9.2/4): If a [...] aspect_specification
+                  --  is given that directly specifies an aspect of an entity,
+                  --  then it is illegal to give another [...]
+                  --  aspect_specification that directly specifies the same
+                  --  aspect of the entity.
+                  --  We only check Subp directly as per "directly specifies"
+                  --  above and because the case of pragma Inline is really
+                  --  special given its pre aspect usage.
+
+                  Check_Duplicate_Pragma (Subp);
+                  Record_Rep_Item (Subp, N);
+
                   Make_Inline (Subp);
 
                   --  For the pragma case, climb homonym chain. This is
@@ -9936,8 +10066,8 @@ package body Sem_Prag is
                      while Present (Homonym (Subp))
                        and then Scope (Homonym (Subp)) = Current_Scope
                      loop
-                        Make_Inline (Homonym (Subp));
                         Subp := Homonym (Subp);
+                        Make_Inline (Subp);
                      end loop;
                   end if;
                end if;
@@ -10307,25 +10437,39 @@ package body Sem_Prag is
                   else
                      Add_To_Config_Boolean_Restrictions (No_Elaboration_Code);
                   end if;
+
+               --  Special processing for No_Tasking restriction (not just a
+               --  warning) when it appears as a configuration pragma.
+
+               elsif R_Id = No_Tasking
+                 and then No (Cunit (Main_Unit))
+                 and then not Warn
+               then
+                  Set_Global_No_Tasking;
                end if;
 
-               --  If this is a warning, then set the warning unless we already
-               --  have a real restriction active (we never want a warning to
-               --  override a real restriction).
+               Set_Restriction (R_Id, N, Warn);
 
-               if Warn then
-                  if not Restriction_Active (R_Id) then
-                     Set_Restriction (R_Id, N);
-                     Restriction_Warnings (R_Id) := True;
-                  end if;
+               if R_Id = No_Dynamic_CPU_Assignment
+                 or else R_Id = No_Tasks_Unassigned_To_CPU
+               then
+                  --  These imply No_Dependence =>
+                  --     "System.Multiprocessors.Dispatching_Domains".
+                  --  This is not strictly what the AI says, but it eliminates
+                  --  the need for run-time checks, which are undesirable in
+                  --  this context.
 
-               --  If real restriction case, then set it and make sure that the
-               --  restriction warning flag is off, since a real restriction
-               --  always overrides a warning.
+                  Set_Restriction_No_Dependence
+                    (Sel_Comp
+                       (Sel_Comp ("system", "multiprocessors", Loc),
+                        "dispatching_domains"),
+                     Warn);
+               end if;
 
-               else
-                  Set_Restriction (R_Id, N);
-                  Restriction_Warnings (R_Id) := False;
+               if R_Id = No_Tasks_Unassigned_To_CPU then
+                  --  Likewise, imply No_Dynamic_CPU_Assignment
+
+                  Set_Restriction (No_Dynamic_CPU_Assignment, N, Warn);
                end if;
 
                --  Check for obsolescent restrictions in Ada 2005 mode
@@ -10469,26 +10613,7 @@ package body Sem_Prag is
                     ("pragma ignored, value too large??", Arg);
                end if;
 
-               --  Warning case. If the real restriction is active, then we
-               --  ignore the request, since warning never overrides a real
-               --  restriction. Otherwise we set the proper warning. Note that
-               --  this circuit sets the warning again if it is already set,
-               --  which is what we want, since the constant may have changed.
-
-               if Warn then
-                  if not Restriction_Active (R_Id) then
-                     Set_Restriction
-                       (R_Id, N, Integer (UI_To_Int (Val)));
-                     Restriction_Warnings (R_Id) := True;
-                  end if;
-
-               --  Real restriction case, set restriction and make sure warning
-               --  flag is off since real restriction always overrides warning.
-
-               else
-                  Set_Restriction (R_Id, N, Integer (UI_To_Int (Val)));
-                  Restriction_Warnings (R_Id) := False;
-               end if;
+               Set_Restriction (R_Id, N, Warn, Integer (UI_To_Int (Val)));
             end if;
 
             Next (Arg);
@@ -11042,7 +11167,7 @@ package body Sem_Prag is
       --    Set required policies
 
       --      pragma Task_Dispatching_Policy (FIFO_Within_Priorities)
-      --        (For Ravenscar and GNAT_Extended_Ravenscar profiles)
+      --        (For Ravenscar, Jorvik, and GNAT_Extended_Ravenscar profiles)
       --      pragma Task_Dispatching_Policy (EDF_Across_Priorities)
       --        (For GNAT_Ravenscar_EDF profile)
       --      pragma Locking_Policy (Ceiling_Locking)
@@ -11080,13 +11205,6 @@ package body Sem_Prag is
             Error_Msg_String (1 .. Name_Len) := Name_Buffer (1 .. Name_Len);
          end Set_Error_Msg_To_Profile_Name;
 
-         --  Local variables
-
-         Nod     : Node_Id;
-         Pref    : Node_Id;
-         Pref_Id : Node_Id;
-         Sel_Id  : Node_Id;
-
          Profile_Dispatching_Policy : Character;
 
       --  Start of processing for Set_Ravenscar_Profile
@@ -11158,423 +11276,119 @@ package body Sem_Prag is
          --    No_Dependence => Ada.Calendar
          --    No_Dependence => Ada.Task_Attributes
          --  are already set by previous call to Set_Profile_Restrictions.
+         --  Really???
 
          --  Set the following restrictions which were added to Ada 2005:
          --    No_Dependence => Ada.Execution_Time.Group_Budget
          --    No_Dependence => Ada.Execution_Time.Timers
 
          if Ada_Version >= Ada_2005 then
-            Pref_Id := Make_Identifier (Loc, Name_Find ("ada"));
-            Sel_Id  := Make_Identifier (Loc, Name_Find ("execution_time"));
-
-            Pref :=
-              Make_Selected_Component
-                (Sloc          => Loc,
-                 Prefix        => Pref_Id,
-                 Selector_Name => Sel_Id);
-
-            Sel_Id := Make_Identifier (Loc, Name_Find ("group_budgets"));
-
-            Nod :=
-              Make_Selected_Component
-                (Sloc          => Loc,
-                 Prefix        => Pref,
-                 Selector_Name => Sel_Id);
-
-            Set_Restriction_No_Dependence
-              (Unit    => Nod,
-               Warn    => Treat_Restrictions_As_Warnings,
-               Profile => Ravenscar);
-
-            Sel_Id := Make_Identifier (Loc, Name_Find ("timers"));
-
-            Nod :=
-              Make_Selected_Component
-                (Sloc          => Loc,
-                 Prefix        => Pref,
-                 Selector_Name => Sel_Id);
-
-            Set_Restriction_No_Dependence
-              (Unit    => Nod,
-               Warn    => Treat_Restrictions_As_Warnings,
-               Profile => Ravenscar);
+            declare
+               Execution_Time : constant Node_Id :=
+                 Sel_Comp ("ada", "execution_time", Loc);
+               Group_Budgets : constant Node_Id :=
+                 Sel_Comp (Execution_Time, "group_budgets");
+               Timers : constant Node_Id :=
+                 Sel_Comp (Execution_Time, "timers");
+            begin
+               Set_Restriction_No_Dependence
+                 (Unit    => Group_Budgets,
+                  Warn    => Treat_Restrictions_As_Warnings,
+                  Profile => Ravenscar);
+               Set_Restriction_No_Dependence
+                 (Unit    => Timers,
+                  Warn    => Treat_Restrictions_As_Warnings,
+                  Profile => Ravenscar);
+            end;
          end if;
 
          --  Set the following restriction which was added to Ada 2012 (see
-         --  AI-0171):
+         --  AI05-0171):
          --    No_Dependence => System.Multiprocessors.Dispatching_Domains
 
          if Ada_Version >= Ada_2012 then
-            Pref_Id := Make_Identifier (Loc, Name_Find ("system"));
-            Sel_Id  := Make_Identifier (Loc, Name_Find ("multiprocessors"));
-
-            Pref :=
-              Make_Selected_Component
-                (Sloc          => Loc,
-                 Prefix        => Pref_Id,
-                 Selector_Name => Sel_Id);
-
-            Sel_Id := Make_Identifier (Loc, Name_Find ("dispatching_domains"));
-
-            Nod :=
-              Make_Selected_Component
-                (Sloc          => Loc,
-                 Prefix        => Pref,
-                 Selector_Name => Sel_Id);
-
             Set_Restriction_No_Dependence
-              (Unit    => Nod,
+              (Sel_Comp
+                 (Sel_Comp ("system", "multiprocessors", Loc),
+                  "dispatching_domains"),
                Warn    => Treat_Restrictions_As_Warnings,
                Profile => Ravenscar);
-         end if;
-      end Set_Ravenscar_Profile;
 
-      -----------------------------------
-      -- Validate_Acc_Condition_Clause --
-      -----------------------------------
-
-      procedure Validate_Acc_Condition_Clause (Clause : Node_Id) is
-      begin
-         Analyze_And_Resolve (Clause);
+            --  Set the following restriction which was added to Ada 2020,
+            --  but as a binding interpretation:
+            --     No_Dependence => Ada.Synchronous_Barriers
+            --  for Ravenscar (and therefore for Ravenscar variants) but not
+            --  for Jorvik. The unit Ada.Synchronous_Barriers was introduced
+            --  in Ada2012 (AI05-0174).
 
-         if not Is_Boolean_Type (Etype (Clause)) then
-            Error_Pragma ("expected a boolean");
+            if Profile /= Jorvik then
+               Set_Restriction_No_Dependence
+                 (Sel_Comp ("ada", "synchronous_barriers", Loc),
+                  Warn    => Treat_Restrictions_As_Warnings,
+                  Profile => Ravenscar);
+            end if;
          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;
+      end Set_Ravenscar_Profile;
 
-            Analyze_And_Resolve (Expr);
+   --  Start of processing for Analyze_Pragma
 
-            Expr := Acc_Next (Expr);
-         end loop;
-      end Validate_Acc_Data_Clause;
+   begin
+      --  The following code is a defense against recursion. Not clear that
+      --  this can happen legitimately, but perhaps some error situations can
+      --  cause it, and we did see this recursion during testing.
 
-      ----------------------------------
-      -- Validate_Acc_Int_Expr_Clause --
-      ----------------------------------
+      if Analyzed (N) then
+         return;
+      else
+         Set_Analyzed (N);
+      end if;
 
-      procedure Validate_Acc_Int_Expr_Clause (Clause : Node_Id) is
-      begin
-         Analyze_And_Resolve (Clause);
+      Check_Restriction_No_Use_Of_Pragma (N);
 
-         if not Is_Integer_Type (Etype (Clause)) then
-            Error_Pragma_Arg ("expected an integer", Clause);
-         end if;
-      end Validate_Acc_Int_Expr_Clause;
+      if Get_Aspect_Id (Chars (Pragma_Identifier (N))) /= No_Aspect then
+         --  6.1/3 No_Specification_of_Aspect: Identifies an aspect for which
+         --    no aspect_specification, attribute_definition_clause, or pragma
+         --    is given.
+         Check_Restriction_No_Specification_Of_Aspect (N);
+      end if;
 
-      ---------------------------------------
-      -- Validate_Acc_Int_Expr_List_Clause --
-      ---------------------------------------
+      --  Ignore pragma if Ignore_Pragma applies. Also ignore pragma
+      --  Default_Scalar_Storage_Order if the -gnatI switch was given.
 
-      procedure Validate_Acc_Int_Expr_List_Clause (Clause : Node_Id) is
-         Expr : Node_Id;
+      if Should_Ignore_Pragma_Sem (N)
+        or else (Prag_Id = Pragma_Default_Scalar_Storage_Order
+                  and then Ignore_Rep_Clauses)
+      then
+         return;
+      end if;
 
-      begin
-         Expr := Acc_First (Clause);
-         while Present (Expr) loop
-            Analyze_And_Resolve (Expr);
+      --  Deal with unrecognized pragma
 
-            if not Is_Integer_Type (Etype (Expr)) then
-               Error_Pragma ("expected an integer");
+      if not Is_Pragma_Name (Pname) then
+         declare
+            Msg_Issued : Boolean := False;
+         begin
+            Check_Restriction
+              (Msg_Issued, No_Unrecognized_Pragmas, Pragma_Identifier (N));
+            if not Msg_Issued and then Warn_On_Unrecognized_Pragma then
+               Error_Msg_Name_1 := Pname;
+               Error_Msg_N ("?g?unrecognized pragma%!", Pragma_Identifier (N));
+
+               for PN in First_Pragma_Name .. Last_Pragma_Name loop
+                  if Is_Bad_Spelling_Of (Pname, PN) then
+                     Error_Msg_Name_1 := PN;
+                     Error_Msg_N -- CODEFIX
+                       ("\?g?possible misspelling of %!",
+                        Pragma_Identifier (N));
+                     exit;
+                  end if;
+               end loop;
             end if;
+         end;
 
-            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
-      --  The following code is a defense against recursion. Not clear that
-      --  this can happen legitimately, but perhaps some error situations can
-      --  cause it, and we did see this recursion during testing.
-
-      if Analyzed (N) then
-         return;
-      else
-         Set_Analyzed (N);
-      end if;
-
-      Check_Restriction_No_Use_Of_Pragma (N);
-
-      --  Ignore pragma if Ignore_Pragma applies. Also ignore pragma
-      --  Default_Scalar_Storage_Order if the -gnatI switch was given.
-
-      if Should_Ignore_Pragma_Sem (N)
-        or else (Prag_Id = Pragma_Default_Scalar_Storage_Order
-                  and then Ignore_Rep_Clauses)
-      then
-         return;
-      end if;
-
-      --  Deal with unrecognized pragma
-
-      if not Is_Pragma_Name (Pname) then
-         if Warn_On_Unrecognized_Pragma then
-            Error_Msg_Name_1 := Pname;
-            Error_Msg_N ("?g?unrecognized pragma%!", Pragma_Identifier (N));
-
-            for PN in First_Pragma_Name .. Last_Pragma_Name loop
-               if Is_Bad_Spelling_Of (Pname, PN) then
-                  Error_Msg_Name_1 := PN;
-                  Error_Msg_N -- CODEFIX
-                    ("\?g?possible misspelling of %!", Pragma_Identifier (N));
-                  exit;
-               end if;
-            end loop;
-         end if;
-
-         return;
-      end if;
+         return;
+      end if;
 
       --  Here to start processing for recognized pragma
 
@@ -11627,6 +11441,12 @@ package body Sem_Prag is
          end if;
       end if;
 
+      --  Mark assertion pragmas as Ghost depending on their enclosing context
+
+      if Assertion_Expression_Pragma (Prag_Id) then
+         Mark_Ghost_Pragma (N, Current_Scope);
+      end if;
+
       --  Preset arguments
 
       Arg_Count := 0;
@@ -11634,6 +11454,7 @@ package body Sem_Prag is
       Arg2      := Empty;
       Arg3      := Empty;
       Arg4      := Empty;
+      Arg5      := Empty;
 
       if Present (Pragma_Argument_Associations (N)) then
          Arg_Count := List_Length (Pragma_Argument_Associations (N));
@@ -11647,6 +11468,10 @@ package body Sem_Prag is
 
                if Present (Arg3) then
                   Arg4 := Next (Arg3);
+
+                  if Present (Arg4) then
+                     Arg5 := Next (Arg4);
+                  end if;
                end if;
             end if;
          end if;
@@ -11699,7 +11524,7 @@ package body Sem_Prag is
          --    SIMPLE_OPTION
          --  | NAME_VALUE_OPTION
 
-         --  SIMPLE_OPTION ::= Ghost | Synchronous
+         --  SIMPLE_OPTION ::= Ghost | Relaxed_Initialization | Synchronous
 
          --  NAME_VALUE_OPTION ::=
          --    Part_Of => ABSTRACT_STATE
@@ -11769,15 +11594,16 @@ package body Sem_Prag is
             is
                --  Flags used to verify the consistency of options
 
-               AR_Seen          : Boolean := False;
-               AW_Seen          : Boolean := False;
-               ER_Seen          : Boolean := False;
-               EW_Seen          : Boolean := False;
-               External_Seen    : Boolean := False;
-               Ghost_Seen       : Boolean := False;
-               Others_Seen      : Boolean := False;
-               Part_Of_Seen     : Boolean := False;
-               Synchronous_Seen : Boolean := False;
+               AR_Seen                     : Boolean := False;
+               AW_Seen                     : Boolean := False;
+               ER_Seen                     : Boolean := False;
+               EW_Seen                     : Boolean := False;
+               External_Seen               : Boolean := False;
+               Ghost_Seen                  : Boolean := False;
+               Others_Seen                 : Boolean := False;
+               Part_Of_Seen                : Boolean := False;
+               Relaxed_Initialization_Seen : Boolean := False;
+               Synchronous_Seen            : Boolean := False;
 
                --  Flags used to store the static value of all external states'
                --  expressions.
@@ -11936,10 +11762,10 @@ package body Sem_Prag is
                   --  external properties.
 
                   elsif Nkind (Prop) = N_Identifier
-                    and then Nam_In (Chars (Prop), Name_Async_Readers,
-                                                   Name_Async_Writers,
-                                                   Name_Effective_Reads,
-                                                   Name_Effective_Writes)
+                    and then Chars (Prop) in Name_Async_Readers
+                                           | Name_Async_Writers
+                                           | Name_Effective_Reads
+                                           | Name_Effective_Writes
                   then
                      null;
 
@@ -12258,6 +12084,12 @@ package body Sem_Prag is
                            Check_Duplicate_Option (Opt, Synchronous_Seen);
                            Check_Ghost_Synchronous;
 
+                        --  Relaxed_Initialization
+
+                        elsif Chars (Opt) = Name_Relaxed_Initialization then
+                           Check_Duplicate_Option
+                             (Opt, Relaxed_Initialization_Seen);
+
                         --  Option Part_Of without an encapsulating state is
                         --  illegal (SPARK RM 7.1.4(8)).
 
@@ -12410,8 +12242,8 @@ package body Sem_Prag is
 
             Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True);
 
-            if not Nkind_In (Pack_Decl, N_Generic_Package_Declaration,
-                                        N_Package_Declaration)
+            if Nkind (Pack_Decl) not in
+                 N_Generic_Package_Declaration | N_Package_Declaration
             then
                Pragma_Misplaced;
                return;
@@ -12474,306 +12306,6 @@ package body Sem_Prag is
             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 --
          ------------
@@ -13023,10 +12555,6 @@ package body Sem_Prag is
             Check_Ada_83_Warning;
             Check_Valid_Library_Unit_Pragma;
 
-            if Nkind (N) = N_Null_Statement then
-               return;
-            end if;
-
             Lib_Entity := Find_Lib_Unit_Name;
 
             --  A pragma that applies to a Ghost entity becomes Ghost for the
@@ -13343,8 +12871,9 @@ package body Sem_Prag is
             if Arg_Count > 1 then
                Check_Optional_Identifier (Arg2, Name_Message);
 
-               --  Provide semantic annnotations for optional argument, for
+               --  Provide semantic annotations for optional argument, for
                --  ASIS use, before rewriting.
+               --  Is this still needed???
 
                Preanalyze_And_Resolve (Expression (Arg2), Standard_String);
                Append_To (New_Args, New_Copy_Tree (Arg2));
@@ -13374,30 +12903,31 @@ package body Sem_Prag is
 
          --  ASSERTION_KIND ::= RM_ASSERTION_KIND | ID_ASSERTION_KIND
 
-         --  RM_ASSERTION_KIND ::= Assert               |
-         --                        Static_Predicate     |
-         --                        Dynamic_Predicate    |
-         --                        Pre                  |
-         --                        Pre'Class            |
-         --                        Post                 |
-         --                        Post'Class           |
-         --                        Type_Invariant       |
-         --                        Type_Invariant'Class
-
-         --  ID_ASSERTION_KIND ::= Assert_And_Cut            |
-         --                        Assume                    |
-         --                        Contract_Cases            |
-         --                        Debug                     |
-         --                        Default_Initial_Condition |
-         --                        Ghost                     |
-         --                        Initial_Condition         |
-         --                        Loop_Invariant            |
-         --                        Loop_Variant              |
-         --                        Postcondition             |
-         --                        Precondition              |
-         --                        Predicate                 |
-         --                        Refined_Post              |
-         --                        Statement_Assertions
+         --  RM_ASSERTION_KIND ::= Assert                     |
+         --                        Static_Predicate           |
+         --                        Dynamic_Predicate          |
+         --                        Pre                        |
+         --                        Pre'Class                  |
+         --                        Post                       |
+         --                        Post'Class                 |
+         --                        Type_Invariant             |
+         --                        Type_Invariant'Class       |
+         --                        Default_Initial_Condition
+
+         --  ID_ASSERTION_KIND ::= Assert_And_Cut       |
+         --                        Assume               |
+         --                        Contract_Cases       |
+         --                        Debug                |
+         --                        Ghost                |
+         --                        Initial_Condition    |
+         --                        Loop_Invariant       |
+         --                        Loop_Variant         |
+         --                        Postcondition        |
+         --                        Precondition         |
+         --                        Predicate            |
+         --                        Refined_Post         |
+         --                        Statement_Assertions |
+         --                        Subprogram_Variant
 
          --  Note: The RM_ASSERTION_KIND list is language-defined, and the
          --  ID_ASSERTION_KIND list contains implementation-defined additions
@@ -13545,9 +13075,7 @@ package body Sem_Prag is
                      --  The Ghost policy must be either Check or Ignore
                      --  (SPARK RM 6.9(6)).
 
-                     if not Nam_In (Chars (Policy), Name_Check,
-                                                    Name_Ignore)
-                     then
+                     if Chars (Policy) not in Name_Check | Name_Ignore then
                         Error_Pragma_Arg
                           ("argument of pragma % Ghost must be Check or "
                            & "Ignore", Policy);
@@ -13678,41 +13206,66 @@ package body Sem_Prag is
             | Pragma_No_Caching
          =>
          Async_Effective : declare
-            Obj_Decl : Node_Id;
-            Obj_Id   : Entity_Id;
-
+            Obj_Or_Type_Decl : Node_Id;
+            Obj_Or_Type_Id   : Entity_Id;
          begin
             GNAT_Pragma;
             Check_No_Identifiers;
             Check_At_Most_N_Arguments  (1);
 
-            Obj_Decl := Find_Related_Context (N, Do_Checks => True);
-
-            --  Object declaration
-
-            if Nkind (Obj_Decl) /= N_Object_Declaration then
-               Pragma_Misplaced;
-               return;
+            Obj_Or_Type_Decl := Find_Related_Context (N, Do_Checks => True);
+
+            --  Pragma must apply to a object declaration or to a type
+            --  declaration (only the former in the No_Caching case).
+            --  Original_Node is necessary to account for untagged derived
+            --  types that are rewritten as subtypes of their
+            --  respective root types.
+
+            if Nkind (Obj_Or_Type_Decl) /= N_Object_Declaration then
+               if Prag_Id = Pragma_No_Caching
+                  or else Nkind (Original_Node (Obj_Or_Type_Decl)) not in
+                            N_Full_Type_Declaration    |
+                            N_Private_Type_Declaration |
+                            N_Formal_Type_Declaration  |
+                            N_Task_Type_Declaration    |
+                            N_Protected_Type_Declaration
+               then
+                  Pragma_Misplaced;
+                  return;
+               end if;
             end if;
 
-            Obj_Id := Defining_Entity (Obj_Decl);
+            Obj_Or_Type_Id := Defining_Entity (Obj_Or_Type_Decl);
 
             --  Perform minimal verification to ensure that the argument is at
-            --  least a variable. Subsequent finer grained checks will be done
-            --  at the end of the declarative region the contains the pragma.
+            --  least a variable or a type. Subsequent finer grained checks
+            --  will be done at the end of the declarative region that
+            --  contains the pragma.
 
-            if Ekind (Obj_Id) = E_Variable then
+            if Ekind (Obj_Or_Type_Id) = E_Variable
+              or else Is_Type (Obj_Or_Type_Id)
+            then
+
+               --  In the case of a type, pragma is a type-related
+               --  representation item and so requires checks common to
+               --  all type-related representation items.
+
+               if Is_Type (Obj_Or_Type_Id)
+                 and then Rep_Item_Too_Late (Obj_Or_Type_Id, N)
+               then
+                  return;
+               end if;
 
                --  A pragma that applies to a Ghost entity becomes Ghost for
                --  the purposes of legality checks and removal of ignored Ghost
                --  code.
 
-               Mark_Ghost_Pragma (N, Obj_Id);
+               Mark_Ghost_Pragma (N, Obj_Or_Type_Id);
 
                --  Chain the pragma on the contract for further processing by
                --  Analyze_External_Property_In_Decl_Part.
 
-               Add_Contract_Item (N, Obj_Id);
+               Add_Contract_Item (N, Obj_Or_Type_Id);
 
                --  Analyze the Boolean expression (if any)
 
@@ -13723,7 +13276,8 @@ package body Sem_Prag is
             --  Otherwise the external property applies to a constant
 
             else
-               Error_Pragma ("pragma % must apply to a volatile object");
+               Error_Pragma
+                 ("pragma % must apply to a volatile type or object");
             end if;
          end Async_Effective;
 
@@ -13897,7 +13451,6 @@ package body Sem_Prag is
             D    : Node_Id;
             E    : Entity_Id;
             E_Id : Node_Id;
-            K    : Node_Kind;
 
          begin
             Check_Ada_83_Warning;
@@ -13926,18 +13479,20 @@ package body Sem_Prag is
             end if;
 
             D := Declaration_Node (E);
-            K := Nkind (D);
 
-            if (K = N_Full_Type_Declaration and then Is_Array_Type (E))
+            if (Nkind (D) = N_Full_Type_Declaration and then Is_Array_Type (E))
               or else
-                ((Ekind (E) = E_Constant or else Ekind (E) = E_Variable)
-                   and then Nkind (D) = N_Object_Declaration
+                (Nkind (D) = N_Object_Declaration
+                   and then Ekind (E) in E_Constant | E_Variable
                    and then Nkind (Object_Definition (D)) =
                                        N_Constrained_Array_Definition)
+              or else
+                 (Ada_Version >= Ada_2020
+                   and then Nkind (D) = N_Formal_Type_Declaration)
             then
-               --  The flag is set on the object, or on the base type
+               --  The flag is set on the base type, or on the object
 
-               if Nkind (D) /= N_Object_Declaration then
+               if Nkind (D) = N_Full_Type_Declaration then
                   E := Base_Type (E);
                end if;
 
@@ -14356,7 +13911,7 @@ package body Sem_Prag is
             --  identifier is Name.
 
             if Nkind (Arg1) /= N_Pragma_Argument_Association
-              or else Nam_In (Chars (Arg1), No_Name, Name_Name)
+              or else Chars (Arg1) in No_Name | Name_Name
             then
                --  Old syntax
 
@@ -14369,7 +13924,7 @@ package body Sem_Prag is
 
                --  Check forbidden check kind
 
-               if Nam_In (Chars (Kind), Name_Name, Name_Policy) then
+               if Chars (Kind) in Name_Name | Name_Policy then
                   Error_Msg_Name_2 := Chars (Kind);
                   Error_Pragma_Arg
                     ("pragma% does not allow% as check name", Arg1);
@@ -14553,7 +14108,7 @@ package body Sem_Prag is
          --  pragma Complex_Representation ([Entity =>] LOCAL_NAME);
 
          when Pragma_Complex_Representation => Complex_Representation : declare
-            E_Id : Entity_Id;
+            E_Id : Node_Id;
             E    : Entity_Id;
             Ent  : Entity_Id;
 
@@ -14892,9 +14447,9 @@ package body Sem_Prag is
             --  or subprogram body because it cannot benefit from forward
             --  references.
 
-            if Nkind_In (Subp_Decl, N_Entry_Body,
-                                    N_Subprogram_Body,
-                                    N_Subprogram_Body_Stub)
+            if Nkind (Subp_Decl) in N_Entry_Body
+                                  | N_Subprogram_Body
+                                  | N_Subprogram_Body_Stub
             then
                --  The legality checks of pragma Contract_Cases are affected by
                --  the SPARK mode in effect and the volatility of the context.
@@ -15109,20 +14664,155 @@ package body Sem_Prag is
                  ("pragma% requires function returning a 'C'P'P_Class type",
                    Arg1);
             end if;
-         end CPP_Constructor;
+         end CPP_Constructor;
+
+         -----------------
+         -- CPP_Virtual --
+         -----------------
+
+         when Pragma_CPP_Virtual =>
+            GNAT_Pragma;
+
+            if Warn_On_Obsolescent_Feature then
+               Error_Msg_N
+                 ("'G'N'A'T pragma Cpp'_Virtual is now obsolete and has no "
+                  & "effect?j?", N);
+            end if;
+
+         --------------------
+         -- CUDA_Execute --
+         --------------------
+
+         --    pragma CUDA_Execute (PROCEDURE_CALL_STATEMENT,
+         --                         EXPRESSION,
+         --                         EXPRESSION,
+         --                         [, EXPRESSION
+         --                         [, EXPRESSION]]);
+
+         when Pragma_CUDA_Execute => CUDA_Execute : declare
+
+            function Is_Acceptable_Dim3 (N : Node_Id) return Boolean;
+            --  Returns True if N is an acceptable argument for CUDA_Execute,
+            --  False otherwise.
+
+            ------------------------
+            -- Is_Acceptable_Dim3 --
+            ------------------------
+
+            function Is_Acceptable_Dim3 (N : Node_Id) return Boolean is
+               Expr : Node_Id;
+            begin
+               if Is_RTE (Etype (N), RE_Dim3)
+                 or else Is_Integer_Type (Etype (N))
+               then
+                  return True;
+               end if;
+
+               if Nkind (N) = N_Aggregate
+                 and then List_Length (Expressions (N)) = 3
+               then
+                  Expr := First (Expressions (N));
+                  while Present (Expr) loop
+                     Analyze_And_Resolve (Expr, Any_Integer);
+                     Next (Expr);
+                  end loop;
+                  return True;
+               end if;
+
+               return False;
+            end Is_Acceptable_Dim3;
+
+            --  Local variables
+
+            Block_Dimensions : constant Node_Id := Get_Pragma_Arg (Arg3);
+            Grid_Dimensions  : constant Node_Id := Get_Pragma_Arg (Arg2);
+            Kernel_Call      : constant Node_Id := Get_Pragma_Arg (Arg1);
+            Shared_Memory    : Node_Id;
+            Stream           : Node_Id;
+
+            --  Start of processing for CUDA_Execute
+
+         begin
+            GNAT_Pragma;
+            Check_At_Least_N_Arguments (3);
+            Check_At_Most_N_Arguments (5);
+
+            Analyze_And_Resolve (Kernel_Call);
+            if Nkind (Kernel_Call) /= N_Function_Call
+               or else Etype (Kernel_Call) /= Standard_Void_Type
+            then
+               --  In `pragma CUDA_Execute (Kernel_Call (...), ...)`,
+               --  GNAT sees Kernel_Call as an N_Function_Call since
+               --  Kernel_Call "looks" like an expression. However, only
+               --  procedures can be kernels, so to make things easier for the
+               --  user the error message complains about Kernel_Call not being
+               --  a procedure call.
+
+               Error_Msg_N ("first argument of & must be a procedure call", N);
+            end if;
+
+            Analyze (Grid_Dimensions);
+            if not Is_Acceptable_Dim3 (Grid_Dimensions) then
+               Error_Msg_N
+                 ("second argument of & must be an Integer, Dim3 or aggregate "
+                  & "containing 3 Integers", N);
+            end if;
+
+            Analyze (Block_Dimensions);
+            if not Is_Acceptable_Dim3 (Block_Dimensions) then
+               Error_Msg_N
+                 ("third argument of & must be an Integer, Dim3 or aggregate "
+                  & "containing 3 Integers", N);
+            end if;
+
+            if Present (Arg4) then
+               Shared_Memory := Get_Pragma_Arg (Arg4);
+               Analyze_And_Resolve (Shared_Memory, Any_Integer);
+
+               if Present (Arg5) then
+                  Stream := Get_Pragma_Arg (Arg5);
+                  Analyze_And_Resolve (Stream, RTE (RE_Stream_T));
+               end if;
+            end if;
+         end CUDA_Execute;
 
          -----------------
-         -- CPP_Virtual --
+         -- CUDA_Global --
          -----------------
 
-         when Pragma_CPP_Virtual =>
+         --  pragma CUDA_Global (IDENTIFIER);
+
+         when Pragma_CUDA_Global => CUDA_Global : declare
+            Arg_Node    : Node_Id;
+            Kernel_Proc : Entity_Id;
+            Pack_Id     : Entity_Id;
+         begin
             GNAT_Pragma;
+            Check_At_Least_N_Arguments (1);
+            Check_At_Most_N_Arguments (1);
+            Check_Optional_Identifier (Arg1, Name_Entity);
+            Check_Arg_Is_Local_Name (Arg1);
 
-            if Warn_On_Obsolescent_Feature then
-               Error_Msg_N
-                 ("'G'N'A'T pragma Cpp'_Virtual is now obsolete and has no "
-                  & "effect?j?", N);
+            Arg_Node := Get_Pragma_Arg (Arg1);
+            Analyze (Arg_Node);
+
+            Kernel_Proc := Entity (Arg_Node);
+            Pack_Id := Scope (Kernel_Proc);
+
+            if Ekind (Kernel_Proc) /= E_Procedure then
+               Error_Msg_NE ("& must be a procedure", N, Kernel_Proc);
+
+            elsif Ekind (Pack_Id) /= E_Package
+              or else not Is_Library_Level_Entity (Pack_Id)
+            then
+               Error_Msg_NE
+                  ("& must reside in a library-level package", N, Kernel_Proc);
+
+            else
+               Set_Is_CUDA_Kernel (Kernel_Proc);
+               Add_CUDA_Kernel (Pack_Id, Kernel_Proc);
             end if;
+         end CUDA_Global;
 
          ----------------
          -- CPP_Vtable --
@@ -15152,13 +14842,13 @@ package body Sem_Prag is
             Ada_2012_Pragma;
             Check_No_Identifiers;
             Check_Arg_Count (1);
+            Arg := Get_Pragma_Arg (Arg1);
 
             --  Subprogram case
 
             if Nkind (P) = N_Subprogram_Body then
                Check_In_Main_Program;
 
-               Arg := Get_Pragma_Arg (Arg1);
                Analyze_And_Resolve (Arg, Any_Integer);
 
                Ent := Defining_Unit_Name (Specification (P));
@@ -15205,7 +14895,6 @@ package body Sem_Prag is
             --  Task case
 
             elsif Nkind (P) = N_Task_Definition then
-               Arg := Get_Pragma_Arg (Arg1);
                Ent := Defining_Identifier (Parent (P));
 
                --  The expression must be analyzed in the special manner
@@ -15214,6 +14903,16 @@ package body Sem_Prag is
 
                Preanalyze_Spec_Expression (Arg, RTE (RE_CPU_Range));
 
+               --  See comment in Sem_Ch13 about the following restrictions
+
+               if Is_OK_Static_Expression (Arg) then
+                  if Expr_Value (Arg) = Uint_0 then
+                     Check_Restriction (No_Tasks_Unassigned_To_CPU, N);
+                  end if;
+               else
+                  Check_Restriction (No_Dynamic_CPU_Assignment, N);
+               end if;
+
             --  Anything else is incorrect
 
             else
@@ -15302,11 +15001,11 @@ package body Sem_Prag is
                Call := Get_Pragma_Arg (Arg1);
             end if;
 
-            if Nkind_In (Call, N_Expanded_Name,
-                               N_Function_Call,
-                               N_Identifier,
-                               N_Indexed_Component,
-                               N_Selected_Component)
+            if Nkind (Call) in N_Expanded_Name
+                             | N_Function_Call
+                             | N_Identifier
+                             | N_Indexed_Component
+                             | N_Selected_Component
             then
                --  If this pragma Debug comes from source, its argument was
                --  parsed as a name form (which is syntactically identical).
@@ -15413,7 +15112,7 @@ package body Sem_Prag is
          begin
             GNAT_Pragma;
             Check_No_Identifiers;
-            Check_At_Most_N_Arguments (1);
+            Check_At_Most_N_Arguments (2);  -- Accounts for implicit type arg
 
             Typ  := Empty;
             Stmt := Prev (N);
@@ -15441,8 +15140,8 @@ package body Sem_Prag is
                --  The associated private type [extension] has been found, stop
                --  the search.
 
-               elsif Nkind_In (Stmt, N_Private_Extension_Declaration,
-                                     N_Private_Type_Declaration)
+               elsif Nkind (Stmt) in N_Private_Extension_Declaration
+                                   | N_Private_Type_Declaration
                then
                   Typ := Defining_Entity (Stmt);
                   exit;
@@ -15476,6 +15175,27 @@ package body Sem_Prag is
 
             Set_Has_Own_DIC (Typ);
 
+            --  A type entity argument is appended to facilitate inheriting the
+            --  aspect/pragma from parent types (see Build_DIC_Procedure_Body),
+            --  though that extra argument isn't documented for the pragma.
+
+            if not Present (Arg2) then
+               --  When the pragma has no arguments, create an argument with
+               --  the value Empty, so the type name argument can be appended
+               --  following it (since it's expected as the second argument).
+
+               if not Present (Arg1) then
+                  Set_Pragma_Argument_Associations (N, New_List (
+                    Make_Pragma_Argument_Association (Sloc (Typ),
+                      Expression => Empty)));
+               end if;
+
+               Append_To
+                 (Pragma_Argument_Associations (N),
+                  Make_Pragma_Argument_Association (Sloc (Typ),
+                    Expression => New_Occurrence_Of (Typ, Sloc (Typ))));
+            end if;
+
             --  Chain the pragma on the rep item chain for further processing
 
             Discard := Rep_Item_Too_Late (Typ, N, FOnly => True);
@@ -15535,7 +15255,7 @@ package body Sem_Prag is
          -- Default_Storage_Pool --
          --------------------------
 
-         --  pragma Default_Storage_Pool (storage_pool_NAME | null);
+         --  pragma Default_Storage_Pool (storage_pool_NAME | null | Standard);
 
          when Pragma_Default_Storage_Pool => Default_Storage_Pool : declare
             Pool : Node_Id;
@@ -15576,6 +15296,18 @@ package body Sem_Prag is
 
                   Set_Etype (Pool, Empty);
 
+               --  Case of Default_Storage_Pool (Standard);
+
+               elsif Nkind (Pool) = N_Identifier
+                 and then Chars (Pool) = Name_Standard
+               then
+                  Analyze (Pool);
+
+                  if Entity (Pool) /= Standard_Standard then
+                     Error_Pragma_Arg
+                       ("package Standard is not directly visible", Arg1);
+                  end if;
+
                --  Case of Default_Storage_Pool (storage_pool_NAME);
 
                else
@@ -15583,7 +15315,7 @@ package body Sem_Prag is
                   --  argument is "null".
 
                   if Is_Configuration_Pragma then
-                     Error_Pragma_Arg ("NULL expected", Arg1);
+                     Error_Pragma_Arg ("NULL or Standard expected", Arg1);
                   end if;
 
                   --  The expected type for a non-"null" argument is
@@ -15691,9 +15423,9 @@ package body Sem_Prag is
                --  or subprogram body because it cannot benefit from forward
                --  references.
 
-               if Nkind_In (Subp_Decl, N_Entry_Body,
-                                       N_Subprogram_Body,
-                                       N_Subprogram_Body_Stub)
+               if Nkind (Subp_Decl) in N_Entry_Body
+                                     | N_Subprogram_Body
+                                     | N_Subprogram_Body_Stub
                then
                   --  The legality checks of pragmas Depends and Global are
                   --  affected by the SPARK mode in effect and the volatility
@@ -16035,10 +15767,6 @@ package body Sem_Prag is
             Check_Ada_83_Warning;
             Check_Valid_Library_Unit_Pragma;
 
-            if Nkind (N) = N_Null_Statement then
-               return;
-            end if;
-
             Cunit_Node := Cunit (Current_Sem_Unit);
             Cunit_Ent  := Cunit_Entity (Current_Sem_Unit);
 
@@ -16047,8 +15775,8 @@ package body Sem_Prag is
 
             Mark_Ghost_Pragma (N, Cunit_Ent);
 
-            if Nkind_In (Unit (Cunit_Node), N_Package_Body,
-                                            N_Subprogram_Body)
+            if Nkind (Unit (Cunit_Node)) in
+                 N_Package_Body | N_Subprogram_Body
             then
                Error_Pragma ("pragma% must refer to a spec, not a body");
             else
@@ -17022,8 +16750,8 @@ package body Sem_Prag is
                --  Task unit declared without a definition cannot be subject to
                --  pragma Ghost (SPARK RM 6.9(19)).
 
-               elsif Nkind_In (Stmt, N_Single_Task_Declaration,
-                                     N_Task_Type_Declaration)
+               elsif Nkind (Stmt) in
+                       N_Single_Task_Declaration | N_Task_Type_Declaration
                then
                   Error_Pragma ("pragma % cannot apply to a task type");
                   return;
@@ -17036,8 +16764,8 @@ package body Sem_Prag is
                   --  When pragma Ghost applies to an untagged derivation, the
                   --  derivation is transformed into a [sub]type declaration.
 
-                  if Nkind_In (Stmt, N_Full_Type_Declaration,
-                                     N_Subtype_Declaration)
+                  if Nkind (Stmt) in
+                       N_Full_Type_Declaration | N_Subtype_Declaration
                     and then Comes_From_Source (Orig_Stmt)
                     and then Nkind (Orig_Stmt) = N_Full_Type_Declaration
                     and then Nkind (Type_Definition (Orig_Stmt)) =
@@ -17071,14 +16799,14 @@ package body Sem_Prag is
 
                --  The pragma applies to a legal construct, stop the traversal
 
-               elsif Nkind_In (Stmt, N_Abstract_Subprogram_Declaration,
-                                     N_Full_Type_Declaration,
-                                     N_Generic_Subprogram_Declaration,
-                                     N_Object_Declaration,
-                                     N_Private_Extension_Declaration,
-                                     N_Private_Type_Declaration,
-                                     N_Subprogram_Declaration,
-                                     N_Subtype_Declaration)
+               elsif Nkind (Stmt) in N_Abstract_Subprogram_Declaration
+                                   | N_Full_Type_Declaration
+                                   | N_Generic_Subprogram_Declaration
+                                   | N_Object_Declaration
+                                   | N_Private_Extension_Declaration
+                                   | N_Private_Type_Declaration
+                                   | N_Subprogram_Declaration
+                                   | N_Subtype_Declaration
                then
                   Id := Defining_Entity (Stmt);
                   exit;
@@ -17107,12 +16835,12 @@ package body Sem_Prag is
             --  Protected and task types cannot be subject to pragma Ghost
             --  (SPARK RM 6.9(19)).
 
-            if Nkind_In (Context, N_Protected_Body, N_Protected_Definition)
+            if Nkind (Context) in N_Protected_Body | N_Protected_Definition
             then
                Error_Pragma ("pragma % cannot apply to a protected type");
                return;
 
-            elsif Nkind_In (Context, N_Task_Body, N_Task_Definition) then
+            elsif Nkind (Context) in N_Task_Body | N_Task_Definition then
                Error_Pragma ("pragma % cannot apply to a task type");
                return;
             end if;
@@ -17229,7 +16957,7 @@ package body Sem_Prag is
                      return;
                   end if;
 
-               --  Otherwie the expression is not static
+               --  Otherwise the expression is not static
 
                else
                   Error_Pragma_Arg
@@ -17306,9 +17034,9 @@ package body Sem_Prag is
                --  or subprogram body because it cannot benefit from forward
                --  references.
 
-               if Nkind_In (Subp_Decl, N_Entry_Body,
-                                       N_Subprogram_Body,
-                                       N_Subprogram_Body_Stub)
+               if Nkind (Subp_Decl) in N_Entry_Body
+                                     | N_Subprogram_Body
+                                     | N_Subprogram_Body_Stub
                then
                   --  The legality checks of pragmas Depends and Global are
                   --  affected by the SPARK mode in effect and the volatility
@@ -17359,8 +17087,8 @@ package body Sem_Prag is
             begin
                GP := Parent (Parent (N));
 
-               if Nkind_In (GP, N_Package_Declaration,
-                                N_Generic_Package_Declaration)
+               if Nkind (GP) in
+                    N_Package_Declaration | N_Generic_Package_Declaration
                then
                   GP := Parent (GP);
                end if;
@@ -17373,15 +17101,12 @@ package body Sem_Prag is
 
                   if Present (CS) then
 
-                     --  If we have multiple instances, concatenate them, but
-                     --  not in ASIS, where we want the original tree.
+                     --  If we have multiple instances, concatenate them.
 
-                     if not ASIS_Mode then
-                        Start_String (Strval (CS));
-                        Store_String_Char (' ');
-                        Store_String_Chars (Strval (Str));
-                        Set_Strval (CS, End_String);
-                     end if;
+                     Start_String (Strval (CS));
+                     Store_String_Char (' ');
+                     Store_String_Chars (Strval (Str));
+                     Set_Strval (CS, End_String);
 
                   else
                      Set_Ident_String (Current_Sem_Unit, Str);
@@ -17511,8 +17236,8 @@ package body Sem_Prag is
                   --  "synchronized".
 
                    or else
-                    (Ekind_In (Typ, E_Record_Type_With_Private,
-                                    E_Record_Subtype_With_Private)
+                    (Ekind (Typ) in E_Record_Type_With_Private
+                                  | E_Record_Subtype_With_Private
                        and then Synchronized_Present (Parent (Typ))))
                then
                   null;
@@ -17527,7 +17252,7 @@ package body Sem_Prag is
                --  By_Protected_Procedure to the primitive procedure of a task
                --  interface.
 
-               if Chars (Arg2) = Name_By_Protected_Procedure
+               if Chars (Get_Pragma_Arg (Arg2)) = Name_By_Protected_Procedure
                  and then Is_Interface (Typ)
                  and then Is_Task_Interface (Typ)
                then
@@ -17552,6 +17277,18 @@ package body Sem_Prag is
                return;
             end if;
 
+            --  Ada 2012 (AI12-0279): Cannot apply the implementation_kind
+            --  By_Protected_Procedure to a procedure that has aspect Yield
+
+            if Chars (Get_Pragma_Arg (Arg2)) = Name_By_Protected_Procedure
+              and then Has_Yield_Aspect (Proc_Id)
+            then
+               Error_Pragma_Arg
+                 ("implementation kind By_Protected_Procedure cannot be "
+                  & "applied to entities with aspect 'Yield", Arg2);
+               return;
+            end if;
+
             Record_Rep_Item (Proc_Id, N);
          end Implemented;
 
@@ -17818,7 +17555,6 @@ package body Sem_Prag is
             D    : Node_Id;
             E_Id : Node_Id;
             E    : Entity_Id;
-            K    : Node_Kind;
 
          begin
             Check_Ada_83_Warning;
@@ -17885,11 +17621,10 @@ package body Sem_Prag is
             end if;
 
             D := Declaration_Node (E);
-            K := Nkind (D);
 
             --  The flag is set on the base type, or on the object
 
-            if K = N_Full_Type_Declaration
+            if Nkind (D) = N_Full_Type_Declaration
               and then (Is_Array_Type (E) or else Is_Record_Type (E))
             then
                Set_Has_Independent_Components (Base_Type (E));
@@ -17958,8 +17693,8 @@ package body Sem_Prag is
 
             Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True);
 
-            if not Nkind_In (Pack_Decl, N_Generic_Package_Declaration,
-                                        N_Package_Declaration)
+            if Nkind (Pack_Decl) not in
+                 N_Generic_Package_Declaration | N_Package_Declaration
             then
                Pragma_Misplaced;
                return;
@@ -18006,15 +17741,17 @@ package body Sem_Prag is
          --    Short_Float
          --  | Float
          --  | Long_Float
-         --  | Long_Long_Flat
+         --  | Long_Long_Float
          --  | Signed_8
          --  | Signed_16
          --  | Signed_32
          --  | Signed_64
+         --  | Signed_128
          --  | Unsigned_8
          --  | Unsigned_16
          --  | Unsigned_32
          --  | Unsigned_64
+         --  | Unsigned_128
 
          when Pragma_Initialize_Scalars => Do_Initialize_Scalars : declare
             Seen : array (Scalar_Id) of Node_Id := (others => Empty);
@@ -18067,7 +17804,14 @@ package body Sem_Prag is
             begin
                Analyze_And_Resolve (Val_Expr, Any_Integer);
 
-               if Is_OK_Static_Expression (Val_Expr) then
+               if (Scal_Typ = Name_Signed_128
+                    or else Scal_Typ = Name_Unsigned_128)
+                 and then Ttypes.System_Max_Integer_Size < 128
+               then
+                  Error_Msg_Name_1 := Scal_Typ;
+                  Error_Msg_N ("value cannot be set for type %", Val_Expr);
+
+               elsif Is_OK_Static_Expression (Val_Expr) then
                   Set_Invalid_Scalar_Value (Scal_Typ, Expr_Value (Val_Expr));
 
                else
@@ -18230,8 +17974,8 @@ package body Sem_Prag is
 
             Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True);
 
-            if not Nkind_In (Pack_Decl, N_Generic_Package_Declaration,
-                                        N_Package_Declaration)
+            if Nkind (Pack_Decl) not in
+                 N_Generic_Package_Declaration | N_Package_Declaration
             then
                Pragma_Misplaced;
                return;
@@ -18568,7 +18312,7 @@ package body Sem_Prag is
                Preanalyze_Spec_Expression (Arg, RTE (RE_Interrupt_Priority));
             end if;
 
-            if not Nkind_In (P, N_Task_Definition, N_Protected_Definition) then
+            if Nkind (P) not in N_Task_Definition | N_Protected_Definition then
                Pragma_Misplaced;
                return;
 
@@ -18767,9 +18511,9 @@ package body Sem_Prag is
             --  A [class-wide] invariant may be associated a [limited] private
             --  type or a private extension.
 
-            elsif Ekind_In (Typ, E_Limited_Private_Type,
-                                 E_Private_Type,
-                                 E_Record_Type_With_Private)
+            elsif Ekind (Typ) in E_Limited_Private_Type
+                               | E_Private_Type
+                               | E_Record_Type_With_Private
             then
                null;
 
@@ -18814,16 +18558,7 @@ package body Sem_Prag is
             --  The pragma defines a type-specific invariant, the type is said
             --  to have invariants of its "own".
 
-            Set_Has_Own_Invariants (Typ);
-
-            --  Set the Invariants_Ignored flag if that policy is in effect
-
-            Set_Invariants_Ignored (Typ,
-              Present (Check_Policy_List)
-                and then
-                  (Policy_In_Effect (Name_Invariant) = Name_Ignore
-                     and then
-                   Policy_In_Effect (Name_Type_Invariant) = Name_Ignore));
+            Set_Has_Own_Invariants (Base_Type (Typ));
 
             --  If the invariant is class-wide, then it can be inherited by
             --  derived or interface implementing types. The type is said to
@@ -19188,6 +18923,17 @@ package body Sem_Prag is
                      Set_Linker_Section_Pragma
                        (Entity (Corresponding_Aspect (N)), N);
 
+                     --  Propagate it to its ultimate aliased entity to
+                     --  facilitate the backend processing this attribute
+                     --  in instantiations of generic subprograms.
+
+                     if Present (Alias (Entity (Corresponding_Aspect (N))))
+                     then
+                        Set_Linker_Section_Pragma
+                          (Ultimate_Alias
+                            (Entity (Corresponding_Aspect (N))), N);
+                     end if;
+
                   --  Pragma case, we must climb the homonym chain, but skip
                   --  any for which the linker section is already set.
 
@@ -19196,6 +18942,15 @@ package body Sem_Prag is
                         if No (Linker_Section_Pragma (Ent)) then
                            Set_Linker_Section_Pragma (Ent, N);
 
+                           --  Propagate it to its ultimate aliased entity to
+                           --  facilitate the backend processing this attribute
+                           --  in instantiations of generic subprograms.
+
+                           if Present (Alias (Ent)) then
+                              Set_Linker_Section_Pragma
+                                (Ultimate_Alias (Ent), N);
+                           end if;
+
                            --  A pragma that applies to a Ghost entity becomes
                            --  Ghost for the purposes of legality checks and
                            --  removal of ignored Ghost code.
@@ -19409,8 +19164,7 @@ package body Sem_Prag is
                if Chars (Variant) = No_Name then
                   Error_Pragma_Arg_Ident ("expect name `Increases`", Variant);
 
-               elsif not Nam_In (Chars (Variant), Name_Decreases,
-                                                  Name_Increases)
+               elsif Chars (Variant) not in Name_Decreases | Name_Increases
                then
                   declare
                      Name : String := Get_Name_String (Chars (Variant));
@@ -19644,7 +19398,8 @@ package body Sem_Prag is
             --  Otherwise the pragma is associated with an illegal construct
 
             else
-               Error_Pragma ("pragma % must apply to a protected entry");
+               Error_Pragma
+                 ("pragma % must apply to a protected entry declaration");
                return;
             end if;
 
@@ -19716,17 +19471,13 @@ package body Sem_Prag is
             GNAT_Pragma;
             Check_Valid_Library_Unit_Pragma;
 
-            if Nkind (N) = N_Null_Statement then
-               return;
-            end if;
-
             --  Must appear for a spec or generic spec
 
-            if not Nkind_In (Unit (Cunit (Current_Sem_Unit)),
-                             N_Generic_Package_Declaration,
-                             N_Generic_Subprogram_Declaration,
-                             N_Package_Declaration,
-                             N_Subprogram_Declaration)
+            if Nkind (Unit (Cunit (Current_Sem_Unit))) not in
+                 N_Generic_Package_Declaration    |
+                 N_Generic_Subprogram_Declaration |
+                 N_Package_Declaration            |
+                 N_Subprogram_Declaration
             then
                Error_Pragma
                  (Fix_Error
@@ -19857,7 +19608,7 @@ package body Sem_Prag is
 
                --  The pragma must apply to an access-to-object type
 
-               if Ekind_In (Typ, E_Access_Type, E_General_Access_Type) then
+               if Ekind (Typ) in E_Access_Type | E_General_Access_Type then
                   null;
 
                --  Give a detailed error message on all other access type kinds
@@ -19941,7 +19692,53 @@ package body Sem_Prag is
 
          --  pragma No_Return (procedure_LOCAL_NAME {, procedure_Local_Name});
 
-         when Pragma_No_Return => No_Return : declare
+         when Pragma_No_Return => Prag_No_Return : declare
+
+            function Check_No_Return
+               (E : Entity_Id;
+                N : Node_Id) return Boolean;
+            --  Check rule 6.5.1(4/3) of the Ada RM. If the rule is violated,
+            --  emit an error message and return False, otherwise return True.
+            --  6.5.1 Nonreturning procedures:
+            --  4/3 "Aspect No_Return shall not be specified for a null
+            --  procedure nor an instance of a generic unit."
+
+            ---------------------
+            -- Check_No_Return --
+            ---------------------
+
+            function Check_No_Return
+               (E : Entity_Id;
+                N : Node_Id) return Boolean
+            is
+            begin
+               if Ekind (E) = E_Procedure then
+
+                  --  If E is a generic instance, marking it with No_Return
+                  --  is forbidden, but having it inherit the No_Return of
+                  --  the generic is allowed. We check if E is inheriting its
+                  --  No_Return flag from the generic by checking if No_Return
+                  --  is already set.
+
+                  if Is_Generic_Instance (E) and then not No_Return (E) then
+                     Error_Msg_NE
+                       ("generic instance & is marked as No_Return", N, E);
+                     Error_Msg_NE
+                       ("\generic procedure & must be marked No_Return",
+                        N,
+                        Generic_Parent (Parent (E)));
+                     return False;
+
+                  elsif Null_Present (Subprogram_Specification (E)) then
+                     Error_Msg_NE
+                       ("null procedure & cannot be marked No_Return", N, E);
+                     return False;
+                  end if;
+               end if;
+
+               return True;
+            end Check_No_Return;
+
             Arg   : Node_Id;
             E     : Entity_Id;
             Found : Boolean;
@@ -19975,7 +19772,7 @@ package body Sem_Prag is
                   raise Pragma_Exit;
                end if;
 
-               --  Loop to find matching procedures
+               --  Loop to find matching procedures or functions (Ada 2020)
 
                E := Entity (Id);
 
@@ -19983,8 +19780,13 @@ package body Sem_Prag is
                while Present (E)
                  and then Scope (E) = Current_Scope
                loop
-                  if Ekind_In (E, E_Generic_Procedure, E_Procedure) then
+                  --  Ada 2020 (AI12-0269): A function can be No_Return
 
+                  if Ekind (E) in E_Generic_Procedure | E_Procedure
+                    or else (Ada_Version >= Ada_2020
+                              and then
+                             Ekind (E) in E_Generic_Function | E_Function)
+                  then
                      --  Check that the pragma is not applied to a body.
                      --  First check the specless body case, to give a
                      --  different error message. These checks do not apply
@@ -20008,7 +19810,9 @@ package body Sem_Prag is
                         end if;
                      end if;
 
-                     Set_No_Return (E);
+                     if Check_No_Return (E, N) then
+                        Set_No_Return (E);
+                     end if;
 
                      --  A pragma that applies to a Ghost entity becomes Ghost
                      --  for the purposes of legality checks and removal of
@@ -20047,7 +19851,10 @@ package body Sem_Prag is
 
                      --  Set flag on any alias as well
 
-                     if Is_Overloadable (E) and then Present (Alias (E)) then
+                     if Is_Overloadable (E)
+                       and then Present (Alias (E))
+                       and then Check_No_Return (Alias (E), N)
+                     then
                         Set_No_Return (Alias (E));
                      end if;
 
@@ -20064,8 +19871,14 @@ package body Sem_Prag is
                if not Found then
                   if Entity (Id) = Current_Scope
                     and then From_Aspect_Specification (N)
+                    and then Check_No_Return (Entity (Id), N)
                   then
                      Set_No_Return (Entity (Id));
+
+                  elsif Ada_Version >= Ada_2020 then
+                     Error_Pragma_Arg
+                       ("no subprogram& found for pragma%", Arg);
+
                   else
                      Error_Pragma_Arg ("no procedure& found for pragma%", Arg);
                   end if;
@@ -20073,7 +19886,7 @@ package body Sem_Prag is
 
                Next (Arg);
             end loop;
-         end No_Return;
+         end Prag_No_Return;
 
          -----------------
          -- No_Run_Time --
@@ -20269,8 +20082,7 @@ package body Sem_Prag is
 
                if Present (Ename) then
 
-                  --  If entity name matches, we are fine. Save entity in
-                  --  pragma argument, for ASIS use.
+                  --  If entity name matches, we are fine.
 
                   if Chars (Ename) = Chars (Ent) then
                      Set_Entity (Ename, Ent);
@@ -20297,7 +20109,7 @@ package body Sem_Prag is
                            exit;
 
                         else
-                           Ent := Next_Literal (Ent);
+                           Next_Literal (Ent);
                         end if;
                      end loop;
                   end if;
@@ -20371,9 +20183,8 @@ package body Sem_Prag is
               and then
                 (Chars (Arg1) = Name_Entity
                    or else
-                     Nkind_In (Get_Pragma_Arg (Arg1), N_Character_Literal,
-                                                      N_Identifier,
-                                                      N_Operator_Symbol))
+                     Nkind (Get_Pragma_Arg (Arg1)) in
+                       N_Character_Literal | N_Identifier | N_Operator_Symbol)
             then
                Ename := Get_Pragma_Arg (Arg1);
 
@@ -20809,9 +20620,8 @@ package body Sem_Prag is
                      --  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,
-                                              E_Variable)
+                     elsif Ekind (Item_Id) in
+                             E_Abstract_State | E_Constant | E_Variable
                      then
                         Has_Item := True;
                         Constits := Part_Of_Constituents (State_Id);
@@ -21128,9 +20938,9 @@ package body Sem_Prag is
                Check_Arg_Is_Library_Level_Local_Name (Arg1);
 
                if not Is_Entity_Name (Get_Pragma_Arg (Arg1))
-                 or else not
-                   Ekind_In (Entity (Get_Pragma_Arg (Arg1)), E_Variable,
-                                                             E_Constant)
+                 or else
+                   Ekind (Entity (Get_Pragma_Arg (Arg1))) not in
+                     E_Variable | E_Constant
                then
                   Error_Pragma_Arg ("pragma% only applies to objects", Arg1);
                end if;
@@ -21237,19 +21047,6 @@ package body Sem_Prag is
             Map_Pragma_Name (From => Chars (New_Name), To => Chars (Old_Name));
          end Rename_Pragma;
 
-         -------------
-         -- Polling --
-         -------------
-
-         --  pragma Polling (ON | OFF);
-
-         when Pragma_Polling =>
-            GNAT_Pragma;
-            Check_Arg_Count (1);
-            Check_No_Identifiers;
-            Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off);
-            Polling_Required := (Chars (Get_Pragma_Arg (Arg1)) = Name_On);
-
          -----------------------------------
          -- Post/Post_Class/Postcondition --
          -----------------------------------
@@ -21397,9 +21194,7 @@ package body Sem_Prag is
             Set_Has_Delayed_Freeze (Typ);
 
             Set_Predicates_Ignored (Typ,
-              Present (Check_Policy_List)
-                and then
-                  Policy_In_Effect (Name_Dynamic_Predicate) = Name_Ignore);
+              Policy_In_Effect (Name_Dynamic_Predicate) = Name_Ignore);
             Discard := Rep_Item_Too_Late (Typ, N, FOnly => True);
          end Predicate;
 
@@ -21461,10 +21256,6 @@ package body Sem_Prag is
             Check_Ada_83_Warning;
             Check_Valid_Library_Unit_Pragma;
 
-            if Nkind (N) = N_Null_Statement then
-               return;
-            end if;
-
             Ent := Find_Lib_Unit_Name;
 
             --  A pragma that applies to a Ghost entity becomes Ghost for the
@@ -21586,7 +21377,7 @@ package body Sem_Prag is
 
             --  Task or Protected, must be of type Integer
 
-            elsif Nkind_In (P, N_Protected_Definition, N_Task_Definition) then
+            elsif Nkind (P) in N_Protected_Definition | N_Task_Definition then
                Arg := Get_Pragma_Arg (Arg1);
                Ent := Defining_Identifier (Parent (P));
 
@@ -21765,9 +21556,16 @@ package body Sem_Prag is
                Argx : constant Node_Id := Get_Pragma_Arg (Arg1);
 
             begin
-               if Chars (Argx) = Name_Ravenscar then
+               if Nkind (Argx) /= N_Identifier then
+                  Error_Msg_N
+                    ("argument of pragma Profile must be an identifier", N);
+
+               elsif Chars (Argx) = Name_Ravenscar then
                   Set_Ravenscar_Profile (Ravenscar, N);
 
+               elsif Chars (Argx) = Name_Jorvik then
+                  Set_Ravenscar_Profile (Jorvik, N);
+
                elsif Chars (Argx) = Name_Gnat_Extended_Ravenscar then
                   Set_Ravenscar_Profile (GNAT_Extended_Ravenscar, N);
 
@@ -21950,7 +21748,7 @@ package body Sem_Prag is
 
                --  Now declare the operators. We do this during analysis rather
                --  than expansion, since we want the operators available if we
-               --  are operating in -gnatc or ASIS mode.
+               --  are operating in -gnatc mode.
 
                Declare_Shift_Operator (Name_Rotate_Left);
                Declare_Shift_Operator (Name_Rotate_Right);
@@ -21995,9 +21793,8 @@ package body Sem_Prag is
 
             procedure Check_Arg (Arg : Node_Id) is
             begin
-               if not Nkind_In (Original_Node (Arg),
-                                N_String_Literal,
-                                N_Identifier)
+               if Nkind (Original_Node (Arg)) not in
+                    N_String_Literal | N_Identifier
                then
                   Error_Pragma_Arg
                     ("inappropriate argument for pragma %", Arg);
@@ -22013,7 +21810,7 @@ package body Sem_Prag is
 
             Def_Id := Entity (Internal);
 
-            if not Ekind_In (Def_Id, E_Constant, E_Variable) then
+            if Ekind (Def_Id) not in E_Constant | E_Variable then
                Error_Pragma_Arg
                  ("pragma% must designate an object", Internal);
             end if;
@@ -22104,10 +21901,6 @@ package body Sem_Prag is
                Check_Valid_Library_Unit_Pragma;
             end if;
 
-            if Nkind (N) = N_Null_Statement then
-               return;
-            end if;
-
             Ent := Find_Lib_Unit_Name;
 
             --  A pragma that applies to a Ghost entity becomes Ghost for the
@@ -22163,9 +21956,8 @@ package body Sem_Prag is
                loop
                   Def_Id := Get_Base_Subprogram (E);
 
-                  if not Ekind_In (Def_Id, E_Function,
-                                           E_Generic_Function,
-                                           E_Operator)
+                  if Ekind (Def_Id) not in
+                       E_Function | E_Generic_Function | E_Operator
                   then
                      Error_Pragma_Arg
                        ("pragma% requires a function name", Arg1);
@@ -22645,10 +22437,6 @@ package body Sem_Prag is
             Check_Ada_83_Warning;
             Check_Valid_Library_Unit_Pragma;
 
-            if Nkind (N) = N_Null_Statement then
-               return;
-            end if;
-
             Cunit_Node := Cunit (Current_Sem_Unit);
             K          := Nkind (Unit (Cunit_Node));
             Cunit_Ent  := Cunit_Entity (Current_Sem_Unit);
@@ -22688,10 +22476,6 @@ package body Sem_Prag is
             Check_Ada_83_Warning;
             Check_Valid_Library_Unit_Pragma;
 
-            if Nkind (N) = N_Null_Statement then
-               return;
-            end if;
-
             Cunit_Node := Cunit (Current_Sem_Unit);
             Cunit_Ent  := Cunit_Entity (Current_Sem_Unit);
 
@@ -22700,8 +22484,8 @@ package body Sem_Prag is
 
             Mark_Ghost_Pragma (N, Cunit_Ent);
 
-            if not Nkind_In (Unit (Cunit_Node), N_Package_Declaration,
-                                                N_Generic_Package_Declaration)
+            if Nkind (Unit (Cunit_Node)) not in
+                 N_Package_Declaration | N_Generic_Package_Declaration
             then
                Error_Pragma
                  ("pragma% can only apply to a package declaration");
@@ -22888,10 +22672,6 @@ package body Sem_Prag is
             Check_Ada_83_Warning;
             Check_Valid_Library_Unit_Pragma;
 
-            if Nkind (N) = N_Null_Statement then
-               return;
-            end if;
-
             Cunit_Node := Cunit (Current_Sem_Unit);
             Cunit_Ent  := Cunit_Entity (Current_Sem_Unit);
 
@@ -22900,8 +22680,8 @@ package body Sem_Prag is
 
             Mark_Ghost_Pragma (N, Cunit_Ent);
 
-            if not Nkind_In (Unit (Cunit_Node), N_Package_Declaration,
-                                                N_Generic_Package_Declaration)
+            if Nkind (Unit (Cunit_Node)) not in
+                 N_Package_Declaration | N_Generic_Package_Declaration
             then
                Error_Pragma
                  ("pragma% can only apply to a package declaration");
@@ -23203,7 +22983,7 @@ package body Sem_Prag is
                   --  anonymous type whose name cannot be used to issue error
                   --  messages. Recover the original entity of the type.
 
-                  if Ekind_In (Entity, E_Protected_Type, E_Task_Type) then
+                  if Ekind (Entity) in E_Protected_Type | E_Task_Type then
                      Err_Id :=
                        Defining_Entity
                          (Original_Node (Unit_Declaration_Node (Entity)));
@@ -23235,6 +23015,11 @@ package body Sem_Prag is
                   --  pragma in which case the current pragma is illegal as
                   --  it cannot "complete".
 
+                  elsif Get_SPARK_Mode_From_Annotation (N) = Off
+                    and then (Is_Generic_Unit (Entity) or else In_Instance)
+                  then
+                     null;
+
                   else
                      Error_Msg_N ("incorrect use of SPARK_Mode", Err_N);
                      Error_Msg_Sloc := Sloc (Err_Id);
@@ -23260,28 +23045,28 @@ package body Sem_Prag is
 
                procedure Add_Entity_To_Name_Buffer is
                begin
-                  if Ekind_In (E, E_Entry, E_Entry_Family) then
+                  if Ekind (E) in E_Entry | E_Entry_Family then
                      Add_Str_To_Name_Buffer ("entry");
 
-                  elsif Ekind_In (E, E_Generic_Package,
-                                     E_Package,
-                                     E_Package_Body)
+                  elsif Ekind (E) in E_Generic_Package
+                                   | E_Package
+                                   | E_Package_Body
                   then
                      Add_Str_To_Name_Buffer ("package");
 
-                  elsif Ekind_In (E, E_Protected_Body, E_Protected_Type) then
+                  elsif Ekind (E) in E_Protected_Body | E_Protected_Type then
                      Add_Str_To_Name_Buffer ("protected type");
 
-                  elsif Ekind_In (E, E_Function,
-                                     E_Generic_Function,
-                                     E_Generic_Procedure,
-                                     E_Procedure,
-                                     E_Subprogram_Body)
+                  elsif Ekind (E) in E_Function
+                                   | E_Generic_Function
+                                   | E_Generic_Procedure
+                                   | E_Procedure
+                                   | E_Subprogram_Body
                   then
                      Add_Str_To_Name_Buffer ("subprogram");
 
                   else
-                     pragma Assert (Ekind_In (E, E_Task_Body, E_Task_Type));
+                     pragma Assert (Ekind (E) in E_Task_Body | E_Task_Type);
                      Add_Str_To_Name_Buffer ("task type");
                   end if;
                end Add_Entity_To_Name_Buffer;
@@ -23340,7 +23125,7 @@ package body Sem_Prag is
                --    * The mode of the context
                --    * The mode of the spec (if any)
 
-               if Nkind_In (Decl, N_Entry_Body, N_Subprogram_Body) then
+               if Nkind (Decl) in N_Entry_Body | N_Subprogram_Body then
 
                   --  A stand-alone subprogram body
 
@@ -23390,7 +23175,7 @@ package body Sem_Prag is
 
                else
                   pragma Assert
-                    (Nkind_In (Decl, N_Protected_Body, N_Task_Body));
+                    (Nkind (Decl) in N_Protected_Body | N_Task_Body);
 
                   Check_Pragma_Conformance
                     (Context_Pragma => SPARK_Pragma (Body_Id),
@@ -23512,8 +23297,8 @@ package body Sem_Prag is
                --  SPARK_Mode of the context because the task does not have any
                --  entries that could inherit the mode.
 
-               if not Nkind_In (Decl, N_Single_Task_Declaration,
-                                      N_Task_Type_Declaration)
+               if Nkind (Decl) not in
+                    N_Single_Task_Declaration | N_Task_Type_Declaration
                then
                   Set_SPARK_Context;
                end if;
@@ -23560,16 +23345,6 @@ package body Sem_Prag is
          --  Start of processing for Do_SPARK_Mode
 
          begin
-            --  When a SPARK_Mode pragma appears inside an instantiation whose
-            --  enclosing context has SPARK_Mode set to "off", the pragma has
-            --  no semantic effect.
-
-            if Ignore_SPARK_Mode_Pragmas_In_Instance then
-               Rewrite (N, Make_Null_Statement (Loc));
-               Analyze (N);
-               return;
-            end if;
-
             GNAT_Pragma;
             Check_No_Identifiers;
             Check_At_Most_N_Arguments (1);
@@ -23586,6 +23361,18 @@ package body Sem_Prag is
             Mode_Id := Get_SPARK_Mode_Type (Mode);
             Context := Parent (N);
 
+            --  When a SPARK_Mode pragma appears inside an instantiation whose
+            --  enclosing context has SPARK_Mode set to "off", the pragma has
+            --  no semantic effect.
+
+            if Ignore_SPARK_Mode_Pragmas_In_Instance
+              and then Mode_Id /= Off
+            then
+               Rewrite (N, Make_Null_Statement (Loc));
+               Analyze (N);
+               return;
+            end if;
+
             --  The pragma appears in a configuration file
 
             if No (Context) then
@@ -23672,8 +23459,8 @@ package body Sem_Prag is
                   --    procedure Proc ...;
                   --    pragma SPARK_Mode ...;
 
-                  elsif Nkind_In (Stmt, N_Generic_Subprogram_Declaration,
-                                        N_Subprogram_Declaration)
+                  elsif Nkind (Stmt) in N_Generic_Subprogram_Declaration
+                                      | N_Subprogram_Declaration
                     or else (Nkind (Stmt) = N_Entry_Declaration
                               and then Is_Protected_Type
                                          (Scope (Defining_Entity (Stmt))))
@@ -23718,11 +23505,11 @@ package body Sem_Prag is
                --    protected body Prot is
                --       pragma SPARK_Mode ...;
 
-               if Nkind_In (Context, N_Entry_Body,
-                                     N_Package_Body,
-                                     N_Protected_Body,
-                                     N_Subprogram_Body,
-                                     N_Task_Body)
+               if Nkind (Context) in N_Entry_Body
+                                   | N_Package_Body
+                                   | N_Protected_Body
+                                   | N_Subprogram_Body
+                                   | N_Task_Body
                then
                   Process_Body (Context);
 
@@ -23739,9 +23526,9 @@ package body Sem_Prag is
                --    private
                --       pragma SPARK_Mode ...;
 
-               elsif Nkind_In (Context, N_Package_Specification,
-                                        N_Protected_Definition,
-                                        N_Task_Definition)
+               elsif Nkind (Context) in N_Package_Specification
+                                      | N_Protected_Definition
+                                      | N_Task_Definition
                then
                   if List_Containing (N) = Visible_Declarations (Context) then
                      Process_Visible_Part (Parent (Context));
@@ -23767,8 +23554,8 @@ package body Sem_Prag is
                --    procedure Proc ...;
                --    pragma SPARK_Mode ...;
 
-               elsif Nkind_In (Context, N_Generic_Subprogram_Declaration,
-                                        N_Subprogram_Declaration)
+               elsif Nkind (Context) in N_Generic_Subprogram_Declaration
+                                      | N_Subprogram_Declaration
                then
                   Process_Overloadable (Context);
 
@@ -23897,6 +23684,9 @@ package body Sem_Prag is
                   Error_Pragma_Arg
                     ("argument for pragma% must be function of one argument",
                      Arg);
+               elsif Is_Abstract_Subprogram (Ent) then
+                  Error_Pragma_Arg
+                    ("argument for pragma% cannot be abstract", Arg);
                end if;
             end Check_OK_Stream_Convert_Function;
 
@@ -24069,19 +23859,152 @@ package body Sem_Prag is
                         end if;
                      end if;
 
-                  elsif Chars (A) = Name_On then
-                     if not Ignore_Style_Checks_Pragmas then
-                        Style_Check := True;
-                     end if;
+                  elsif Chars (A) = Name_On then
+                     if not Ignore_Style_Checks_Pragmas then
+                        Style_Check := True;
+                     end if;
+
+                  elsif Chars (A) = Name_Off then
+                     if not Ignore_Style_Checks_Pragmas then
+                        Style_Check := False;
+                     end if;
+                  end if;
+               end if;
+            end if;
+         end Style_Checks;
+
+         ------------------------
+         -- Subprogram_Variant --
+         ------------------------
+
+         --  pragma Subprogram_Variant ( SUBPROGRAM_VARIANT_ITEM
+         --                           {, SUBPROGRAM_VARIANT_ITEM } );
+
+         --  SUBPROGRAM_VARIANT_ITEM ::=
+         --    CHANGE_DIRECTION => discrete_EXPRESSION
+
+         --  CHANGE_DIRECTION ::= Increases | Decreases
+
+         --  Characteristics:
+
+         --    * Analysis - The annotation undergoes initial checks to verify
+         --    the legal placement and context. Secondary checks preanalyze the
+         --    expressions in:
+
+         --       Analyze_Subprogram_Variant_In_Decl_Part
+
+         --    * Expansion - The annotation is expanded during the expansion of
+         --    the related subprogram [body] contract as performed in:
+
+         --       Expand_Subprogram_Contract
+
+         --    * Template - The annotation utilizes the generic template of the
+         --    related subprogram [body] when it is:
+
+         --       aspect on subprogram declaration
+         --       aspect on stand-alone subprogram body
+         --       pragma on stand-alone subprogram body
+
+         --    The annotation must prepare its own template when it is:
+
+         --       pragma on subprogram declaration
+
+         --    * Globals - Capture of global references must occur after full
+         --    analysis.
+
+         --    * Instance - The annotation is instantiated automatically when
+         --    the related generic subprogram [body] is instantiated except for
+         --    the "pragma on subprogram declaration" case. In that scenario
+         --    the annotation must instantiate itself.
+
+         when Pragma_Subprogram_Variant => Subprogram_Variant : declare
+            Spec_Id   : Entity_Id;
+            Subp_Decl : Node_Id;
+            Subp_Spec : Node_Id;
+
+         begin
+            GNAT_Pragma;
+            Check_No_Identifiers;
+            Check_Arg_Count (1);
+
+            --  Ensure the proper placement of the pragma. Subprogram_Variant
+            --  must be associated with a subprogram declaration or a body that
+            --  acts as a spec.
+
+            Subp_Decl :=
+              Find_Related_Declaration_Or_Body (N, Do_Checks => True);
+
+            --  Generic subprogram
+
+            if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
+               null;
+
+            --  Body acts as spec
+
+            elsif Nkind (Subp_Decl) = N_Subprogram_Body
+              and then No (Corresponding_Spec (Subp_Decl))
+            then
+               null;
+
+            --  Body stub acts as spec
+
+            elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
+              and then No (Corresponding_Spec_Of_Stub (Subp_Decl))
+            then
+               null;
+
+            --  Subprogram
+
+            elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
+               Subp_Spec := Specification (Subp_Decl);
+
+               --  Pragma Subprogram_Variant is forbidden on null procedures,
+               --  as this may lead to potential ambiguities in behavior when
+               --  interface null procedures are involved. Also, it just
+               --  wouldn't make sense, because null procedure is not
+               --  recursive.
+
+               if Nkind (Subp_Spec) = N_Procedure_Specification
+                 and then Null_Present (Subp_Spec)
+               then
+                  Error_Msg_N (Fix_Error
+                    ("pragma % cannot apply to null procedure"), N);
+                  return;
+               end if;
+
+            else
+               Pragma_Misplaced;
+               return;
+            end if;
+
+            Spec_Id := Unique_Defining_Entity (Subp_Decl);
+
+            --  A pragma that applies to a Ghost entity becomes Ghost for the
+            --  purposes of legality checks and removal of ignored Ghost code.
+
+            Mark_Ghost_Pragma (N, Spec_Id);
+            Ensure_Aggregate_Form (Get_Argument (N, Spec_Id));
+
+            --  Chain the pragma on the contract for further processing by
+            --  Analyze_Subprogram_Variant_In_Decl_Part.
 
-                  elsif Chars (A) = Name_Off then
-                     if not Ignore_Style_Checks_Pragmas then
-                        Style_Check := False;
-                     end if;
-                  end if;
-               end if;
+            Add_Contract_Item (N, Defining_Entity (Subp_Decl));
+
+            --  Fully analyze the pragma when it appears inside a subprogram
+            --  body because it cannot benefit from forward references.
+
+            if Nkind (Subp_Decl) in N_Subprogram_Body
+                                  | N_Subprogram_Body_Stub
+            then
+               --  The legality checks of pragma Subprogram_Variant are
+               --  affected by the SPARK mode in effect and the volatility
+               --  of the context. Analyze all pragmas in a specific order.
+
+               Analyze_If_Present (Pragma_SPARK_Mode);
+               Analyze_If_Present (Pragma_Volatile_Function);
+               Analyze_Subprogram_Variant_In_Decl_Part (N);
             end if;
-         end Style_Checks;
+         end Subprogram_Variant;
 
          --------------
          -- Subtitle --
@@ -24529,8 +24452,8 @@ package body Sem_Prag is
             --  in a library-level package. First determine whether the current
             --  compilation unit is a legal context.
 
-            if Nkind_In (Pack_Decl, N_Package_Declaration,
-                                    N_Generic_Package_Declaration)
+            if Nkind (Pack_Decl) in N_Package_Declaration
+                                  | N_Generic_Package_Declaration
             then
                null;
 
@@ -24566,11 +24489,11 @@ package body Sem_Prag is
             --  The context is a [generic] subprogram declared at the top level
             --  of the [generic] package unit.
 
-            elsif Nkind_In (Subp_Decl, N_Generic_Subprogram_Declaration,
-                                       N_Subprogram_Declaration)
+            elsif Nkind (Subp_Decl) in N_Generic_Subprogram_Declaration
+                                     | N_Subprogram_Declaration
               and then Present (Context)
-              and then Nkind_In (Context, N_Generic_Package_Declaration,
-                                          N_Package_Declaration)
+              and then Nkind (Context) in N_Generic_Package_Declaration
+                                        | N_Package_Declaration
             then
                null;
 
@@ -24595,10 +24518,10 @@ package body Sem_Prag is
 
             Add_Contract_Item (N, Subp_Id);
 
-            --  Preanalyze the original aspect argument "Name" for ASIS or for
-            --  a generic subprogram to properly capture global references.
+            --  Preanalyze the original aspect argument "Name" for a generic
+            --  subprogram to properly capture global references.
 
-            if ASIS_Mode or else Is_Generic_Subprogram (Subp_Id) then
+            if Is_Generic_Subprogram (Subp_Id) then
                Asp_Arg := Test_Case_Arg (N, Name_Name, From_Aspect => True);
 
                if Present (Asp_Arg) then
@@ -24624,9 +24547,9 @@ package body Sem_Prag is
             --  or subprogram body because it cannot benefit from forward
             --  references.
 
-            if Nkind_In (Subp_Decl, N_Entry_Body,
-                                    N_Subprogram_Body,
-                                    N_Subprogram_Body_Stub)
+            if Nkind (Subp_Decl) in N_Entry_Body
+                                  | N_Subprogram_Body
+                                  | N_Subprogram_Body_Stub
             then
                --  The legality checks of pragma Test_Case are affected by the
                --  SPARK mode in effect and the volatility of the context.
@@ -24932,18 +24855,15 @@ package body Sem_Prag is
          --  body, not in the spec).
 
          when Pragma_Unimplemented_Unit => Unimplemented_Unit : declare
-            Cunitent : constant Entity_Id   :=
+            Cunitent : constant Entity_Id :=
                          Cunit_Entity (Get_Source_Unit (Loc));
-            Ent_Kind : constant Entity_Kind := Ekind (Cunitent);
 
          begin
             GNAT_Pragma;
             Check_Arg_Count (0);
 
             if Operating_Mode = Generate_Code
-              or else Ent_Kind = E_Generic_Function
-              or else Ent_Kind = E_Generic_Procedure
-              or else Ent_Kind = E_Generic_Package
+              or else Is_Generic_Unit (Cunitent)
             then
                Get_Name_String (Chars (Cunitent));
                Set_Casing (Mixed_Case);
@@ -25289,7 +25209,7 @@ package body Sem_Prag is
 
             Spec_Id := Unique_Defining_Entity (Subp_Decl);
 
-            if not Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
+            if Ekind (Spec_Id) not in E_Function | E_Generic_Function then
                Pragma_Misplaced;
                return;
             end if;
@@ -25377,7 +25297,7 @@ package body Sem_Prag is
          --  DETAILS ::= static_string_EXPRESSION
          --  DETAILS ::= On | Off, static_string_EXPRESSION
 
-         --  TOOL_NAME ::= GNAT | GNATProve
+         --  TOOL_NAME ::= GNAT | GNATprove
 
          --  REASON ::= Reason => STRING_LITERAL {& STRING_LITERAL}
 
@@ -25450,10 +25370,10 @@ package body Sem_Prag is
                --  was given otherwise, by shifting the arguments.
 
                if Nkind (Argx) = N_Identifier
-                 and then Nam_In (Chars (Argx), Name_Gnat, Name_Gnatprove)
+                 and then Chars (Argx) in Name_Gnat | Name_Gnatprove
                then
                   if Chars (Argx) = Name_Gnat then
-                     if CodePeer_Mode or GNATprove_Mode or ASIS_Mode then
+                     if CodePeer_Mode or GNATprove_Mode then
                         Rewrite (N, Make_Null_Statement (Loc));
                         Analyze (N);
                         raise Pragma_Exit;
@@ -25503,7 +25423,7 @@ package body Sem_Prag is
                   --  On/Off one argument case was processed by parser
 
                   if Nkind (Argx) = N_Identifier
-                    and then Nam_In (Chars (Argx), Name_On, Name_Off)
+                    and then Chars (Argx) in Name_On | Name_Off
                   then
                      null;
 
@@ -25875,7 +25795,7 @@ package body Sem_Prag is
            and then
              (Etype (Nod) = Disp_Typ
                or else Etype (Nod) = Class_Wide_Type (Disp_Typ))
-           and then Ekind_In (Entity (Nod), E_Constant, E_Variable)
+           and then Ekind (Entity (Nod)) in E_Constant | E_Variable
          then
             Error_Msg_NE
               ("object in class-wide condition must be formal of type &",
@@ -26026,18 +25946,17 @@ package body Sem_Prag is
       --  matched items found in pragma Depends.
 
       procedure Check_Output_States
-        (Spec_Id      : Entity_Id;
-         Spec_Inputs  : Elist_Id;
+        (Spec_Inputs  : Elist_Id;
          Spec_Outputs : Elist_Id;
          Body_Inputs  : Elist_Id;
          Body_Outputs : Elist_Id);
       --  Determine whether pragma Depends contains an output state with a
       --  visible refinement and if so, ensure that pragma Refined_Depends
-      --  mentions all its constituents as outputs. Spec_Id is the entity of
-      --  the related subprograms. Spec_Inputs and Spec_Outputs denote the
-      --  inputs and outputs of the subprogram spec synthesized from pragma
-      --  Depends. Body_Inputs and Body_Outputs denote the inputs and outputs
-      --  of the subprogram body synthesized from pragma Refined_Depends.
+      --  mentions all its constituents as outputs. Spec_Inputs and
+      --  Spec_Outputs denote the inputs and outputs of the subprogram spec
+      --  synthesized from pragma Depends. Body_Inputs and Body_Outputs denote
+      --  the inputs and outputs of the subprogram body synthesized from pragma
+      --  Refined_Depends.
 
       function Collect_States (Clauses : List_Id) return Elist_Id;
       --  Given a normalized list of dependencies obtained from calling
@@ -26059,11 +25978,8 @@ package body Sem_Prag is
       --  all special cases. Matched_Items contains the entities of all matched
       --  items found in pragma Depends.
 
-      procedure Report_Extra_Clauses
-        (Spec_Id : Entity_Id;
-         Clauses : List_Id);
-      --  Emit an error for each extra clause found in list Clauses. Spec_Id
-      --  denotes the entity of the related subprogram.
+      procedure Report_Extra_Clauses (Clauses : List_Id);
+      --  Emit an error for each extra clause found in list Clauses
 
       -----------------------------
       -- Check_Dependency_Clause --
@@ -26257,9 +26173,8 @@ package body Sem_Prag is
                      if Is_Entity_Name (Ref_Item) then
                         Ref_Item_Id := Entity_Of (Ref_Item);
 
-                        if Ekind_In (Ref_Item_Id, E_Abstract_State,
-                                                  E_Constant,
-                                                  E_Variable)
+                        if Ekind (Ref_Item_Id) in
+                             E_Abstract_State | E_Constant | E_Variable
                           and then Present (Encapsulating_State (Ref_Item_Id))
                           and then Find_Encapsulating_State
                                      (Dep_States, Ref_Item_Id) = Dep_Item_Id
@@ -26327,7 +26242,7 @@ package body Sem_Prag is
          --  Do not perform this check in an instance because it was already
          --  performed successfully in the generic template.
 
-         if Is_Generic_Instance (Spec_Id) then
+         if In_Instance then
             return;
          end if;
 
@@ -26494,8 +26409,7 @@ package body Sem_Prag is
       -------------------------
 
       procedure Check_Output_States
-        (Spec_Id      : Entity_Id;
-         Spec_Inputs  : Elist_Id;
+        (Spec_Inputs  : Elist_Id;
          Spec_Outputs : Elist_Id;
          Body_Inputs  : Elist_Id;
          Body_Outputs : Elist_Id)
@@ -26588,7 +26502,7 @@ package body Sem_Prag is
          --  Do not perform this check in an instance because it was already
          --  performed successfully in the generic template.
 
-         if Is_Generic_Instance (Spec_Id) then
+         if In_Instance then
             null;
 
          --  Inspect the outputs of pragma Depends looking for a state with a
@@ -26897,9 +26811,8 @@ package body Sem_Prag is
 
                --  The input must be a constituent of a state
 
-               if Ekind_In (Input_Id, E_Abstract_State,
-                                      E_Constant,
-                                      E_Variable)
+               if Ekind (Input_Id) in
+                    E_Abstract_State | E_Constant | E_Variable
                  and then Present (Encapsulating_State (Input_Id))
                then
                   State_Id := Encapsulating_State (Input_Id);
@@ -26933,17 +26846,14 @@ package body Sem_Prag is
       -- Report_Extra_Clauses --
       --------------------------
 
-      procedure Report_Extra_Clauses
-        (Spec_Id : Entity_Id;
-         Clauses : List_Id)
-      is
+      procedure Report_Extra_Clauses (Clauses : List_Id) is
          Clause : Node_Id;
 
       begin
          --  Do not perform this check in an instance because it was already
          --  performed successfully in the generic template.
 
-         if Is_Generic_Instance (Spec_Id) then
+         if In_Instance then
             null;
 
          elsif Present (Clauses) then
@@ -27078,20 +26988,12 @@ package body Sem_Prag is
             --  constituents appear as outputs in the dependency refinement.
 
             Check_Output_States
-              (Spec_Id      => Spec_Id,
-               Spec_Inputs  => Spec_Inputs,
+              (Spec_Inputs  => Spec_Inputs,
                Spec_Outputs => Spec_Outputs,
                Body_Inputs  => Body_Inputs,
                Body_Outputs => Body_Outputs);
          end if;
 
-         --  Matching is disabled in ASIS because clauses are not normalized as
-         --  this is a tree altering activity similar to expansion.
-
-         if ASIS_Mode then
-            goto Leave;
-         end if;
-
          --  Multiple dependency clauses appear as component associations of an
          --  aggregate. Note that the clauses are copied because the algorithm
          --  modifies them and this should not be visible in Depends.
@@ -27149,7 +27051,7 @@ package body Sem_Prag is
          Remove_Extra_Clauses (Refinements, Matched_Items);
 
          if Serious_Errors_Detected = Errors then
-            Report_Extra_Clauses (Spec_Id, Refinements);
+            Report_Extra_Clauses (Refinements);
          end if;
       end if;
 
@@ -27402,7 +27304,7 @@ package body Sem_Prag is
          --  Do not perform this check in an instance because it was already
          --  performed successfully in the generic template.
 
-         if Is_Generic_Instance (Spec_Id) then
+         if In_Instance then
             null;
 
          --  Inspect the In_Out items of the corresponding Global pragma
@@ -27511,7 +27413,7 @@ package body Sem_Prag is
          --  Do not perform this check in an instance because it was already
          --  performed successfully in the generic template.
 
-         if Is_Generic_Instance (Spec_Id) then
+         if In_Instance then
             null;
 
          --  Inspect the Input items of the corresponding Global pragma looking
@@ -27634,7 +27536,7 @@ package body Sem_Prag is
          --  Do not perform this check in an instance because it was already
          --  performed successfully in the generic template.
 
-         if Is_Generic_Instance (Spec_Id) then
+         if In_Instance then
             null;
 
          --  Inspect the Output items of the corresponding Global pragma
@@ -27740,7 +27642,7 @@ package body Sem_Prag is
          --  Do not perform this check in an instance because it was already
          --  performed successfully in the generic template.
 
-         if Is_Generic_Instance (Spec_Id) then
+         if In_Instance then
             null;
 
          --  Inspect the Proof_In items of the corresponding Global pragma
@@ -27818,9 +27720,7 @@ package body Sem_Prag is
          --  Start of processing for Check_Refined_Global_Item
 
          begin
-            if Ekind_In (Item_Id, E_Abstract_State,
-                                  E_Constant,
-                                  E_Variable)
+            if Ekind (Item_Id) in E_Abstract_State | E_Constant | E_Variable
             then
                Enc_State := Find_Encapsulating_State (States, Item_Id);
             end if;
@@ -27906,7 +27806,7 @@ package body Sem_Prag is
          --  Do not perform this check in an instance because it was already
          --  performed successfully in the generic template.
 
-         if Is_Generic_Instance (Spec_Id) then
+         if In_Instance then
             null;
 
          elsif Nkind (List) = N_Null then
@@ -27914,9 +27814,9 @@ package body Sem_Prag is
 
          --  Single global item declaration
 
-         elsif Nkind_In (List, N_Expanded_Name,
-                               N_Identifier,
-                               N_Selected_Component)
+         elsif Nkind (List) in N_Expanded_Name
+                             | N_Identifier
+                             | N_Selected_Component
          then
             Check_Refined_Global_Item (List, Global_Mode);
 
@@ -28046,9 +27946,9 @@ package body Sem_Prag is
 
          --  Single global item declaration
 
-         elsif Nkind_In (List, N_Expanded_Name,
-                               N_Identifier,
-                               N_Selected_Component)
+         elsif Nkind (List) in N_Expanded_Name
+                             | N_Identifier
+                             | N_Selected_Component
          then
             Collect_Global_Item (List, Mode);
 
@@ -28157,7 +28057,7 @@ package body Sem_Prag is
          --  Do not perform this check in an instance because it was already
          --  performed successfully in the generic template.
 
-         if Is_Generic_Instance (Spec_Id) then
+         if In_Instance then
             null;
 
          else
@@ -28180,7 +28080,7 @@ package body Sem_Prag is
          --  Do not perform this check in an instance because it was already
          --  performed successfully in the generic template.
 
-         if Is_Generic_Instance (Spec_Id) then
+         if In_Instance then
             null;
 
          else
@@ -28244,7 +28144,7 @@ package body Sem_Prag is
       --  body contract is instantiated. Since the generic template is legal,
       --  do not perform this check in the instance to circumvent this oddity.
 
-      if Is_Generic_Instance (Spec_Id) then
+      if In_Instance then
          null;
 
       --  Non-instance case
@@ -28360,7 +28260,7 @@ package body Sem_Prag is
       --  in the generic template.
 
       if Serious_Errors_Detected = Errors
-        and then not Is_Generic_Instance (Spec_Id)
+        and then not In_Instance
         and then not Has_Null_State
         and then No_Constit
       then
@@ -28593,35 +28493,69 @@ package body Sem_Prag is
                         Constit, Encapsulating_State (Constit_Id));
                   end if;
 
-               --  The only other source of legal constituents is the body
-               --  state space of the related package.
-
                else
-                  if Present (Body_States) then
-                     State_Elmt := First_Elmt (Body_States);
-                     while Present (State_Elmt) loop
+                  declare
+                     Pack_Id   : Entity_Id;
+                     Placement : State_Space_Kind;
+                  begin
+                     --  Find where the constituent lives with respect to the
+                     --  state space.
 
-                        --  Consume a valid constituent to signal that it has
-                        --  been encountered.
+                     Find_Placement_In_State_Space
+                       (Item_Id   => Constit_Id,
+                        Placement => Placement,
+                        Pack_Id   => Pack_Id);
 
-                        if Node (State_Elmt) = Constit_Id then
-                           Remove_Elmt (Body_States, State_Elmt);
-                           Collect_Constituent;
-                           return;
-                        end if;
+                     --  The constituent is part of the visible state of a
+                     --  private child package, but lacks a Part_Of indicator.
 
-                        Next_Elmt (State_Elmt);
-                     end loop;
-                  end if;
+                     if Placement = Visible_State_Space
+                       and then Is_Child_Unit (Pack_Id)
+                       and then not Is_Generic_Unit (Pack_Id)
+                       and then Is_Private_Descendant (Pack_Id)
+                     then
+                        Error_Msg_Name_1 := Chars (State_Id);
+                        SPARK_Msg_NE
+                          ("& cannot act as constituent of state %",
+                           Constit, Constit_Id);
+                        Error_Msg_Sloc :=
+                          Sloc (Enclosing_Declaration (Constit_Id));
+                        SPARK_Msg_NE
+                          ("\missing Part_Of indicator # should specify "
+                           & "encapsulator &",
+                           Constit, State_Id);
 
-                  --  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)).
+                     --  The only other source of legal constituents is the
+                     --  body state space of the related package.
 
-                  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);
+                     else
+                        if Present (Body_States) then
+                           State_Elmt := First_Elmt (Body_States);
+                           while Present (State_Elmt) loop
+
+                              --  Consume a valid constituent to signal that it
+                              --  has been encountered.
+
+                              if Node (State_Elmt) = Constit_Id then
+                                 Remove_Elmt (Body_States, State_Elmt);
+                                 Collect_Constituent;
+                                 return;
+                              end if;
+
+                              Next_Elmt (State_Elmt);
+                           end loop;
+                        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;
                end if;
             end Match_Constituent;
 
@@ -28735,9 +28669,8 @@ package body Sem_Prag is
 
                   --  The constituent is a valid state or object
 
-                  elsif Ekind_In (Constit_Id, E_Abstract_State,
-                                              E_Constant,
-                                              E_Variable)
+                  elsif Ekind (Constit_Id) in
+                          E_Abstract_State | E_Constant | E_Variable
                   then
                      Match_Constituent (Constit_Id);
 
@@ -29044,6 +28977,20 @@ package body Sem_Prag is
          --  in the refinement clause.
 
          Report_Unused_Constituents (Part_Of_Constits);
+
+         --  Avoid a cascading error reporting a missing refinement by adding a
+         --  dummy constituent.
+
+         if No (Refinement_Constituents (State_Id)) then
+            Set_Refinement_Constituents (State_Id, New_Elmt_List (Any_Id));
+         end if;
+
+         --  At this point the refinement might be dummy, but must be
+         --  well-formed, to prevent cascaded errors.
+
+         pragma Assert (Has_Null_Refinement (State_Id)
+                          xor
+                        Has_Non_Null_Refinement (State_Id));
       end Analyze_Refinement_Clause;
 
       -----------------------------
@@ -29124,6 +29071,156 @@ package body Sem_Prag is
       Set_Is_Analyzed_Pragma (N);
    end Analyze_Refined_State_In_Decl_Part;
 
+   ---------------------------------------------
+   -- Analyze_Subprogram_Variant_In_Decl_Part --
+   ---------------------------------------------
+
+   --  WARNING: This routine manages Ghost regions. Return statements must be
+   --  replaced by gotos which jump to the end of the routine and restore the
+   --  Ghost mode.
+
+   procedure Analyze_Subprogram_Variant_In_Decl_Part
+     (N         : Node_Id;
+      Freeze_Id : Entity_Id := Empty)
+   is
+      Subp_Decl : constant Node_Id   := Find_Related_Declaration_Or_Body (N);
+      Spec_Id   : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
+
+      procedure Analyze_Variant (Variant : Node_Id);
+      --  Verify the legality of a single contract case
+
+      ---------------------
+      -- Analyze_Variant --
+      ---------------------
+
+      procedure Analyze_Variant (Variant : Node_Id) is
+         Direction       : Node_Id;
+         Expr            : Node_Id;
+         Errors          : Nat;
+         Extra_Direction : Node_Id;
+
+      begin
+         if Nkind (Variant) /= N_Component_Association then
+            Error_Msg_N ("wrong syntax in subprogram variant", Variant);
+            return;
+         end if;
+
+         Direction := First (Choices (Variant));
+         Expr      := Expression (Variant);
+
+         --  Each variant must have exactly one direction
+
+         Extra_Direction := Next (Direction);
+
+         if Present (Extra_Direction) then
+            Error_Msg_N
+              ("subprogram variant case must have exactly one direction",
+               Extra_Direction);
+         end if;
+
+         --  Check placement of OTHERS if available (SPARK RM 6.1.3(1))
+
+         if Nkind (Direction) = N_Identifier then
+            if Chars (Direction) /= Name_Decreases
+                 and then
+               Chars (Direction) /= Name_Increases
+            then
+               Error_Msg_N ("wrong direction", Direction);
+            end if;
+         else
+            Error_Msg_N ("wrong syntax", Direction);
+         end if;
+
+         Errors := Serious_Errors_Detected;
+         Preanalyze_Assert_Expression (Expr, Any_Discrete);
+
+         --  Emit a clarification message when the variant expression
+         --  contains at least one undefined reference, possibly due
+         --  to contract freezing.
+
+         if Errors /= Serious_Errors_Detected
+           and then Present (Freeze_Id)
+           and then Has_Undefined_Reference (Expr)
+         then
+            Contract_Freeze_Error (Spec_Id, Freeze_Id);
+         end if;
+      end Analyze_Variant;
+
+      --  Local variables
+
+      Variants : 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
+
+      Variant       : Node_Id;
+      Restore_Scope : Boolean := False;
+
+   --  Start of processing for Analyze_Subprogram_Variant_In_Decl_Part
+
+   begin
+      --  Do not analyze the pragma multiple times
+
+      if Is_Analyzed_Pragma (N) then
+         return;
+      end if;
+
+      --  Set the Ghost mode in effect from the pragma. Due to the delayed
+      --  analysis of the pragma, the Ghost mode at point of declaration and
+      --  point of analysis may not necessarily be the same. Use the mode in
+      --  effect at the point of declaration.
+
+      Set_Ghost_Mode (N);
+
+      --  Single and multiple contract cases must appear in aggregate form. If
+      --  this is not the case, then either the parser of the analysis of the
+      --  pragma failed to produce an aggregate.
+
+      pragma Assert (Nkind (Variants) = N_Aggregate);
+
+      --  Only "change_direction => discrete_expression" clauses are allowed
+
+      if Present (Component_Associations (Variants))
+        and then No (Expressions (Variants))
+      then
+
+         --  Ensure that the formal parameters are visible when analyzing all
+         --  clauses. This falls out of the general rule of aspects pertaining
+         --  to subprogram declarations.
+
+         if not In_Open_Scopes (Spec_Id) then
+            Restore_Scope := True;
+            Push_Scope (Spec_Id);
+
+            if Is_Generic_Subprogram (Spec_Id) then
+               Install_Generic_Formals (Spec_Id);
+            else
+               Install_Formals (Spec_Id);
+            end if;
+         end if;
+
+         Variant := First (Component_Associations (Variants));
+         while Present (Variant) loop
+            Analyze_Variant (Variant);
+            Next (Variant);
+         end loop;
+
+         if Restore_Scope then
+            End_Scope;
+         end if;
+
+      --  Otherwise the pragma is illegal
+
+      else
+         Error_Msg_N ("wrong syntax for subprogram variant", N);
+      end if;
+
+      Set_Is_Analyzed_Pragma (N);
+
+      Restore_Ghost_Region (Saved_GM, Saved_IGR);
+   end Analyze_Subprogram_Variant_In_Decl_Part;
+
    ------------------------------------
    -- Analyze_Test_Case_In_Decl_Part --
    ------------------------------------
@@ -29144,10 +29241,10 @@ package body Sem_Prag is
          Arg : Node_Id;
 
       begin
-         --  Preanalyze the original aspect argument for ASIS or for a generic
-         --  subprogram to properly capture global references.
+         --  Preanalyze the original aspect argument for a generic subprogram
+         --  to properly capture global references.
 
-         if ASIS_Mode or else Is_Generic_Subprogram (Spec_Id) then
+         if Is_Generic_Subprogram (Spec_Id) then
             Arg :=
               Test_Case_Arg
                 (Prag        => N,
@@ -29426,11 +29523,11 @@ package body Sem_Prag is
             if Ename = Pnm
               or else Pnm = Name_Assertion
               or else (Pnm = Name_Statement_Assertions
-                        and then Nam_In (Ename, Name_Assert,
-                                                Name_Assert_And_Cut,
-                                                Name_Assume,
-                                                Name_Loop_Invariant,
-                                                Name_Loop_Variant))
+                        and then Ename in Name_Assert
+                                        | Name_Assert_And_Cut
+                                        | Name_Assume
+                                        | Name_Loop_Invariant
+                                        | Name_Loop_Variant)
             then
                Policy := Chars (Get_Pragma_Arg (Last (PPA)));
 
@@ -29504,44 +29601,38 @@ package body Sem_Prag is
       ER   : Boolean;
       EW   : Boolean)
    is
-   begin
-      --  All properties enabled
-
-      if AR and AW and ER and EW then
-         null;
-
-      --  Async_Readers + Effective_Writes
-      --  Async_Readers + Async_Writers + Effective_Writes
-
-      elsif AR and EW and not ER then
-         null;
-
-      --  Async_Writers + Effective_Reads
-      --  Async_Readers + Async_Writers + Effective_Reads
-
-      elsif AW and ER and not EW then
-         null;
-
-      --  Async_Readers + Async_Writers
-
-      elsif AR and AW and not ER and not EW then
-         null;
+      type Properties is array (Positive range 1 .. 4) of Boolean;
+      type Combinations is array (Positive range <>) of Properties;
+      --  Arrays of Async_Readers, Async_Writers, Effective_Writes and
+      --  Effective_Reads properties and their combinations, respectively.
+
+      Specified : constant Properties := (AR, AW, EW, ER);
+      --  External properties, as given by the Item pragma
+
+      Allowed : constant Combinations :=
+        (1 => (True,  False, True,  False),
+         2 => (False, True,  False, True),
+         3 => (True,  False, False, False),
+         4 => (False, True,  False, False),
+         5 => (True,  True,  True,  False),
+         6 => (True,  True,  False, True),
+         7 => (True,  True,  False, False),
+         8 => (True,  True,  True,  True));
+      --  Allowed combinations, as listed in the SPARK RM 7.1.2(6) table
 
-      --  Async_Readers
-
-      elsif AR and not AW and not ER and not EW then
-         null;
-
-      --  Async_Writers
+   begin
+      --  Check if the specified properties match any of the allowed
+      --  combination; if not, then emit an error.
 
-      elsif AW and not AR and not ER and not EW then
-         null;
+      for J in Allowed'Range loop
+         if Specified = Allowed (J) then
+            return;
+         end if;
+      end loop;
 
-      else
-         SPARK_Msg_N
-           ("illegal combination of external properties (SPARK RM 7.1.2(6))",
-            Item);
-      end if;
+      SPARK_Msg_N
+        ("illegal combination of external properties (SPARK RM 7.1.2(6))",
+         Item);
    end Check_External_Properties;
 
    ----------------
@@ -29565,11 +29656,11 @@ package body Sem_Prag is
               or else (Pnm = Name_Assertion
                         and then Is_Valid_Assertion_Kind (Nam))
               or else (Pnm = Name_Statement_Assertions
-                        and then Nam_In (Nam, Name_Assert,
-                                              Name_Assert_And_Cut,
-                                              Name_Assume,
-                                              Name_Loop_Invariant,
-                                              Name_Loop_Variant))
+                        and then Nam in Name_Assert
+                                      | Name_Assert_And_Cut
+                                      | Name_Assume
+                                      | Name_Loop_Invariant
+                                      | Name_Loop_Variant)
             then
                case (Chars (Get_Pragma_Arg (Last (PPA)))) is
                   when Name_Check
@@ -29649,7 +29740,7 @@ package body Sem_Prag is
             --  they depend on variable input. This check is left to the SPARK
             --  prover.
 
-            elsif Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
+            elsif Ekind (Item_Id) in E_Abstract_State | E_Variable then
                return True;
 
             --  Recursively peek into nested packages and instantiations
@@ -29871,7 +29962,7 @@ package body Sem_Prag is
       --  explicit contract.
 
       Prags        : constant Node_Id := Contract (Parent_Subp);
-      In_Spec_Expr : Boolean;
+      In_Spec_Expr : Boolean := In_Spec_Expression;
       Installed    : Boolean;
       Prag         : Node_Id;
       New_Prag     : Node_Id;
@@ -29886,8 +29977,8 @@ package body Sem_Prag is
          Prag := Pre_Post_Conditions (Prags);
 
          while Present (Prag) loop
-            if Nam_In (Pragma_Name_Unmapped (Prag),
-                       Name_Precondition, Name_Postcondition)
+            if Pragma_Name_Unmapped (Prag)
+                 in Name_Precondition | Name_Postcondition
               and then Class_Present (Prag)
             then
                --  The generated pragma must be analyzed in the context of
@@ -30040,11 +30131,11 @@ package body Sem_Prag is
 
          procedure Collect_Global_Item (Item : Node_Id; Mode : Name_Id) is
          begin
-            if Nam_In (Mode, Name_In_Out, Name_Input) then
+            if Mode in Name_In_Out | Name_Input then
                Append_New_Elmt (Item, Subp_Inputs);
             end if;
 
-            if Nam_In (Mode, Name_In_Out, Name_Output) then
+            if Mode in Name_In_Out | Name_Output then
                Append_New_Elmt (Item, Subp_Outputs);
             end if;
          end Collect_Global_Item;
@@ -30062,9 +30153,9 @@ package body Sem_Prag is
 
          --  Single global item declaration
 
-         elsif Nkind_In (List, N_Expanded_Name,
-                               N_Identifier,
-                               N_Selected_Component)
+         elsif Nkind (List) in N_Expanded_Name
+                             | N_Identifier
+                             | N_Selected_Component
          then
             Collect_Global_Item (List, Mode);
 
@@ -30116,13 +30207,13 @@ package body Sem_Prag is
       --  Process all formal parameters of entries, [generic] subprograms, and
       --  their bodies.
 
-      if Ekind_In (Subp_Id, E_Entry,
-                            E_Entry_Family,
-                            E_Function,
-                            E_Generic_Function,
-                            E_Generic_Procedure,
-                            E_Procedure,
-                            E_Subprogram_Body)
+      if Ekind (Subp_Id) in E_Entry
+                          | E_Entry_Family
+                          | E_Function
+                          | E_Generic_Function
+                          | E_Generic_Procedure
+                          | E_Procedure
+                          | E_Subprogram_Body
       then
          Subp_Decl := Unit_Declaration_Node (Subp_Id);
          Spec_Id   := Unique_Defining_Entity (Subp_Decl);
@@ -30131,14 +30222,24 @@ package body Sem_Prag is
 
          Formal := First_Entity (Spec_Id);
          while Present (Formal) loop
-            if Ekind_In (Formal, E_In_Out_Parameter, E_In_Parameter) then
+            if Ekind (Formal) in E_In_Out_Parameter | E_In_Parameter then
+
+               --  IN parameters can act as output when the related type is
+               --  access-to-variable.
+
+               if Ekind (Formal) = E_In_Parameter
+                 and then Is_Access_Variable (Etype (Formal))
+               then
+                  Append_New_Elmt (Formal, Subp_Outputs);
+               end if;
+
                Append_New_Elmt (Formal, Subp_Inputs);
             end if;
 
-            if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
+            if Ekind (Formal) in E_In_Out_Parameter | E_Out_Parameter then
                Append_New_Elmt (Formal, Subp_Outputs);
 
-               --  Out parameters can act as inputs when the related type is
+               --  OUT parameters can act as inputs when the related type is
                --  tagged, unconstrained array, unconstrained record, or record
                --  with unconstrained components.
 
@@ -30155,7 +30256,7 @@ package body Sem_Prag is
       --  Otherwise the input denotes a task type, a task body, or the
       --  anonymous object created for a single task type.
 
-      elsif Ekind_In (Subp_Id, E_Task_Type, E_Task_Body)
+      elsif Ekind (Subp_Id) in E_Task_Type | E_Task_Body
         or else Is_Single_Task_Object (Subp_Id)
       then
          Subp_Decl := Declaration_Node (Subp_Id);
@@ -30167,13 +30268,13 @@ package body Sem_Prag is
       --  outputs.
 
       if Is_Entry_Body (Subp_Id)
-        or else Ekind_In (Subp_Id, E_Subprogram_Body, E_Task_Body)
+        or else Ekind (Subp_Id) in E_Subprogram_Body | E_Task_Body
       then
          Depends := Get_Pragma (Subp_Id, Pragma_Refined_Depends);
          Global  := Get_Pragma (Subp_Id, Pragma_Refined_Global);
 
       --  Subprogram declaration or stand-alone body case, look for pragmas
-      --  Depends and Global
+      --  Depends and Global.
 
       else
          Depends := Get_Pragma (Spec_Id, Pragma_Depends);
@@ -30225,7 +30326,7 @@ package body Sem_Prag is
 
          Append_New_Elmt (Typ, Subp_Inputs);
 
-         if Ekind_In (Spec_Id, E_Entry, E_Entry_Family, E_Procedure) then
+         if Ekind (Spec_Id) in E_Entry | E_Entry_Family | E_Procedure then
             Append_New_Elmt (Typ, Subp_Outputs);
          end if;
 
@@ -30274,8 +30375,8 @@ package body Sem_Prag is
 
    function Delay_Config_Pragma_Analyze (N : Node_Id) return Boolean is
    begin
-      return Nam_In (Pragma_Name_Unmapped (N),
-                     Name_Interrupt_State, Name_Priority_Specific_Dispatching);
+      return Pragma_Name_Unmapped (N)
+        in Name_Interrupt_State | Name_Priority_Specific_Dispatching;
    end Delay_Config_Pragma_Analyze;
 
    -----------------------
@@ -30365,7 +30466,9 @@ package body Sem_Prag is
 
          --  Skip internally generated code
 
-         elsif not Comes_From_Source (Stmt) then
+         elsif not Comes_From_Source (Stmt)
+           and then not Comes_From_Source (Original_Node (Stmt))
+         then
 
             --  The anonymous object created for a single concurrent type is a
             --  suitable context.
@@ -30430,10 +30533,10 @@ package body Sem_Prag is
       Stmt    : Node_Id;
 
       Look_For_Body : constant Boolean :=
-                        Nam_In (Prag_Nam, Name_Refined_Depends,
-                                          Name_Refined_Global,
-                                          Name_Refined_Post,
-                                          Name_Refined_State);
+                        Prag_Nam in Name_Refined_Depends
+                                  | Name_Refined_Global
+                                  | Name_Refined_Post
+                                  | Name_Refined_State;
       --  Refinement pragmas must be associated with a subprogram body [stub]
 
    --  Start of processing for Find_Related_Declaration_Or_Body
@@ -30510,6 +30613,20 @@ package body Sem_Prag is
 
                elsif Present (Generic_Parent (Specification (Stmt))) then
                   return Stmt;
+
+               --  Ada 2020: contract on formal subprogram or on generated
+               --  Access_Subprogram_Wrapper, which appears after the related
+               --  Access_Subprogram declaration.
+
+               elsif Is_Generic_Actual_Subprogram (Defining_Entity (Stmt))
+                 and then Ada_Version >= Ada_2020
+               then
+                  return Stmt;
+
+               elsif Is_Access_Subprogram_Wrapper (Defining_Entity (Stmt))
+                 and then Ada_Version >= Ada_2020
+               then
+                  return Stmt;
                end if;
             end if;
 
@@ -30675,14 +30792,12 @@ package body Sem_Prag is
       Args : constant List_Id := Pragma_Argument_Associations (Prag);
 
    begin
-      --  Use the expression of the original aspect when compiling for ASIS or
-      --  when analyzing the template of a generic unit. In both cases the
-      --  aspect's tree must be decorated to allow for ASIS queries or to save
-      --  the global references in the generic context.
+      --  Use the expression of the original aspect when analyzing the template
+      --  of a generic unit. In both cases the aspect's tree must be decorated
+      --  to save the global references in the generic context.
 
       if From_Aspect_Specification (Prag)
-        and then (ASIS_Mode or else (Present (Context_Id)
-                                      and then Is_Generic_Unit (Context_Id)))
+        and then (Present (Context_Id) and then Is_Generic_Unit (Context_Id))
       then
          return Corresponding_Aspect (Prag);
 
@@ -30970,10 +31085,6 @@ package body Sem_Prag is
    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,
@@ -31009,6 +31120,8 @@ package body Sem_Prag is
       Pragma_C_Pass_By_Copy                 =>  0,
       Pragma_Comment                        => -1,
       Pragma_Common_Object                  =>  0,
+      Pragma_CUDA_Execute                   => -1,
+      Pragma_CUDA_Global                    => -1,
       Pragma_Compile_Time_Error             => -1,
       Pragma_Compile_Time_Warning           => -1,
       Pragma_Compiler_Unit                  => -1,
@@ -31024,11 +31137,11 @@ package body Sem_Prag is
       Pragma_Deadline_Floor                 => -1,
       Pragma_Debug                          => -1,
       Pragma_Debug_Policy                   =>  0,
-      Pragma_Detect_Blocking                =>  0,
       Pragma_Default_Initial_Condition      => -1,
       Pragma_Default_Scalar_Storage_Order   =>  0,
       Pragma_Default_Storage_Pool           =>  0,
       Pragma_Depends                        => -1,
+      Pragma_Detect_Blocking                =>  0,
       Pragma_Disable_Atomic_Synchronization =>  0,
       Pragma_Discard_Names                  =>  0,
       Pragma_Dispatching_Domain             => -1,
@@ -31050,9 +31163,9 @@ package body Sem_Prag is
       Pragma_Extensions_Allowed             =>  0,
       Pragma_Extensions_Visible             =>  0,
       Pragma_External                       => -1,
-      Pragma_Favor_Top_Level                =>  0,
       Pragma_External_Name_Casing           =>  0,
       Pragma_Fast_Math                      =>  0,
+      Pragma_Favor_Top_Level                =>  0,
       Pragma_Finalize_Storage_Only          =>  0,
       Pragma_Ghost                          =>  0,
       Pragma_Global                         => -1,
@@ -31116,17 +31229,15 @@ package body Sem_Prag is
       Pragma_Obsolescent                    =>  0,
       Pragma_Optimize                       =>  0,
       Pragma_Optimize_Alignment             =>  0,
+      Pragma_Ordered                        =>  0,
       Pragma_Overflow_Mode                  =>  0,
       Pragma_Overriding_Renamings           =>  0,
-      Pragma_Ordered                        =>  0,
       Pragma_Pack                           =>  0,
       Pragma_Page                           =>  0,
       Pragma_Part_Of                        =>  0,
       Pragma_Partition_Elaboration_Policy   =>  0,
       Pragma_Passive                        =>  0,
       Pragma_Persistent_BSS                 =>  0,
-      Pragma_Polling                        =>  0,
-      Pragma_Prefix_Exception_Messages      =>  0,
       Pragma_Post                           => -1,
       Pragma_Postcondition                  => -1,
       Pragma_Post_Class                     => -1,
@@ -31136,6 +31247,7 @@ package body Sem_Prag is
       Pragma_Predicate_Failure              => -1,
       Pragma_Preelaborable_Initialization   => -1,
       Pragma_Preelaborate                   =>  0,
+      Pragma_Prefix_Exception_Messages      =>  0,
       Pragma_Pre_Class                      => -1,
       Pragma_Priority                       => -1,
       Pragma_Priority_Specific_Dispatching  =>  0,
@@ -31154,35 +31266,36 @@ package body Sem_Prag is
       Pragma_Refined_Post                   => -1,
       Pragma_Refined_State                  => -1,
       Pragma_Relative_Deadline              =>  0,
-      Pragma_Rename_Pragma                  =>  0,
       Pragma_Remote_Access_Type             => -1,
       Pragma_Remote_Call_Interface          => -1,
       Pragma_Remote_Types                   => -1,
+      Pragma_Rename_Pragma                  =>  0,
       Pragma_Restricted_Run_Time            =>  0,
       Pragma_Restriction_Warnings           =>  0,
       Pragma_Restrictions                   =>  0,
       Pragma_Reviewable                     => -1,
       Pragma_Secondary_Stack_Size           => -1,
-      Pragma_Short_Circuit_And_Or           =>  0,
       Pragma_Share_Generic                  =>  0,
       Pragma_Shared                         =>  0,
       Pragma_Shared_Passive                 =>  0,
+      Pragma_Short_Circuit_And_Or           =>  0,
       Pragma_Short_Descriptors              =>  0,
       Pragma_Simple_Storage_Pool_Type       =>  0,
       Pragma_Source_File_Name               =>  0,
       Pragma_Source_File_Name_Project       =>  0,
       Pragma_Source_Reference               =>  0,
       Pragma_SPARK_Mode                     =>  0,
+      Pragma_Static_Elaboration_Desired     =>  0,
       Pragma_Storage_Size                   => -1,
       Pragma_Storage_Unit                   =>  0,
-      Pragma_Static_Elaboration_Desired     =>  0,
       Pragma_Stream_Convert                 =>  0,
       Pragma_Style_Checks                   =>  0,
+      Pragma_Subprogram_Variant             => -1,
       Pragma_Subtitle                       =>  0,
       Pragma_Suppress                       =>  0,
-      Pragma_Suppress_Exception_Locations   =>  0,
       Pragma_Suppress_All                   =>  0,
       Pragma_Suppress_Debug_Info            =>  0,
+      Pragma_Suppress_Exception_Locations   =>  0,
       Pragma_Suppress_Initialization        =>  0,
       Pragma_System_Name                    =>  0,
       Pragma_Task_Dispatching_Policy        =>  0,
@@ -31441,7 +31554,6 @@ package body Sem_Prag is
             --  RM defined
 
               Name_Assert
-            | Name_Assertion_Policy
             | Name_Static_Predicate
             | Name_Dynamic_Predicate
             | Name_Pre
@@ -31469,6 +31581,7 @@ package body Sem_Prag is
             | Name_Predicate
             | Name_Refined_Post
             | Name_Statement_Assertions
+            | Name_Subprogram_Variant
          =>
             return True;
 
@@ -31516,6 +31629,9 @@ package body Sem_Prag is
       Arg1x : constant Node_Id := Get_Pragma_Arg (Arg1);
       Arg2  : constant Node_Id := Next (Arg1);
 
+      Pname   : constant Name_Id   := Pragma_Name_Unmapped (N);
+      Prag_Id : constant Pragma_Id := Get_Pragma_Id (Pname);
+
    begin
       Analyze_And_Resolve (Arg1x, Standard_Boolean);
 
@@ -31529,8 +31645,6 @@ package body Sem_Prag is
 
             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 (Expr_Value_S (Get_Pragma_Arg (Arg2)));
                Str_Len : constant Nat       := String_Length (Str);
@@ -31590,10 +31704,12 @@ package body Sem_Prag is
 
                   if Force then
                      if Cont = False then
-                        Error_Msg ("<<~!!", Eloc);
+                        Error_Msg
+                           ("<<~!!", Eloc, Is_Compile_Time_Pragma => True);
                         Cont := True;
                      else
-                        Error_Msg ("\<<~!!", Eloc);
+                        Error_Msg
+                           ("\<<~!!", Eloc, Is_Compile_Time_Pragma => True);
                      end if;
 
                   --  Error, rather than warning, or in a body, so we do not
@@ -31604,10 +31720,12 @@ package body Sem_Prag is
 
                   else
                      if Cont = False then
-                        Error_Msg ("<<~", Eloc);
+                        Error_Msg
+                           ("<<~", Eloc, Is_Compile_Time_Pragma => True);
                         Cont := True;
                      else
-                        Error_Msg ("\<<~", Eloc);
+                        Error_Msg
+                           ("\<<~", Eloc, Is_Compile_Time_Pragma => True);
                      end if;
                   end if;
 
@@ -31616,13 +31734,17 @@ package body Sem_Prag is
             end;
          end if;
 
-      --  Arg1x is not known at compile time, so issue a warning. This can
-      --  happen only if the pragma's processing was deferred until after the
-      --  back end is run (see Process_Compile_Time_Warning_Or_Error).
-      --  Note that the warning control switch applies to both pragmas.
+      --  Arg1x is not known at compile time, so possibly issue an error
+      --  or warning. This can happen only if the pragma's processing
+      --  was deferred until after the back end is run (see
+      --  Process_Compile_Time_Warning_Or_Error). Note that the warning
+      --  control switch applies to only the warning case.
+
+      elsif Prag_Id = Pragma_Compile_Time_Error then
+         Error_Msg_N ("condition is not known at compile time", Arg1x);
 
       elsif Warn_On_Unknown_Compile_Time_Warning then
-         Error_Msg_N ("?condition is not known at compile time", Arg1x);
+         Error_Msg_N ("??condition is not known at compile time", Arg1x);
       end if;
    end Validate_Compile_Time_Warning_Or_Error;
 
@@ -31927,7 +32049,6 @@ package body Sem_Prag is
       elsif Nkind (N) = N_Identifier
         and then From_Policy
         and then Serious_Errors_Detected = 0
-        and then not ASIS_Mode
       then
          if Chars (N) = Name_Precondition
            or else Chars (N) = Name_Postcondition
@@ -32090,6 +32211,64 @@ package body Sem_Prag is
       Generate_Reference (Entity (With_Item), N, Set_Ref => False);
    end Set_Elab_Unit_Name;
 
+   -----------------------
+   -- Set_Overflow_Mode --
+   -----------------------
+
+   procedure Set_Overflow_Mode (N : Node_Id) is
+
+      function Get_Overflow_Mode (Arg : Node_Id) return Overflow_Mode_Type;
+      --  Function to process one pragma argument, Arg
+
+      -----------------------
+      -- Get_Overflow_Mode --
+      -----------------------
+
+      function Get_Overflow_Mode (Arg : Node_Id) return Overflow_Mode_Type is
+         Argx : constant Node_Id := Get_Pragma_Arg (Arg);
+
+      begin
+         if Chars (Argx) = Name_Strict then
+            return Strict;
+
+         elsif Chars (Argx) = Name_Minimized then
+            return Minimized;
+
+         elsif Chars (Argx) = Name_Eliminated then
+            return Eliminated;
+
+         else
+            raise Program_Error;
+         end if;
+      end Get_Overflow_Mode;
+
+      --  Local variables
+
+      Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N));
+      Arg2 : constant Node_Id := Next (Arg1);
+
+   --  Start of processing for Set_Overflow_Mode
+
+   begin
+      --  Process first argument
+
+      Scope_Suppress.Overflow_Mode_General :=
+        Get_Overflow_Mode (Arg1);
+
+      --  Case of only one argument
+
+      if No (Arg2) then
+         Scope_Suppress.Overflow_Mode_Assertions :=
+           Scope_Suppress.Overflow_Mode_General;
+
+      --  Case of two arguments present
+
+      else
+         Scope_Suppress.Overflow_Mode_Assertions  :=
+           Get_Overflow_Mode (Arg2);
+      end if;
+   end Set_Overflow_Mode;
+
    -------------------
    -- Test_Case_Arg --
    -------------------
@@ -32104,10 +32283,8 @@ package body Sem_Prag is
       Args   : Node_Id;
 
    begin
-      pragma Assert (Nam_In (Arg_Nam, Name_Ensures,
-                                      Name_Mode,
-                                      Name_Name,
-                                      Name_Requires));
+      pragma Assert
+        (Arg_Nam in Name_Ensures | Name_Mode | Name_Name | Name_Requires);
 
       --  The caller requests the aspect argument
 
@@ -32186,9 +32363,9 @@ package body Sem_Prag is
       return Empty;
    end Test_Case_Arg;
 
-   -----------------------------------------
+   --------------------------------------------
    -- Defer_Compile_Time_Warning_Error_To_BE --
-   -----------------------------------------
+   --------------------------------------------
 
    procedure Defer_Compile_Time_Warning_Error_To_BE (N : Node_Id) is
       Arg1  : constant Node_Id := First (Pragma_Argument_Associations (N));