From: Johannes Kanig <kanig@adacore.com>
Date: Thu, 11 Apr 2013 10:17:18 +0000 (+0000)
Subject: debug.adb: Reservation and documentation for -gnatd.G switch.
X-Git-Tag: releases/gcc-4.9.0~6547
X-Git-Url: http://git.ipfire.org/?a=commitdiff_plain;h=0213fb4e3c39b3fcb889252ea358cf5775a541dd;p=thirdparty%2Fgcc.git

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 30fbe66a56c4..dc0dd405be59 100644
--- 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 ae66737c4be5..183413ff0810 100644
--- 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 7a1c4f5ecd75..47c27da01141 100644
--- 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