[Ada] Synchronized object definition in SPARK updated

The definition of what types yield synchronized objected in SPARK has
been updated to see through the privacy boundary.

2019-07-04  Yannick Moy  <moy@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.

From-SVN: r273056

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index d49d33112fa48024b1a37701b3e9a2736c59aeeb..665b2b008705d3b11f20edb797dfc0569fecc29d 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+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

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 77eefdc25c39083279d6652a1ef67e0f2923425e..0fdbed6bef4785c0e9d84412878d55f4a23e937c 100644 (file)
--- 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 cf953b5af8c479cf6192d2364e78cf67e363f399..fc041c82e6701652a303f12220afcf5aedac5eb3 100644 (file)
--- 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 (file)
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 (file)
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 (file)
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;