The definition of what types yield synchronized objected in SPARK has
been updated to see through the privacy boundary.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-07-04 Yannick Moy <m...@adacore.com>
gcc/ada/
* sem_util.adb (Yields_Synchronized_Object): Adapt to new SPARK
rule.
gcc/testsuite/
* gnat.dg/synchronized2.adb, gnat.dg/synchronized2.ads,
gnat.dg/synchronized2_pkg.ads: New testcase.--- gcc/ada/sem_util.adb
+++ 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
--- /dev/null
new file mode 100644
+++ 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;
--- /dev/null
new file mode 100644
+++ 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;
--- /dev/null
new file mode 100644
+++ 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;
