This is the mail archive of the mailing list for the GCC project.

Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

[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  <>


	* 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
       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)) =
-       or else Nkind (Expr) = N_Op_Concat;
+        or else Nkind (Expr) = N_Op_Concat;
    end Is_Subpath_Expression;

Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]