Checks were suppressed to avoid undesired expansion in Alfa mode. It turns out
these checks are needed during semantic analysis for the frontend to properly
mark nodes as needing or not a run-time check, and the special expansion done
in Alfa mode prevents the undesired expansion of checks. So reenable checks in
Alfa mode.
Tested on x86_64-pc-linux-gnu, committed on trunk
2012-10-29 Yannick Moy <m...@adacore.com>
* gnat1drv.adb (Adjust_Global_Switches): Do not suppress checks
in Alfa mode.
Index: gnat1drv.adb
===================================================================
--- gnat1drv.adb (revision 192908)
+++ gnat1drv.adb (working copy)
@@ -419,7 +419,6 @@
-- Set switches for formal verification mode
if Debug_Flag_Dot_FF then
-
Alfa_Mode := True;
-- Set strict standard interpretation of compiler permissions
@@ -448,16 +447,14 @@
Restrict.Restrictions.Set (No_Initialize_Scalars) := True;
- -- Suppress all language checks since they are handled implicitly by
- -- the formal verification backend.
- -- Turn off dynamic elaboration checks.
- -- Turn off alignment checks.
- -- Turn off validity checking.
+ -- Note: at this point we used to suppress various checks, but that
+ -- is not what we want. We need the semantic processing for these
+ -- checks (which will set flags like Do_Overflow_Check, showing the
+ -- points at which potential checks are required semantically). We
+ -- don't want the expansion associated with these checks, but that
+ -- happens anyway because this expansion is simply not done in the
+ -- Alfa version of the expander.
- Suppress_Options := Suppress_All;
- Dynamic_Elaboration_Checks := False;
- Reset_Validity_Check_Options;
-
-- Kill debug of generated code, since it messes up sloc values
Debug_Generated_Code := False;
