projects / gcc.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 257baf5)
[Ada] Fix for possibly null ranges in 'Update and delta_aggregate
authorPiotr Trojanek <trojanek@adacore.com>
Tue, 2 Jun 2020 22:17:21 +0000 (00:17 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Wed, 15 Jul 2020 13:42:49 +0000 (09:42 -0400)
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.

gcc/ada/exp_spark.adb patch | blob | history

diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 40621bd9e33ad5530fedc23a0083d4fdcfae5fe4..6454902f06b8ee438552951eab463721f7098527 100644 (file)
--- 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