ada: Support new SPARK aspect Exit_Cases

The aspect Exit_Cases allows annotating a subprogram with a list of
cases specifying, for all input which satisfy a guard, how the
subprogram is allowed to terminate. For now, it can only be either
returning normally or propagating an exception. This contract is not
checked at runtime, it is only meant for static verification in SPARK.

gcc/ada/ChangeLog:

	* aspects.ads: Add aspect Aspect_Exit_Cases.
	* contracts.adb (Analyze_Entry_Or_Subprogram_Contract): Handle Exit_Cases.
	(Expand_Subprogram_Contract): Idem.
	* einfo-utils.adb (Get_Pragma): Allow Pragma_Exit_Cases.
	* einfo-utils.ads (Get_Pragma): Idem.
	* exp_prag.adb (Expand_Pragma_Exit_Cases): Ignore the pragma, currently we don't expand it.
	* exp_prag.ads (Expand_Pragma_Exit_Cases): Idem.
	* inline.adb (Remove_Aspects_And_Pragmas): Add Exit_Cases to the list.
	(Remove_Items): Idem.
	* par-prag.adb (Last_Arg_Is_Reason): Idem.
	* sem_ch12.adb: Idem.
	* sem_ch13.adb: Idem.
	* sem_util.adb: Idem.
	* sem_util.ads: Idem.
	* sinfo.ads: Idem.
	* snames.ads-tmpl: Add names Name_Exit_Cases, Name_Exception_Raised, and Name_Normal_Return
	as well as pragma Pragma_Exit_Cases.
	* sem_prag.adb (Analyze_Exit_Cases_In_Decl_Part): Make sure that a
	pragma or aspect Exit_Cases is well formed.
	(Analyze_Pragma): Make sure that a pragma or aspect Exit_Cases is at the right place.
	* sem_prag.ads (Analyze_Exit_Cases_In_Decl_Part): Declaration.
	* doc/gnat_rm/implementation_defined_pragmas.rst: Document the Exit_Cases pragma.
	* doc/gnat_rm/implementation_defined_aspects.rst: Document the Exit_Cases aspect.
	* gnat_rm.texi: Regenerate.

0 files changed, 0 insertions, 0 deletions