diff options
Diffstat (limited to 'gcc/ada')
| -rw-r--r-- | gcc/ada/ChangeLog | 5 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 11 |
2 files changed, 15 insertions, 1 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index d49d331..665b2b0 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,10 @@ 2019-07-04 Yannick Moy <moy@adacore.com> + * sem_util.adb (Yields_Synchronized_Object): Adapt to new SPARK + rule. + +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. diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 77eefdc..0fdbed6 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -26442,6 +26442,7 @@ package body Sem_Util is -- synchronized object. if Etype (Typ) /= Typ + and then not Is_Private_Type (Etype (Typ)) and then not Yields_Synchronized_Object (Etype (Typ)) then return False; @@ -26457,11 +26458,19 @@ package body Sem_Util is elsif Is_Synchronized_Interface (Typ) then return True; - -- A task type yelds a synchronized object by default + -- A task type yields a synchronized object by default elsif Is_Task_Type (Typ) then return True; + -- A private type yields a synchronized object if its underlying type + -- does. + + elsif Is_Private_Type (Typ) + and then Present (Underlying_Type (Typ)) + then + return Yields_Synchronized_Object (Underlying_Type (Typ)); + -- Otherwise the type does not yield a synchronized object else |