diff options
| author | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2013-04-11 10:17:18 +0000 |
|---|---|---|
| committer | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2013-04-11 10:17:18 +0000 |
| commit | d7a8e67531b07ae0cda1be006f9c3511d3320e35 (patch) | |
| tree | d7cb3bee821cf19de72d6d13f05aedd55d412baf /gcc/ada/debug.adb | |
| parent | d1eda9b3957e0dbb6cf7102a81d62ccad13d93be (diff) | |
| download | gcc-d7a8e67531b07ae0cda1be006f9c3511d3320e35.tar.gz | |
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.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@197757 138bc75d-0d04-0410-961f-82ee72b054a4
Diffstat (limited to 'gcc/ada/debug.adb')
| -rw-r--r-- | gcc/ada/debug.adb | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index ae66737c4be..183413ff081 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 |