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, 1 insertions, 0 deletions

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