Index: gnat1drv.adb
===================================================================
--- gnat1drv.adb	(revision 194190)
+++ gnat1drv.adb	(working copy)
@@ -201,7 +201,9 @@
 
          Dynamic_Elaboration_Checks := False;
 
-         --  Set STRICT mode for overflow checks if not set explicitly
+         --  Set STRICT mode for overflow checks if not set explicitly. This
+         --  prevents suppressing of overflow checks by default, in code down
+         --  below.
 
          if Suppress_Options.Overflow_Checks_General = Not_Set then
             Suppress_Options.Overflow_Checks_General    := Strict;
@@ -268,6 +270,129 @@
          Try_Semantics := True;
       end if;
 
+      --  Set switches for formal verification mode
+
+      if Debug_Flag_Dot_VV then
+         Formal_Extensions := True;
+      end if;
+
+      if Debug_Flag_Dot_FF then
+         Alfa_Mode := True;
+
+         --  Set strict standard interpretation of compiler permissions
+
+         if Debug_Flag_Dot_DD then
+            Strict_Alfa_Mode := True;
+         end if;
+
+         --  Turn off inlining, which would confuse formal verification output
+         --  and gain nothing.
+
+         Front_End_Inlining := False;
+         Inline_Active      := False;
+
+         --  Disable front-end optimizations, to keep the tree as close to the
+         --  source code as possible, and also to avoid inconsistencies between
+         --  trees when using different optimization switches.
+
+         Optimization_Level := 0;
+
+         --  Enable some restrictions systematically to simplify the generated
+         --  code (and ease analysis). Note that restriction checks are also
+         --  disabled in Alfa mode, see Restrict.Check_Restriction, and user
+         --  specified Restrictions pragmas are ignored, see
+         --  Sem_Prag.Process_Restrictions_Or_Restriction_Warnings.
+
+         Restrict.Restrictions.Set (No_Initialize_Scalars) := True;
+
+         --  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.
+
+         --  Turn off dynamic elaboration checks: generates inconsistencies in
+         --  trees between specs compiled as part of a main unit or as part of
+         --  a with-clause.
+
+         Dynamic_Elaboration_Checks := False;
+
+         --  Set STRICT mode for overflow checks if not set explicitly. This
+         --  prevents suppressing of overflow checks by default, in code down
+         --  below.
+
+         if Suppress_Options.Overflow_Checks_General = Not_Set then
+            Suppress_Options.Overflow_Checks_General    := Strict;
+            Suppress_Options.Overflow_Checks_Assertions := Strict;
+         end if;
+
+         --  Kill debug of generated code, since it messes up sloc values
+
+         Debug_Generated_Code := False;
+
+         --  Turn cross-referencing on in case it was disabled (e.g. by -gnatD)
+         --  as it is needed for computing effects of subprograms in the formal
+         --  verification backend.
+
+         Xref_Active := True;
+
+         --  Polling mode forced off, since it generates confusing junk
+
+         Polling_Required := False;
+
+         --  Set operating mode to Generate_Code, but full front-end expansion
+         --  is not desirable in Alfa mode, so a light expansion is performed
+         --  instead.
+
+         Operating_Mode := Generate_Code;
+
+         --  Skip call to gigi
+
+         Debug_Flag_HH := True;
+
+         --  Disable Expressions_With_Actions nodes
+
+         --  The gnat2why backend does not deal with Expressions_With_Actions
+         --  in all places (in particular assertions). It is difficult to
+         --  determine in the frontend which cases are allowed, so we disable
+         --  Expressions_With_Actions entirely. Even in the cases where
+         --  gnat2why deals with Expressions_With_Actions, it is easier to
+         --  deal with the original constructs (quantified, conditional and
+         --  case expressions) instead of the rewritten ones.
+
+         Use_Expression_With_Actions := False;
+
+         --  Enable assertions and debug pragmas, since they give valuable
+         --  extra information for formal verification.
+
+         Assertions_Enabled    := True;
+         Debug_Pragmas_Enabled := True;
+
+         --  Turn off style check options since we are not interested in any
+         --  front-end warnings when we are getting Alfa output.
+
+         Reset_Style_Check_Options;
+
+         --  Suppress compiler warnings, since what we are interested in here
+         --  is what formal verification can find out.
+
+         Warning_Mode := Suppress;
+
+         --  Suppress the generation of name tables for enumerations, which are
+         --  not needed for formal verification, and fall outside the Alfa
+         --  subset (use of pointers).
+
+         Global_Discard_Names := True;
+
+         --  Suppress the expansion of tagged types and dispatching calls,
+         --  which lead to the generation of non-Alfa code (use of pointers),
+         --  which is more complex to formally verify than the original source.
+
+         Tagged_Type_Expansion := False;
+      end if;
+
       --  Set Configurable_Run_Time mode if system.ads flag set
 
       if Targparm.Configurable_Run_Time_On_Target or Debug_Flag_YY then
@@ -335,8 +460,8 @@
 
       --  Set proper status for overflow check mechanism
 
-      --  If already set (by -gnato or above in CodePeer mode) then we have
-      --  nothing to do.
+      --  If already set (by -gnato or above in Alfa or CodePeer mode) then we
+      --  have nothing to do.
 
       if Opt.Suppress_Options.Overflow_Checks_General /= Not_Set then
          null;
@@ -430,114 +555,6 @@
          Back_End_Handles_Limited_Types := False;
       end if;
 
-      --  Set switches for formal verification mode
-
-      if Debug_Flag_Dot_VV then
-         Formal_Extensions := True;
-      end if;
-
-      if Debug_Flag_Dot_FF then
-         Alfa_Mode := True;
-
-         --  Set strict standard interpretation of compiler permissions
-
-         if Debug_Flag_Dot_DD then
-            Strict_Alfa_Mode := True;
-         end if;
-
-         --  Turn off inlining, which would confuse formal verification output
-         --  and gain nothing.
-
-         Front_End_Inlining := False;
-         Inline_Active      := False;
-
-         --  Disable front-end optimizations, to keep the tree as close to the
-         --  source code as possible, and also to avoid inconsistencies between
-         --  trees when using different optimization switches.
-
-         Optimization_Level := 0;
-
-         --  Enable some restrictions systematically to simplify the generated
-         --  code (and ease analysis). Note that restriction checks are also
-         --  disabled in Alfa mode, see Restrict.Check_Restriction, and user
-         --  specified Restrictions pragmas are ignored, see
-         --  Sem_Prag.Process_Restrictions_Or_Restriction_Warnings.
-
-         Restrict.Restrictions.Set (No_Initialize_Scalars) := True;
-
-         --  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.
-
-         --  Kill debug of generated code, since it messes up sloc values
-
-         Debug_Generated_Code := False;
-
-         --  Turn cross-referencing on in case it was disabled (e.g. by -gnatD)
-         --  as it is needed for computing effects of subprograms in the formal
-         --  verification backend.
-
-         Xref_Active := True;
-
-         --  Polling mode forced off, since it generates confusing junk
-
-         Polling_Required := False;
-
-         --  Set operating mode to Generate_Code, but full front-end expansion
-         --  is not desirable in Alfa mode, so a light expansion is performed
-         --  instead.
-
-         Operating_Mode := Generate_Code;
-
-         --  Skip call to gigi
-
-         Debug_Flag_HH := True;
-
-         --  Disable Expressions_With_Actions nodes
-
-         --  The gnat2why backend does not deal with Expressions_With_Actions
-         --  in all places (in particular assertions). It is difficult to
-         --  determine in the frontend which cases are allowed, so we disable
-         --  Expressions_With_Actions entirely. Even in the cases where
-         --  gnat2why deals with Expressions_With_Actions, it is easier to
-         --  deal with the original constructs (quantified, conditional and
-         --  case expressions) instead of the rewritten ones.
-
-         Use_Expression_With_Actions := False;
-
-         --  Enable assertions and debug pragmas, since they give valuable
-         --  extra information for formal verification.
-
-         Assertions_Enabled    := True;
-         Debug_Pragmas_Enabled := True;
-
-         --  Turn off style check options since we are not interested in any
-         --  front-end warnings when we are getting Alfa output.
-
-         Reset_Style_Check_Options;
-
-         --  Suppress compiler warnings, since what we are interested in here
-         --  is what formal verification can find out.
-
-         Warning_Mode := Suppress;
-
-         --  Suppress the generation of name tables for enumerations, which are
-         --  not needed for formal verification, and fall outside the Alfa
-         --  subset (use of pointers).
-
-         Global_Discard_Names := True;
-
-         --  Suppress the expansion of tagged types and dispatching calls,
-         --  which lead to the generation of non-Alfa code (use of pointers),
-         --  which is more complex to formally verify than the original source.
-
-         Tagged_Type_Expansion := False;
-      end if;
-
       --  If the inlining level has not been set by the user, compute it from
       --  the optimization level: 1 at -O1/-O2 (and -Os), 2 at -O3 and above.
 
