r273349 - in /trunk/gcc/ada: ChangeLog sem_aux....

[pmderodat@gcc.gnu.org]

Author: pmderodat
Date: Wed Jul 10 09:02:42 2019
New Revision: 273349

URL: https://gcc.gnu.org/viewcvs?rev=273349&root=gcc&view=rev
Log:
[Ada] Fix spurious messages on global variables for SPARK pointer support

Pointer support in GNATprove leads to spurious messages about global
variables, with local variables declared in local packages and protected
components. Now fixed.

There is no impact on compilation.

2019-07-10  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_aux.adb, sem_aux.ads (Is_Protected_Operation): New
	function to determine if a subprogram is protected.
	* sem_spark.adb (Setup_Protected_Components): New procedure to
	add protected components to the environment.
	(Check_Callable_Body): Call the new Setup_Protected_Components.
	(Check_Package_Spec): Merge local environment with enclosing one
	when done.

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