From: Yannick Moy <moy@adacore.com>
Date: Thu, 4 Jul 2019 08:06:00 +0000 (+0000)
Subject: [Ada] Fix crash in SPARK ownership checking
X-Git-Tag: upstream/12.2.0~23442
X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=194dc648e4b40ac705103cfc92dff0c11b82fb5a;p=platform%2Fupstream%2Fgcc.git

[Ada] Fix crash in SPARK ownership checking

Analysis could crash on extended return of a non-deep type, now fixed.
This has no impact on compilation.

2019-07-04  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_spark.adb (Check_Statement): Only check permission of
	object in extended return when it is of a deep type.

From-SVN: r273055
---

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 597e331..d49d331 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2019-07-04  Yannick Moy  <moy@adacore.com>
+
+	* sem_spark.adb (Check_Statement): Only check permission of
+	object in extended return when it is of a deep type.
+
 2019-07-04  Justin Squirek  <squirek@adacore.com>
 
 	* sem_ch12.adb (Perform_Appropriate_Analysis): Added for
diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb
index 1b1ba0f..fb46e62 100644
--- a/gcc/ada/sem_spark.adb
+++ b/gcc/ada/sem_spark.adb
@@ -2902,10 +2902,13 @@ package body Sem_SPARK is
                Check_List (Return_Object_Declarations (Stmt));
                Check_Node (Handled_Statement_Sequence (Stmt));
 
-               Perm := Get_Perm (Obj);
+               if Is_Deep (Etype (Obj)) then
+                  Perm := Get_Perm (Obj);
 
-               if Perm /= Read_Write then
-                  Perm_Error (Decl, Read_Write, Perm, Expl => Get_Expl (Obj));
+                  if Perm /= Read_Write then
+                     Perm_Error (Decl, Read_Write, Perm,
+                                 Expl => Get_Expl (Obj));
+                  end if;
                end if;
 
                if Ekind_In (Subp, E_Procedure, E_Entry)