diff options
| author | Johannes Kanig <kanig@adacore.com> | 2013-04-11 10:17:18 +0000 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2013-04-11 12:17:18 +0200 |
| commit | 0213fb4e3c39b3fcb889252ea358cf5775a541dd (patch) | |
| tree | d7cb3bee821cf19de72d6d13f05aedd55d412baf | |
| parent | 0088ba92b6bf944a69843de484a14be7c822713f (diff) | |
| download | gcc-0213fb4e3c39b3fcb889252ea358cf5775a541dd.zip gcc-0213fb4e3c39b3fcb889252ea358cf5775a541dd.tar.gz gcc-0213fb4e3c39b3fcb889252ea358cf5775a541dd.tar.bz2 | |
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
| -rw-r--r-- | gcc/ada/ChangeLog | 6 | ||||
| -rw-r--r-- | gcc/ada/debug.adb | 9 | ||||
| -rw-r--r-- | gcc/ada/gnat1drv.adb | 11 |
3 files changed, 24 insertions, 2 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 30fbe66..dc0dd40 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 ae66737..183413f 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 7a1c4f5..47c27da 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 |