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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 30fbe66a56c449a150db4073243d0cb8b1690743..dc0dd405be590db0e34276e5fba07fa5ce9f5e44 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,9 @@
+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.

diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index ae66737c4be522b4cbb148dc30873f9b92d116db..183413ff0810d7dbac23332373a1bfe7fc4f61be 100644 (file)
--- a/gcc/ada/debug.adb
+++ b/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

diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 7a1c4f5ecd759a77b1eccb8c090e8394a1a43350..47c27da01141360f4c1e265bff1f0c77890a4b19 100644 (file)
--- a/gcc/ada/gnat1drv.adb
+++ b/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