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.



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

1 files changed, 14 insertions, 14 deletions

diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 10ad1e907d3..4f1dde72f34 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -292,20 +292,20 @@ procedure Gnat1drv is
          Formal_Extensions := True;
       end if;
 
-      --  Enable Alfa_Mode when using -gnatd.F switch
+      --  Enable SPARK_Mode when using -gnatd.F switch
 
       if Debug_Flag_Dot_FF then
-         Alfa_Mode := True;
+         SPARK_Mode := True;
       end if;
 
-      --  Alfa_Mode is also activated by default in the gnat2why executable
+      --  SPARK_Mode is also activated by default in the gnat2why executable
 
-      if Alfa_Mode then
+      if SPARK_Mode then
 
          --  Set strict standard interpretation of compiler permissions
 
          if Debug_Flag_Dot_DD then
-            Strict_Alfa_Mode := True;
+            SPARK_Strict_Mode := True;
          end if;
 
          --  Distinguish between the two modes of gnat2why: frame condition
@@ -334,7 +334,7 @@ procedure Gnat1drv is
 
          --  Enable some restrictions systematically to simplify the generated
          --  code (and ease analysis). Note that restriction checks are also
-         --  disabled in Alfa mode, see Restrict.Check_Restriction, and user
+         --  disabled in SPARK mode, see Restrict.Check_Restriction, and user
          --  specified Restrictions pragmas are ignored, see
          --  Sem_Prag.Process_Restrictions_Or_Restriction_Warnings.
 
@@ -346,7 +346,7 @@ procedure Gnat1drv is
          --  points at which potential checks are required semantically). We
          --  don't want the expansion associated with these checks, but that
          --  happens anyway because this expansion is simply not done in the
-         --  Alfa version of the expander.
+         --  SPARK version of the expander.
 
          --  Turn off dynamic elaboration checks: generates inconsistencies in
          --  trees between specs compiled as part of a main unit or as part of
@@ -378,7 +378,7 @@ procedure Gnat1drv is
          Polling_Required := False;
 
          --  Set operating mode to Generate_Code, but full front-end expansion
-         --  is not desirable in Alfa mode, so a light expansion is performed
+         --  is not desirable in SPARK mode, so a light expansion is performed
          --  instead.
 
          Operating_Mode := Generate_Code;
@@ -405,7 +405,7 @@ procedure Gnat1drv is
          Assertions_Enabled := True;
 
          --  Turn off style check options since we are not interested in any
-         --  front-end warnings when we are getting Alfa output.
+         --  front-end warnings when we are getting SPARK output.
 
          Reset_Style_Check_Options;
 
@@ -415,13 +415,13 @@ procedure Gnat1drv is
          Warning_Mode := Suppress;
 
          --  Suppress the generation of name tables for enumerations, which are
-         --  not needed for formal verification, and fall outside the Alfa
+         --  not needed for formal verification, and fall outside the SPARK
          --  subset (use of pointers).
 
          Global_Discard_Names := True;
 
          --  Suppress the expansion of tagged types and dispatching calls,
-         --  which lead to the generation of non-Alfa code (use of pointers),
+         --  which lead to the generation of non-SPARK code (use of pointers),
          --  which is more complex to formally verify than the original source.
 
          Tagged_Type_Expansion := False;
@@ -495,7 +495,7 @@ procedure Gnat1drv is
 
       --  Set proper status for overflow check mechanism
 
-      --  If already set (by -gnato or above in Alfa or CodePeer mode) then we
+      --  If already set (by -gnato or above in SPARK or CodePeer mode) then we
       --  have nothing to do.
 
       if Opt.Suppress_Options.Overflow_Mode_General /= Not_Set then
@@ -1062,12 +1062,12 @@ begin
       elsif CodePeer_Mode then
          Back_End_Mode := Generate_Object;
 
-      --  It is not an error to analyze in Alfa mode a spec which requires a
+      --  It is not an error to analyze in SPARK mode a spec which requires a
       --  body, when the body is not available. During frame condition
       --  generation, the corresponding ALI file is generated. During
       --  translation to Why, Why code is generated for the spec.
 
-      elsif Alfa_Mode then
+      elsif SPARK_Mode then
          if Frame_Condition_Mode then
             Back_End_Mode := Declarations_Only;
          else