aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2019-08-14 09:51:16 +0000
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>2019-08-14 09:51:16 +0000
commit9d7921310e5a265f0db62e45a881c266b8e4bec1 (patch)
treed70887e24a90ce400637867de0b9364d3e734079
parentebe1a04f30e07c84264da571ac4da003e8c4bc05 (diff)
downloadgcc-9d7921310e5a265f0db62e45a881c266b8e4bec1.zip
gcc-9d7921310e5a265f0db62e45a881c266b8e4bec1.tar.gz
gcc-9d7921310e5a265f0db62e45a881c266b8e4bec1.tar.bz2
[Ada] Fix spurious ownership error in GNATprove
Like Is_Path_Expression, function Is_Subpath_Expression should consider the possibility that the subpath is a type conversion or type qualification over the actual subpath node. This avoids spurious ownership errors in GNATprove. There is no impact on compilation. 2019-08-14 Yannick Moy <moy@adacore.com> gcc/ada/ * sem_spark.adb (Is_Subpath_Expression): Take into account conversion and qualification. From-SVN: r274452
-rw-r--r--gcc/ada/ChangeLog5
-rw-r--r--gcc/ada/sem_spark.adb9
2 files changed, 13 insertions, 1 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index b693032..250d174 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2019-08-14 Yannick Moy <moy@adacore.com>
+
+ * sem_spark.adb (Is_Subpath_Expression): Take into account
+ conversion and qualification.
+
2019-08-14 Eric Botcazou <ebotcazou@adacore.com>
* sem_ch7.adb (Install_Private_Declarations)
diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb
index a60a6cb..542f694 100644
--- a/gcc/ada/sem_spark.adb
+++ b/gcc/ada/sem_spark.adb
@@ -4266,6 +4266,12 @@ package body Sem_SPARK is
is
begin
return Is_Path_Expression (Expr, Is_Traversal)
+
+ or else (Nkind_In (Expr, N_Qualified_Expression,
+ N_Type_Conversion,
+ N_Unchecked_Type_Conversion)
+ and then Is_Subpath_Expression (Expression (Expr)))
+
or else (Nkind (Expr) = N_Attribute_Reference
and then
(Get_Attribute_Id (Attribute_Name (Expr)) =
@@ -4276,7 +4282,8 @@ package body Sem_SPARK is
or else
Get_Attribute_Id (Attribute_Name (Expr)) =
Attribute_Image))
- or else Nkind (Expr) = N_Op_Concat;
+
+ or else Nkind (Expr) = N_Op_Concat;
end Is_Subpath_Expression;
---------------------------