diff options
author | Yannick Moy <moy@adacore.com> | 2019-08-14 09:51:16 +0000 |
---|---|---|
committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-08-14 09:51:16 +0000 |
commit | 9d7921310e5a265f0db62e45a881c266b8e4bec1 (patch) | |
tree | d70887e24a90ce400637867de0b9364d3e734079 | |
parent | ebe1a04f30e07c84264da571ac4da003e8c4bc05 (diff) | |
download | gcc-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/ChangeLog | 5 | ||||
-rw-r--r-- | gcc/ada/sem_spark.adb | 9 |
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; --------------------------- |