diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads
index bd8e7c61a83..19f7c07130f 100644
--- a/gcc/ada/aspects.ads
+++ b/gcc/ada/aspects.ads
@@ -72,6 +72,7 @@ package Aspects is
       Aspect_Address,
       Aspect_Aggregate,
       Aspect_Alignment,
+      Aspect_Always_Terminates,             -- GNAT
       Aspect_Annotate,                      -- GNAT
       Aspect_Async_Readers,                 -- GNAT
       Aspect_Async_Writers,                 -- GNAT
@@ -261,6 +262,7 @@ package Aspects is
 
    Implementation_Defined_Aspect : constant array (Aspect_Id) of Boolean :=
      (Aspect_Abstract_State             => True,
+      Aspect_Always_Terminates          => True,
       Aspect_Annotate                   => True,
       Aspect_Async_Readers              => True,
       Aspect_Async_Writers              => True,
@@ -370,6 +372,7 @@ package Aspects is
       Aspect_Address                    => Expression,
       Aspect_Aggregate                  => Expression,
       Aspect_Alignment                  => Expression,
+      Aspect_Always_Terminates          => Expression,
       Aspect_Annotate                   => Expression,
       Aspect_Async_Readers              => Optional_Expression,
       Aspect_Async_Writers              => Optional_Expression,
@@ -477,6 +480,7 @@ package Aspects is
       Aspect_Address                      => True,
       Aspect_Aggregate                    => False,
       Aspect_Alignment                    => True,
+      Aspect_Always_Terminates            => False,
       Aspect_Annotate                     => False,
       Aspect_Async_Readers                => False,
       Aspect_Async_Writers                => False,
@@ -630,6 +634,7 @@ package Aspects is
       Aspect_Aggregate                    => Name_Aggregate,
       Aspect_Alignment                    => Name_Alignment,
       Aspect_All_Calls_Remote             => Name_All_Calls_Remote,
+      Aspect_Always_Terminates            => Name_Always_Terminates,
       Aspect_Annotate                     => Name_Annotate,
       Aspect_Async_Readers                => Name_Async_Readers,
       Aspect_Async_Writers                => Name_Async_Writers,
@@ -980,6 +985,7 @@ package Aspects is
       Aspect_Write                        => Always_Delay,
 
       Aspect_Abstract_State               => Never_Delay,
+      Aspect_Always_Terminates            => Never_Delay,
       Aspect_Annotate                     => Never_Delay,
       Aspect_Async_Readers                => Never_Delay,
       Aspect_Async_Writers                => Never_Delay,
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 19073d1e4d8..0e87cee3ef5 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -109,9 +109,9 @@ package body Contracts is
    procedure Expand_Subprogram_Contract (Body_Id : Entity_Id);
    --  Expand the contracts of a subprogram body and its correspoding spec (if
    --  any). This routine processes all [refined] pre- and postconditions as
-   --  well as Contract_Cases, Exceptional_Cases, Subprogram_Variant,
-   --  invariants and predicates. Body_Id denotes the entity of the
-   --  subprogram body.
+   --  well as Always_Terminates, Contract_Cases, Exceptional_Cases,
+   --  Subprogram_Variant, invariants and predicates. Body_Id denotes the
+   --  entity of the subprogram body.
 
    procedure Preanalyze_Condition
      (Subp : Entity_Id;
@@ -225,6 +225,7 @@ package body Contracts is
          end if;
 
       --  Entry or subprogram declarations, the applicable pragmas are:
+      --    Always_Terminates
       --    Attach_Handler
       --    Contract_Cases
       --    Depends
@@ -260,7 +261,8 @@ package body Contracts is
          then
             Add_Classification;
 
-         elsif Prag_Nam in Name_Contract_Cases
+         elsif Prag_Nam in Name_Always_Terminates
+                         | Name_Contract_Cases
                          | Name_Exceptional_Cases
                          | Name_Subprogram_Variant
                          | Name_Test_Case
@@ -663,10 +665,10 @@ package body Contracts is
             Gen_Id => Spec_Id);
       end if;
 
-      --  Deal with preconditions, [refined] postconditions, Contract_Cases,
-      --  Exceptional_Cases, Subprogram_Variant, invariants and predicates
-      --  associated with body and its spec. Do not expand the contract of
-      --  subprogram body stubs.
+      --  Deal with preconditions, [refined] postconditions, Always_Terminates,
+      --  Contract_Cases, Exceptional_Cases, Subprogram_Variant, invariants and
+      --  predicates associated with body and its spec. Do not expand the
+      --  contract of subprogram body stubs.
 
       if Nkind (Body_Decl) = N_Subprogram_Body then
          Expand_Subprogram_Contract (Body_Id);
@@ -789,7 +791,10 @@ package body Contracts is
          while Present (Prag) loop
             Prag_Nam := Pragma_Name (Prag);
 
-            if Prag_Nam = Name_Contract_Cases then
+            if Prag_Nam = Name_Always_Terminates then
+               Analyze_Always_Terminates_In_Decl_Part (Prag);
+
+            elsif Prag_Nam = Name_Contract_Cases then
 
                --  Do not analyze the contract cases of an entry declaration
                --  unless annotating the original tree for GNATprove.
@@ -1533,6 +1538,7 @@ package body Contracts is
          Analyze_Entry_Or_Subprogram_Body_Contract (Stub_Id);
 
       --  The stub acts as its own spec, the applicable pragmas are:
+      --    Always_Terminates
       --    Contract_Cases
       --    Depends
       --    Exceptional_Cases
@@ -2879,7 +2885,10 @@ package body Contracts is
                Prag := Contract_Test_Cases (Items);
                while Present (Prag) loop
                   if Is_Checked (Prag) then
-                     if Pragma_Name (Prag) = Name_Contract_Cases then
+                     if Pragma_Name (Prag) = Name_Always_Terminates then
+                        Expand_Pragma_Always_Terminates (Prag);
+
+                     elsif Pragma_Name (Prag) = Name_Contract_Cases then
                         Expand_Pragma_Contract_Cases
                           (CCs     => Prag,
                            Subp_Id => Subp_Id,
diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads
index d52e1aaed4a..c3dc5d67734 100644
--- a/gcc/ada/contracts.ads
+++ b/gcc/ada/contracts.ads
@@ -37,6 +37,7 @@ package Contracts is
    --  The following are valid pragmas:
    --
    --    Abstract_State
+   --    Always_Terminates
    --    Async_Readers
    --    Async_Writers
    --    Attach_Handler
@@ -81,6 +82,7 @@ package Contracts is
    --  subprogram body Body_Id as if they appeared at the end of a declarative
    --  region. Pragmas in question are:
    --
+   --    Always_Terminates  (stand alone subprogram body)
    --    Contract_Cases     (stand alone subprogram body)
    --    Depends            (stand alone subprogram body)
    --    Exceptional_Cases  (stand alone subprogram body)
@@ -100,6 +102,7 @@ package Contracts is
    --  subprogram Subp_Id as if they appeared at the end of a declarative
    --  region. The pragmas in question are:
    --
+   --    Always_Terminates
    --    Contract_Cases
    --    Depends
    --    Exceptional_Cases
@@ -175,6 +178,7 @@ package Contracts is
    --  stub Stub_Id as if they appeared at the end of a declarative region. The
    --  pragmas in question are:
    --
+   --    Always_Terminates
    --    Contract_Cases
    --    Depends
    --    Exceptional_Cases
diff --git a/gcc/ada/einfo-utils.adb b/gcc/ada/einfo-utils.adb
index d1db66ff697..dad3a654743 100644
--- a/gcc/ada/einfo-utils.adb
+++ b/gcc/ada/einfo-utils.adb
@@ -1017,6 +1017,7 @@ package body Einfo.Utils is
       --  Contract / subprogram variant / test case pragmas
 
       Is_CTC : constant Boolean :=
+                  Id = Pragma_Always_Terminates         or else
                   Id = Pragma_Contract_Cases            or else
                   Id = Pragma_Exceptional_Cases         or else
                   Id = Pragma_Subprogram_Variant        or else
diff --git a/gcc/ada/einfo-utils.ads b/gcc/ada/einfo-utils.ads
index e8055020a67..fee771c20f4 100644
--- a/gcc/ada/einfo-utils.ads
+++ b/gcc/ada/einfo-utils.ads
@@ -439,6 +439,7 @@ package Einfo.Utils is
    --  node, otherwise Empty is returned. The following contract pragmas that
    --  appear in N_Contract nodes are also handled by this routine:
    --    Abstract_State
+   --    Always_Terminates
    --    Async_Readers
    --    Async_Writers
    --    Attach_Handler
diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index e660196c0f1..1cc4653a3b0 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -269,6 +269,16 @@ package body Exp_Prag is
       end;
    end Expand_Pragma_Abort_Defer;
 
+   -------------------------------------
+   -- Expand_Pragma_Always_Terminates --
+   -------------------------------------
+
+   procedure Expand_Pragma_Always_Terminates (Prag : Node_Id) is
+      pragma Unreferenced (Prag);
+   begin
+      null;
+   end Expand_Pragma_Always_Terminates;
+
    --------------------------
    -- Expand_Pragma_Check --
    --------------------------
diff --git a/gcc/ada/exp_prag.ads b/gcc/ada/exp_prag.ads
index 9f810dab227..10ccaf70c67 100644
--- a/gcc/ada/exp_prag.ads
+++ b/gcc/ada/exp_prag.ads
@@ -31,6 +31,10 @@ package Exp_Prag is
 
    procedure Expand_N_Pragma (N : Node_Id);
 
+   procedure Expand_Pragma_Always_Terminates (Prag : Node_Id);
+   --  This routine only exists for consistency with other pragmas, since
+   --  Always_Terminates has no meaningful expansion.
+
    procedure Expand_Pragma_Contract_Cases
      (CCs     : Node_Id;
       Subp_Id : Entity_Id;
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index a4c32e984da..edb90a9fe20 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -312,6 +312,7 @@ package body Inline is
    --  Remove all aspects and/or pragmas that have no meaning in inlined body
    --  Body_Decl. The analysis of these items is performed on the non-inlined
    --  body. The items currently removed are:
+   --    Always_Terminates
    --    Contract_Cases
    --    Global
    --    Depends
@@ -5225,7 +5226,8 @@ package body Inline is
             end if;
 
             if Present (Item_Id)
-              and then Chars (Item_Id) in Name_Contract_Cases
+              and then Chars (Item_Id) in Name_Always_Terminates
+                                        | Name_Contract_Cases
                                         | Name_Global
                                         | Name_Depends
                                         | Name_Exceptional_Cases
diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb
index ac50c846bf9..b1398625fe2 100644
--- a/gcc/ada/par-prag.adb
+++ b/gcc/ada/par-prag.adb
@@ -1315,6 +1315,7 @@ begin
          | Pragma_Aggregate_Individually_Assign
          | Pragma_All_Calls_Remote
          | Pragma_Allow_Integer_Address
+         | Pragma_Always_Terminates
          | Pragma_Annotate
          | Pragma_Assert
          | Pragma_Assert_And_Cut
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index a38ab284ce7..f584a9f3fb5 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -261,9 +261,10 @@ package body Sem_Ch12 is
    --  as annotations:
 
    --     package                  subprogram [body]
-   --       Abstract_State           Contract_Cases
-   --       Initial_Condition        Depends
-   --       Initializes              Exceptional_Cases
+   --       Abstract_State           Always_Terminates
+   --       Initial_Condition        Contract_Cases
+   --       Initializes              Depends
+   --                                Exceptional_Cases
    --                                Extensions_Visible
    --                                Global
    --     package body               Post
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 2b8b64aa392..e771c0d2020 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -1407,6 +1407,7 @@ package body Sem_Ch13 is
          Is_Instance : Boolean := False);
       --  Subsidiary to the analysis of aspects
       --    Abstract_State
+      --    Always_Terminates
       --    Attach_Handler
       --    Contract_Cases
       --    Depends
@@ -1667,10 +1668,11 @@ package body Sem_Ch13 is
       --  analyzed right now.
 
       --  Note that there is a special handling for Pre, Post, Test_Case,
-      --  Contract_Cases, Exceptional_Cases and Subprogram_Variant aspects.
-      --  In these cases, we do not have to worry about delay issues, since the
-      --  pragmas themselves deal with delay of visibility for the expression
-      --  analysis. Thus, we just insert the pragma after the node N.
+      --  Contract_Cases, Always_Terminates, Exceptional_Cases and
+      --  Subprogram_Variant aspects. In these cases, we do not have to worry
+      --  about delay issues, since the pragmas themselves deal with delay of
+      --  visibility for the expression analysis. Thus, we just insert the
+      --  pragma after the node N.
 
       --  Loop through aspects
 
@@ -4297,9 +4299,9 @@ package body Sem_Ch13 is
 
                --  Case 4: Aspects requiring special handling
 
-               --  Pre/Post/Test_Case/Contract_Cases/Exceptional_Cases and
-               --  Subprogram_Variant whose corresponding pragmas take care
-               --  of the delay.
+               --  Pre/Post/Test_Case/Contract_Cases/Always_Terminates/
+               --  Exceptional_Cases and Subprogram_Variant whose corresponding
+               --  pragmas take care of the delay.
 
                --  Pre/Post
 
@@ -4531,6 +4533,19 @@ package body Sem_Ch13 is
                   Insert_Pragma (Aitem);
                   goto Continue;
 
+               --  Always_Terminates
+
+               when Aspect_Always_Terminates =>
+                  Aitem := Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_Always_Terminates);
+
+                  Decorate (Aspect, Aitem);
+                  Insert_Pragma (Aitem);
+                  goto Continue;
+
                --  Exceptional_Cases
 
                when Aspect_Exceptional_Cases =>
@@ -11315,6 +11330,7 @@ package body Sem_Ch13 is
          --  Here is the list of aspects that don't require delay analysis
 
          when Aspect_Abstract_State
+            | Aspect_Always_Terminates
             | Aspect_Annotate
             | Aspect_Async_Readers
             | Aspect_Async_Writers
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index abc0e5dbb9d..bca4eb50430 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -420,6 +420,79 @@ package body Sem_Prag is
       end if;
    end Adjust_External_Name_Case;
 
+   --------------------------------------------
+   -- Analyze_Always_Terminates_In_Decl_Part --
+   --------------------------------------------
+
+   procedure Analyze_Always_Terminates_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);
+      Expr      : constant Node_Id   := Expression (Get_Argument (N, Spec_Id));
+
+      Saved_GM  : constant Ghost_Mode_Type := Ghost_Mode;
+      Saved_IGR : constant Node_Id         := Ignored_Ghost_Region;
+      --  Save the Ghost-related attributes to restore on exit
+
+      Errors        : Nat;
+      Restore_Scope : Boolean := False;
+
+   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);
+
+      --  Ensure that the subprogram and its formals are visible when analyzing
+      --  the expression of the pragma.
+
+      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;
+
+      Errors := Serious_Errors_Detected;
+      Preanalyze_Assert_Expression (Expr, Standard_Boolean);
+
+      --  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 Restore_Scope then
+         End_Scope;
+      end if;
+
+      --  Currently it is not possible to inline pre/postconditions on a
+      --  subprogram subject to pragma Inline_Always.
+
+      Set_Is_Analyzed_Pragma (N);
+
+      Restore_Ghost_Region (Saved_GM, Saved_IGR);
+   end Analyze_Always_Terminates_In_Decl_Part;
+
    -----------------------------------------
    -- Analyze_Contract_Cases_In_Decl_Part --
    -----------------------------------------
@@ -13202,6 +13275,131 @@ package body Sem_Prag is
                Opt.Allow_Integer_Address := True;
             end if;
 
+         -----------------------
+         -- Always_Terminates --
+         -----------------------
+
+         --  pragma Always_Terminates (boolean_EXPRESSION);
+
+         --  Characteristics:
+
+         --    * Analysis - The annotation undergoes initial checks to verify
+         --    the legal placement and context. Secondary checks preanalyze the
+         --    expressions in:
+
+         --       Analyze_Always_Terminates_Cases_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_Always_Terminates => Always_Terminates : 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. Exceptional_Cases
+            --  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 Always_Terminates 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 procedures always
+               --  terminate anyway.
+
+               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;
+            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);
+
+            --  Chain the pragma on the contract for further processing by
+            --  Analyze_Always_Terminates_In_Decl_Part.
+
+            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 Always_Terminates 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_Always_Terminates_In_Decl_Part (N);
+            end if;
+         end Always_Terminates;
+
          --------------
          -- Annotate --
          --------------
@@ -31990,6 +32188,7 @@ package body Sem_Prag is
       Pragma_Aggregate_Individually_Assign  => 0,
       Pragma_All_Calls_Remote               => -1,
       Pragma_Allow_Integer_Address          => -1,
+      Pragma_Always_Terminates              => -1,
       Pragma_Annotate                       => 93,
       Pragma_Assert                         => -1,
       Pragma_Assert_And_Cut                 => -1,
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index 49c1d0b4892..e8e9856d8a3 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -38,6 +38,7 @@ package Sem_Prag is
    Aspect_Specifying_Pragma : constant array (Pragma_Id) of Boolean :=
      (Pragma_Abstract_State               => True,
       Pragma_All_Calls_Remote             => True,
+      Pragma_Always_Terminates            => True,
       Pragma_Annotate                     => True,
       Pragma_Async_Readers                => True,
       Pragma_Async_Writers                => True,
@@ -133,7 +134,8 @@ package Sem_Prag is
    --  expression.
 
    Assertion_Expression_Pragma : constant array (Pragma_Id) of Boolean :=
-     (Pragma_Assert                    => True,
+     (Pragma_Always_Terminates         => True,
+      Pragma_Assert                    => True,
       Pragma_Assert_And_Cut            => True,
       Pragma_Assume                    => True,
       Pragma_Check                     => True,
@@ -210,7 +212,8 @@ package Sem_Prag is
    --  of subprogram bodies.
 
    Pragma_Significant_To_Subprograms : constant array (Pragma_Id) of Boolean :=
-     (Pragma_Contract_Cases     => True,
+     (Pragma_Always_Terminates  => True,
+      Pragma_Contract_Cases     => True,
       Pragma_Depends            => True,
       Pragma_Exceptional_Cases  => True,
       Pragma_Ghost              => True,
@@ -241,6 +244,13 @@ package Sem_Prag is
    procedure Analyze_Pragma (N : Node_Id);
    --  Analyze procedure for pragma reference node N
 
+   procedure Analyze_Always_Terminates_In_Decl_Part
+     (N         : Node_Id;
+      Freeze_Id : Entity_Id := Empty);
+   --  Perform full analysis of delayed pragma Always_Terminates. Freeze_Id is
+   --  the entity of [generic] package body or [generic] subprogram body which
+   --  caused "freezing" of the related contract where the pragma resides.
+
    procedure Analyze_Contract_Cases_In_Decl_Part
      (N         : Node_Id;
       Freeze_Id : Entity_Id := Empty);
@@ -445,6 +455,7 @@ package Sem_Prag is
      (Prag      : Node_Id;
       Do_Checks : Boolean := False) return Node_Id;
    --  Subsidiary to the analysis of pragmas
+   --    Always_Terminates
    --    Contract_Cases
    --    Depends
    --    Exceptional_Cases
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index c736bc34bb1..b82978ba99e 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -20558,7 +20558,8 @@ package body Sem_Util is
          Nam := Pragma_Name (Item);
       end if;
 
-      return    Nam = Name_Contract_Cases
+      return    Nam = Name_Always_Terminates
+        or else Nam = Name_Contract_Cases
         or else Nam = Name_Depends
         or else Nam = Name_Exceptional_Cases
         or else Nam = Name_Extensions_Visible
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 539ebebafcb..3751fb73702 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -2349,6 +2349,7 @@ package Sem_Util is
    function Is_Subprogram_Contract_Annotation (Item : Node_Id) return Boolean;
    --  Determine whether aspect specification or pragma Item is one of the
    --  following subprogram contract annotations:
+   --    Always_Terminates
    --    Contract_Cases
    --    Depends
    --    Exceptional_Cases
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index b565221f730..0efbd4479e0 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -1711,6 +1711,7 @@ package Sinfo is
    --    a source construct, applies to a generic unit or its body, and denotes
    --    one of the following contract-related annotations:
    --      Abstract_State
+   --      Always_Terminates
    --      Contract_Cases
    --      Depends
    --      Exceptional_Cases
@@ -7978,6 +7979,7 @@ package Sinfo is
       --  establish dependencies between subprogram or package inputs and
       --  outputs. Currently the following pragmas appear in this list:
       --    Abstract_States
+      --    Always_Terminates
       --    Async_Readers
       --    Async_Writers
       --    Constant_After_Elaboration
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index 135b2533f9b..5044abbc7d0 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -503,6 +503,7 @@ package Snames is
    Name_Abort_Defer                    : constant Name_Id := N + $; -- GNAT
    Name_Abstract_State                 : constant Name_Id := N + $; -- GNAT
    Name_All_Calls_Remote               : constant Name_Id := N + $;
+   Name_Always_Terminates              : constant Name_Id := N + $; -- GNAT
    Name_Assert                         : constant Name_Id := N + $; -- Ada 05
    Name_Assert_And_Cut                 : constant Name_Id := N + $; -- GNAT
    Name_Assume                         : constant Name_Id := N + $; -- GNAT
@@ -1813,6 +1814,7 @@ package Snames is
       Pragma_Abort_Defer,
       Pragma_Abstract_State,
       Pragma_All_Calls_Remote,
+      Pragma_Always_Terminates,
       Pragma_Assert,
       Pragma_Assert_And_Cut,
       Pragma_Assume,
