2013-04-11 Robert Dewar <dewar@adacore.com>

[pf3gnuchains/gcc-fork.git] / gcc / ada / gnat1drv.adb

diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 7a59c52..4bfe7a6 100644 (file)
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -61,6 +61,7 @@ with Sem_Ch13;
 with Sem_Elim;
 with Sem_Eval;
 with Sem_Type;
+with Set_Targ;
 with Sinfo;    use Sinfo;
 with Sinput.L; use Sinput.L;
 with Snames;
@@ -293,8 +294,15 @@ procedure Gnat1drv is
          Formal_Extensions := True;
       end if;
 
+      --  Enable Alfa_Mode when using -gnatd.F switch
+
       if Debug_Flag_Dot_FF then
          Alfa_Mode := True;
+      end if;
+
+      --  Alfa_Mode is also activated by default in the gnat2why executable
+
+      if Alfa_Mode then
 
          --  Set strict standard interpretation of compiler permissions
 
@@ -302,6 +310,18 @@ procedure Gnat1drv is
             Strict_Alfa_Mode := True;
          end if;
 
+         --  Distinguish between the two modes of gnat2why: frame condition
+         --  generation (generation of ALI files) and translation of Why (no
+         --  ALI files generated). This is done with the switch -gnatd.G,
+         --  which activates frame condition mode. The other changes in
+         --  behavior depending on this switch are done in gnat2why directly.
+
+         if Debug_Flag_Dot_GG then
+            Frame_Condition_Mode := True;
+         else
+            Opt.Disable_ALI_File := True;
+         end if;
+
          --  Turn off inlining, which would confuse formal verification output
          --  and gain nothing.
 
@@ -408,6 +428,7 @@ procedure Gnat1drv is
          --  which is more complex to formally verify than the original source.
 
          Tagged_Type_Expansion := False;
+
       end if;
 
       --  Set Configurable_Run_Time mode if system.ads flag set
@@ -858,6 +879,14 @@ begin
          Usage;
       end if;
 
+      --  Generate target dependent output file if requested
+
+      if Target_Dependent_Info_Write then
+         Set_Targ.Write_Target_Dependent_Values;
+      end if;
+
+      --  Call the front end
+
       Original_Operating_Mode := Operating_Mode;
       Frontend;
 
@@ -1030,11 +1059,24 @@ begin
       elsif Main_Kind in N_Generic_Renaming_Declaration then
          Back_End_Mode := Generate_Object;
 
-      --  It's not an error to generate SCIL for e.g. a spec which has a body
+      --  It is not an error to analyze in CodePeer mode a spec which requires
+      --  a body, in order to generate SCIL for this spec.
 
       elsif CodePeer_Mode then
          Back_End_Mode := Generate_Object;
 
+      --  It is not an error to analyze in Alfa 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
+         if Frame_Condition_Mode then
+            Back_End_Mode := Declarations_Only;
+         else
+            Back_End_Mode := Generate_Object;
+         end if;
+
       --  In all other cases (specs which have bodies, generics, and bodies
       --  where subunits are missing), we cannot generate code and we generate
       --  a warning message. Note that generic instantiations are gone at this