diff options
| author | Hristian Kirtchev <kirtchev@adacore.com> | 2014-06-13 09:51:30 +0000 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-06-13 11:51:30 +0200 |
| commit | c00b86e2c30d599d4f6893ac09fca13b17dde96c (patch) | |
| tree | 8ac6fe0159c6de9e241a8a39c5160ee40c9a5535 /gcc | |
| parent | e3a325f2f013b6f934863fcd4187154666f84237 (diff) | |
| download | gcc-c00b86e2c30d599d4f6893ac09fca13b17dde96c.zip gcc-c00b86e2c30d599d4f6893ac09fca13b17dde96c.tar.gz gcc-c00b86e2c30d599d4f6893ac09fca13b17dde96c.tar.bz2 | |
freeze.adb (Freeze_Entity): Remove the check concerning volatile types in SPARK as it is poorly placed and...
2014-06-13 Hristian Kirtchev <kirtchev@adacore.com>
* freeze.adb (Freeze_Entity): Remove the check concerning volatile
types in SPARK as it is poorly placed and poorly formulated. The
check was flagging ALL volatile entities as illegal in SPARK.
* sem_prag.adb (Process_Atomic_Shared_Volatile): Flag volatile
types as illegal in SPARK.
From-SVN: r211615
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 8 | ||||
| -rw-r--r-- | gcc/ada/freeze.adb | 8 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 8 |
3 files changed, 16 insertions, 8 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index fb9e804..98c3856 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,11 @@ +2014-06-13 Hristian Kirtchev <kirtchev@adacore.com> + + * freeze.adb (Freeze_Entity): Remove the check concerning volatile + types in SPARK as it is poorly placed and poorly formulated. The + check was flagging ALL volatile entities as illegal in SPARK. + * sem_prag.adb (Process_Atomic_Shared_Volatile): Flag volatile + types as illegal in SPARK. + 2014-06-13 Robert Dewar <dewar@adacore.com> * sem_cat.adb: Minor reformatting. diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index e1bfc9a..ec944a1 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -3686,14 +3686,6 @@ package body Freeze is Analyze_Aspects_At_Freeze_Point (E); end if; - -- The following check is only relevant when SPARK_Mode is on as this - -- is not a standard Ada legality rule. Volatile types are not allowed - -- (SPARK RM C.6(1)). - - if SPARK_Mode = On and then Is_SPARK_Volatile (E) then - Error_Msg_N ("volatile type not allowed", E); - end if; - -- Here to freeze the entity Set_Is_Frozen (E); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index c4f10ee..284cdb5 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -6370,6 +6370,14 @@ package body Sem_Prag is Set_Treat_As_Volatile (E); Set_Treat_As_Volatile (Underlying_Type (E)); + -- The following check is only relevant when SPARK_Mode is on as + -- this is not a standard Ada legality rule. Volatile types are + -- not allowed (SPARK RM C.6(1)). + + if SPARK_Mode = On and then Prag_Id = Pragma_Volatile then + Error_Msg_N ("volatile type not allowed", E); + end if; + elsif K = N_Object_Declaration or else (K = N_Component_Declaration and then Original_Record_Component (E) = E) |