Patchwork [Ada] Next step in implementing extended overflow checking

login
register
mail settings
Submitter Arnaud Charlet
Date Oct. 1, 2012, 8:27 a.m.
Message ID <20121001082743.GA28481@adacore.com>
Download mbox | patch
Permalink /patch/188239/
State New
Headers show

Comments

Arnaud Charlet - Oct. 1, 2012, 8:27 a.m.
This patch defines the four modes of overflow handling (SUPPRESSED,
CHECKED, MINIMIZED, ELIMINATED), and adds the Overflow_Checks pragma
and extedned -gnato switch to et them. But for now Checked, Minimized,
and Eliminated are all treated as Checked, so the behavior is unchanged.

The following program:

     1. procedure over2 is
     2.    function Ident (X : Integer) return Integer is
     3.    begin
     4.       return X;
     5.    end;
     6.    x : integer := Ident (Integer'Last);
     7.    procedure g;
     8.    pragma Postcondition (x + 2 = 0);
     9.    procedure g is begin null; end;
    10. begin
    11.    g;
    12. end;

compiled with -gnata -gnato10 generates

  raised SYSTEM.ASSERTIONS.ASSERT_FAILURE :
   failed postcondition from over2.adb:8

since -gnato10 turns off overflow checking in assertions
resulting in the postcondition giving a result of false.

compiled with -gnata -gnato01 generates

  raised CONSTRAINT_ERROR : over2.adb:8 overflow check failed

since -gnato01 turns on overflow checking in assertions
resulting in the overflow being detected.

The following test program:

     1. pragma Overflow_Checks
     2.   (Suppressed, Assertions => Checked);
     3. procedure over21 is
     4.    function Ident (X : Integer) return Integer is
     5.    begin return X; end;
     6.    x : integer := Ident (Integer'Last);
     7.    procedure g;
     8.    pragma Postcondition (x + 2 = 0);
     9.    procedure g is begin null; end;
    10. begin
    11.    g;
    12. end;

compiled with -gnata result in

  raised CONSTRAINT_ERROR : over21.adb:8 overflow check failed

The following test program:

     1. pragma Overflow_Checks
     2.   (Checked, Assertions => Suppressed);
     3. procedure over22 is
     4.    function Ident (X : Integer) return Integer is
     5.    begin return X; end;
     6.    x : integer := Ident (Integer'Last);
     7.    procedure g;
     8.    pragma Postcondition (x + 2 = 0);
     9.    procedure g is begin null; end;
    10. begin
    11.    g;
    12. end;

compiled with -gnata generates

  raised SYSTEM.ASSERTIONS.ASSERT_FAILURE :
   failed postcondition from over22.adb:8

Tested on x86_64-pc-linux-gnu, committed on trunk

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

	* checks.adb: Remove reference to Enable_Overflow_Checks Use
	Suppress_Options rather than Scope_Suppress.
	* gnat1drv.adb (Adjust_Global_Switches): Handle new overflow
	settings (Adjust_Global_Switches): Initialize Scope_Suppress
	from Suppress_Options.
	* opt.adb: Remove Enable_Overflow_Checks (use Suppress_Options
	instead).
	* opt.ads: Remove Overflow_Checks_Unsuppressed (not used)
	Remove Enable_Overflow_Checks (use Suppress_Options instead)
	Suppress_Options is now current setting (replaces Scope_Suppress).
	* osint.adb (Initialize): Deal with initializing overflow
	checking.
	* par-prag.adb: Add dummy entry for pragma Overflow_Checks.
	* sem.adb (Semantics): Save and restore In_Assertion_Expr Use
	Suppress_Options instead of Scope_Suppress.
	* sem.ads (In_Assertion_Expr): New flag (Scope_Suppress):
	Removed, use Suppress_Options instead.
	* sem_eval.adb (Compile_Time_Compare): Return Unknown in
	preanalysis mode.
	* sem_prag.adb (Process_Suppress_Unsuppress): Setting of
	Overflow_Checks_Unsuppressed removed (not used anywhere!)
	(Analyze_Pragma, case Check): Set In_Assertion_Expression
	(Analyze_Pragma, case Overflow_Checks): Implement new pragma
	* snames.ads-tmpl: Add names needed for handling pragma
	Overflow_Checks
	* switch-c.adb (Scan_Front_End_Switches) Handle -gnato? and
	-gnato?? where ? is 0-3
	* types.ads: Updates and fixes to comment on Suppress_Record.

Patch

Index: switch-c.adb
===================================================================
--- switch-c.adb	(revision 191888)
+++ switch-c.adb	(working copy)
@@ -128,9 +128,8 @@ 
 
       --  Handle switches that do not start with -gnat
 
-      if Ptr + 3 > Max
-        or else Switch_Chars (Ptr .. Ptr + 3) /= "gnat"
-      then
+      if Ptr + 3 > Max or else Switch_Chars (Ptr .. Ptr + 3) /= "gnat" then
+
          --  There are two front-end switches that do not start with -gnat:
          --  -I, --RTS
 
@@ -755,11 +754,78 @@ 
 
             when 'o' =>
                Ptr := Ptr + 1;
-               Suppress_Options.Suppress (Overflow_Check) := False;
-               Suppress_Options.Overflow_Checks_General := Check_All;
-               Suppress_Options.Overflow_Checks_Assertions := Check_All;
-               Opt.Enable_Overflow_Checks := True;
 
+               --  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;
+
+               --  At least one digit after the -gnato
+
+               else
+                  --  Handle first digit after -gnato
+
+                  case Switch_Chars (Ptr) is
+                     when '0' =>
+                        Suppress_Options.Overflow_Checks_General :=
+                          Suppressed;
+
+                     when '1' =>
+                        Suppress_Options.Overflow_Checks_General :=
+                          Checked;
+
+                     when '2' =>
+                        Suppress_Options.Overflow_Checks_General :=
+                          Minimized;
+
+                     when '3' =>
+                        Suppress_Options.Overflow_Checks_General :=
+                          Eliminated;
+
+                     when others =>
+                        raise Program_Error;
+                  end case;
+
+                  Ptr := Ptr + 1;
+
+                  --  Only one digit after -gnato, set assertions mode to
+                  --  be the same as general mode.
+
+                  if Ptr > Max
+                    or else Switch_Chars (Ptr) not in '0' .. '3'
+                  then
+                     Suppress_Options.Overflow_Checks_Assertions :=
+                       Suppress_Options.Overflow_Checks_General;
+
+                  --  Process second digit after -gnato
+
+                  else
+                     case Switch_Chars (Ptr) is
+                        when '0' =>
+                           Suppress_Options.Overflow_Checks_Assertions :=
+                             Suppressed;
+
+                        when '1' =>
+                           Suppress_Options.Overflow_Checks_Assertions :=
+                             Checked;
+
+                        when '2' =>
+                           Suppress_Options.Overflow_Checks_Assertions :=
+                             Minimized;
+
+                        when '3' =>
+                           Suppress_Options.Overflow_Checks_Assertions :=
+                             Eliminated;
+
+                        when others =>
+                           raise Program_Error;
+                     end case;
+
+                     Ptr := Ptr + 1;
+                  end if;
+               end if;
+
             --  Processing for O switch
 
             when 'O' =>
@@ -793,13 +859,12 @@ 
                         Suppress_Options.Suppress (J) := True;
                      end if;
 
-                     Suppress_Options.Overflow_Checks_General    := Suppress;
-                     Suppress_Options.Overflow_Checks_Assertions := Suppress;
+                     Suppress_Options.Overflow_Checks_General    := Suppressed;
+                     Suppress_Options.Overflow_Checks_Assertions := Suppressed;
                   end loop;
 
-                  Validity_Checks_On         := False;
-                  Opt.Suppress_Checks        := True;
-                  Opt.Enable_Overflow_Checks := False;
+                  Validity_Checks_On  := False;
+                  Opt.Suppress_Checks := True;
                end if;
 
             --  Processing for P switch
Index: types.ads
===================================================================
--- types.ads	(revision 191888)
+++ types.ads	(working copy)
@@ -706,51 +706,56 @@ 
    --  The following provides precise details on the mode used to check
    --  intermediate overflows in expressions for signed integer arithmetic.
 
-   type Overflow_Check_Type is
-     (Suppress,
-      --  Intermediate overflow suppressed. If an arithmetic operation creates
+   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.
 
-      Check_All,
-      --  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.
+      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.
 
-      Minimize,
+      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.
+      --  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.
 
-      Eliminate);
+      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.
+      --  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.
 
    --  The following structure captures the state of check suppression or
    --  activation at a particular point in the program execution.
 
    type Suppress_Record is record
       Suppress : Suppress_Array;
-      --  Indicates suppression status of each possible check
+      --  Indicates suppression status of each possible check. Note: there
+      --  is an entry for Overflow_Checks 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).
 
       Overflow_Checks_General : Overflow_Check_Type;
-      --  This field is relevant only if Suppress (Overflow_Check) is False.
-      --  It indicates the mode of overflow checking to be applied to general
-      --  expressions outside assertions.
+      --  This field indicates the mode of overflow checking to be applied to
+      --  general expressions outside assertions.
 
       Overflow_Checks_Assertions : Overflow_Check_Type;
-      --  This field is relevant only if Suppress (Overflow_Check) is False.
-      --  It indicates the mode of overflow checking to be applied to any
-      --  expressions occuring inside assertions.
+      --  This field  indicates the mode of overflow checking to be applied to
+      --  any expressions occuring inside assertions.
    end record;
 
    Suppress_All : constant Suppress_Record :=
-                    ((others => True), Suppress, Suppress);
+                    ((others => True), Suppressed, Suppressed);
    --  Constant used to initialize Suppress_Record value to all suppressed.
 
    -----------------------------------
Index: checks.adb
===================================================================
--- checks.adb	(revision 191892)
+++ checks.adb	(working copy)
@@ -3912,19 +3912,6 @@ 
       --  the computed expression is in the range Lor .. Hir. We can use this
       --  to restrict the possible range of results.
 
-      --  If one of the computed bounds is outside the range of the base type,
-      --  the expression may raise an exception and we had better indicate that
-      --  the evaluation has failed, at least if checks are enabled.
-
-      if OK1
-        and then Enable_Overflow_Checks
-        and then not Is_Entity_Name (N)
-        and then (Lor < Lo or else Hir > Hi)
-      then
-         OK := False;
-         return;
-      end if;
-
       if OK1 then
 
          --  If the refined value of the low bound is greater than the type
@@ -6184,10 +6171,20 @@ 
 
    function Overflow_Checks_Suppressed (E : Entity_Id) return Boolean is
    begin
+      --  Check overflow suppressed on entity
+
       if Present (E) and then Checks_May_Be_Suppressed (E) then
-         return Is_Check_Suppressed (E, Overflow_Check);
+         if Is_Check_Suppressed (E, Overflow_Check) then
+            return True;
+         end if;
+      end if;
+
+      --  Else return appropriate scope setting
+
+      if In_Assertion_Expr = 0 then
+         return Scope_Suppress.Overflow_Checks_General = Suppressed;
       else
-         return Scope_Suppress.Suppress (Overflow_Check);
+         return Scope_Suppress.Overflow_Checks_Assertions = Suppressed;
       end if;
    end Overflow_Checks_Suppressed;
 
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 191890)
+++ sem_prag.adb	(working copy)
@@ -286,7 +286,9 @@ 
       --  Preanalyze the boolean expression, we treat this as a spec expression
       --  (i.e. similar to a default expression).
 
+      In_Assertion_Expr := In_Assertion_Expr + 1;
       Preanalyze_Spec_Expression (Get_Pragma_Arg (Arg1), Standard_Boolean);
+      In_Assertion_Expr := In_Assertion_Expr - 1;
 
       --  In ASIS mode, for a pragma generated from a source aspect, also
       --  analyze the original aspect expression.
@@ -5672,12 +5674,11 @@ 
 
          if C = All_Checks or else C = Overflow_Check then
             if Suppress_Case then
-               Scope_Suppress.Overflow_Checks_General    := Suppress;
-               Scope_Suppress.Overflow_Checks_Assertions := Suppress;
+               Scope_Suppress.Overflow_Checks_General    := Suppressed;
+               Scope_Suppress.Overflow_Checks_Assertions := Suppressed;
             else
-               Scope_Suppress.Overflow_Checks_General    := Check_All;
-               Scope_Suppress.Overflow_Checks_Assertions := Check_All;
-               Opt.Overflow_Checks_Unsuppressed := True;
+               Scope_Suppress.Overflow_Checks_General    := Minimized;
+               Scope_Suppress.Overflow_Checks_Assertions := Minimized;
             end if;
          end if;
 
@@ -6799,7 +6800,7 @@ 
          -- Assertion_Policy --
          ----------------------
 
-         --  pragma Assertion_Policy (Check | Disable |Ignore)
+         --  pragma Assertion_Policy (Check | Disable | Ignore)
 
          when Pragma_Assertion_Policy => Assertion_Policy : declare
             Policy : Node_Id;
@@ -7289,7 +7290,9 @@ 
             --  Check is active
 
             else
+               In_Assertion_Expr := In_Assertion_Expr + 1;
                Analyze_And_Resolve (Expr, Any_Boolean);
+               In_Assertion_Expr := In_Assertion_Expr - 1;
             end if;
          end Check;
 
@@ -11753,6 +11756,76 @@ 
             Optimize_Alignment_Local := True;
          end Optimize_Alignment;
 
+         ---------------------
+         -- Overflow_Checks --
+         ---------------------
+
+         --  pragma Overflow_Checks
+         --    ([General => ] MODE [, [Assertions => ] MODE);
+
+         --  MODE := SUPPRESSED | CHECKED | MINIMIZED | ELIMINATED
+
+         when Pragma_Overflow_Checks => Overflow_Checks : declare
+            function Get_Check_Mode
+              (Name : Name_Id;
+               Arg  : Node_Id) return Overflow_Check_Type;
+            --  Function to process one pragma argument, Arg. If an identifier
+            --  is present, it must be Name. Check type is returned if a valid
+            --  argument exists, otherwise an error is signalled.
+
+            --------------------
+            -- Get_Check_Mode --
+            --------------------
+
+            function Get_Check_Mode
+              (Name : Name_Id;
+               Arg  : Node_Id) return Overflow_Check_Type
+            is
+               Argx : constant Node_Id := Get_Pragma_Arg (Arg);
+
+            begin
+               Check_Optional_Identifier (Arg, Name);
+               Check_Arg_Is_Identifier (Argx);
+
+               if Chars (Argx) = Name_Suppressed then
+                  return Suppressed;
+               elsif Chars (Argx) = Name_Checked then
+                  return Checked;
+               elsif Chars (Argx) = Name_Minimized then
+                  return Minimized;
+               elsif Chars (Argx) = Name_Eliminated then
+                  return Eliminated;
+               else
+                  Error_Pragma_Arg ("invalid argument for pragma%", Argx);
+               end if;
+            end Get_Check_Mode;
+
+         --  Start of processing for Overflow_Checks
+
+         begin
+            GNAT_Pragma;
+            Check_At_Least_N_Arguments (1);
+            Check_At_Most_N_Arguments (2);
+
+            --  Process first argument
+
+            Suppress_Options.Overflow_Checks_General :=
+              Get_Check_Mode (Name_General, Arg1);
+
+            --  Case of only one argument
+
+            if Arg_Count = 1 then
+               Scope_Suppress.Overflow_Checks_Assertions :=
+                 Scope_Suppress.Overflow_Checks_General;
+
+            --  Case of two arguments present
+
+            else
+               Scope_Suppress.Overflow_Checks_Assertions  :=
+                 Get_Check_Mode (Name_Assertions, Arg2);
+            end if;
+         end Overflow_Checks;
+
          -------------
          -- Ordered --
          -------------
@@ -15173,6 +15246,7 @@ 
       Pragma_Obsolescent                    =>  0,
       Pragma_Optimize                       => -1,
       Pragma_Optimize_Alignment             => -1,
+      Pragma_Overflow_Checks                =>  0,
       Pragma_Ordered                        =>  0,
       Pragma_Pack                           =>  0,
       Pragma_Page                           => -1,
Index: sem.adb
===================================================================
--- sem.adb	(revision 191888)
+++ sem.adb	(working copy)
@@ -33,6 +33,7 @@ 
 with Lib;      use Lib;
 with Lib.Load; use Lib.Load;
 with Nlists;   use Nlists;
+with Opt;      use Opt;
 with Output;   use Output;
 with Restrict; use Restrict;
 with Sem_Attr; use Sem_Attr;
@@ -1353,13 +1354,14 @@ 
       --  these variables, and also that such calls do not disturb the settings
       --  for units being analyzed at a higher level.
 
-      S_Current_Sem_Unit : constant Unit_Number_Type := Current_Sem_Unit;
-      S_Full_Analysis    : constant Boolean          := Full_Analysis;
-      S_GNAT_Mode        : constant Boolean          := GNAT_Mode;
-      S_Global_Dis_Names : constant Boolean          := Global_Discard_Names;
-      S_In_Spec_Expr     : constant Boolean          := In_Spec_Expression;
-      S_Inside_A_Generic : constant Boolean          := Inside_A_Generic;
-      S_Outer_Gen_Scope  : constant Entity_Id        := Outer_Generic_Scope;
+      S_Current_Sem_Unit  : constant Unit_Number_Type := Current_Sem_Unit;
+      S_Full_Analysis     : constant Boolean          := Full_Analysis;
+      S_GNAT_Mode         : constant Boolean          := GNAT_Mode;
+      S_Global_Dis_Names  : constant Boolean          := Global_Discard_Names;
+      S_In_Assertion_Expr : constant Nat              := In_Assertion_Expr;
+      S_In_Spec_Expr      : constant Boolean          := In_Spec_Expression;
+      S_Inside_A_Generic  : constant Boolean          := Inside_A_Generic;
+      S_Outer_Gen_Scope   : constant Entity_Id        := Outer_Generic_Scope;
 
       Generic_Main : constant Boolean :=
                        Nkind (Unit (Cunit (Main_Unit)))
@@ -1453,6 +1455,7 @@ 
 
       Full_Analysis      := True;
       Inside_A_Generic   := False;
+      In_Assertion_Expr  := 0;
       In_Spec_Expression := False;
 
       Set_Comes_From_Source_Default (False);
@@ -1526,6 +1529,7 @@ 
       Full_Analysis        := S_Full_Analysis;
       Global_Discard_Names := S_Global_Dis_Names;
       GNAT_Mode            := S_GNAT_Mode;
+      In_Assertion_Expr    := S_In_Assertion_Expr;
       In_Spec_Expression   := S_In_Spec_Expr;
       Inside_A_Generic     := S_Inside_A_Generic;
       Outer_Generic_Scope  := S_Outer_Gen_Scope;
Index: sem.ads
===================================================================
--- sem.ads	(revision 191888)
+++ sem.ads	(working copy)
@@ -203,7 +203,6 @@ 
 
 with Alloc;
 with Einfo;  use Einfo;
-with Opt;    use Opt;
 with Table;
 with Types;  use Types;
 
@@ -243,6 +242,15 @@ 
    --  frozen from start, because the tree on which they depend will not
    --  be available at the freeze point.
 
+   In_Assertion_Expr : Nat := 0;
+   --  This is set non-zero if we are within the expression of an assertion
+   --  pragma or aspect. It is a counter which is incremented at the start
+   --  of expanding such an expression, and decremented on completion of
+   --  expanding that expression. Probably a boolean would be good enough,
+   --  since we think that such expressions cannot nest, but that might not
+   --  be true in the future (e.g. if let expressions are added to Ada) so
+   --  we prepare for that future possibility by making it a counter.
+
    In_Inlined_Body : Boolean := False;
    --  Switch to indicate that we are analyzing and resolving an inlined body.
    --  Type checking is disabled in this context, because types are known to be
@@ -310,13 +318,13 @@ 
    --  that are applicable to all entities. A similar search is needed for any
    --  non-predefined check even if no specific entity is involved.
 
-   Scope_Suppress : Suppress_Record := Suppress_Options;
+   Scope_Suppress : Suppress_Record;
    --  This variable contains the current scope based settings of the suppress
-   --  switches. It is initialized from the options as shown, and then modified
-   --  by pragma Suppress. On entry to each scope, the current setting is saved
-   --  the scope stack, and then restored on exit from the scope. This record
-   --  may be rapidly checked to determine the current status of a check if
-   --  no specific entity is involved or if the specific entity involved is
+   --  switches. It is initialized from Suppress_Options in Gnat1drv, and then
+   --  modified by pragma Suppress. On entry to each scope, the current setting
+   --  is saved the scope stack, and then restored on exit from the scope. This
+   --  record may be rapidly checked to determine the current status of a check
+   --  if no specific entity is involved or if the specific entity involved is
    --  one for which no specific Suppress/Unsuppress pragma has been set (as
    --  indicated by the Checks_May_Be_Suppressed flag being set).
 
Index: gnat1drv.adb
===================================================================
--- gnat1drv.adb	(revision 191888)
+++ gnat1drv.adb	(working copy)
@@ -197,12 +197,10 @@ 
                                            Alignment_Check   => True,
                                            Division_Check    => True,
                                            Elaboration_Check => True,
-                                           Overflow_Check    => True,
                                            others            => False),
-            Overflow_Checks_General    => Suppress,
-            Overflow_Checks_Assertions => Suppress);
+            Overflow_Checks_General    => Suppressed,
+            Overflow_Checks_Assertions => Suppressed);
 
-         Enable_Overflow_Checks     := False;
          Dynamic_Elaboration_Checks := False;
 
          --  Kill debug of generated code, since it messes up sloc values
@@ -330,23 +328,29 @@ 
          Exception_Mechanism := Back_End_Exceptions;
       end if;
 
-      --  Set proper status for overflow checks. We turn on overflow checks if
-      --  -gnatp was not specified, and either -gnato is set or the back-end
-      --  takes care of overflow checks. Otherwise we suppress overflow checks
-      --  by default (since front end checks are expensive).
+      --  Set proper status for overflow checks. If already set (by -gnato or
+      --  -gnatp) then we have nothing to do.
 
-      if not Opt.Suppress_Checks
-        and then (Opt.Enable_Overflow_Checks
-                    or else
-                      (Targparm.Backend_Divide_Checks_On_Target
-                        and
-                       Targparm.Backend_Overflow_Checks_On_Target))
+      if Opt.Suppress_Options.Overflow_Checks_General /= Not_Set then
+         null;
+
+      --  If we have backend divide and overflow checks, then by default
+      --  overflow checks are minimized, which is a reasonable setting.
+
+      elsif Targparm.Backend_Divide_Checks_On_Target
+              and
+            Targparm.Backend_Overflow_Checks_On_Target
       then
-         Suppress_Options.Suppress (Overflow_Check) := False;
+         Suppress_Options.Overflow_Checks_General    := Minimized;
+         Suppress_Options.Overflow_Checks_Assertions := Minimized;
+
+      --  Otherwise for now, default is checks are suppressed. This is likely
+      --  to change in the future, but for now this is the compatible behavior
+      --  with previous versions of GNAT.
+
       else
-         Suppress_Options.Suppress (Overflow_Check)  := True;
-         Suppress_Options.Overflow_Checks_General    := Check_All;
-         Suppress_Options.Overflow_Checks_Assertions := Check_All;
+         Suppress_Options.Overflow_Checks_General    := Suppressed;
+         Suppress_Options.Overflow_Checks_Assertions := Suppressed;
       end if;
 
       --  Set default for atomic synchronization. As this synchronization
@@ -437,8 +441,7 @@ 
          --  Turn off alignment checks.
          --  Turn off validity checking.
 
-         Suppress_Options := Suppress_All;
-         Enable_Overflow_Checks := False;
+         Suppress_Options           := Suppress_All;
          Dynamic_Elaboration_Checks := False;
          Reset_Validity_Check_Options;
 
@@ -517,6 +520,12 @@ 
             Inline_Level := 2;
          end if;
       end if;
+
+      --  Finally capture adjusted value of Suppress_Options as the initial
+      --  value for Scope_Suppress, which will be modified as we move from
+      --  scope to scope (by Suppress/Unsuppress/Overflow_Checks pragmas).
+
+      Sem.Scope_Suppress := Opt.Suppress_Options;
    end Adjust_Global_Switches;
 
    --------------------
Index: par-prag.adb
===================================================================
--- par-prag.adb	(revision 191888)
+++ par-prag.adb	(working copy)
@@ -1199,6 +1199,7 @@ 
            Pragma_Ordered                        |
            Pragma_Optimize                       |
            Pragma_Optimize_Alignment             |
+           Pragma_Overflow_Checks                |
            Pragma_Pack                           |
            Pragma_Passive                        |
            Pragma_Preelaborable_Initialization   |
Index: opt.adb
===================================================================
--- opt.adb	(revision 191888)
+++ opt.adb	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2011, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -259,7 +259,6 @@ 
       Tree_Read_Bool (Debug_Pragmas_Disabled);
       Tree_Read_Bool (Debug_Pragmas_Enabled);
       Tree_Read_Int  (Int (Default_Pool));
-      Tree_Read_Bool (Enable_Overflow_Checks);
       Tree_Read_Bool (Full_List);
 
       Ada_Version_Config :=
@@ -326,7 +325,6 @@ 
       Tree_Write_Bool (Debug_Pragmas_Disabled);
       Tree_Write_Bool (Debug_Pragmas_Enabled);
       Tree_Write_Int  (Int (Default_Pool));
-      Tree_Write_Bool (Enable_Overflow_Checks);
       Tree_Write_Bool (Full_List);
       Tree_Write_Int  (Int (Version_String'Length));
       Tree_Write_Data (Version_String'Address, Version_String'Length);
Index: opt.ads
===================================================================
--- opt.ads	(revision 191888)
+++ opt.ads	(working copy)
@@ -486,11 +486,6 @@ 
    --  GNAT
    --  Set to True to generate full elaboration warnings (-gnatwl)
 
-   Enable_Overflow_Checks : Boolean := False;
-   --  GNAT
-   --  Set to True if -gnato (enable overflow checks) switch is set,
-   --  but not -gnatp.
-
    Error_Msg_Line_Length : Nat := 0;
    --  GNAT
    --  Records the error message line length limit. If this is set to zero,
@@ -1068,12 +1063,6 @@ 
    --  True if output of list of objects is requested (-O switch set). List is
    --  output under the given filename, or standard output if not specified.
 
-   Overflow_Checks_Unsuppressed : Boolean := False;
-   --  GNAT
-   --  This flag is True if there has been at least one pragma with the
-   --  effect of unsuppressing overflow checks, meaning that a more careful
-   --  check of the current mode is required.
-
    Persistent_BSS_Mode : Boolean := False;
    --  GNAT
    --  True if a Persistent_BSS configuration pragma is in effect, causing
@@ -1252,10 +1241,10 @@ 
 
    Suppress_Options : Suppress_Record;
    --  GNAT
-   --  Flags set True to suppress corresponding check, i.e. add an implicit
-   --  pragma Suppress at the outer level of each unit compiled. Note that
-   --  these suppress actions can be overridden by the use of the Unsuppress
-   --  pragma. This variable is initialized by Osint.Initialize.
+   --  Indicates outer level setting of check suppression. This initializes
+   --  the settings of the outer scope level in any unit compiled. This is
+   --  initialized by Osint.Initialize, and further initialized by the
+   --  Adjust_Global_Switches flag in Gnat1drv.
 
    Suppress_Back_Annotation : Boolean := False;
    --  GNAT
Index: sem_eval.adb
===================================================================
--- sem_eval.adb	(revision 191888)
+++ sem_eval.adb	(working copy)
@@ -743,6 +743,16 @@ 
    begin
       Diff.all := No_Uint;
 
+      --  In preanalysis mode, always return Unknown, it is too early to be
+      --  thinking we know the result of a comparison, save that judgment for
+      --  the full analysis. This is particularly important in the case of
+      --  pre and postconditions, which otherwise can be prematurely collapsed
+      --  into having True or False conditions when this is inappropriate.
+
+      if not Full_Analysis then
+         return Unknown;
+      end if;
+
       --  If either operand could raise constraint error, then we cannot
       --  know the result at compile time (since CE may be raised!)
 
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 191889)
+++ snames.ads-tmpl	(working copy)
@@ -408,6 +408,7 @@ 
    Name_No_Strict_Aliasing             : constant Name_Id := N + $; -- GNAT
    Name_Normalize_Scalars              : constant Name_Id := N + $;
    Name_Optimize_Alignment             : constant Name_Id := N + $; -- GNAT
+   Name_Overflow_Checks                : constant Name_Id := N + $; -- GNAT
    Name_Persistent_BSS                 : constant Name_Id := N + $; -- GNAT
    Name_Polling                        : constant Name_Id := N + $; -- GNAT
    Name_Priority_Specific_Dispatching  : constant Name_Id := N + $; -- Ada 05
@@ -651,6 +652,7 @@ 
 
    Name_As_Is                          : constant Name_Id := N + $;
    Name_Assertion                      : constant Name_Id := N + $;
+   Name_Assertions                     : constant Name_Id := N + $;
    Name_Attribute_Name                 : constant Name_Id := N + $;
    Name_Body_File_Name                 : constant Name_Id := N + $;
    Name_Boolean_Entry_Barriers         : constant Name_Id := N + $;
@@ -658,6 +660,8 @@ 
    Name_By_Entry                       : constant Name_Id := N + $;
    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 + $;
@@ -667,6 +671,7 @@ 
    Name_Disable                        : constant Name_Id := N + $;
    Name_Dot_Replacement                : constant Name_Id := N + $;
    Name_Dynamic                        : constant Name_Id := N + $;
+   Name_Eliminated                     : constant Name_Id := N + $;
    Name_Ensures                        : constant Name_Id := N + $;
    Name_Entity                         : constant Name_Id := N + $;
    Name_Entry_Count                    : constant Name_Id := N + $;
@@ -676,6 +681,7 @@ 
    Name_Form                           : constant Name_Id := N + $;
    Name_G_Float                        : constant Name_Id := N + $;
    Name_Gcc                            : constant Name_Id := N + $;
+   Name_General                        : constant Name_Id := N + $;
    Name_Gnat                           : constant Name_Id := N + $;
    Name_GPL                            : constant Name_Id := N + $;
    Name_IEEE_Float                     : constant Name_Id := N + $;
@@ -689,6 +695,7 @@ 
    Name_Max_Size                       : constant Name_Id := N + $;
    Name_Mechanism                      : constant Name_Id := N + $;
    Name_Message                        : constant Name_Id := N + $;
+   Name_Minimized                      : constant Name_Id := N + $;
    Name_Mixedcase                      : constant Name_Id := N + $;
    Name_Mode                           : constant Name_Id := N + $;
    Name_Modified_GPL                   : constant Name_Id := N + $;
@@ -727,6 +734,7 @@ 
    Name_Static                         : constant Name_Id := N + $;
    Name_Stack_Size                     : 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 + $;
    Name_Task_Type                      : constant Name_Id := N + $;
    Name_Time_Slicing_Enabled           : constant Name_Id := N + $;
@@ -1656,6 +1664,7 @@ 
       Pragma_No_Strict_Aliasing,
       Pragma_Normalize_Scalars,
       Pragma_Optimize_Alignment,
+      Pragma_Overflow_Checks,
       Pragma_Persistent_BSS,
       Pragma_Polling,
       Pragma_Priority_Specific_Dispatching,
Index: osint.adb
===================================================================
--- osint.adb	(revision 191888)
+++ osint.adb	(working copy)
@@ -1655,11 +1655,12 @@ 
       Src_Search_Directories.Init;
       Lib_Search_Directories.Init;
 
-      --  Start off by setting all suppress options to False, these will
-      --  be reset later (turning some on if -gnato is not specified, and
-      --  turning all of them on if -gnatp is specified).
+      --  Start off by setting all suppress options, to False. The special
+      --  overflow fields are set to Not_Set (they will be set by -gnatp, or
+      --  by -gnato, or, if neither of these appear, in Adjust_Global_Switches
+      --  in Gnat1drv.
 
-      Suppress_Options := ((others => False), Check_All, Check_All);
+      Suppress_Options := ((others => False), Not_Set, Not_Set);
 
       --  Reserve the first slot in the search paths table. This is the
       --  directory of the main source file or main library file and is filled