[Ada] Keep checks in Alfa mode for formal verification

Message ID 20121029095843.GA16125@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Oct. 29, 2012, 9:58 a.m.
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.


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;