]> git.ipfire.org Git - thirdparty/gcc.git/commitdiff
[Ada] Fix spurious ownership error in GNATprove
authorpmderodat <pmderodat@138bc75d-0d04-0410-961f-82ee72b054a4>
Wed, 14 Aug 2019 09:51:16 +0000 (09:51 +0000)
committerpmderodat <pmderodat@138bc75d-0d04-0410-961f-82ee72b054a4>
Wed, 14 Aug 2019 09:51:16 +0000 (09:51 +0000)
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.

git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@274452 138bc75d-0d04-0410-961f-82ee72b054a4

gcc/ada/ChangeLog
gcc/ada/sem_spark.adb

index b69303240fc70fce1c03a9c95a70e307354f367c..250d174b032310f74f9255e7757e393ab4acd799 100644 (file)
@@ -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)
index a60a6cb4bacc51c5db3b48626fc531dc05cd52c2..542f694978bd71f72a9e4ddebd82838379e38bc4 100644 (file)
@@ -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;
 
    ---------------------------