@@ -2467,10 +2467,11 @@ package body Sem_Prag is
elsif SPARK_Mode = On
and then Ekind (Item_Id) = E_Variable
- and then Is_Effectively_Volatile (Item_Id)
+ and then Is_Effectively_Volatile_For_Reading (Item_Id)
then
- -- An effectively volatile object cannot appear as a global
- -- item of a nonvolatile function (SPARK RM 7.1.3(8)).
+ -- An effectively volatile object for reading cannot appear
+ -- as a global item of a nonvolatile function (SPARK RM
+ -- 7.1.3(8)).
if Ekind (Spec_Id) in E_Function | E_Generic_Function
and then not Is_Volatile_Function (Spec_Id)
@@ -3428,7 +3428,7 @@ package body Sem_Res is
procedure Flag_Effectively_Volatile_Objects (Expr : Node_Id);
-- Emit an error concerning the illegal usage of an effectively volatile
- -- object in interfering context (SPARK RM 7.1.3(10)).
+ -- object for reading in interfering context (SPARK RM 7.1.3(10)).
procedure Insert_Default;
-- If the actual is missing in a call, insert in the actuals list
@@ -3687,7 +3687,7 @@ package body Sem_Res is
procedure Flag_Effectively_Volatile_Objects (Expr : Node_Id) is
function Flag_Object (N : Node_Id) return Traverse_Result;
-- Determine whether arbitrary node N denotes an effectively volatile
- -- object and if it does, emit an error.
+ -- object for reading and if it does, emit an error.
-----------------
-- Flag_Object --
@@ -3707,9 +3707,7 @@ package body Sem_Res is
Id := Entity (N);
if Is_Object (Id)
- and then Is_Effectively_Volatile (Id)
- and then (Async_Writers_Enabled (Id)
- or else Effective_Reads_Enabled (Id))
+ and then Is_Effectively_Volatile_For_Reading (Id)
then
Error_Msg_N
("volatile object cannot appear in this context (SPARK "
@@ -4876,17 +4874,17 @@ package body Sem_Res is
if SPARK_Mode = On and then Comes_From_Source (A) then
- -- An effectively volatile object may act as an actual when the
- -- corresponding formal is of a non-scalar effectively volatile
- -- type (SPARK RM 7.1.3(10)).
+ -- An effectively volatile object for reading may act as an
+ -- actual when the corresponding formal is of a non-scalar
+ -- effectively volatile type for reading (SPARK RM 7.1.3(10)).
if not Is_Scalar_Type (Etype (F))
- and then Is_Effectively_Volatile (Etype (F))
+ and then Is_Effectively_Volatile_For_Reading (Etype (F))
then
null;
- -- An effectively volatile object may act as an actual in a
- -- call to an instance of Unchecked_Conversion.
+ -- An effectively volatile object for reading may act as an
+ -- actual in a call to an instance of Unchecked_Conversion.
-- (SPARK RM 7.1.3(10)).
elsif Is_Unchecked_Conversion_Instance (Nam) then
@@ -4894,18 +4892,18 @@ package body Sem_Res is
-- The actual denotes an object
- elsif Is_Effectively_Volatile_Object (A) then
+ elsif Is_Effectively_Volatile_Object_For_Reading (A) then
Error_Msg_N
("volatile object cannot act as actual in a call (SPARK "
& "RM 7.1.3(10))", A);
-- Otherwise the actual denotes an expression. Inspect the
- -- expression and flag each effectively volatile object with
- -- enabled property Async_Writers or Effective_Reads as illegal
- -- because it apprears within an interfering context. Note that
- -- this is usually done in Resolve_Entity_Name, but when the
- -- effectively volatile object appears as an actual in a call,
- -- the call must be resolved first.
+ -- expression and flag each effectively volatile object
+ -- for reading as illegal because it apprears within an
+ -- interfering context. Note that this is usually done in
+ -- Resolve_Entity_Name, but when the effectively volatile
+ -- object for reading appears as an actual in a call, the
+ -- call must be resolved first.
else
Flag_Effectively_Volatile_Objects (A);
@@ -4923,7 +4921,7 @@ package body Sem_Res is
A_Id := Entity (A);
if Ekind (A_Id) = E_Variable
- and then Is_Effectively_Volatile (Etype (A_Id))
+ and then Is_Effectively_Volatile_For_Reading (Etype (A_Id))
and then Effective_Reads_Enabled (A_Id)
then
Error_Msg_NE
@@ -7770,14 +7768,11 @@ package body Sem_Res is
if SPARK_Mode = On then
- -- An effectively volatile object subject to enabled properties
- -- Async_Writers or Effective_Reads must appear in non-interfering
- -- context (SPARK RM 7.1.3(10)).
+ -- An effectively volatile object for reading must appear in
+ -- non-interfering context (SPARK RM 7.1.3(10)).
if Is_Object (E)
- and then Is_Effectively_Volatile (E)
- and then (Async_Writers_Enabled (E)
- or else Effective_Reads_Enabled (E))
+ and then Is_Effectively_Volatile_For_Reading (E)
and then not Is_OK_Volatile_Context (Par, N)
then
SPARK_Msg_N
@@ -127,6 +127,15 @@ package body Sem_Util is
-- Determine whether arbitrary entity Id denotes an atomic object as per
-- RM C.6(7).
+ generic
+ with function Is_Effectively_Volatile_Entity
+ (Id : Entity_Id) return Boolean;
+ -- Function to use on object and type entities
+ function Is_Effectively_Volatile_Object_Shared
+ (N : Node_Id) return Boolean;
+ -- Shared function used to detect effectively volatile objects and
+ -- effectively volatile objects for reading.
+
function Is_Fully_Initialized_Variant (Typ : Entity_Id) return Boolean;
-- Subsidiary to Is_Fully_Initialized_Type. For an unconstrained type
-- with discriminants whose default values are static, examine only the
@@ -3626,7 +3635,7 @@ package body Sem_Util is
Formal := First_Formal (Func_Id);
while Present (Formal) loop
- if Is_Effectively_Volatile (Etype (Formal)) then
+ if Is_Effectively_Volatile_For_Reading (Etype (Formal)) then
Error_Msg_NE
("nonvolatile function & cannot have a volatile parameter",
Formal, Func_Id);
@@ -3637,7 +3646,7 @@ package body Sem_Util is
-- Inspect the return type
- if Is_Effectively_Volatile (Etype (Func_Id)) then
+ if Is_Effectively_Volatile_For_Reading (Etype (Func_Id)) then
Error_Msg_NE
("nonvolatile function & cannot have a volatile return type",
Result_Definition (Parent (Func_Id)), Func_Id);
@@ -11222,11 +11231,11 @@ package body Sem_Util is
begin
-- Inspect the formal parameters looking for an effectively volatile
- -- type.
+ -- type for reading.
Formal := First_Formal (Subp_Id);
while Present (Formal) loop
- if Is_Effectively_Volatile (Etype (Formal)) then
+ if Is_Effectively_Volatile_For_Reading (Etype (Formal)) then
return True;
end if;
@@ -11236,7 +11245,7 @@ package body Sem_Util is
-- Inspect the return type of functions
if Ekind (Subp_Id) in E_Function | E_Generic_Function
- and then Is_Effectively_Volatile (Etype (Subp_Id))
+ and then Is_Effectively_Volatile_For_Reading (Etype (Subp_Id))
then
return True;
end if;
@@ -11610,7 +11619,7 @@ package body Sem_Util is
if Ekind (Item_Id) = E_Abstract_State then
return State_Has_Enabled_Property;
- elsif Ekind (Item_Id) = E_Variable then
+ elsif Ekind (Item_Id) in E_Variable | E_Constant then
return Type_Or_Variable_Has_Enabled_Property (Item_Id);
-- Other objects can only inherit properties through their type. We
@@ -15747,35 +15756,115 @@ package body Sem_Util is
end if;
end Is_Effectively_Volatile;
+ -----------------------------------------
+ -- Is_Effectively_Volatile_For_Reading --
+ -----------------------------------------
+
+ function Is_Effectively_Volatile_For_Reading
+ (Id : Entity_Id) return Boolean
+ is
+ begin
+ -- A concurrent type is effectively volatile for reading
+
+ if Is_Concurrent_Type (Id) then
+ return True;
+
+ elsif Is_Effectively_Volatile (Id) then
+
+ -- Other volatile types and objects are effectively volatile for
+ -- reading when they have property Async_Writers or Effective_Reads
+ -- set to True. This includes the case of an array type whose
+ -- Volatile_Components aspect is True (hence it is effectively
+ -- volatile) which does not have the properties Async_Writers
+ -- and Effective_Reads set to False.
+
+ if Async_Writers_Enabled (Id)
+ or else Effective_Reads_Enabled (Id)
+ then
+ return True;
+
+ -- In addition, an array type is effectively volatile for reading
+ -- when its component type is effectively volatile for reading.
+
+ elsif Is_Array_Type (Id) then
+ declare
+ Anc : Entity_Id := Base_Type (Id);
+ begin
+ if Is_Private_Type (Anc) then
+ Anc := Full_View (Anc);
+ end if;
+
+ -- Test for presence of ancestor, as the full view of a
+ -- private type may be missing in case of error.
+
+ return
+ Present (Anc)
+ and then Is_Effectively_Volatile_For_Reading
+ (Component_Type (Anc));
+ end;
+ end if;
+ end if;
+
+ return False;
+
+ end Is_Effectively_Volatile_For_Reading;
+
------------------------------------
-- Is_Effectively_Volatile_Object --
------------------------------------
function Is_Effectively_Volatile_Object (N : Node_Id) return Boolean is
+ function Is_Effectively_Volatile_Object_Inst
+ is new Is_Effectively_Volatile_Object_Shared (Is_Effectively_Volatile);
+ begin
+ return Is_Effectively_Volatile_Object_Inst (N);
+ end Is_Effectively_Volatile_Object;
+
+ ------------------------------------------------
+ -- Is_Effectively_Volatile_Object_For_Reading --
+ ------------------------------------------------
+
+ function Is_Effectively_Volatile_Object_For_Reading
+ (N : Node_Id) return Boolean
+ is
+ function Is_Effectively_Volatile_Object_For_Reading_Inst
+ is new Is_Effectively_Volatile_Object_Shared
+ (Is_Effectively_Volatile_For_Reading);
+ begin
+ return Is_Effectively_Volatile_Object_For_Reading_Inst (N);
+ end Is_Effectively_Volatile_Object_For_Reading;
+
+ -------------------------------------------
+ -- Is_Effectively_Volatile_Object_Shared --
+ -------------------------------------------
+
+ function Is_Effectively_Volatile_Object_Shared
+ (N : Node_Id) return Boolean
+ is
begin
if Is_Entity_Name (N) then
return Is_Object (Entity (N))
- and then Is_Effectively_Volatile (Entity (N));
+ and then Is_Effectively_Volatile_Entity (Entity (N));
elsif Nkind (N) in N_Indexed_Component | N_Slice then
- return Is_Effectively_Volatile_Object (Prefix (N));
+ return Is_Effectively_Volatile_Object_Shared (Prefix (N));
elsif Nkind (N) = N_Selected_Component then
return
- Is_Effectively_Volatile_Object (Prefix (N))
+ Is_Effectively_Volatile_Object_Shared (Prefix (N))
or else
- Is_Effectively_Volatile_Object (Selector_Name (N));
+ Is_Effectively_Volatile_Object_Shared (Selector_Name (N));
elsif Nkind (N) in N_Qualified_Expression
| N_Unchecked_Type_Conversion
| N_Type_Conversion
then
- return Is_Effectively_Volatile_Object (Expression (N));
+ return Is_Effectively_Volatile_Object_Shared (Expression (N));
else
return False;
end if;
- end Is_Effectively_Volatile_Object;
+ end Is_Effectively_Volatile_Object_Shared;
-------------------
-- Is_Entry_Body --
@@ -408,7 +408,7 @@ package Sem_Util is
procedure Check_Nonvolatile_Function_Profile (Func_Id : Entity_Id);
-- Verify that the profile of nonvolatile function Func_Id does not contain
- -- effectively volatile parameters or return type.
+ -- effectively volatile parameters or return type for reading.
procedure Check_Part_Of_Reference (Var_Id : Entity_Id; Ref : Node_Id);
-- Verify the legality of reference Ref to variable Var_Id when the
@@ -1289,7 +1289,8 @@ package Sem_Util is
function Has_Effectively_Volatile_Profile
(Subp_Id : Entity_Id) return Boolean;
-- Determine whether subprogram Subp_Id has an effectively volatile formal
- -- parameter or returns an effectively volatile value.
+ -- parameter for reading or returns an effectively volatile value for
+ -- reading.
function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean;
-- Determine whether type Typ defines "full default initialization" as
@@ -1797,10 +1798,30 @@ package Sem_Util is
-- * A protected type
-- * Descendant of type Ada.Synchronous_Task_Control.Suspension_Object
- function Is_Effectively_Volatile_Object (N : Node_Id) return Boolean;
+ function Is_Effectively_Volatile_For_Reading
+ (Id : Entity_Id) return Boolean;
+ -- Determine whether a type or object denoted by entity Id is effectively
+ -- volatile for reading (SPARK RM 7.1.2). To qualify as such, the entity
+ -- must be either
+ -- * Volatile without No_Caching and have Async_Writers or
+ -- Effective_Reads set to True
+ -- * An array type subject to aspect Volatile_Components, unless it has
+ -- Async_Writers and Effective_Reads set to False
+ -- * An array type whose component type is effectively volatile for
+ -- reading
+ -- * A protected type
+ -- * Descendant of type Ada.Synchronous_Task_Control.Suspension_Object
+
+ function Is_Effectively_Volatile_Object
+ (N : Node_Id) return Boolean;
-- Determine whether an arbitrary node denotes an effectively volatile
-- object (SPARK RM 7.1.2).
+ function Is_Effectively_Volatile_Object_For_Reading
+ (N : Node_Id) return Boolean;
+ -- Determine whether an arbitrary node denotes an effectively volatile
+ -- object for reading (SPARK RM 7.1.2).
+
function Is_Entry_Body (Id : Entity_Id) return Boolean;
-- Determine whether entity Id is the body entity of an entry [family]