ada: Update of SPARK RM legality rules on ghost code

Update checking of ghost code after a small change in SPARK RM
rules 6.9(15) and 6.9(20), so that the Ghost assertion policy
that matters when checking the validity of a reference to a ghost entity
in an assertion expression is the Ghost assertion policy at the point
of declaration of the entity.

Also fix references to SPARK RM rules in comments, which were off by two
in many cases after the insertion of rules 13 and 14 regarding generic
instantiations.

gcc/ada/

	* contracts.adb: Fix references to SPARK RM rules.
	* freeze.adb: Same.
	* ghost.adb: Fix references to SPARK RM rules.
	(Check_Ghost_Context): Update checking of references to
	ghost entities in assertion expressions.
	* sem_ch6.adb: Fix references to SPARK RM rules.
	* sem_prag.adb: Same.

1 files changed, 1 insertions, 1 deletions

diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 810b360..9fc9e05 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -1114,7 +1114,7 @@ package body Contracts is
       if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
 
          --  A Ghost object cannot be of a type that yields a synchronized
-         --  object (SPARK RM 6.9(19)).
+         --  object (SPARK RM 6.9(21)).
 
          if Yields_Synchronized_Object (Obj_Typ) then
             Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id);