diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb
index 852f0c2a1f9..c14769c640c 100644
--- a/gcc/ada/aspects.adb
+++ b/gcc/ada/aspects.adb
@@ -41,20 +41,20 @@ package body Aspects is
    --  type. False means it is not inherited.
 
    Base_Aspect : constant array (Aspect_Id) of Boolean :=
-     (Aspect_Atomic                  => True,
-      Aspect_Atomic_Components       => True,
-      Aspect_Constant_Indexing       => True,
-      Aspect_Default_Iterator        => True,
-      Aspect_Discard_Names           => True,
-      Aspect_Independent_Components  => True,
-      Aspect_Iterator_Element        => True,
-      Aspect_Stable_Properties       => True,
-      Aspect_Type_Invariant          => True,
-      Aspect_Unchecked_Union         => True,
-      Aspect_Variable_Indexing       => True,
-      Aspect_Volatile                => True,
-      Aspect_Volatile_Full_Access    => True,
-      others                         => False);
+     (Aspect_Atomic                 => True,
+      Aspect_Atomic_Components      => True,
+      Aspect_Constant_Indexing      => True,
+      Aspect_Default_Iterator       => True,
+      Aspect_Discard_Names          => True,
+      Aspect_Independent_Components => True,
+      Aspect_Iterator_Element       => True,
+      Aspect_Stable_Properties      => True,
+      Aspect_Type_Invariant         => True,
+      Aspect_Unchecked_Union        => True,
+      Aspect_Variable_Indexing      => True,
+      Aspect_Volatile               => True,
+      Aspect_Volatile_Full_Access   => True,
+      others                        => False);
 
    --  The following array indicates type aspects that are inherited and apply
    --  to the class-wide type as well.
diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads
index 19f7c07130f..05677978037 100644
--- a/gcc/ada/aspects.ads
+++ b/gcc/ada/aspects.ads
@@ -372,7 +372,7 @@ package Aspects is
       Aspect_Address                    => Expression,
       Aspect_Aggregate                  => Expression,
       Aspect_Alignment                  => Expression,
-      Aspect_Always_Terminates          => Expression,
+      Aspect_Always_Terminates          => Optional_Expression,
       Aspect_Annotate                   => Expression,
       Aspect_Async_Readers              => Optional_Expression,
       Aspect_Async_Writers              => Optional_Expression,
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index bca4eb50430..1fa946439ee 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -430,7 +430,8 @@ package body Sem_Prag is
    is
       Subp_Decl : constant Node_Id   := Find_Related_Declaration_Or_Body (N);
       Spec_Id   : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
-      Expr      : constant Node_Id   := Expression (Get_Argument (N, Spec_Id));
+      Arg1      : constant Node_Id   :=
+        First (Pragma_Argument_Associations (N));
 
       Saved_GM  : constant Ghost_Mode_Type := Ghost_Mode;
       Saved_IGR : constant Node_Id         := Ignored_Ghost_Region;
@@ -446,51 +447,52 @@ package body Sem_Prag is
          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.
+      if Present (Arg1) then
 
-      Set_Ghost_Mode (N);
+         --  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.
 
-      --  Ensure that the subprogram and its formals are visible when analyzing
-      --  the expression of the pragma.
+         Set_Ghost_Mode (N);
 
-      if not In_Open_Scopes (Spec_Id) then
-         Restore_Scope := True;
+         --  Ensure that the subprogram and its formals are visible when
+         --  analyzing the expression of the pragma.
 
-         if Is_Generic_Subprogram (Spec_Id) then
-            Push_Scope (Spec_Id);
-            Install_Generic_Formals (Spec_Id);
-         else
-            Push_Scope (Spec_Id);
-            Install_Formals (Spec_Id);
+         if not In_Open_Scopes (Spec_Id) then
+            Restore_Scope := True;
+
+            if Is_Generic_Subprogram (Spec_Id) then
+               Push_Scope (Spec_Id);
+               Install_Generic_Formals (Spec_Id);
+            else
+               Push_Scope (Spec_Id);
+               Install_Formals (Spec_Id);
+            end if;
          end if;
-      end if;
 
-      Errors := Serious_Errors_Detected;
-      Preanalyze_Assert_Expression (Expr, Standard_Boolean);
+         Errors := Serious_Errors_Detected;
+         Preanalyze_Assert_Expression (Expression (Arg1), Standard_Boolean);
 
-      --  Emit a clarification message when the expression contains at least
-      --  one undefined reference, possibly due to contract freezing.
+         --  Emit a clarification message when the 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;
+         if Errors /= Serious_Errors_Detected
+           and then Present (Freeze_Id)
+           and then Has_Undefined_Reference (Expression (Arg1))
+         then
+            Contract_Freeze_Error (Spec_Id, Freeze_Id);
+         end if;
 
-      if Restore_Scope then
-         End_Scope;
-      end if;
+         if Restore_Scope then
+            End_Scope;
+         end if;
 
-      --  Currently it is not possible to inline pre/postconditions on a
-      --  subprogram subject to pragma Inline_Always.
+         Restore_Ghost_Region (Saved_GM, Saved_IGR);
+      end if;
 
       Set_Is_Analyzed_Pragma (N);
 
-      Restore_Ghost_Region (Saved_GM, Saved_IGR);
    end Analyze_Always_Terminates_In_Decl_Part;
 
    -----------------------------------------
@@ -13279,7 +13281,7 @@ package body Sem_Prag is
          -- Always_Terminates --
          -----------------------
 
-         --  pragma Always_Terminates (boolean_EXPRESSION);
+         --  pragma Always_Terminates [ (boolean_EXPRESSION) ];
 
          --  Characteristics:
 
@@ -13321,7 +13323,7 @@ package body Sem_Prag is
          begin
             GNAT_Pragma;
             Check_No_Identifiers;
-            Check_Arg_Count (1);
+            Check_At_Most_N_Arguments (1);
 
             --  Ensure the proper placement of the pragma. Exceptional_Cases
             --  must be associated with a subprogram declaration or a body that
@@ -14011,7 +14013,7 @@ package body Sem_Prag is
          begin
             GNAT_Pragma;
             Check_No_Identifiers;
-            Check_At_Most_N_Arguments  (1);
+            Check_At_Most_N_Arguments (1);
 
             Obj_Or_Type_Decl := Find_Related_Context (N, Do_Checks => True);
 
