diff options
| author | Yannick Moy <moy@adacore.com> | 2019-07-04 08:06:00 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-07-04 08:06:00 +0000 |
| commit | 194dc648e4b40ac705103cfc92dff0c11b82fb5a (patch) | |
| tree | 6fae4dacd64dd3a0bef0bebc35242418ef303f50 /gcc | |
| parent | 7273107b948b81edc084b33e8e8fd4f3b4115f72 (diff) | |
| download | gcc-194dc648e4b40ac705103cfc92dff0c11b82fb5a.zip gcc-194dc648e4b40ac705103cfc92dff0c11b82fb5a.tar.gz gcc-194dc648e4b40ac705103cfc92dff0c11b82fb5a.tar.bz2 | |
[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
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 5 | ||||
| -rw-r--r-- | gcc/ada/sem_spark.adb | 9 |
2 files changed, 11 insertions, 3 deletions
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) |