r274454 - in /trunk/gcc/ada: ChangeLog sem_spar...

[pmderodat@gcc.gnu.org]

Author: pmderodat
Date: Wed Aug 14 09:51:25 2019
New Revision: 274454

URL: https://gcc.gnu.org/viewcvs?rev=274454&root=gcc&view=rev
Log:
[Ada] Expose part of ownership checking for use in GNATprove

GNATprove needs to be able to call a subset of the ownership legality
rules from marking. This is provided by a new function
Sem_SPARK.Is_Legal.

There is no impact on compilation.

2019-08-14  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_spark.adb, sem_spark.ads (Is_Legal): New function exposed
	for use in GNATprove, to test legality rules not related to
	permissions.
	(Check_Declaration_Legality): Extract the part of
	Check_Declaration that checks rules not related to permissions.
	(Check_Declaration): Call the new Check_Declaration_Legality.
	(Check_Type_Legality): Rename of Check_Type. Introduce
	parameters to force or not checking, and update a flag detecting
	illegalities.
	(Check_Node): Ignore attribute references in statement position.

Modified:
    trunk/gcc/ada/ChangeLog
    trunk/gcc/ada/sem_spark.adb
    trunk/gcc/ada/sem_spark.ads