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));