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

[pmderodat@gcc.gnu.org]

Author: pmderodat
Date: Wed Aug 14 09:51:21 2019
New Revision: 274453

URL: https://gcc.gnu.org/viewcvs?rev=274453&root=gcc&view=rev
Log:
[Ada] Check SPARK restriction on Old/Loop_Entry with pointers

--#! r336866
--#! no-mail

SPARK RM rule 3.10(14) restricts the use of Old and Loop_Entry
attributes on prefixes of an owning or observing type (i.e. a type with
access inside).

There is no impact on compilation.

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

gcc/ada/

	* sem_spark.adb (Check_Old_Loop_Entry): New procedure to check
	correct use of Old  and Loop_Entry.
	(Check_Node): Check subprogram contracts.
	(Check_Pragma): Check Loop_Variant.
	(Check_Safe_Pointers): Apply checking to library-level
	subprogram  declarations as well, in order to check their
	contract.

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