[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 (file)
--- 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 (file)
--- 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)