adabkend.adb, [...]: Everything with name 'Alfa' renamed in 'SPARK'.

2013-04-24  Yannick Moy  <moy@adacore.com>

	* adabkend.adb, ali-util.adb, ali.adb, debug.adb,
	errout.adb, errout.ads, erroutc.adb, exp_ch3.adb, exp_ch4.adb,
	exp_ch6.adb, exp_ch7.adb, exp_dbug.adb, exp_util.adb,
	expander.adb, freeze.adb, gnat1drv.adb, lib-writ.adb,
	lib-writ.ads, lib-xref.adb, lib-xref.ads, opt.adb, opt.ads,
	restrict.adb, sem_aggr.adb, sem_attr.adb, sem_ch3.adb,
	sem_ch4.adb, sem_ch5.adb, sem_ch6.adb, sem_eval.adb, sem_prag.adb,
	sem_res.adb, sem_util.adb: Everything with name
	'Alfa' renamed in 'SPARK'. Update comments.
	Renaming of units with name 'Alfa', renamed with 'SPARK' instead.
	* exp_alfa.adb: renamed exp_spark.adb.
	* exp_alfa.ads: renamed exp_spark.ads.
	* get_alfa.adb: renamed get_spark_xrefs.adb.
	* get_alfa.ads: renamed get_spark_xrefs.ads.
	* lib-xref-alfa.adb: renamed lib-xref-spark_specific.adb.
	* put_alfa.adb: renamed put_spark_xrefs.adb.
	* put_alfa.ads: renamed put_spark_xrefs.ads.
	* alfa.adb: renamed spark_xrefs.adb.
	* alfa.ads: renamed spark_xrefs.ads.
	* alfa_test.adb: renamed spark_xrefs_test.adb.

From-SVN: r198234

1 files changed, 18 insertions, 18 deletions

diff --git a/gcc/ada/lib-xref.adb b/gcc/ada/lib-xref.adb
index ba9221b..8825f06 100644
--- a/gcc/ada/lib-xref.adb
+++ b/gcc/ada/lib-xref.adb
@@ -79,7 +79,7 @@ package body Lib.Xref is
       --  Unit number corresponding to Loc. Value is undefined and not
       --  referenced if Loc is set to No_Location.
 
-      --  The following components are only used for Alfa cross-references
+      --  The following components are only used for SPARK cross-references
 
       Ref_Scope : Entity_Id;
       --  Entity of the closest subprogram or package enclosing the reference
@@ -151,11 +151,11 @@ package body Lib.Xref is
      Hash       => Hash,
      Equal      => Equal);
 
-   ----------------------
-   -- Alfa Information --
-   ----------------------
+   -----------------------------
+   -- SPARK Xrefs Information --
+   -----------------------------
 
-   package body Alfa is separate;
+   package body SPARK_Specific is separate;
 
    ------------------------
    --  Local Subprograms --
@@ -632,10 +632,10 @@ package body Lib.Xref is
            or else (Typ = 'b' and then Is_Generic_Instance (E))
 
             --  Allow the generation of references to reads, writes and calls
-            --  in Alfa mode when the related context comes from an instance.
+            --  in SPARK mode when the related context comes from an instance.
 
            or else
-             (Alfa_Mode
+             (SPARK_Mode
                 and then In_Extended_Main_Code_Unit (N)
                 and then (Typ = 'm' or else Typ = 'r' or else Typ = 's'))
          then
@@ -885,12 +885,12 @@ package body Lib.Xref is
 
          --  Ignore references from within an instance. The only exceptions to
          --  this are default subprograms, for which we generate an implicit
-         --  reference and compilations in Alfa_Mode.
+         --  reference and compilations in SPARK mode.
 
          and then
            (Instantiation_Location (Sloc (N)) = No_Location
              or else Typ = 'i'
-             or else Alfa_Mode)
+             or else SPARK_Mode)
 
         --  Ignore dummy references
 
@@ -973,11 +973,11 @@ package body Lib.Xref is
             return;
          end if;
 
-         --  In Alfa mode, consider the underlying entity renamed instead of
+         --  In SPARK mode, consider the underlying entity renamed instead of
          --  the renaming, which is needed to compute a valid set of effects
          --  (reads, writes) for the enclosing subprogram.
 
-         if Alfa_Mode then
+         if SPARK_Mode then
             Ent := Get_Through_Renamings (Ent);
 
             --  If no enclosing object, then it could be a reference to any
@@ -987,10 +987,10 @@ package body Lib.Xref is
 
             if No (Ent) then
                if Actual_Typ = 'w' then
-                  Alfa.Generate_Dereference (Nod, 'r');
-                  Alfa.Generate_Dereference (Nod, 'w');
+                  SPARK_Specific.Generate_Dereference (Nod, 'r');
+                  SPARK_Specific.Generate_Dereference (Nod, 'w');
                else
-                  Alfa.Generate_Dereference (Nod, 'r');
+                  SPARK_Specific.Generate_Dereference (Nod, 'r');
                end if;
 
                return;
@@ -1006,14 +1006,14 @@ package body Lib.Xref is
             Actual_Typ := 'P';
          end if;
 
-         if Alfa_Mode then
+         if SPARK_Mode then
             Ref := Sloc (Nod);
             Def := Sloc (Ent);
 
-            Ref_Scope := Alfa.Enclosing_Subprogram_Or_Package (Nod);
-            Ent_Scope := Alfa.Enclosing_Subprogram_Or_Package (Ent);
+            Ref_Scope := SPARK_Specific.Enclosing_Subprogram_Or_Package (Nod);
+            Ent_Scope := SPARK_Specific.Enclosing_Subprogram_Or_Package (Ent);
 
-            --  Since we are reaching through renamings in Alfa mode, we may
+            --  Since we are reaching through renamings in SPARK mode, we may
             --  end up with standard constants. Ignore those.
 
             if Sloc (Ent_Scope) <= Standard_Location