===================================================================
@@ -2971,11 +2971,18 @@
and then Is_Discrete_Type (S_Typ) = Is_Discrete_Type (Target_Typ)
and then
(In_Subrange_Of (S_Typ, Target_Typ, Fixed_Int)
+
+ -- Also check if the expression itself is in the range of the
+ -- target type if it is a known at compile time value. We skip
+ -- this test if S_Typ is set since for OUT and IN OUT parameters
+ -- the Expr itself is not relevant to the checking.
+
or else
- Is_In_Range (Expr, Target_Typ,
- Assume_Valid => True,
- Fixed_Int => Fixed_Int,
- Int_Real => Int_Real))
+ (No (Source_Typ)
+ and then Is_In_Range (Expr, Target_Typ,
+ Assume_Valid => True,
+ Fixed_Int => Fixed_Int,
+ Int_Real => Int_Real)))
then
return;
In -gnatc or GNATprove mode, there were cases in which the Do_Range_Check flag was not set on an OUT parameter, causing e.g. GNAT prove to miss the requirement for proving that an out parameter result was in range. This is now corrected, the following test, compiled in -gnatd.F (GNATprove mode) with -gnatdt generates a log file with a single instance of the Do_Range_Check flag set on X in line 11 of the body (the out parameter). 1. package Out_Subcheck is 2. 3. type Index_Type is range 0 .. 10; 4. subtype Valid_Index_Type is Index_Type range 1 .. 10; 5. 6. procedure Read (Z : out Index_Type); 7. 8. function Read_Validate return Valid_Index_Type; 9. end Out_Subcheck; 1. package body Out_Subcheck is 2. 3. procedure Read (Z : out Index_Type) is 4. begin 5. Z := 0; 6. end Read; 7. 8. function Read_Validate return Valid_Index_Type is 9. X : Valid_Index_Type; 10. begin 11. Read (X); --@RANGE_CHECK:FAIL 12. return X; 13. end Read_Validate; 14. 15. end Out_Subcheck; Tested on x86_64-pc-linux-gnu, committed on trunk 2014-08-04 Robert Dewar <dewar@adacore.com> * checks.adb (Apply_Scalar_Range_Check): Make sure we handle case of OUT and IN OUT parameter correctly (where Source_Typ is set), we were missing one case where a check must be applied.