[Ada] Keep checks in Alfa mode for formal verification

Arnaud Charlet charlet@adacore.com
Mon Oct 29 10:12:00 GMT 2012


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  <moy@adacore.com>

	* gnat1drv.adb (Adjust_Global_Switches): Do not suppress checks
	in Alfa mode.

-------------- next part --------------
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;


More information about the Gcc-patches mailing list