From: Yannick Moy <moy@adacore.com>
Date: Thu, 4 Jul 2019 08:06:05 +0000 (+0000)
Subject: [Ada] Synchronized object definition in SPARK updated
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9193307b56ea03321bb66e2f7e30c6e98d724efc;p=gcc.git

[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 d49d33112fa..665b2b00870 100644
--- 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 77eefdc25c3..0fdbed6bef4 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 cf953b5af8c..fc041c82e67 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 00000000000..1c111ef941c
--- /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 00000000000..780edebc82a
--- /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 00000000000..57cae9c0bb7
--- /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;