This corrects the problem of failing to set the Do_Range_Check
flag for the right operand of integer exponentiation when needed.
It supercedes the special check previously made in checks to
unconditionally set the flag in gnatprove mode. The flag is now
properly set, with proper range analysis, in both gnatprove and
ordinary -gnatc modes.

The following test, when compiled with -gnatws and either
-gnatc or -gnatd.F:

     1. procedure ExpRange (B, X : Integer) is
     2.    Z1,Z2,Z3 : Integer;
     3.    G : Natural;
     4. begin
     5.    Z1 := B ** X;   -- Check needed
     6.    Z2 := B ** G;   -- No check needed
     7.    Z3 := B ** 4;   -- No check needed
     8. end ExpRange;

Generates a Do_Range_Check on line 5 for X, but no flag is
set for line 6 or line 7. If -gnatdt is used to generate a
log file, grepping the log file for Do_Range_Check will get
a single hit on line 5.

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

2014-01-20  Robert Dewar  <de...@adacore.com>

        * checks.adb (Apply_Range_Check): Remove gnatprove special
        casing of exponentiation.
        * sem_res.adb (Resolve_Op_Expon): Apply range check to right
        operand for integer case to check range against Natural.

Index: checks.adb
===================================================================
--- checks.adb  (revision 206831)
+++ checks.adb  (working copy)
@@ -2797,19 +2797,6 @@
          return;
       end if;
 
-      --  Ensure that the exponent is a natural. The flag is set only in formal
-      --  verification mode as the expander takes care of this check and there
-      --  is no expansion phase in GNATprove_Mode.
-
-      --  Doesn't seem right to do this unconditionally, we should check the
-      --  range of the exponent operand. If we do that, it seems like we should
-      --  then set the flag unconditionally and have the expander check the
-      --  flag to see whether to generate a check ???
-
-      if GNATprove_Mode and then Nkind (Expr) = N_Op_Expon then
-         Set_Do_Range_Check (Right_Opnd (Expr));
-      end if;
-
       Is_Unconstrained_Subscr_Ref :=
         Is_Subscr_Ref and then not Is_Constrained (Arr_Typ);
 
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 206832)
+++ sem_res.adb (working copy)
@@ -8393,6 +8393,12 @@
       Resolve (Left_Opnd (N), B_Typ);
       Resolve (Right_Opnd (N), Standard_Integer);
 
+      --  For integer types, right argument must be in Natural range
+
+      if Is_Integer_Type (Typ) then
+         Apply_Scalar_Range_Check (Right_Opnd (N), Standard_Natural);
+      end if;
+
       Check_Unset_Reference (Left_Opnd  (N));
       Check_Unset_Reference (Right_Opnd (N));
 

Reply via email to