diff options
Diffstat (limited to 'gcc/ada/debug.adb')
-rw-r--r-- | gcc/ada/debug.adb | 40 |
1 files changed, 27 insertions, 13 deletions
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index bcb6ee3322c..d0923fcd28a 100644 --- a/gcc/ada/debug.adb +++ b/gcc/ada/debug.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2012, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2013, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -124,17 +124,17 @@ package body Debug is -- d.D Strict Alfa mode -- d.E Force Alfa mode for gnat2why -- d.F Alfa mode - -- d.G Precondition only mode for gnat2why + -- d.G Frame condition mode for gnat2why -- d.H Standard package only mode for gnat2why - -- d.I SCIL generation mode + -- d.I Do not ignore enum representation clauses in CodePeer mode -- d.J Disable parallel SCIL generation mode -- d.K Alfa detection only mode for gnat2why -- d.L Depend on back end for limited types in if and case expressions - -- d.M + -- d.M Relaxed RM semantics -- d.N Add node to all entities -- d.O Dump internal SCO tables -- d.P Previous (non-optimized) handling of length comparisons - -- d.Q + -- d.Q Flow Analysis mode for gnat2why -- d.R Restrictions in ali files in positional form -- d.S Force Optimize_Alignment (Space) -- d.T Force Optimize_Alignment (Time) @@ -143,7 +143,7 @@ package body Debug is -- d.W Print out debugging information for Walk_Library_Items -- d.X Use Expression_With_Actions -- d.Y Do not use Expression_With_Actions - -- d.Z + -- d.Z Dump flow analysis graphs, for debugging purposes (gnat2why) -- d1 Error msgs have node numbers where possible -- d2 Eliminate error flags in verbose form error messages @@ -603,19 +603,22 @@ 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 Precondition only mode for gnat2why. In this mode, gnat2why will - -- only generate Why code that checks for the well-guardedness of - -- preconditions. + -- 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 -- file will be ignored. - -- d.I Generate SCIL mode. Generate intermediate code for the sake of - -- of static analysis tools, and ensure additional tree consistency - -- between different compilations of specs. + -- d.I Do not ignore enum representation clauses in CodePeer mode. + -- The default of ignoring representation clauses for enumeration + -- types in CodePeer is good for the majority of Ada code, but in some + -- cases being able to change this default might be useful to remove + -- some false positives. -- d.J Disable parallel SCIL generation. Normally SCIL file generation is -- done in parallel to speed processing. This switch disables this @@ -629,6 +632,9 @@ package body Debug is -- case expansion, leaving it up to the back end to handle conditional -- expressions correctly. + -- d.M Relaxed RM semantics. This flag sets Opt.Relaxed_RM_Semantics + -- See Opt.Relaxed_RM_Semantics for more details. + -- d.N Enlarge entities by one node (but don't attempt to use this extra -- node for storage of any flags or fields). This can be used to do -- experiments on the impact of increasing entity sizes. @@ -642,6 +648,9 @@ package body Debug is -- This is there in case we find a situation where the optimization -- malfunctions, to provide a work around. + -- d.Q Flow Analysis mode for gnat2why. When this flag is given, + -- gnat2why will do flow analysis, and no translation to Why is done. + -- d.R As documented in lib-writ.ads, restrictions in the ali file can -- have two forms, positional and named. The named notation is the -- current preferred form, but the use of this debug switch will force @@ -674,6 +683,11 @@ package body Debug is -- forces use of the new N_Expression_With_Actions node in these other -- cases and is intended for transitional use. + -- d.Z In gnat2why, in Flow analysis mode (-gnatd.Q), dump the different + -- graphs (control flow, control dependence) for debugging purposes. + -- This debug flag will be removed when flow analysis is sufficiently + -- stable. + -- d.Y Prevents the use of the N_Expression_With_Actions node even in the -- case of the gcc back end. Provided as a back up in case the new -- scheme has problems. |