r235115 - in /trunk/gcc/ada: ChangeLog contract...

[charlet@gcc.gnu.org]

Author: charlet
Date: Mon Apr 18 10:22:13 2016
New Revision: 235115

URL: https://gcc.gnu.org/viewcvs?rev=235115&root=gcc&view=rev
Log:
2016-04-18  Hristian Kirtchev  <kirtchev@adacore.com>

	* contracts.adb (Analyze_Object_Contract): Update references to
	SPARK RM.
	* freeze.adb (Freeze_Entity): Update references to SPARK RM.
	* ghost.adb Add with and use clauses for Sem_Disp.
	(Check_Ghost_Derivation): Removed.
	(Check_Ghost_Overriding):
	Reimplemented.	(Check_Ghost_Policy): Update references to SPARK RM.
	(Check_Ghost_Primitive): New routine.
	(Check_Ghost_Refinement): New routine.	(Is_OK_Ghost_Context):
	Update references to SPARK RM.	(Is_OK_Pragma): Update references
	to SPARK RM. Predicates are now a valid context for references
	to Ghost entities.
	* ghost.ads (Check_Ghost_Derivation): Removed.
	(Check_Ghost_Overriding): Update the comment on usage.
	(Check_Ghost_Primitive): New routine.
	(Check_Ghost_Refinement): New routine.
	(Remove_Ignored_Ghost_Code): Update references to SPARK RM.
	* sem_ch3.adb (Process_Full_View): Remove the now obsolete check
	related to Ghost derivations
	* sem_ch6.adb (Check_Conformance): Remove now obsolete check
	related to the convention-like behavior of pragma Ghost.
	(Check_For_Primitive_Subprogram): Verify that the Ghost policy
	of a tagged type and its primitive agree.
	* sem_prag.adb (Analyze_Pragma): Update references to SPARK
	RM. Move the verification of pragma Assertion_Policy Ghost
	to the proper place. Remove the now obsolete check related
	to Ghost derivations.
	(Collect_Constituent): Add a call to Check_Ghost_Refinement.
	* sem_res.adb (Resolve_Actuals): Update references to SPARK RM.


Modified:
    trunk/gcc/ada/ChangeLog
    trunk/gcc/ada/contracts.adb
    trunk/gcc/ada/freeze.adb
    trunk/gcc/ada/ghost.adb
    trunk/gcc/ada/ghost.ads
    trunk/gcc/ada/sem_ch3.adb
    trunk/gcc/ada/sem_ch6.adb
    trunk/gcc/ada/sem_prag.adb
    trunk/gcc/ada/sem_res.adb