From: Yannick Moy Date: Wed, 14 Aug 2019 09:51:16 +0000 (+0000) Subject: [Ada] Fix spurious ownership error in GNATprove X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9d7921310e5a265f0db62e45a881c266b8e4bec1;p=gcc.git [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 gcc/ada/ * sem_spark.adb (Is_Subpath_Expression): Take into account conversion and qualification. From-SVN: r274452 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index b69303240fc..250d174b032 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2019-08-14 Yannick Moy + + * sem_spark.adb (Is_Subpath_Expression): Take into account + conversion and qualification. + 2019-08-14 Eric Botcazou * sem_ch7.adb (Install_Private_Declarations) diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb index a60a6cb4bac..542f694978b 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; ---------------------------