aspects.adb: Add an entry for SPARK_Mode in table Canonical_Aspect.

2013-07-05  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb: Add an entry for SPARK_Mode in table Canonical_Aspect.
	* aspects.ads: Add an entry for SPARK_Mode in tables Aspect_Id,
	Aspect_Argument, Aspect_Names.
	* atree.adb (Node32): New routine.
	(Set_Node32): New routine.
	* atree.ads (Node32): New routine.
	(Set_Node32): New routine.
	* einfo.adb: Node32 is now used as SPARK_Mode_Pragmas.
	(Set_SPARK_Mode_Pragmas): New routine.
	(SPARK_Mode_Pragmas): New routine.
	(Write_Field32_Name): Add and entry for SPARK_Modes.
	* einfo.ads: Add attribute SPARK_Mode_Pragmas along with usage
	in various entities.
	(Set_SPARK_Mode_Pragmas): New routine and
	pragma Inline.
	(SPARK_Mode_Pragmas): New routine and pragma Inline.
	* gnat_rm.texi: Add sections explaining the syntax and semantics
	of aspect/pragma SPARK_Mode.
	* gnat_ugn.texi: Add pragma SPARK_Mode to the list of
	configuration pragmas.
	* lib.adb (Set_SPARK_Mode_Pragma): New routine.
	(SPARK_Mode_Pragma): New routine.
	* lib.ads: Alphabetize the comments on fields of record
	Unit_Record. Add new field SPARK_Mode_Pragma along with
	comment on its usage. Update the layout of record Unit_Record.
	(Set_SPARK_Mode_Pragma): New routine and pragma Inline.
	(SPARK_Mode_Pragma): New routine and pragma Inline.
	* lib-load.adb (Create_Dummy_Package_Unit): Initialize
	field SPARK_Mode_Pragma.
	(Load_Main_Source): Initialize field SPARK_Mode_Pragma.
	(Load_Unit): Initialize field SPARK_Mode_Pragma.
	* lib-writ.adb (Add_Preprocessing_Dependency): Initialize field
	SPARK_Mode_Pragma.
	(Ensure_System_Dependency): Initialize field SPARK_Mode_Pragma.
	* opt.ads: Alphabetize verification flags. Store the
	compilation-wide SPARK mode in variable Global_SPARK_Mode.
	* par-prag.adb: Pragma SPARK_Mode does not need special processing
	by the parser.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Convert aspect
	SPARK_Mode into a pragma.
	(Check_Aspect_At_Freeze_Point): Aspect SPARK_Mode does not need
	delayed processing.
	* sem_prag.adb: Add an entry for SPARK_Mode in table Sig_Flags.
	(Analyze_Pragma): Add processing for pragma SPARK_Mode.
	(Get_SPARK_Mode_Id): New routine.
	(Is_Elaboration_SPARK_Mode): New routine.
	(Is_Private_SPARK_Mode): New routine.
	* sem_prag.ads (Get_SPARK_Mode_Id): New routine.
	(Is_Elaboration_SPARK_Mode): New routine.
	(Is_Private_SPARK_Mode): New routine.
	* sinfo.ads: Update the comment on the usage of field Next_Pragma.
	* snames.ads-tmpl: Add new predefined name for SPARK_Mode and
	Auto. Add new pragma Id for SPARK_Mode.
	* types.ads: Add new type SPARK_Mode_Id.

From-SVN: r200711

1 files changed, 70 insertions, 67 deletions

diff --git a/gcc/ada/lib-load.adb b/gcc/ada/lib-load.adb
index be4c537..6d65c81 100644
--- a/gcc/ada/lib-load.adb
+++ b/gcc/ada/lib-load.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -206,28 +206,29 @@ package body Lib.Load is
       Unum := Units.Last;
 
       Units.Table (Unum) := (
-        Cunit            => Cunit,
-        Cunit_Entity     => Cunit_Entity,
-        Dependency_Num   => 0,
-        Dynamic_Elab     => False,
-        Error_Location   => Sloc (With_Node),
-        Expected_Unit    => Spec_Name,
-        Fatal_Error      => True,
-        Generate_Code    => False,
-        Has_Allocator    => False,
-        Has_RACW         => False,
-        Is_Compiler_Unit => False,
-        Ident_String     => Empty,
-        Loading          => False,
-        Main_Priority    => Default_Main_Priority,
-        Main_CPU         => Default_Main_CPU,
-        Munit_Index      => 0,
-        Serial_Number    => 0,
-        Source_Index     => No_Source_File,
-        Unit_File_Name   => Get_File_Name (Spec_Name, Subunit => False),
-        Unit_Name        => Spec_Name,
-        Version          => 0,
-        OA_Setting       => 'O');
+        Cunit             => Cunit,
+        Cunit_Entity      => Cunit_Entity,
+        Dependency_Num    => 0,
+        Dynamic_Elab      => False,
+        Error_Location    => Sloc (With_Node),
+        Expected_Unit     => Spec_Name,
+        Fatal_Error       => True,
+        Generate_Code     => False,
+        Has_Allocator     => False,
+        Has_RACW          => False,
+        Is_Compiler_Unit  => False,
+        Ident_String      => Empty,
+        Loading           => False,
+        Main_Priority     => Default_Main_Priority,
+        Main_CPU          => Default_Main_CPU,
+        Munit_Index       => 0,
+        Serial_Number     => 0,
+        Source_Index      => No_Source_File,
+        Unit_File_Name    => Get_File_Name (Spec_Name, Subunit => False),
+        Unit_Name         => Spec_Name,
+        Version           => 0,
+        OA_Setting        => 'O',
+        SPARK_Mode_Pragma => Empty);
 
       Set_Comes_From_Source_Default (Save_CS);
       Set_Error_Posted (Cunit_Entity);
@@ -312,28 +313,29 @@ package body Lib.Load is
          end if;
 
          Units.Table (Main_Unit) := (
-           Cunit            => Empty,
-           Cunit_Entity     => Empty,
-           Dependency_Num   => 0,
-           Dynamic_Elab     => False,
-           Error_Location   => No_Location,
-           Expected_Unit    => No_Unit_Name,
-           Fatal_Error      => False,
-           Generate_Code    => False,
-           Has_Allocator    => False,
-           Has_RACW         => False,
-           Is_Compiler_Unit => False,
-           Ident_String     => Empty,
-           Loading          => True,
-           Main_Priority    => Default_Main_Priority,
-           Main_CPU         => Default_Main_CPU,
-           Munit_Index      => 0,
-           Serial_Number    => 0,
-           Source_Index     => Main_Source_File,
-           Unit_File_Name   => Fname,
-           Unit_Name        => No_Unit_Name,
-           Version          => Version,
-           OA_Setting       => 'O');
+           Cunit             => Empty,
+           Cunit_Entity      => Empty,
+           Dependency_Num    => 0,
+           Dynamic_Elab      => False,
+           Error_Location    => No_Location,
+           Expected_Unit     => No_Unit_Name,
+           Fatal_Error       => False,
+           Generate_Code     => False,
+           Has_Allocator     => False,
+           Has_RACW          => False,
+           Is_Compiler_Unit  => False,
+           Ident_String      => Empty,
+           Loading           => True,
+           Main_Priority     => Default_Main_Priority,
+           Main_CPU          => Default_Main_CPU,
+           Munit_Index       => 0,
+           Serial_Number     => 0,
+           Source_Index      => Main_Source_File,
+           Unit_File_Name    => Fname,
+           Unit_Name         => No_Unit_Name,
+           Version           => Version,
+           OA_Setting        => 'O',
+           SPARK_Mode_Pragma => Empty);
       end if;
    end Load_Main_Source;
 
@@ -675,28 +677,29 @@ package body Lib.Load is
 
          if Src_Ind /= No_Source_File then
             Units.Table (Unum) := (
-              Cunit            => Empty,
-              Cunit_Entity     => Empty,
-              Dependency_Num   => 0,
-              Dynamic_Elab     => False,
-              Error_Location   => Sloc (Error_Node),
-              Expected_Unit    => Uname_Actual,
-              Fatal_Error      => False,
-              Generate_Code    => False,
-              Has_Allocator    => False,
-              Has_RACW         => False,
-              Is_Compiler_Unit => False,
-              Ident_String     => Empty,
-              Loading          => True,
-              Main_Priority    => Default_Main_Priority,
-              Main_CPU         => Default_Main_CPU,
-              Munit_Index      => 0,
-              Serial_Number    => 0,
-              Source_Index     => Src_Ind,
-              Unit_File_Name   => Fname,
-              Unit_Name        => Uname_Actual,
-              Version          => Source_Checksum (Src_Ind),
-              OA_Setting       => 'O');
+              Cunit             => Empty,
+              Cunit_Entity      => Empty,
+              Dependency_Num    => 0,
+              Dynamic_Elab      => False,
+              Error_Location    => Sloc (Error_Node),
+              Expected_Unit     => Uname_Actual,
+              Fatal_Error       => False,
+              Generate_Code     => False,
+              Has_Allocator     => False,
+              Has_RACW          => False,
+              Is_Compiler_Unit  => False,
+              Ident_String      => Empty,
+              Loading           => True,
+              Main_Priority     => Default_Main_Priority,
+              Main_CPU          => Default_Main_CPU,
+              Munit_Index       => 0,
+              Serial_Number     => 0,
+              Source_Index      => Src_Ind,
+              Unit_File_Name    => Fname,
+              Unit_Name         => Uname_Actual,
+              Version           => Source_Checksum (Src_Ind),
+              OA_Setting        => 'O',
+              SPARK_Mode_Pragma => Empty);
 
             --  Parse the new unit