2012-12-05 Yannick Moy <moy@adacore.com>

	* gnat1drv.adb (Adjust_Global_Switches): Move setting of flags for
	Alfa mode before general treatment of flags, so that overflow checks
	settings are set appropriately in Alfa mode. Also set the mode to
	STRICT in Alfa mode if not already set by the user.

2012-12-05  Robert Dewar  <dewar@adacore.com>

	* sem_ch3.adb: Minor reformatting.

2012-12-05  Steve Baird  <baird@adacore.com>

	* sinfo.ads: Improve comments about SCIL-related node kinds and selector
	functions.

2012-12-05  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch10.adb (Build_Limited_Views): Even though the unit is
	not analyzed, place its entity on the name in the with clause,
	so that warnings on unused with-clause are properly supported
	for limited withs.

2012-12-05  Robert Dewar  <dewar@adacore.com>

	* gnat_ugn.texi: Update overflow description. Pragma
	Overflow_Checks changed to Overflow_Mode.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@194191 138bc75d-0d04-0410-961f-82ee72b054a4

1 files changed, 128 insertions, 111 deletions

diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 4d0485a9fbd..62fdc4babda 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -201,7 +201,9 @@ procedure Gnat1drv is
 
          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 @@ procedure Gnat1drv is
          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 @@ procedure Gnat1drv is
 
       --  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 @@ procedure Gnat1drv is
          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.