debug.adb: Reservation and documentation for -gnatd.G switch.

2013-04-11  Johannes Kanig  <kanig@adacore.com>

	* debug.adb: Reservation and documentation for -gnatd.G switch.
	* gnat1drv.adb (Adjust_Global_Switches) Take into account -gnatd.G
	switch, and set ALI file generation accordingly.

From-SVN: r197757

gcc/ada/ChangeLog

+2013-04-11  Johannes Kanig  <kanig@adacore.com>
+
+	* debug.adb: Reservation and documentation for -gnatd.G switch.
+	* gnat1drv.adb (Adjust_Global_Switches) Take into account -gnatd.G
+	switch, and set ALI file generation accordingly.
+
 2013-04-11  Robert Dewar  <dewar@adacore.com>
 
 	* exp_ch4.adb, exp_dist.adb: Minor reformatting.

gcc/ada/debug.adb

@@ -124,7 +124,7 @@ package body Debug is
    --  d.D  Strict Alfa mode
    --  d.E  Force Alfa mode for gnat2why
    --  d.F  Alfa mode
-   --  d.G
+   --  d.G  Frame condition mode for gnat2why
    --  d.H  Standard package only mode for gnat2why
    --  d.I
    --  d.J  Disable parallel SCIL generation mode
@@ -603,7 +603,12 @@ package body Debug is
 
    --  d.F  Alfa mode. Generate AST in a form suitable for formal verification,
    --       as well as additional cross reference information in ALI files to
-   --       compute effects of subprograms.
+   --       compute effects of subprograms. Note that ALI files are only
+   --       written when option d.G is also given.
+
+   --  d.G  Frame condition mode for gnat2why. In this mode, gnat2why will not
+   --       generate Why code. Instead, it generates ALI files with an extra
+   --       section which contains the effects of subprograms.
 
    --  d.H  Standard package only mode for gnat2why. In this mode, gnat2why
    --       will only generate Why code for package Standard. Any given input

gcc/ada/gnat1drv.adb

@@ -408,6 +408,17 @@ procedure Gnat1drv is
          --  which is more complex to formally verify than the original source.
 
          Tagged_Type_Expansion := False;
+
+         --  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 not Debug_Flag_Dot_GG then
+            Opt.Disable_ALI_File := True;
+         end if;
+
       end if;
 
       --  Set Configurable_Run_Time mode if system.ads flag set