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

diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb
index c6b3bed..e660196 100644
--- a/gcc/ada/exp_prag.adb
+++ b/gcc/ada/exp_prag.adb
@@ -1978,6 +1978,47 @@ package body Exp_Prag is
       In_Assertion_Expr := In_Assertion_Expr - 1;
    end Expand_Pragma_Contract_Cases;
 
+   -------------------------------------
+   -- Expand_Pragma_Exceptional_Cases --
+   -------------------------------------
+
+   --  Aspect Exceptional_Cases shoule be expanded in the following manner:
+
+   --  Original declaration
+
+   --     procedure P (...) with
+   --        Exceptional_Cases =>
+   --           (Exp_1 => True,
+   --            Exp_2 => Post_4);
+
+   --  Expanded body
+
+   --     procedure P (...) is
+   --     begin
+   --        --  normal body of of P
+   --        declare
+   --        ...
+   --        end;
+   --
+   --     exception
+   --        when Exp1 =>
+   --           pragma Assert (True);
+   --           raise;
+   --        when E : Exp2 =>
+   --           pragma Assert (Post_4);
+   --           raise;
+   --        when others =>
+   --           pragma Assert (False);
+   --           raise;
+   --     end P;
+
+   procedure Expand_Pragma_Exceptional_Cases (Prag : Node_Id) is
+   begin
+      --  Currently we don't expand this pragma
+
+      Rewrite (Prag, Make_Null_Statement (Sloc (Prag)));
+   end Expand_Pragma_Exceptional_Cases;
+
    ---------------------------------------
    -- Expand_Pragma_Import_Or_Interface --
    ---------------------------------------