checks.ads, [...]: Minor changes throughout for new overflow checking.

2012-11-06  Robert Dewar  <dewar@adacore.com>

	* checks.ads, checks.adb, exp_ch4.adb: Minor changes throughout for
	new overflow checking.
	* exp_util.adb (Insert_Actions): Remove special casing of
	Overflow_Check.
	* gnat1drv.adb (Adjust_Global_Switches): Fixes for new handling
	of overflow checks.
	* sem.adb (Analyze): Remove special casing of Overflow_Check
	(Analyze_List): ditto.
	* sem_prag.adb (Analyze_Pragma, case Overflow_Checks): Remove
	SUPPRESSED and change CHECKED to STRICT.
	* sem_res.adb (Analyze_And_Resolve): No longer treat
	Overflow_Check specially.
	(Preanalyze_And_Resolve): ditto.
	(Resolve): ditto.
	* snames.ads-tmpl: Replace Name_Checked by Name_Strict.
	* switch-c.adb (Get_Overflow_Mode): Eliminate 0 setting,
	CHECKED => STRICT.
	* types.ads (Overflow_Check_Type): Remove Suppressed, change
	Checked to Strict (Suppress_Record): Overflow check controlled
	by Suppress array.

From-SVN: r193233

gcc/ada/ChangeLog

+2012-11-06  Robert Dewar  <dewar@adacore.com>
+
+	* checks.ads, checks.adb, exp_ch4.adb: Minor changes throughout for
+	new overflow checking.
+	* exp_util.adb (Insert_Actions): Remove special casing of
+	Overflow_Check.
+	* gnat1drv.adb (Adjust_Global_Switches): Fixes for new handling
+	of overflow checks.
+	* sem.adb (Analyze): Remove special casing of Overflow_Check
+	(Analyze_List): ditto.
+	* sem_prag.adb (Analyze_Pragma, case Overflow_Checks): Remove
+	SUPPRESSED and change CHECKED to STRICT.
+	* sem_res.adb (Analyze_And_Resolve): No longer treat
+	Overflow_Check specially.
+	(Preanalyze_And_Resolve): ditto.
+	(Resolve): ditto.
+	* snames.ads-tmpl: Replace Name_Checked by Name_Strict.
+	* switch-c.adb (Get_Overflow_Mode): Eliminate 0 setting,
+	CHECKED => STRICT.
+	* types.ads (Overflow_Check_Type): Remove Suppressed, change
+	Checked to Strict (Suppress_Record): Overflow check controlled
+	by Suppress array.
+
 2012-11-06  Ed Schonberg  <schonberg@adacore.com>
 
 	* sem_res.adb (Preanalyze_And_Resolve): In Alfa mode do not

gcc/ada/checks.ads

@@ -72,12 +72,11 @@ package Checks is
    --  determine whether check C is suppressed either on the entity E or
    --  as the result of a scope suppress pragma. If Checks_May_Be_Suppressed
    --  is False, then the status of the check can be determined simply by
-   --  examining Scope_Checks (C), so this routine is not called in that case.
+   --  examining Scope_Suppress, so this routine is not called in that case.
 
-   function Overflow_Check_Mode (E : Entity_Id) return Overflow_Check_Type;
+   function Overflow_Check_Mode return Overflow_Check_Type;
    --  Returns current overflow checking mode, taking into account whether
-   --  we are inside an assertion expression. Always returns Suppressed if
-   --  overflow checks are suppressed for entity E.
+   --  we are inside an assertion expression.
 
    -------------------------------------------
    -- Procedures to Activate Checking Flags --
@@ -142,7 +141,10 @@ package Checks is
    --  overflow checking for dependent expressions. This routine handles
    --  front end vs back end overflow checks (in the front end case it expands
    --  the necessary check). Note that divide is handled separately using
-   --  Apply_Divide_Checks.
+   --  Apply_Divide_Checks. Node N may or may not have Do_Overflow_Check.
+   --  In STRICT mode, there is nothing to do if this flag is off, but in
+   --  MINIMIZED/ELIMINATED mode we still have to deal with possible use
+   --  of doing operations in Long_Long_Integer or Bignum mode.
 
    procedure Apply_Constraint_Check
      (N          : Node_Id;
@@ -266,15 +268,16 @@ package Checks is
    --  Insert_Action of the whole block (it is returned unanalyzed). The Loc
    --  parameter is used to supply Sloc values for the constructed tree.
 
-   procedure Minimize_Eliminate_Overflow_Checks
+   procedure Minimize_Eliminate_Overflows
      (N         : Node_Id;
       Lo        : out Uint;
       Hi        : out Uint;
       Top_Level : Boolean);
    --  This is the main routine for handling MINIMIZED and ELIMINATED overflow
-   --  checks. On entry N is a node whose result is a signed integer subtype.
-   --  If the node is an arithmetic operation, then a range analysis is carried
-   --  out, and there are three possibilities:
+   --  processing. On entry N is a node whose result is a signed integer
+   --  subtype. The Do_Overflow_Check flag may or may not be set on N. If the
+   --  node is an arithmetic operation, then a range analysis is carried out,
+   --  and there are three possibilities:
    --
    --    The node is left unchanged (apart from expansion of an exponentiation
    --    operation). This happens if the routine can determine that the result
@@ -313,16 +316,16 @@ package Checks is
    --  The routine is called in three situations if we are operating in either
    --  MINIMIZED or ELIMINATED modes.
    --
-   --    Overflow checks applied to the top node of an expression tree when
+   --    Overflow processing applied to the top node of an expression tree when
    --    that node is an arithmetic operator. In this case the result is
    --    converted to the appropriate result type (there is special processing
    --    when the parent is a conversion, see body for details).
    --
-   --    Overflow checks are applied to the operands of a comparison operation.
+   --    Overflow processing applied to the operands of a comparison operation.
    --    In this case, the comparison is done on the result Long_Long_Integer
    --    or Bignum values, without raising any exceptions.
    --
-   --    Overflow checks are applied to the left operand of a membership test.
+   --    Overflow processing applied to the left operand of a membership test.
    --    In this case no exception is raised if a Long_Long_Integer or Bignum
    --    result is outside the range of the type of that left operand (it is
    --    just that the result of IN is false in that case).
@@ -332,13 +335,13 @@ package Checks is
    --
    --  Top_Level is used to avoid inefficient unnecessary transitions into the
    --  Bignum domain. If Top_Level is True, it means that the caller will have
-   --  to convert any Bignum value back to Long_Long_Integer, checking that the
-   --  value is in range. This is the normal case for a top level operator in
-   --  a subexpression. There is no point in going into Bignum mode to avoid an
-   --  overflow just so we can check for overflow the next moment. For calls
-   --  from comparisons and membership tests, and for all recursive calls, we
-   --  do want to transition into the Bignum domain if necessary. Note that
-   --  this setting is only relevant in ELIMINATED mode.
+   --  to convert any Bignum value back to Long_Long_Integer, possibly checking
+   --  that the value is in range. This is the normal case for a top level
+   --  operator in a subexpression. There is no point in going into Bignum mode
+   --  to avoid an overflow just so we can check for overflow the next moment.
+   --  For calls from comparisons and membership tests, and for all recursive
+   --  calls, we do want to transition into the Bignum domain if necessary.
+   --  Note that this setting is only relevant in ELIMINATED mode.
 
    -------------------------------------------------------
    -- Control and Optimization of Range/Overflow Checks --
@@ -370,9 +373,7 @@ package Checks is
    --  has no effect. If a check is needed then this routine sets the flag
    --  Do_Overflow_Check in node N to True, unless it can be determined that
    --  the check is not needed. The only condition under which this is the
-   --  case is if there was an identical check earlier on. These optimziations
-   --  apply to CHECKED mode, but not to MINIMIZED/ELIMINATED modes. See the
-   --  body for a full explanation.
+   --  case is if there was an identical check earlier on.
 
    procedure Enable_Range_Check (N : Node_Id);
    --  Set Do_Range_Check flag in node N True, unless it can be determined

gcc/ada/exp_ch4.adb

@@ -213,19 +213,19 @@ package body Exp_Ch4 is
    --  Convert_To_Actual_Subtype if necessary).
 
    function Minimized_Eliminated_Overflow_Check (N : Node_Id) return Boolean;
-   --  For signed arithmetic operations with Do_Overflow_Check set when the
-   --  current overflow mode is MINIMIZED or ELIMINATED, we need to make a
-   --  call to Apply_Arithmetic_Overflow_Checks as the first thing we do. We
-   --  then return. We count on the recursive apparatus for overflow checks
-   --  to call us back with an equivalent operation that does not have the
-   --  Do_Overflow_Check flag set, and that is when we will proceed with the
-   --  expansion of the operator (e.g. converting X+0 to X, or X**2 to X*X).
-   --  We cannot do these optimizations without first making this check, since
-   --  there may be operands further down the tree that are relying on the
-   --  recursive calls triggered by the top level nodes to properly process
-   --  overflow checking and remaining expansion on these nodes. Note that
-   --  this call back may be skipped if the operation is done in Bignum mode
-   --  but that's fine, since the Bignum call takes care of everything.
+   --  For signed arithmetic operations when the current overflow mode is
+   --  MINIMIZED or ELIMINATED, we must call Apply_Arithmetic_Overflow_Checks
+   --  as the first thing we do. We then return. We count on the recursive
+   --  apparatus for overflow checks to call us back with an equivalent
+   --  operation that is in CHECKED mode, avoiding a recursive entry into this
+   --  routine, and that is when we will proceed with the expansion of the
+   --  operator (e.g. converting X+0 to X, or X**2 to X*X). We cannot do
+   --  these optimizations without first making this check, since there may be
+   --  operands further down the tree that are relying on the recursive calls
+   --  triggered by the top level nodes to properly process overflow checking
+   --  and remaining expansion on these nodes. Note that this call back may be
+   --  skipped if the operation is done in Bignum mode but that's fine, since
+   --  the Bignum call takes care of everything.
 
    procedure Optimize_Length_Comparison (N : Node_Id);
    --  Given an expression, if it is of the form X'Length op N (or the other
@@ -2274,8 +2274,8 @@ package body Exp_Ch4 is
       LLIB : constant Entity_Id := Base_Type (Standard_Long_Long_Integer);
       --  Entity for Long_Long_Integer'Base
 
-      Check : constant Overflow_Check_Type := Overflow_Check_Mode (Empty);
-      --  Current checking mode
+      Check : constant Overflow_Check_Type := Overflow_Check_Mode;
+      --  Current overflow checking mode
 
       procedure Set_True;
       procedure Set_False;
@@ -2320,9 +2320,9 @@ package body Exp_Ch4 is
       --  our operands using the Minimize_Eliminate circuitry which applies
       --  this processing to the two operand subtrees.
 
-      Minimize_Eliminate_Overflow_Checks
+      Minimize_Eliminate_Overflows
         (Left_Opnd (N),  Llo, Lhi, Top_Level => False);
-      Minimize_Eliminate_Overflow_Checks
+      Minimize_Eliminate_Overflows
         (Right_Opnd (N), Rlo, Rhi, Top_Level => False);
 
       --  See if the range information decides the result of the comparison.
@@ -3721,7 +3721,7 @@ package body Exp_Ch4 is
       --  Entity for Long_Long_Integer'Base (Standard should export this???)
 
    begin
-      Minimize_Eliminate_Overflow_Checks (Lop, Lo, Hi, Top_Level => False);
+      Minimize_Eliminate_Overflows (Lop, Lo, Hi, Top_Level => False);
 
       --  If right operand is a subtype name, and the subtype name has no
       --  predicate, then we can just replace the right operand with an
@@ -3751,9 +3751,9 @@ package body Exp_Ch4 is
       --  have not been processed for minimized or eliminated checks.
 
       if Nkind (Rop) = N_Range then
-         Minimize_Eliminate_Overflow_Checks
+         Minimize_Eliminate_Overflows
            (Low_Bound (Rop), Lo, Hi, Top_Level => False);
-         Minimize_Eliminate_Overflow_Checks
+         Minimize_Eliminate_Overflows
            (High_Bound (Rop), Lo, Hi, Top_Level => False);
 
          --  We have A in B .. C, treated as  A >= B and then A <= C
@@ -5498,7 +5498,7 @@ package body Exp_Ch4 is
          --  in which case, this usage makes sense, and in any case, we have
          --  actually eliminated the danger of optimization above.
 
-         if Overflow_Check_Mode (Restyp) not in Minimized_Or_Eliminated then
+         if Overflow_Check_Mode not in Minimized_Or_Eliminated then
             Error_Msg_N ("?explicit membership test may be optimized away", N);
             Error_Msg_N -- CODEFIX
               ("\?use ''Valid attribute instead", N);
@@ -5526,7 +5526,7 @@ package body Exp_Ch4 is
       --  type, then expand with a separate procedure. Note the use of the
       --  flag No_Minimize_Eliminate to prevent infinite recursion.
 
-      if Overflow_Check_Mode (Empty) in Minimized_Or_Eliminated
+      if Overflow_Check_Mode in Minimized_Or_Eliminated
         and then Is_Signed_Integer_Type (Ltyp)
         and then not No_Minimize_Eliminate (N)
       then
@@ -11785,8 +11785,7 @@ package body Exp_Ch4 is
    begin
       return
         Is_Signed_Integer_Type (Etype (N))
-          and then Do_Overflow_Check (N)
-          and then Overflow_Check_Mode (Empty) in Minimized_Or_Eliminated;
+          and then Overflow_Check_Mode in Minimized_Or_Eliminated;
    end Minimized_Eliminated_Overflow_Check;
 
    --------------------------------

gcc/ada/exp_util.adb

@@ -3840,11 +3840,11 @@ package body Exp_Util is
    begin
       if Suppress = All_Checks then
          declare
-            Svg : constant Suppress_Record := Scope_Suppress;
+            Sva : constant Suppress_Array := Scope_Suppress.Suppress;
          begin
-            Scope_Suppress := Suppress_All;
+            Scope_Suppress.Suppress := (others => True);
             Insert_Actions (Assoc_Node, Ins_Actions);
-            Scope_Suppress := Svg;
+            Scope_Suppress.Suppress := Sva;
          end;
 
       else
@@ -6727,7 +6727,7 @@ package body Exp_Util is
 
       --  All this must not have any checks
 
-      Scope_Suppress := Suppress_All;
+      Scope_Suppress.Suppress := (others => True);
 
       --  If it is a scalar type and we need to capture the value, just make
       --  a copy. Likewise for a function call, an attribute reference, an

gcc/ada/gnat1drv.adb

@@ -192,14 +192,12 @@ procedure Gnat1drv is
 
          --  Enable all other language checks
 
-         Suppress_Options :=
-           (Suppress                   => (Access_Check      => True,
-                                           Alignment_Check   => True,
-                                           Division_Check    => True,
-                                           Elaboration_Check => True,
-                                           others            => False),
-            Overflow_Checks_General    => Suppressed,
-            Overflow_Checks_Assertions => Suppressed);
+         Suppress_Options.Suppress :=
+           (Access_Check      => True,
+            Alignment_Check   => True,
+            Division_Check    => True,
+            Elaboration_Check => True,
+            others            => False);
 
          Dynamic_Elaboration_Checks := False;
 
@@ -328,42 +326,50 @@ procedure Gnat1drv is
          Exception_Mechanism := Back_End_Exceptions;
       end if;
 
-      --  Set proper status for overflow checks
+      --  Set proper status for overflow check mechanism
 
-      --  If already set (by - gnato or -gnatp) then we have nothing to do
+      --  If already set (by -gnato) then we have nothing to do
 
       if Opt.Suppress_Options.Overflow_Checks_General /= Not_Set then
          null;
 
-      --  Otherwise set appropriate default mode. Note: at present we set
-      --  SUPPRESSED in all three of the following cases. They are separated
-      --  because in the future we may make different choices.
+      --  Otherwise set overflow mode defaults
 
-      --  By default suppress overflow checks in -gnatg mode
+      else
+         --  Otherwise set overflow checks off by default
 
-      elsif GNAT_Mode then
-         Suppress_Options.Overflow_Checks_General    := Suppressed;
-         Suppress_Options.Overflow_Checks_Assertions := Suppressed;
+         Suppress_Options.Suppress (Overflow_Check) := True;
 
-      --  If we have backend divide and overflow checks, then by default
-      --  overflow checks are suppressed. Historically this code used to
-      --  activate overflow checks, although no target currently has these
-      --  flags set, so this was dead code anyway.
+         --  Set appropriate default overflow handling mode. Note: at present
+         --  we set STRICT in all three of the following cases. They are
+         --  separated because in the future we may make different choices.
 
-      elsif Targparm.Backend_Divide_Checks_On_Target
-              and
-            Targparm.Backend_Overflow_Checks_On_Target
-      then
-         Suppress_Options.Overflow_Checks_General    := Suppressed;
-         Suppress_Options.Overflow_Checks_Assertions := Suppressed;
+         --  By default set STRICT mode if -gnatg in effect
 
-      --  Otherwise for now, default is checks are suppressed. This is subject
-      --  to change in the future, but for now this is the compatible behavior
-      --  with previous versions of GNAT.
+         if GNAT_Mode then
+            Suppress_Options.Overflow_Checks_General    := Strict;
+            Suppress_Options.Overflow_Checks_Assertions := Strict;
 
-      else
-         Suppress_Options.Overflow_Checks_General    := Suppressed;
-         Suppress_Options.Overflow_Checks_Assertions := Suppressed;
+         --  If we have backend divide and overflow checks, then by default
+         --  overflow checks are STRICT. Historically this code used to also
+         --  activate overflow checks, although no target currently has these
+         --  flags set, so this was dead code anyway.
+
+         elsif Targparm.Backend_Divide_Checks_On_Target
+           and
+             Targparm.Backend_Overflow_Checks_On_Target
+         then
+            Suppress_Options.Overflow_Checks_General    := Strict;
+            Suppress_Options.Overflow_Checks_Assertions := Strict;
+
+         --  Otherwise for now, default is STRICT mode. This may change in the
+         --  future, but for now this is the compatible behavior with previous
+         --  versions of GNAT.
+
+         else
+            Suppress_Options.Overflow_Checks_General    := Strict;
+            Suppress_Options.Overflow_Checks_Assertions := Strict;
+         end if;
       end if;
 
       --  Set default for atomic synchronization. As this synchronization

gcc/ada/sem.adb

@@ -723,29 +723,15 @@ package body Sem is
    begin
       if Suppress = All_Checks then
          declare
-            Svg : constant Suppress_Record := Scope_Suppress;
+            Svs : constant Suppress_Array := Scope_Suppress.Suppress;
          begin
-            Scope_Suppress := Suppress_All;
+            Scope_Suppress.Suppress := (others => True);
             Analyze (N);
-            Scope_Suppress := Svg;
+            Scope_Suppress.Suppress := Svs;
          end;
 
       elsif Suppress = Overflow_Check then
          declare
-            Svg : constant Overflow_Check_Type :=
-                    Scope_Suppress.Overflow_Checks_General;
-            Sva : constant Overflow_Check_Type :=
-                    Scope_Suppress.Overflow_Checks_Assertions;
-         begin
-            Scope_Suppress.Overflow_Checks_General    := Suppressed;
-            Scope_Suppress.Overflow_Checks_Assertions := Suppressed;
-            Analyze (N);
-            Scope_Suppress.Overflow_Checks_General    := Svg;
-            Scope_Suppress.Overflow_Checks_Assertions := Sva;
-         end;
-
-      else
-         declare
             Svg : constant Boolean := Scope_Suppress.Suppress (Suppress);
          begin
             Scope_Suppress.Suppress (Suppress) := True;
@@ -776,25 +762,11 @@ package body Sem is
    begin
       if Suppress = All_Checks then
          declare
-            Svg : constant Suppress_Record := Scope_Suppress;
-         begin
-            Scope_Suppress := Suppress_All;
-            Analyze_List (L);
-            Scope_Suppress := Svg;
-         end;
-
-      elsif Suppress = Overflow_Check then
-         declare
-            Svg : constant Overflow_Check_Type :=
-                    Scope_Suppress.Overflow_Checks_General;
-            Sva : constant Overflow_Check_Type :=
-                    Scope_Suppress.Overflow_Checks_Assertions;
+            Svs : constant Suppress_Array := Scope_Suppress.Suppress;
          begin
-            Scope_Suppress.Overflow_Checks_General    := Suppressed;
-            Scope_Suppress.Overflow_Checks_Assertions := Suppressed;
+            Scope_Suppress.Suppress := (others => True);
             Analyze_List (L);
-            Scope_Suppress.Overflow_Checks_General    := Svg;
-            Scope_Suppress.Overflow_Checks_Assertions := Sva;
+            Scope_Suppress.Suppress := Svs;
          end;
 
       else
@@ -1051,11 +1023,11 @@ package body Sem is
    begin
       if Suppress = All_Checks then
          declare
-            Svg : constant Suppress_Record := Scope_Suppress;
+            Svs : constant Suppress_Array := Scope_Suppress.Suppress;
          begin
-            Scope_Suppress := Suppress_All;
+            Scope_Suppress.Suppress := (others => True);
             Insert_After_And_Analyze (N, M);
-            Scope_Suppress := Svg;
+            Scope_Suppress.Suppress := Svs;
          end;
 
       else
@@ -1111,11 +1083,11 @@ package body Sem is
    begin
       if Suppress = All_Checks then
          declare
-            Svg : constant Suppress_Record := Scope_Suppress;
+            Svs : constant Suppress_Array := Scope_Suppress.Suppress;
          begin
-            Scope_Suppress := Suppress_All;
+            Scope_Suppress.Suppress := (others => True);
             Insert_Before_And_Analyze (N, M);
-            Scope_Suppress := Svg;
+            Scope_Suppress.Suppress := Svs;
          end;
 
       else
@@ -1170,11 +1142,11 @@ package body Sem is
    begin
       if Suppress = All_Checks then
          declare
-            Svg : constant Suppress_Record := Scope_Suppress;
+            Svs : constant Suppress_Array := Scope_Suppress.Suppress;
          begin
-            Scope_Suppress := Suppress_All;
+            Scope_Suppress.Suppress := (others => True);
             Insert_List_After_And_Analyze (N, L);
-            Scope_Suppress := Svg;
+            Scope_Suppress.Suppress := Svs;
          end;
 
       else
@@ -1228,11 +1200,11 @@ package body Sem is
    begin
       if Suppress = All_Checks then
          declare
-            Svg : constant Suppress_Record := Scope_Suppress;
+            Svs : constant Suppress_Array := Scope_Suppress.Suppress;
          begin
-            Scope_Suppress := Suppress_All;
+            Scope_Suppress.Suppress := (others => True);
             Insert_List_Before_And_Analyze (N, L);
-            Scope_Suppress := Svg;
+            Scope_Suppress.Suppress := Svs;
          end;
 
       else

gcc/ada/sem_prag.adb

@@ -2121,7 +2121,8 @@ package body Sem_Prag is
               (Get_Pragma_Arg (Arg2), Standard_String);
          end if;
 
-         --  Record if pragma is disabled
+         --  For a pragma in the extended main source unit, record enabled
+         --  status in SCO (note: there is never any SCO for an instance).
 
          if Check_Enabled (Pname) then
             Set_SCO_Pragma_Enabled (Loc);
@@ -5058,7 +5059,8 @@ package body Sem_Prag is
 
                   --  If previous error, avoid cascaded errors
 
-                  Applies := True;
+                  Cascaded_Error;
+                  Applies   := True;
                   Effective := True;
 
                else
@@ -5703,18 +5705,6 @@ package body Sem_Prag is
               ("argument of pragma% is not valid check name", Arg1);
          end if;
 
-         --  Special processing for overflow check case
-
-         if C = All_Checks or else C = Overflow_Check then
-            if Suppress_Case then
-               Scope_Suppress.Overflow_Checks_General    := Suppressed;
-               Scope_Suppress.Overflow_Checks_Assertions := Suppressed;
-            else
-               Scope_Suppress.Overflow_Checks_General    := Checked;
-               Scope_Suppress.Overflow_Checks_Assertions := Checked;
-            end if;
-         end if;
-
          if Arg_Count = 1 then
 
             --  Make an entry in the local scope suppress table. This is the
@@ -12007,10 +11997,11 @@ package body Sem_Prag is
          --  pragma Overflow_Checks
          --    ([General => ] MODE [, [Assertions => ] MODE]);
 
-         --  MODE := SUPPRESSED | CHECKED | MINIMIZED | ELIMINATED
+         --  MODE := STRICT | MINIMIZED | ELIMINATED
 
          --  Note: ELIMINATED is allowed only if Long_Long_Integer'Size is 64
-         --  since System.Bignums makes this assumption.
+         --  since System.Bignums makes this assumption. This is true of nearly
+         --  all (all?) targets.
 
          when Pragma_Overflow_Checks => Overflow_Checks : declare
             function Get_Check_Mode
@@ -12034,19 +12025,8 @@ package body Sem_Prag is
                Check_Optional_Identifier (Arg, Name);
                Check_Arg_Is_Identifier (Argx);
 
-               --  Do not suppress overflow checks for formal verification.
-               --  Instead, require that a check is inserted so that formal
-               --  verification can detect wraparound errors.
-
-               if Chars (Argx) = Name_Suppressed then
-                  if Alfa_Mode then
-                     return Checked;
-                  else
-                     return Suppressed;
-                  end if;
-
-               elsif Chars (Argx) = Name_Checked then
-                  return Checked;
+               if Chars (Argx) = Name_Strict then
+                  return Strict;
 
                elsif Chars (Argx) = Name_Minimized then
                   return Minimized;
@@ -14545,6 +14525,7 @@ package body Sem_Prag is
             --  Note: in previous versions of GNAT we used to check for limited
             --  types and give an error, but in fact the standard does allow
             --  Unchecked_Union on limited types, so this check was removed.
+
             --  Similarly, GNAT used to require that all discriminants have
             --  default values, but this is not mandated by the RM.
 

gcc/ada/sem_res.adb

@@ -334,25 +334,11 @@ package body Sem_Res is
    begin
       if Suppress = All_Checks then
          declare
-            Svg : constant Suppress_Record := Scope_Suppress;
+            Sva : constant Suppress_Array := Scope_Suppress.Suppress;
          begin
-            Scope_Suppress := Suppress_All;
+            Scope_Suppress.Suppress := (others => True);
             Analyze_And_Resolve (N, Typ);
-            Scope_Suppress := Svg;
-         end;
-
-      elsif Suppress = Overflow_Check then
-         declare
-            Svg : constant Overflow_Check_Type :=
-                    Scope_Suppress.Overflow_Checks_General;
-            Sva : constant Overflow_Check_Type :=
-                    Scope_Suppress.Overflow_Checks_Assertions;
-         begin
-            Scope_Suppress.Overflow_Checks_General    := Suppressed;
-            Scope_Suppress.Overflow_Checks_Assertions := Suppressed;
-            Analyze_And_Resolve (N, Typ);
-            Scope_Suppress.Overflow_Checks_General    := Svg;
-            Scope_Suppress.Overflow_Checks_Assertions := Sva;
+            Scope_Suppress.Suppress := Sva;
          end;
 
       else
@@ -388,25 +374,11 @@ package body Sem_Res is
    begin
       if Suppress = All_Checks then
          declare
-            Svg : constant Suppress_Record := Scope_Suppress;
-         begin
-            Scope_Suppress := Suppress_All;
-            Analyze_And_Resolve (N);
-            Scope_Suppress := Svg;
-         end;
-
-      elsif Suppress = Overflow_Check then
-         declare
-            Svg : constant Overflow_Check_Type :=
-                    Scope_Suppress.Overflow_Checks_General;
-            Sva : constant Overflow_Check_Type :=
-                    Scope_Suppress.Overflow_Checks_Assertions;
+            Sva : constant Suppress_Array := Scope_Suppress.Suppress;
          begin
-            Scope_Suppress.Overflow_Checks_General    := Suppressed;
-            Scope_Suppress.Overflow_Checks_Assertions := Suppressed;
+            Scope_Suppress.Suppress := (others => True);
             Analyze_And_Resolve (N);
-            Scope_Suppress.Overflow_Checks_General    := Svg;
-            Scope_Suppress.Overflow_Checks_Assertions := Sva;
+            Scope_Suppress.Suppress := Sva;
          end;
 
       else
@@ -1690,19 +1662,23 @@ package body Sem_Res is
       Full_Analysis := False;
       Expander_Mode_Save_And_Set (False);
 
-      --  We suppress all checks for this analysis, except in Alfa mode.
-      --  Otherwise the checks are applied properly, and in the proper
-      --  location, when the default expressions are reanalyzed and reexpanded
-      --  later on.
+      --  Normally, we suppress all checks for this preanalysis. There is no
+      --  point in processing them now, since they will be applied properly
+      --  and in the proper location when the default expressions reanalyzed
+      --  and reexpanded later on. We will also have more information at that
+      --  point for possible suppression of individual checks.
 
-      --  Alfa mode suppresses all expansion but requires the setting of
-      --  checking flags (DIvision_Check and others) in particular for Ada 2012
-      --  constructs such as quantified expressions, that are expanded in two
-      --  separate steps.
+      --  However, in Alfa mode, most expansion is suppressed, and this
+      --  later reanalysis and reexpansion may not occur. Alfa mode does
+      --  require the setting of checking flags for proof purposes, so we
+      --  do the Alfa preanalysis without suppressing checks.
+
+      --  This special handling for Alfa mode is required for example in the
+      --  case of Ada 2012 constructs such as quantified expressions, which are
+      --  expanded in two separate steps.
 
       if Alfa_Mode then
          Analyze_And_Resolve (N, T);
-
       else
          Analyze_And_Resolve (N, T, Suppress => All_Checks);
       end if;
@@ -2946,11 +2922,11 @@ package body Sem_Res is
    begin
       if Suppress = All_Checks then
          declare
-            Svg : constant Suppress_Record := Scope_Suppress;
+            Sva : constant Suppress_Array := Scope_Suppress.Suppress;
          begin
-            Scope_Suppress := Suppress_All;
+            Scope_Suppress.Suppress := (others => True);
             Resolve (N, Typ);
-            Scope_Suppress := Svg;
+            Scope_Suppress.Suppress := Sva;
          end;
 
       else
@@ -5959,16 +5935,6 @@ package body Sem_Res is
 
       Set_Etype (N, Typ);
       Eval_Case_Expression (N);
-
-      --  If we still have a case expression, and overflow checks are enabled
-      --  in MINIMIZED or ELIMINATED modes, then set Do_Overflow_Check to
-      --  ensure that we handle overflow for dependent expressions.
-
-      if Nkind (N) = N_Case_Expression
-        and then Overflow_Check_Mode (Typ) in Minimized_Or_Eliminated
-      then
-         Set_Do_Overflow_Check (N);
-      end if;
    end Resolve_Case_Expression;
 
    -------------------------------
@@ -7215,16 +7181,6 @@ package body Sem_Res is
 
       Set_Etype (N, Typ);
       Eval_If_Expression (N);
-
-      --  If we still have a if expression, and overflow checks are enabled in
-      --  MINIMIZED or ELIMINATED modes, then set Do_Overflow_Check to ensure
-      --  that we handle overflow for dependent expressions.
-
-      if Nkind (N) = N_If_Expression
-        and then Overflow_Check_Mode (Typ) in Minimized_Or_Eliminated
-      then
-         Set_Do_Overflow_Check (N);
-      end if;
    end Resolve_If_Expression;
 
    -------------------------------

gcc/ada/snames.ads-tmpl

@@ -665,7 +665,6 @@ package Snames is
    Name_By_Protected_Procedure         : constant Name_Id := N + $;
    Name_Casing                         : constant Name_Id := N + $;
    Name_Check_All                      : constant Name_Id := N + $;
-   Name_Checked                        : constant Name_Id := N + $;
    Name_Code                           : constant Name_Id := N + $;
    Name_Component                      : constant Name_Id := N + $;
    Name_Component_Size_4               : constant Name_Id := N + $;
@@ -739,6 +738,7 @@ package Snames is
    Name_State                          : constant Name_Id := N + $;
    Name_Static                         : constant Name_Id := N + $;
    Name_Stack_Size                     : constant Name_Id := N + $;
+   Name_Strict                         : constant Name_Id := N + $;
    Name_Subunit_File_Name              : constant Name_Id := N + $;
    Name_Suppressed                     : constant Name_Id := N + $;
    Name_Task_Stack_Size_Default        : constant Name_Id := N + $;

gcc/ada/switch-c.adb

@@ -97,11 +97,8 @@ package body Switch.C is
    function Get_Overflow_Mode (C : Character) return Overflow_Check_Type is
    begin
       case C is
-         when '0' =>
-            return Suppressed;
-
          when '1' =>
-            return Checked;
+            return Strict;
 
          when '2' =>
             return Minimized;
@@ -801,12 +798,13 @@ package body Switch.C is
 
             when 'o' =>
                Ptr := Ptr + 1;
+               Suppress_Options.Suppress (Overflow_Check) := False;
 
                --  Case of no digits after the -gnato
 
-               if Ptr > Max or else Switch_Chars (Ptr) not in '0' .. '3' then
-                  Suppress_Options.Overflow_Checks_General    := Checked;
-                  Suppress_Options.Overflow_Checks_Assertions := Checked;
+               if Ptr > Max or else Switch_Chars (Ptr) not in '1' .. '3' then
+                  Suppress_Options.Overflow_Checks_General    := Strict;
+                  Suppress_Options.Overflow_Checks_Assertions := Strict;
 
                --  At least one digit after the -gnato
 
@@ -821,7 +819,7 @@ package body Switch.C is
                   --  be the same as general mode.
 
                   if Ptr > Max
-                    or else Switch_Chars (Ptr) not in '0' .. '3'
+                    or else Switch_Chars (Ptr) not in '1' .. '3'
                   then
                      Suppress_Options.Overflow_Checks_Assertions :=
                        Suppress_Options.Overflow_Checks_General;
@@ -869,9 +867,6 @@ package body Switch.C is
                      end if;
                   end loop;
 
-                  Suppress_Options.Overflow_Checks_General    := Suppressed;
-                  Suppress_Options.Overflow_Checks_Assertions := Suppressed;
-
                   Validity_Checks_On  := False;
                   Opt.Suppress_Checks := True;
                end if;

gcc/ada/types.ads

@@ -703,43 +703,39 @@ package Types is
    --    4.  Add a new Do_xxx_Check flag to Sinfo (if required)
    --    5.  Add appropriate checks for the new test
 
-   --  The following provides precise details on the mode used to check
-   --  intermediate overflows in expressions for signed integer arithmetic.
+   --  The following provides precise details on the mode used to generate
+   --  code for intermediate overflows in expressions for signed integer
+   --  arithmetic (and how to generate overflow checks if enabled). Note
+   --  that this only affects handling of intermediate results. The final
+   --  result must always fit within the target range, and if overflow
+   --  checking is enabled, the check on the final result is against this
+   --  target range.
 
    type Overflow_Check_Type is (
       Not_Set,
       --  Dummy value used during initialization process to show that the
       --  corresponding value has not yet been initialized.
 
-      Suppressed,
-      --  Overflow checking is suppressed. If an arithmetic operation creates
-      --  an overflow, no exception is raised, and the program is erroneous.
-
-      Checked,
-      --  All operations, including all intermediate operations are checked.
-      --  If the result of any arithmetic operation gives a result outside the
-      --  range of the base type, then a Constraint_Error exception is raised.
+      Strict,
+      --  Operations are done in the base type of the subexpression. If
+      --  overflow checks are enabled, then the check is against the range
+      --  of this base type.
 
       Minimized,
-      --  Where appropriate, arithmetic operations are performed with an
-      --  extended range, using Long_Long_Integer if necessary. As long as the
-      --  result fits in this extended range, then no exception is raised and
-      --  computation continues with the extended result. The final value of an
-      --  expression must fit in the base type of the whole expression. If an
-      --  intermediate result is outside the range of Long_Long_Integer then a
-      --  Constraint_Error exception is raised.
+      --  Where appropriate, intermediate arithmetic operations are performed
+      --  with an extended range, using Long_Long_Integer if necessary. If
+      --  overflow checking is enabled, then the check is against the range
+      --  of Long_Long_Integer.
 
       Eliminated);
       --  In this mode arbitrary precision arithmetic is used as needed to
       --  ensure that it is impossible for intermediate arithmetic to cause an
-      --  overflow. Again the final value of an expression must fit in the base
-      --  type of the whole expression.
+      --  overflow. In this mode, intermediate expressions are not affected by
+      --  the overflow checking mode, since overflows are eliminated.
 
    subtype Minimized_Or_Eliminated is
      Overflow_Check_Type range Minimized .. Eliminated;
-   subtype Suppressed_Or_Checked is
-     Overflow_Check_Type range Suppressed .. Checked;
-   --  Define subtypes so that clients don't need to know ordering. Note that
+   --  Define subtype so that clients don't need to know ordering. Note that
    --  Overflow_Check_Type is not marked as an ordered enumeration type.
 
    --  The following structure captures the state of check suppression or
@@ -747,24 +743,19 @@ package Types is
 
    type Suppress_Record is record
       Suppress : Suppress_Array;
-      --  Indicates suppression status of each possible check. Note: there
-      --  is an entry for Overflow_Check in this array, but it is never used.
-      --  Instead we use the more detailed information in the two components
-      --  that follow this one (Overflow_Checks_General/Assertions).
+      --  Indicates suppression status of each possible check
 
       Overflow_Checks_General : Overflow_Check_Type;
-      --  This field indicates the mode of overflow checking to be applied to
-      --  general expressions outside assertions.
+      --  This field indicates the mode for handling code generation and
+      --  overflow checking (if enabled) for intermediate expression values.
+      --  This applies to general expressions outside assertions.
 
       Overflow_Checks_Assertions : Overflow_Check_Type;
-      --  This field indicates the mode of overflow checking to be applied to
-      --  any expression occuring inside assertions.
+      --  This field indicates the mode for handling code generation and
+      --  overflow checking (if enabled) for intermediate expression values.
+      --  This applies to any expression occuring inside assertions.
    end record;
 
-   Suppress_All : constant Suppress_Record :=
-                    ((others => True), Suppressed, Suppressed);
-   --  Constant used to initialize Suppress_Record value to all suppressed.
-
    -----------------------------------
    -- Global Exception Declarations --
    -----------------------------------