diff options
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 5 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 11 | ||||
| -rw-r--r-- | gcc/testsuite/ChangeLog | 5 | ||||
| -rw-r--r-- | gcc/testsuite/gnat.dg/synchronized2.adb | 5 | ||||
| -rw-r--r-- | gcc/testsuite/gnat.dg/synchronized2.ads | 4 | ||||
| -rw-r--r-- | gcc/testsuite/gnat.dg/synchronized2_pkg.ads | 5 |
6 files changed, 34 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 diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index cf953b5..fc041c82 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,8 @@ +2019-07-04 Yannick Moy <moy@adacore.com> + + * gnat.dg/synchronized2.adb, gnat.dg/synchronized2.ads, + gnat.dg/synchronized2_pkg.ads: New testcase. + 2019-07-04 Justin Squirek <squirek@adacore.com> * gnat.dg/generic_inst4.adb, gnat.dg/generic_inst4_gen.ads, diff --git a/gcc/testsuite/gnat.dg/synchronized2.adb b/gcc/testsuite/gnat.dg/synchronized2.adb new file mode 100644 index 0000000..1c111ef --- /dev/null +++ b/gcc/testsuite/gnat.dg/synchronized2.adb @@ -0,0 +1,5 @@ +with Synchronized2_Pkg; +package body Synchronized2 with SPARK_Mode, Refined_State => (State => C) is + C : Synchronized2_Pkg.T; + procedure Dummy is null; +end; diff --git a/gcc/testsuite/gnat.dg/synchronized2.ads b/gcc/testsuite/gnat.dg/synchronized2.ads new file mode 100644 index 0000000..780edeb --- /dev/null +++ b/gcc/testsuite/gnat.dg/synchronized2.ads @@ -0,0 +1,4 @@ +-- { dg-do compile } +package Synchronized2 with SPARK_Mode, Abstract_State => (State with Synchronous) is + procedure Dummy; +end; diff --git a/gcc/testsuite/gnat.dg/synchronized2_pkg.ads b/gcc/testsuite/gnat.dg/synchronized2_pkg.ads new file mode 100644 index 0000000..57cae9c --- /dev/null +++ b/gcc/testsuite/gnat.dg/synchronized2_pkg.ads @@ -0,0 +1,5 @@ +package Synchronized2_Pkg with SPARK_Mode is + type T is limited private; +private + task type T; +end; |