diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index fb9e804b5f43..98c3856d85af 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,11 @@ +2014-06-13 Hristian Kirtchev + + * 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 * sem_cat.adb: Minor reformatting. diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index e1bfc9a3bbed..ec944a102be5 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 c4f10ee6635f..284cdb5c75b3 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)