FreeChainXenon/gcc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

freeze.adb (Freeze_Record_Type): Update the use of Is_SPARK_Volatile.

Browse source 
2014-05-21  Hristian Kirtchev  <kirtchev@adacore.com>

	* freeze.adb (Freeze_Record_Type): Update the use of
	Is_SPARK_Volatile.
	* sem_ch3.adb (Analyze_Object_Contract): Update the use of
	Is_SPARK_Volatile.
	(Process_Discriminants): Update the use of Is_SPARK_Volatile.
	* sem_ch5.adb (Analyze_Iterator_Specification): Update the use
	of Is_SPARK_Volatile.
	(Analyze_Loop_Parameter_Specification):
	Update the use of Is_SPARK_Volatile.
	* sem_ch6.adb (Process_Formals): Catch an illegal use of an IN
	formal parameter when its type is volatile.
	* sem_prag.adb (Analyze_Global_Item): Update the use of
	Is_SPARK_Volatile.
	* sem_res.adb (Resolve_Entity_Name): Correct the guard which
	determines whether an entity is a volatile source SPARK object.
	* sem_util.adb (Has_Enabled_Property): Accout for external
	properties being set on objects other than abstract states
	and variables. An example would be a formal parameter.
	(Is_SPARK_Volatile): New routine.
	(Is_SPARK_Volatile_Object):
	Remove the entity-specific tests. Call routine Is_SPARK_Volatile
	when checking entities and/or types.
	* sem_util.ads (Is_SPARK_Volatile): New routine.

From-SVN: r210708
This commit is contained in:
Hristian Kirtchev 2014-05-21 13:21:38 +00:00 • committed by Arnaud Charlet
parent 65529f7481
commit ea26c8e414
9 changed files with 94 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
gcc/ada/ChangeLog
View file

@ -1,3 +1,29 @@
2014-05-21 Hristian Kirtchev <kirtchev@adacore.com>
* freeze.adb (Freeze_Record_Type): Update the use of
Is_SPARK_Volatile.
* sem_ch3.adb (Analyze_Object_Contract): Update the use of
Is_SPARK_Volatile.
(Process_Discriminants): Update the use of Is_SPARK_Volatile.
* sem_ch5.adb (Analyze_Iterator_Specification): Update the use
of Is_SPARK_Volatile.
(Analyze_Loop_Parameter_Specification):
Update the use of Is_SPARK_Volatile.
* sem_ch6.adb (Process_Formals): Catch an illegal use of an IN
formal parameter when its type is volatile.
* sem_prag.adb (Analyze_Global_Item): Update the use of
Is_SPARK_Volatile.
* sem_res.adb (Resolve_Entity_Name): Correct the guard which
determines whether an entity is a volatile source SPARK object.
* sem_util.adb (Has_Enabled_Property): Accout for external
properties being set on objects other than abstract states
and variables. An example would be a formal parameter.
(Is_SPARK_Volatile): New routine.
(Is_SPARK_Volatile_Object):
Remove the entity-specific tests. Call routine Is_SPARK_Volatile
when checking entities and/or types.
* sem_util.ads (Is_SPARK_Volatile): New routine.
2014-05-21 Robert Dewar <dewar@adacore.com>
* sem_warn.adb: Minor fix to warning messages (use ?? instead

4
gcc/ada/freeze.adb
View file

@ -3318,7 +3318,7 @@ package body Freeze is
-- they are not standard Ada legality rules.
if SPARK_Mode = On then
if Is_SPARK_Volatile_Object (Rec) then
if Is_SPARK_Volatile (Rec) then
-- A discriminated type cannot be volatile (SPARK RM C.6(4))
@ -3340,7 +3340,7 @@ package body Freeze is
Comp := First_Component (Rec);
while Present (Comp) loop
if Comes_From_Source (Comp)
and then Is_SPARK_Volatile_Object (Comp)
and then Is_SPARK_Volatile (Comp)
then
Error_Msg_Name_1 := Chars (Rec);
Error_Msg_N

8
gcc/ada/sem_ch3.adb
View file

@ -2988,7 +2988,7 @@ package body Sem_Ch3 is
-- actuals in instantiations (SPARK RM 7.1.3(6)).
if SPARK_Mode = On
and then Is_SPARK_Volatile_Object (Obj_Id)
and then Is_SPARK_Volatile (Obj_Id)
and then No (Corresponding_Generic_Association (Parent (Obj_Id)))
then
Error_Msg_N ("constant cannot be volatile", Obj_Id);
@ -3000,7 +3000,7 @@ package body Sem_Ch3 is
-- they are not standard Ada legality rules.
if SPARK_Mode = On then
if Is_SPARK_Volatile_Object (Obj_Id) then
if Is_SPARK_Volatile (Obj_Id) then
-- The declaration of a volatile object must appear at the
-- library level (SPARK RM 7.1.3(7), C.6(6)).
@ -3030,7 +3030,7 @@ package body Sem_Ch3 is
-- A non-volatile object cannot have volatile components
-- (SPARK RM 7.1.3(7)).
if not Is_SPARK_Volatile_Object (Obj_Id)
if not Is_SPARK_Volatile (Obj_Id)
and then Has_Volatile_Component (Obj_Typ)
then
Error_Msg_N
@ -18051,7 +18051,7 @@ package body Sem_Ch3 is
-- (SPARK RM 7.1.3(6)).
if SPARK_Mode = On
and then Is_SPARK_Volatile_Object (Defining_Identifier (Discr))
and then Is_SPARK_Volatile (Defining_Identifier (Discr))
then
Error_Msg_N ("discriminant cannot be volatile", Discr);
end if;

4
gcc/ada/sem_ch5.adb
View file

@ -1986,7 +1986,7 @@ package body Sem_Ch5 is
if SPARK_Mode = On
and then not Of_Present (N)
and then Is_SPARK_Volatile_Object (Ent)
and then Is_SPARK_Volatile (Ent)
then
Error_Msg_N ("loop parameter cannot be volatile", Ent);
end if;
@ -2706,7 +2706,7 @@ package body Sem_Ch5 is
-- when SPARK_Mode is on as it is not a standard Ada legality check
-- (SPARK RM 7.1.3(6)).
if SPARK_Mode = On and then Is_SPARK_Volatile_Object (Id) then
if SPARK_Mode = On and then Is_SPARK_Volatile (Id) then
Error_Msg_N ("loop parameter cannot be volatile", Id);
end if;
end Analyze_Loop_Parameter_Specification;

42
gcc/ada/sem_ch6.adb
View file

@ -11511,23 +11511,35 @@ package body Sem_Ch6 is
-- The following checks are relevant when SPARK_Mode is on as these
-- are not standard Ada legality rules.
if SPARK_Mode = On
and then Ekind_In (Scope (Formal), E_Function, E_Generic_Function)
then
-- A function cannot have a parameter of mode IN OUT or OUT
-- (SPARK RM 6.1).
if SPARK_Mode = On then
if Ekind_In (Scope (Formal), E_Function, E_Generic_Function) then
if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
-- A function cannot have a parameter of mode IN OUT or OUT
-- (SPARK RM 6.1).
if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
Error_Msg_N
("function cannot have parameter of mode `OUT` or "
& "`IN OUT`", Formal);
-- A function cannot have a volatile formal parameter
-- (SPARK RM 7.1.3(10)).
elsif Is_SPARK_Volatile (Formal) then
Error_Msg_N
("function cannot have a volatile formal parameter",
Formal);
end if;
-- A procedure cannot have a formal parameter of mode IN because
-- it behaves as a constant (SPARK RM 7.1.3(6)).
elsif Ekind (Scope (Formal)) = E_Procedure
and then Ekind (Formal) = E_In_Parameter
and then Is_SPARK_Volatile (Formal)
then
Error_Msg_N
("function cannot have parameter of mode `OUT` or `IN OUT`",
Formal);
-- A function cannot have a volatile formal parameter
-- (SPARK RM 7.1.3(10)).
elsif Is_SPARK_Volatile_Object (Formal) then
Error_Msg_N
("function cannot have a volatile formal parameter", Formal);
("formal parameter of mode `IN` cannot be volatile", Formal);
end if;
end if;

5
gcc/ada/sem_prag.adb
View file

@ -2038,9 +2038,8 @@ package body Sem_Prag is
-- SPARK_Mode is on as they are not standard Ada legality
-- rules.
elsif SPARK_Mode = On
and then Is_SPARK_Volatile_Object (Item_Id)
then
elsif SPARK_Mode = On and then Is_SPARK_Volatile (Item_Id) then
-- A volatile object cannot appear as a global item of a
-- function (SPARK RM 7.1.3(9)).

5
gcc/ada/sem_res.adb
View file

@ -6579,8 +6579,9 @@ package body Sem_Res is
-- standard Ada legality rules.
if SPARK_Mode = On
and then Ekind_In (E, E_Abstract_State, E_Variable)
and then Is_SPARK_Volatile_Object (E)
and then Is_Object (E)
and then Is_SPARK_Volatile (E)
and then Comes_From_Source (E)
and then
(Async_Writers_Enabled (E)
or else Effective_Reads_Enabled (E))

32
gcc/ada/sem_util.adb
View file

@ -7466,7 +7466,7 @@ package body Sem_Util is
begin
-- A non-volatile object can never possess external properties
if not Is_SPARK_Volatile_Object (Item_Id) then
if not Is_SPARK_Volatile (Item_Id) then
return False;
-- External properties related to variables come in two flavors -
@ -7514,11 +7514,19 @@ package body Sem_Util is
-- Start of processing for Has_Enabled_Property
begin
-- Abstract states and variables have a flexible scheme of specifying
-- external properties.
if Ekind (Item_Id) = E_Abstract_State then
return State_Has_Enabled_Property;
else pragma Assert (Ekind (Item_Id) = E_Variable);
elsif Ekind (Item_Id) = E_Variable then
return Variable_Has_Enabled_Property;
-- Otherwise a property is enabled when the related object is volatile
else
return Is_SPARK_Volatile (Item_Id);
end if;
end Has_Enabled_Property;
@ -11413,22 +11421,26 @@ package body Sem_Util is
end if;
end Is_SPARK_Object_Reference;
-----------------------
-- Is_SPARK_Volatile --
-----------------------
function Is_SPARK_Volatile (Id : Entity_Id) return Boolean is
begin
return Is_Volatile (Id) or else Is_Volatile (Etype (Id));
end Is_SPARK_Volatile;
------------------------------
-- Is_SPARK_Volatile_Object --
------------------------------
function Is_SPARK_Volatile_Object (N : Node_Id) return Boolean is
begin
if Nkind (N) = N_Defining_Identifier then
return Is_Volatile (N) or else Is_Volatile (Etype (N));
elsif Is_Entity_Name (N) then
return
Is_SPARK_Volatile_Object (Entity (N))
or else Is_Volatile (Etype (N));
if Is_Entity_Name (N) then
return Is_SPARK_Volatile (Entity (N));
elsif Nkind (N) = N_Expanded_Name then
return Is_SPARK_Volatile_Object (Entity (N));
return Is_SPARK_Volatile (Entity (N));
elsif Nkind (N) = N_Indexed_Component then
return Is_SPARK_Volatile_Object (Prefix (N));

7
gcc/ada/sem_util.ads
View file

@ -1302,10 +1302,15 @@ package Sem_Util is
function Is_SPARK_Object_Reference (N : Node_Id) return Boolean;
-- Determines if the tree referenced by N represents an object in SPARK
function Is_SPARK_Volatile (Id : Entity_Id) return Boolean;
-- This routine is similar to predicate Is_Volatile, but it takes SPARK
-- semantics into account. In SPARK volatile components to not render a
-- type volatile.
function Is_SPARK_Volatile_Object (N : Node_Id) return Boolean;
-- Determine whether an arbitrary node denotes a volatile object reference
-- according to the semantics of SPARK. To qualify as volatile, an object
-- must be subject to aspect/pragma Volatile or Atomic or have a [sub]type
-- must be subject to aspect/pragma Volatile or Atomic, or have a [sub]type
-- subject to the same attributes. Note that volatile components do not
-- render an object volatile.