git
/
gcc
mirror of git://gcc.gnu.org/git/gcc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

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
This commit is contained in:
Hristian Kirtchev 2014-06-13 09:51:30 +00:00 committed by Arnaud Charlet
parent e3a325f2f0
commit c00b86e2c3
3 changed files with 16 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
gcc/ada/ChangeLog
View File

@ -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.

8
gcc/ada/freeze.adb
View File

@ -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);

8
gcc/ada/sem_prag.adb
View File

@ -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)