diff options
| author | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2017-10-14 17:07:35 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2017-10-14 17:07:35 +0000 |
| commit | 92b751fdc698c7b2040f986aaa125e4163003a2d (patch) | |
| tree | 9877668163ec28526d8a074dc94e2f8c2e60e565 /gcc/ada/debug.adb | |
| parent | 2e60feb59198791c0a3b58838af26e6e5cd32677 (diff) | |
| download | gcc-92b751fdc698c7b2040f986aaa125e4163003a2d.zip gcc-92b751fdc698c7b2040f986aaa125e4163003a2d.tar.gz gcc-92b751fdc698c7b2040f986aaa125e4163003a2d.tar.bz2 | |
[multiple changes]
2017-10-14 Eric Botcazou <ebotcazou@adacore.com>
* layout.ads (Set_Elem_Alignment): Add Align parameter defaulted to 0.
* layout.adb (Set_Elem_Alignment): Likewise. Use M name as maximum
alignment for consistency. If Align is non-zero, use the minimum of
Align and M for the alignment.
* cstand.adb (Build_Float_Type): Use Set_Elem_Alignment instead of
setting the alignment directly.
2017-10-14 Ed Schonberg <schonberg@adacore.com>
* sem_prag.adb (Analyze_Pragma, case Check): Defer evaluation of the
optional string in an Assert pragma until the expansion of the pragma
has rewritten it as a conditional statement, so that the string
argument is only evaluaed if the assertion fails. This is mandated by
RM 11.4.2.
2017-10-14 Hristian Kirtchev <kirtchev@adacore.com>
* debug.adb: Switch -gnatd.v and associated flag are now used to
enforce the SPARK rules for elaboration in SPARK code.
* sem_elab.adb: Describe switch -gnatd.v.
(Process_Call): Verify the SPARK rules only when -gnatd.v is in effect.
(Process_Instantiation): Verify the SPARK rules only when -gnatd.v is
in effect.
(Process_Variable_Assignment): Clarify why variable assignments are
processed reglardless of whether -gnatd.v is in effect.
* doc/gnat_ugn/elaboration_order_handling_in_gnat.rst: Update the
sections on elaboration code and compilation switches.
* gnat_ugn.texi: Regenerate.
2017-10-14 Gary Dismukes <dismukes@adacore.com>
* exp_util.adb, freeze.adb, sem_aggr.adb, sem_util.ads, sem_util.adb,
sem_warn.adb: Minor reformattings.
From-SVN: r253757
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. |