[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.

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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 597e3311506f526621c08881d3255789546c9706..d49d33112fa48024b1a37701b3e9a2736c59aeeb 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 1b1ba0fc4680d98812ef313892b4b554684ecddd..fb46e62296e94a94025516823409a42f2e59be3b 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)