[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 d49d331..665b2b0 100644 (file)
--- 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 (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 cf953b5..fc041c8 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;