2014-08-04 Hristian Kirtchev <kirtchev@adacore.com>

	* opt.ads Alphabetize various global flags. New flag
	Ignore_Pragma_SPARK_Mode along with a comment on usage.
	* sem_ch6.adb (Analyze_Generic_Subprogram_Body):
	Pragma SPARK_Mode is now allowed in generic units.
	(Analyze_Subprogram_Body_Helper): Do not verify the compatibility
	between the SPARK_Mode of a spec and that of a body when inside
	a generic.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Do not verify the
	compatibility between the SPARK_Mode of a spec and that of a
	body when inside a generic.
	* sem_ch12.adb (Analyze_Generic_Subprogram_Declaration):
	Pragma SPARK_Mode is now allowed in generic units.
	(Analyze_Package_Instantiation): Save and restore the value of
	flag Ignore_ Pragma_SPARK_Mode in a stack-like fasion. Set
	the governing SPARK_Mode before analyzing the instance.
	(Analyze_Subprogram_Instantiation): Save and restore the value
	of flag Ignore_ Pragma_SPARK_Mode in a stack-like fasion. Set
	the governing SPARK_Mode before analyzing the instance.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Emulate the
	placement of a source pragma when inserting the generated pragma
	for aspect SPARK_Mode.
	* sem_prag.adb (Analyze_Pragma): Reimplement the handling of
	pragma SPARK_Mode to allow for generics and their respective
	instantiations.
	* sem_util.ads, sem_util.adb (Check_SPARK_Mode_In_Generic): Removed.
	(Set_Ignore_Pragma_SPARK_Mode): New routine.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@213570 138bc75d-0d04-0410-961f-82ee72b054a4

1 files changed, 31 insertions, 25 deletions

diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index f056f3985d1..2e00d4aa995 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -648,6 +648,20 @@ package Opt is
    --  GNAT
    --  Disable generation of ALI file
 
+   Follow_Links_For_Files : Boolean := False;
+   --  PROJECT MANAGER
+   --  Set to True (-eL) to process the project files in trusted mode. If
+   --  Follow_Links is False, it is assumed that the project doesn't contain
+   --  any file duplicated through symbolic links (although the latter are
+   --  still valid if they point to a file which is outside of the project),
+   --  and that no directory has a name which is a valid source name.
+
+   Follow_Links_For_Dirs : Boolean := False;
+   --  PROJECT MANAGER
+   --  Set to True if directories can be links in this project, and therefore
+   --  additional system calls must be performed to ensure that we always see
+   --  the same full name for each directory.
+
    Force_Checking_Of_Elaboration_Flags : Boolean := False;
    --  GNATBIND
    --  True if binding with forced checking of the elaboration flags
@@ -657,6 +671,13 @@ package Opt is
    --  GNATMAKE, GPRMAKE, GPRBUILD
    --  Set to force recompilations even when the objects are up-to-date.
 
+   Front_End_Inlining : Boolean := False;
+   --  GNAT
+   --  Set True to activate inlining by front-end expansion (even on GCC
+   --  targets, where inlining is normally handled by the back end). Set by
+   --  the flag -gnatN (which is now considered obsolescent, since the GCC
+   --  back end can do a better job of inlining than the front end these days.
+
    Full_Path_Name_For_Brief_Errors : Boolean := False;
    --  PROJECT MANAGER
    --  When True, in Brief_Output mode, each error message line
@@ -684,6 +705,10 @@ package Opt is
    --  True when switch -gnateG is used. When True, create in a file
    --  <source>.prep, if the source is preprocessed.
 
+   Generate_SCIL : Boolean := False;
+   --  GNAT
+   --  Set True to activate SCIL code generation.
+
    Generate_SCO : Boolean := False;
    --  GNAT
    --  True when switch -fdump-scos (or -gnateS) is used. When True, Source
@@ -728,6 +753,12 @@ package Opt is
    --  default value appropriate to the system (in Osint.Initialize), and then
    --  reset if a command line switch is used to change the setting.
 
+   Ignore_Pragma_SPARK_Mode : Boolean := False;
+   --  GNAT
+   --  Set True to ignore the semantics and effects of pragma SPARK_Mode when
+   --  the pragma appears inside an instance whose enclosing context is subject
+   --  to SPARK_Mode "off".
+
    Ignore_Rep_Clauses : Boolean := False;
    --  GNAT
    --  Set True to ignore all representation clauses. Useful when compiling
@@ -798,35 +829,10 @@ package Opt is
    --  then elaboration flag checks are to be generated in the binder
    --  generated file.
 
-   Generate_SCIL : Boolean := False;
-   --  GNAT
-   --  Set True to activate SCIL code generation.
-
    Invalid_Value_Used : Boolean := False;
    --  GNAT
    --  Set True if a valid Invalid_Value attribute is encountered
 
-   Follow_Links_For_Files : Boolean := False;
-   --  PROJECT MANAGER
-   --  Set to True (-eL) to process the project files in trusted mode. If
-   --  Follow_Links is False, it is assumed that the project doesn't contain
-   --  any file duplicated through symbolic links (although the latter are
-   --  still valid if they point to a file which is outside of the project),
-   --  and that no directory has a name which is a valid source name.
-
-   Follow_Links_For_Dirs : Boolean := False;
-   --  PROJECT MANAGER
-   --  Set to True if directories can be links in this project, and therefore
-   --  additional system calls must be performed to ensure that we always see
-   --  the same full name for each directory.
-
-   Front_End_Inlining : Boolean := False;
-   --  GNAT
-   --  Set True to activate inlining by front-end expansion (even on GCC
-   --  targets, where inlining is normally handled by the back end). Set by
-   --  the flag -gnatN (which is now considered obsolescent, since the GCC
-   --  back end can do a better job of inlining than the front end these days.
-
    Inline_Processing_Required : Boolean := False;
    --  GNAT
    --  Set True if inline processing is required. Inline processing is required