diff mbox series

[Ada] Fix for possibly null ranges in 'Update and delta_aggregate

Message ID 20200715134518.GA23672@adacore.com
State New
Headers show
Series [Ada] Fix for possibly null ranges in 'Update and delta_aggregate | expand

Commit Message

Pierre-Marie de Rodat July 15, 2020, 1:45 p.m. UTC 
In expression like "(Arr with delta Low .. High => New_Component_Value)"
bounds Low .. High might denote a null range. In this case both Low and
High can be any values from the base type of the array's index type;
they don't need to belong to the array's index type itself.

This patch removes unnecessary range checks in GNATprove mode.
Compilation is not affected.

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

gcc/ada/

	* exp_spark.adb (Expand_SPARK_Delta_Or_Update): Apply scalar
	range checks against the base type of an index type, not against
	the index type itself.
diff mbox series

Patch

diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -227,9 +227,9 @@  package body Exp_SPARK is
 
                   if Nkind (Index) = N_Range then
                      Apply_Scalar_Range_Check
-                       (Low_Bound  (Index), Etype (Index_Typ));
+                       (Low_Bound  (Index), Base_Type (Etype (Index_Typ)));
                      Apply_Scalar_Range_Check
-                       (High_Bound (Index), Etype (Index_Typ));
+                       (High_Bound (Index), Base_Type (Etype (Index_Typ)));
 
                   --  Otherwise the index denotes a single element