[multiple changes]

2012-10-02  Robert Dewar  <dewar@adacore.com>

	* usage.adb, gnat_rm.texi, vms_data.ads: Add entry for
	/OVERFLOW_CHECKS=?? generating -gnato?? for control
	of extended overflow checking.
	* ug_words: Add entry for -gnato?? for /OVERFLOW_CHECKS=??
	* gnat_ugn.texi: Add documentation for -gnato?? for control of overflow
	checking mode.

2012-10-02  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch4.adb (Analyze_Quantified_Expression): If the iterator in
	a quantified expression is statically known to be null (e.g. a
	array with an empty index type) emit a warning.

From-SVN: r191957

gcc/ada/ChangeLog

 2012-10-02  Robert Dewar  <dewar@adacore.com>
 
+	* usage.adb, gnat_rm.texi, vms_data.ads: Add entry for
+	/OVERFLOW_CHECKS=?? generating -gnato?? for control
+	of extended overflow checking.
+	* ug_words: Add entry for -gnato?? for /OVERFLOW_CHECKS=??
+	* gnat_ugn.texi: Add documentation for -gnato?? for control of overflow
+	checking mode.
+
+2012-10-02  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch4.adb (Analyze_Quantified_Expression): If the iterator in
+	a quantified expression is statically known to be null (e.g. a
+	array with an empty index type) emit a warning.
+
+2012-10-02  Robert Dewar  <dewar@adacore.com>
+
 	* sem_dim.adb: Minor code reorganization.
 	* sem_dim.ads: Add comment.
 

gcc/ada/gnat_rm.texi

@@ -179,6 +179,7 @@ Implementation Defined Pragmas
 * Pragma Obsolescent::
 * Pragma Optimize_Alignment::
 * Pragma Ordered::
+* Pragma Overflow_Checks::
 * Pragma Passive::
 * Pragma Persistent_BSS::
 * Pragma Polling::
@@ -916,6 +917,7 @@ consideration, the use of these pragmas should be minimized.
 * Pragma Obsolescent::
 * Pragma Optimize_Alignment::
 * Pragma Ordered::
+* Pragma Overflow_Checks::
 * Pragma Passive::
 * Pragma Persistent_BSS::
 * Pragma Polling::
@@ -4127,6 +4129,53 @@ as unordered, and will generate warnings for inappropriate uses.
 For additional information please refer to the description of the
 @option{-gnatw.u} switch in the @value{EDITION} User's Guide.
 
+@node Pragma Overflow_Checks
+@unnumberedsec Pragma Overflow_Checks
+@findex Overflow checks
+@findex pragma @code{Overflow_Checks}
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma Overflow_Checks
+ (  [General    =>] MODE
+  [,[Assertions =>] MODE]);
+
+MODE ::= SUPPRESSED | CHECKED | MINIMIZED | ELIMINATED
+@end smallexample
+
+@noindent
+This pragma sets the current overflow mode to the given mode. For details
+of the meaning of these modes, see section on overflow checking in the
+GNAT users guide. If only the @code{General} parameter is present, the
+given mode applies to all expressions. If both parameters are present,
+the @code{General} mode applies to expressions outside assertions, and
+the @code{Eliminated} mode applies to expressions within assertions.
+
+The case of the @code{MODE} parameter is ignored,
+so @code{MINIMIZED}, @code{Minimized} and
+@code{minimized} all have the same effect.
+
+The @code{Overflow_Checks} pragma has the same scoping and placement
+rules as pragma @code{Suppress}, so it can occur either as a
+configuration pragma, specifying a default for the whole
+program, or in a declarative scope, where it applies to the
+remaining declarations and statements in that scope.
+
+The pragma @code{Suppress (Overflow_Check)} sets mode
+
+   General => Suppressed
+
+suppressing all overflow checking within and outside
+assertions.
+
+The pragam @code{Unsuppress (Overflow_Check)} sets mode
+
+   General => Checked
+
+which causes overflow checking of all intermediate overflows.
+This applies both inside and outside assertions.
+
 @node Pragma Passive
 @unnumberedsec Pragma Passive
 @findex Passive

gcc/ada/gnat_ugn.texi

@@ -4325,11 +4325,28 @@ of GNAT other than the JGNAT, .NET or GNAAMP versions), then the use of
 Historically front end inlining was more extensive than the gcc back end
 inlining, but that is no longer the case.
 
+@item -gnato??
+@cindex @option{-gnato??} (@command{gcc})
+Set default overflow cheecking mode. If ?? is a single digit, in the
+range 0-3, it sets the overflow checking mode for all expressions,
+including those outside and within assertions. The meaning of nnn is:
+
+  0   suppress overflow checks (SUPPRESSED)
+  1   all intermediate overflows checked (CHECKED)
+  2   minimize intermediate overflows (MINIMIZED)
+  3   eliminate intermediate overflows (ELIMINATED)
+
+Otherwise ?? can be two digits, both 0-3, and in this case the first
+digit sets the mode (using the above code) for expressions outside an
+assertion, and the second digit sets the mode for expressions within
+an assertion.
+
 @item -gnato
 @cindex @option{-gnato} (@command{gcc})
 Enable numeric overflow checking (which is not normally enabled by
 default). Note that division by zero is a separate check that is not
 controlled by this switch (division by zero checking is on by default).
+The checking mode is set to CHECKED (equivalent to @option{-gnato11}).
 
 @item -gnatp
 @cindex @option{-gnatp} (@command{gcc})

gcc/ada/sem_ch4.adb

@@ -3404,6 +3404,38 @@ package body Sem_Ch4 is
    procedure Analyze_Quantified_Expression (N : Node_Id) is
       QE_Scop : Entity_Id;
 
+      function  Is_Empty_Range (Typ : Entity_Id) return Boolean;
+      --  If the iterator is part of a quantified expression, and the range is
+      --  known to be statically empty, emit a warning and replace expression
+      --  with its static value.
+
+      function  Is_Empty_Range (Typ : Entity_Id) return Boolean is
+         Loc     : constant Source_Ptr := Sloc (N);
+
+      begin
+         if Is_Array_Type (Typ)
+           and then Size_Known_At_Compile_Time (Typ)
+           and then RM_Size (Typ) = 0
+         then
+            if All_Present (N) then
+               Error_Msg_N ("?universal quantified expression "
+               & "over a null range has value True", N);
+               Rewrite (N, New_Occurrence_Of (Standard_True, Loc));
+
+            else
+               Error_Msg_N ("?existential quantified expression "
+               & "over a null range has value False", N);
+               Rewrite (N, New_Occurrence_Of (Standard_False, Loc));
+            end if;
+
+            Analyze (N);
+            return True;
+
+         else
+            return False;
+         end if;
+      end Is_Empty_Range;
+
    begin
       Check_SPARK_Restriction ("quantified expression is not allowed", N);
 
@@ -3425,6 +3457,13 @@ package body Sem_Ch4 is
 
       if Present (Iterator_Specification (N)) then
          Preanalyze (Iterator_Specification (N));
+
+         if Is_Entity_Name (Name (Iterator_Specification (N)))
+           and then Is_Empty_Range (Etype (Name (Iterator_Specification (N))))
+         then
+            return;
+         end if;
+
       else
          Preanalyze (Loop_Parameter_Specification (N));
       end if;

gcc/ada/ug_words

@@ -88,6 +88,7 @@ gcc -c          ^ GNAT COMPILE
 -gnatn2         ^ /INLINE=PRAGMA_LEVEL_2
 -gnatN          ^ /INLINE=FULL
 -gnato          ^ /CHECKS=OVERFLOW
+-gnato??        ^ /OVERFLOW_CHECKS=??
 -gnatp          ^ /CHECKS=SUPPRESS_ALL
 -gnat-p         ^ /CHECKS=UNSUPPRESS_ALL
 -gnatP          ^ /POLLING

gcc/ada/usage.adb

@@ -319,7 +319,15 @@ begin
    --  Line for -gnato switch
 
    Write_Switch_Char ("o");
-   Write_Line ("Enable overflow checking (off by default)");
+   Write_Line ("Enable overflow checking mode to CHECKED (off by default)");
+
+   --  Line for -gnato? switch
+
+   Write_Switch_Char ("o?");
+   Write_Line ("Set SUPPRESSED/CHECKED/MINIMIZED/ELIMINATED (?=0/1/2/3) mode");
+
+   Write_Switch_Char ("o??");
+   Write_Line ("Set mode for general/assertion expressions separately");
 
    --  Line for -gnatO switch
 

gcc/ada/vms_data.ads

@@ -1347,12 +1347,13 @@ package VMS_Data is
    --                      if the /CHECKS qualifier is not present on the
    --                      command line. Same as /NOCHECKS.
    --
-   --     OVERFLOW        Enables overflow checking for integer operations and
-   --                     checks for access before elaboration on subprogram
-   --                     calls. This causes GNAT to generate slower and larger
-   --                     executable programs by adding code to check for both
-   --                     overflow and division by zero (resulting in raising
-   --                     "Constraint_Error" as required by Ada semantics).
+   --     OVERFLOW        Enables overflow checking in CHECKED mode for integer
+   --                     operations and checks for access before elaboration
+   --                     on subprogram calls. This causes GNAT to generate
+   --                     slower and larger executable programs by adding code
+   --                     to check for both overflow and division by zero
+   --                     (resulting in raising "Constraint_Error" as required
+   --                     by Ada semantics).
    --                     Similarly, GNAT does not generate elaboration check
    --                     by default, and you must specify this keyword to
    --                     enable them.
@@ -2108,6 +2109,24 @@ package VMS_Data is
    --   file xyz.adb is compiled with -gnatl=.lst, then the output is written
    --   to file xyz.adb_lst.
 
+   S_GCC_Overflo : aliased constant S := "/OVERFLOW_CHECKS=#"              &
+                                             "-gnato#";
+   --        /OVERFLOW_CHECKS=nn
+   --
+   --   Set default overflow cheecking mode. If nn is a single digit, in the
+   --   range 0-3, it sets the overflow checking mode for all expressions,
+   --   including those outside and within assertions. The meaning of nnn is:
+   --
+   --     0   suppress overflow checks (SUPPRESSED)
+   --     1   all intermediate overflows checked (CHECKED)
+   --     2   minimize intermediate overflows (MINIMIZED)
+   --     3   eliminate intermediate overflows (ELIMINATED)
+   --
+   --   Otherwise nn can be two digits, both 0-3, and in this case the first
+   --   digit sets the mode (using the above code) for expressions outside an
+   --   assertion, and the second digit sets the mode for expressions within
+   --   an assertion.
+
    S_GCC_Pointer : aliased constant S := "/POINTER_SIZE="                  &
                                             "64 "                          &
                                                "-mmalloc64 "               &
@@ -3622,6 +3641,7 @@ package VMS_Data is
                      S_GCC_NoWarnP 'Access,
                      S_GCC_Opt     'Access,
                      S_GCC_OptX    'Access,
+                     S_GCC_Overflo 'Access,
                      S_GCC_Pointer 'Access,
                      S_GCC_Polling 'Access,
                      S_GCC_Project 'Access,