ada: Accept and analyze new aspect Exceptional_Cases

Add new aspect Exceptional_Cases, which is intended for SPARK and
describes in which cases an exception will be raised, and optionally
supply a postcondition that shall be verified in this case.

The implementation is heavily modeled after Subprogram_Variant, which in
turn was heavily modeled after Contract_Cases. Currently the aspect is
only analysed; the code infrastructure required to expand it is prepared
but empty. This is enough for the aspect to be verified by GNATprove.

gcc/ada/

	* aspects.ads
	(Aspect_Id): Add aspect identifier.
	(Aspect_Argument): New aspect accepts an expression.
	(Is_Representation_Aspect): New aspect is not a representation
	aspect.
	(Aspect_Names): Associate name with the new aspect identifier.
	(Aspect_Delay): New aspect is never delayed.
	* contracts.adb
	(Add_Contract_Item): Store new aspect among contract items.
	(Analyze_Entry_Or_Subprogram_Contract): Likewise.
	(Analyze_Subprogram_Body_Stub_Contract): Likewise.
	(Process_Contract_Cases): Expand new aspect, if present.
	* contracts.ads
	(Analyze_Entry_Or_Subprogram_Body_Contract): Mention new aspect in
	spec.
	(Analyze_Entry_Or_Subprogram_Contract): Likewise.
	* einfo-utils.adb
	(Get_Pragma): Allow new aspect to be picked by the backend.
	* einfo-utils.ads
	(Get_Pragma): Mention new aspect in spec.
	* exp_prag.adb
	(Expand_Pragma_Exceptional_Cases): Dummy expansion routine.
	* exp_prag.ads
	(Expand_Pragma_Exceptional_Cases): Add spec for expansion routine.
	* inline.adb
	(Remove_Aspects_And_Pragmas): Remove aspect from bodies to inline.
	* par-prag.adb
	(Par.Prag): Accept pragma in the parser, so it will be checked
	later.
	* sem_ch12.adb
	(Implementation of Generic Contracts): Mention new aspect in
	comment.
	* sem_ch13.adb
	(Analyze_Aspect_Specifications): Transform new aspect info a
	corresponding pragma.
	* sem_prag.adb
	(Analyze_Exceptional_Cases_In_Decl_Part): Analyze aspect
	expression; heavily inspired by the existing code for analysis of
	Subprogram_Variant and exception handlers.
	(Analyze_Pragma): Analyze pragma corresponding to the new aspect.
	(Is_Non_Significant_Pragma_Reference): Add new pragma to the
	table.
	* sem_prag.ads
	(Assertion_Expression_Pragma): New pragma acts as an assertion
	expression, even though it is not currently expanded.
	(Analyze_Exceptional_Cases_In_Decl_Part): Add spec.
	* sem_util.adb
	(Is_Subprogram_Contract_Annotation): Mark new annotation is a
	subprogram contract, so the subprogram with it won't be inlined.
	* sem_util.ads
	(Is_Subprogram_Contract_Annotation): Mention new aspect in
	comment.
	* sinfo.ads
	(Contract_Test_Cases): Mention new aspect in comment.
	* snames.ads-tmpl: Add entries for the new name and pragma.

1 files changed, 14 insertions, 4 deletions

diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index b0a0ab20..c85df0f 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -104,8 +104,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, Subprogram_Variant, invariants and predicates.
-   --  Body_Id denotes the entity of the subprogram body.
+   --  well as Contract_Cases, Exceptional_Cases, Subprogram_Variant,
+   --  invariants and predicates. Body_Id denotes the entity of the
+   --  subprogram body.
 
    procedure Preanalyze_Condition
      (Subp : Entity_Id;
@@ -253,6 +254,7 @@ package body Contracts is
             Add_Classification;
 
          elsif Prag_Nam in Name_Contract_Cases
+                         | Name_Exceptional_Cases
                          | Name_Subprogram_Variant
                          | Name_Test_Case
          then
@@ -629,8 +631,9 @@ package body Contracts is
       end if;
 
       --  Deal with preconditions, [refined] postconditions, Contract_Cases,
-      --  Subprogram_Variant, invariants and predicates associated with body
-      --  and its spec. Do not expand the contract of subprogram body stubs.
+      --  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);
@@ -766,6 +769,9 @@ package body Contracts is
                   Analyze_Contract_Cases_In_Decl_Part (Prag, Freeze_Id);
                end if;
 
+            elsif Prag_Nam = Name_Exceptional_Cases then
+               Analyze_Exceptional_Cases_In_Decl_Part (Prag);
+
             elsif Prag_Nam = Name_Subprogram_Variant then
                Analyze_Subprogram_Variant_In_Decl_Part (Prag);
 
@@ -1493,6 +1499,7 @@ package body Contracts is
       --  The stub acts as its own spec, the applicable pragmas are:
       --    Contract_Cases
       --    Depends
+      --    Exceptional_Cases
       --    Global
       --    Postcondition
       --    Precondition
@@ -2830,6 +2837,9 @@ package body Contracts is
                            Decls   => Decls,
                            Stmts   => Stmts);
 
+                     elsif Pragma_Name (Prag) = Name_Exceptional_Cases then
+                        Expand_Pragma_Exceptional_Cases (Prag);
+
                      elsif Pragma_Name (Prag) = Name_Subprogram_Variant then
                         Expand_Pragma_Subprogram_Variant
                           (Prag       => Prag,