[Ada] Ghost legality rules and SPARK_Mode

[Arnaud Charlet <charlet at adacore dot com>]

This patch decouples the semantic and legality rules of Ghost entities from the
presence of aspect/pragma SPARK_Mode. This way non-SPARK code can utilize Ghost
annotations.

------------
-- Source --
------------

--  ghost_decl.ads

package Ghost_Decl is
   X : Integer := 0 with Ghost;
   Y : Integer := X;
end Ghost_Decl;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c ghost_decl.ads
ghost_decl.ads:3:19: ghost entity cannot appear in this context (SPARK RM
  6.9(12))

Tested on x86_64-pc-linux-gnu, committed on trunk

2014-11-07  Hristian Kirtchev  <kirtchev@adacore.com>

	* freeze.adb (Freeze_Entity): Issue an error regardless of the
	SPARK_Mode when a ghost type is effectively volatile.
	* sem_ch3.adb (Analyze_Object_Contract): Decouple the checks
	related to Ghost from SPARK_Mode.
	* sem_res.adb (Check_Ghost_Policy): Issue an error regardless
	of the SPARK_Mode when the Ghost policies do not match.
	* sem_util.adb (Check_Ghost_Completion): Issue an error regardless
	of the SPARK_Mode when the Ghost policies do not match.

Attachment: difs
Description: Text document