ada: Implement new aspect Always_Terminates for SPARK

This patch allows subprograms to be annotated with aspect
Always_Terminates that requires a boolean expression. When this
expression evaluates to True, the subprogram is required to terminate or
raise an exception, but not loop infinitely.

This aspect is only meant to be used by GNATprove and it has no
meaningful run-time semantics: either the annotated subprogram
terminates and then the aspect expression doesn't matter, or the
subprogram loops infinitely and there is nothing we can do. (We could
also evaluate the aspect expression just to detect run-time errors in
the expression itself, but this can be implemented later, after a
backend support for the aspect is added to GNATprove.)

Implementation of this aspect is heavily based on the implementation of
Subprogram_Variant, which in turn is heavily based on the implementation
of Contract_Cases. Since the new aspect is not yet expanded, there is no
corresponding assertion kind that would control the expansion.

gcc/ada/

	* aspects.ads (Aspect_Id): Add new aspect.
	(Implementation_Defined_Aspect): New aspect is
	implementation-defined.
	(Aspect_Argument): New aspect has an expression argument.
	(Is_Representation_Aspect): New aspect is not a representation
	aspect.
	(Aspect_Names): Link new aspect identifier with a name.
	(Aspect_Delay): New aspect is never delayed.
	* contracts.adb (Expand_Subprogram_Contract): Mention new aspect
	in comment.
	(Add_Contract_Item): Attach pragma corresponding to the new aspect
	to contract items.
	(Analyze_Entry_Or_Subprogram_Contract): Analyze pragma
	corresponding to the new aspect that appears with subprogram spec.
	(Analyze_Subprogram_Body_Stub_Contract): Expand pragma
	corresponding to the new aspect.
	* contracts.ads
	(Add_Contract_Item, Analyze_Entry_Or_Subprogram_Contract)
	(Analyze_Entry_Or_Subprogram_Body_Contract)
	(Analyze_Subprogram_Body_Stub_Contract): Mention new aspect in
	comment.
	* einfo-utils.adb (Get_Pragma): Return pragma attached to
	contract.
	* einfo-utils.ads (Get_Pragma): Mention new contract in comment.
	* exp_prag.adb (Expand_Pragma_Always_Terminates): Placeholder for
	possibly expanding new aspect.
	* exp_prag.ads (Expand_Pragma_Always_Terminates): Dedicated
	routine for expansion of the new aspect.
	* inline.adb (Remove_Aspects_And_Pragmas): Remove aspect from
	inlined bodies.
	* par-prag.adb (Prag): Postpone checking of the pragma until
	analysis.
	* sem_ch12.adb: Mention new aspect in explanation of handling
	contracts on generic units.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Convert new aspect
	into a corresponding pragma.
	(Check_Aspect_At_Freeze_Point): Don't expect new aspect.
	* sem_prag.adb (Analyze_Always_Terminates_In_Decl_Part): Analyze
	pragma corresponding to the new aspect.
	(Analyze_Pragma): Handle pragma corresponding to the new aspect.
	(Is_Non_Significant_Pragma_Reference): Handle references appearing
	within new aspect.
	* sem_prag.ads (Aspect_Specifying_Pragma): New aspect can be
	emulated with a pragma.
	(Assertion_Expression_Pragma): New aspect has an assertion
	expression.
	(Pragma_Significant_To_Subprograms): New aspect is significant to
	subprograms.
	(Analyze_Always_Terminates_In_Decl_Part): Add spec for routine
	that analyses new aspect.
	(Find_Related_Declaration_Or_Body): Mention new aspect in comment.
	* sem_util.adb (Is_Subprogram_Contract_Annotation): New aspect is
	a subprogram contract annotation.
	* sem_util.ads (Is_Subprogram_Contract_Annotation): Mention new
	aspect in comment.
	* sinfo.ads (Is_Generic_Contract_Pragma): New pragma is a generic
	contract.
	(Contract): Explain attaching new pragma to subprogram contract.
	* snames.ads-tmpl (Name_Always_Terminates): New name for the new
	contract.
	(Pragma_Always_Terminates): New pragma identifier.

17 files changed, 295 insertions, 24 deletions

diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads
index bd8e7c6..19f7c07 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 19073d1..0e87cee 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 d52e1aa..c3dc5d6 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 d1db66f..dad3a65 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 e805502..fee771c 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 e660196..1cc4653 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 9f810da..10ccaf7 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 a4c32e9..edb90a9 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 ac50c84..b139862 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 a38ab28..f584a9f 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 2b8b64a..e771c0d 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 abc0e5d..bca4eb5 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 49c1d0b..e8e9856 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 c736bc3..b82978b 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 539ebeb..3751fb7 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 b565221..0efbd44 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 135b253..5044abb 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,