mirror/gcc
2
0
Fork 0
mirror of git://gcc.gnu.org/git/gcc.git synced 2025-03-21 22:51:06 +08:00
Code Issues Packages Projects Releases Wiki Activity

[Ada] Fix spurious ownership error in GNATprove

Browse Source 
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
This commit is contained in:
Yannick Moy 2019-08-14 09:51:16 +00:00 committed by Pierre-Marie de Rodat
parent ebe1a04f30
commit 9d7921310e
2 changed files with 13 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
gcc/ada/ChangeLog
View 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)

9
gcc/ada/sem_spark.adb
View 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;
---------------------------