From 9193307b56ea03321bb66e2f7e30c6e98d724efc Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Thu, 4 Jul 2019 08:06:05 +0000 Subject: [PATCH] [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 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 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/sem_util.adb | 11 ++++++++++- gcc/testsuite/ChangeLog | 5 +++++ gcc/testsuite/gnat.dg/synchronized2.adb | 5 +++++ gcc/testsuite/gnat.dg/synchronized2.ads | 4 ++++ gcc/testsuite/gnat.dg/synchronized2_pkg.ads | 5 +++++ 6 files changed, 34 insertions(+), 1 deletion(-) create mode 100644 gcc/testsuite/gnat.dg/synchronized2.adb create mode 100644 gcc/testsuite/gnat.dg/synchronized2.ads create mode 100644 gcc/testsuite/gnat.dg/synchronized2_pkg.ads 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 + + * sem_util.adb (Yields_Synchronized_Object): Adapt to new SPARK + rule. + 2019-07-04 Yannick Moy * 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 + + * gnat.dg/synchronized2.adb, gnat.dg/synchronized2.ads, + gnat.dg/synchronized2_pkg.ads: New testcase. + 2019-07-04 Justin Squirek * 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; -- 2.30.2