This is the mail archive of the
gcc-patches@gcc.gnu.org
mailing list for the GCC project.
[Ada] Fix spurious ownership error in GNATprove
- From: Pierre-Marie de Rodat <derodat at adacore dot com>
- To: gcc-patches at gcc dot gnu dot org
- Cc: Yannick Moy <moy at adacore dot com>
- Date: Wed, 14 Aug 2019 05:53:12 -0400
- Subject: [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.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-08-14 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb (Is_Subpath_Expression): Take into account
conversion and qualification.
--- gcc/ada/sem_spark.adb
+++ 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;
---------------------------