diff options
Diffstat (limited to 'gcc/ada/debug.adb')
| -rw-r--r-- | gcc/ada/debug.adb | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index 4e74720..2a81204 100644 --- a/gcc/ada/debug.adb +++ b/gcc/ada/debug.adb @@ -112,7 +112,7 @@ package body Debug is -- d.s Strict secondary stack management -- d.t Disable static allocation of library level dispatch tables -- d.u Enable Modify_Tree_For_C (update tree for c) - -- d.v + -- d.v Enforce SPARK elaboration rules in SPARK code -- d.w Do not check for infinite loops -- d.x No exception handlers -- d.y Disable implicit pragma Elaborate_All on task bodies @@ -600,6 +600,13 @@ package body Debug is -- d.u Sets Modify_Tree_For_C mode in which tree is modified to make it -- easier to generate code using a C compiler. + -- d.v This flag enforces the elaboration rules defined in the SPARK + -- Reference Manual, chapter 7.7, to all SPARK code within a unit. As + -- a result, constructs which violate the rules in chapter 7.7 are no + -- longer accepted, even if the implementation is able to statically + -- ensure that accepting these constructs does not introduce the + -- possibility of failing an elaboration check. + -- d.w This flag turns off the scanning of loops to detect possible -- infinite loops. |