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.

1 files changed, 19 insertions, 10 deletions

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,