diff options
| author | Hristian Kirtchev <kirtchev@adacore.com> | 2018-05-30 08:57:21 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2018-05-30 08:57:21 +0000 |
| commit | 56a05ce0839d83fbbbc7e57d085ca483b884b805 (patch) | |
| tree | 4522a0436bfd55179c72a8e6645bd2499cfdcb5d /gcc/testsuite | |
| parent | 131780ac08a8dfc1b9c14a9d5c38575fcc34b205 (diff) | |
| download | gcc-56a05ce0839d83fbbbc7e57d085ca483b884b805.zip gcc-56a05ce0839d83fbbbc7e57d085ca483b884b805.tar.gz gcc-56a05ce0839d83fbbbc7e57d085ca483b884b805.tar.bz2 | |
[Ada] Spurious error on legal synchronized constituent
This patch corrects the predicate which determines whether an entity denotes a
synchronized object as per SPARK RM 9.1. to account for a case where the object
is not atomic, but its type is.
The patch also cleans up various atomic object-related predicates.
2018-05-30 Hristian Kirtchev <kirtchev@adacore.com>
gcc/ada/
* sem_util.adb (Is_Atomic_Object): Cleaned up. Split the entity logic
in a separate routine.
(Is_Atomic_Object_Entity): New routine.
(Is_Atomic_Prefix): Cleaned up.
(Is_Synchronized_Object): Check that the object is atomic, or its type
is atomic.
(Object_Has_Atomic_Components): Removed.
* sem_util.ads (Is_Atomic_Object): Reword the comment on usage.
(Is_Atomic_Object_Entity): New routine.
gcc/testsuite/
* gnat.dg/synchronized1.adb, gnat.dg/synchronized1.ads: New testcase.
From-SVN: r260933
Diffstat (limited to 'gcc/testsuite')
| -rw-r--r-- | gcc/testsuite/ChangeLog | 4 | ||||
| -rw-r--r-- | gcc/testsuite/gnat.dg/synchronized1.adb | 14 | ||||
| -rw-r--r-- | gcc/testsuite/gnat.dg/synchronized1.ads | 7 |
3 files changed, 25 insertions, 0 deletions
diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index f1c2179..2e35d64 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,7 @@ +2018-05-30 Hristian Kirtchev <kirtchev@adacore.com> + + * gnat.dg/synchronized1.adb, gnat.dg/synchronized1.ads: New testcase. + 2018-05-29 Uros Bizjak <ubizjak@gmail.com> PR target/85950 diff --git a/gcc/testsuite/gnat.dg/synchronized1.adb b/gcc/testsuite/gnat.dg/synchronized1.adb new file mode 100644 index 0000000..d07c351 --- /dev/null +++ b/gcc/testsuite/gnat.dg/synchronized1.adb @@ -0,0 +1,14 @@ +-- { dg-do compile } +-- { dg-options "-gnatws" } + +package body Synchronized1 + with SPARK_Mode, + Refined_State => (State => Curr_State) +is + type Reactor_State is (Stopped, Working) with Atomic; + + Curr_State : Reactor_State + with Async_Readers, Async_Writers; + + procedure Force_Body is null; +end Synchronized1; diff --git a/gcc/testsuite/gnat.dg/synchronized1.ads b/gcc/testsuite/gnat.dg/synchronized1.ads new file mode 100644 index 0000000..f814c91 --- /dev/null +++ b/gcc/testsuite/gnat.dg/synchronized1.ads @@ -0,0 +1,7 @@ +package Synchronized1 + with SPARK_Mode, + Abstract_State => (State with Synchronous), + Initializes => State +is + procedure Force_Body; +end Synchronized1; |