This patch updates the resolution of actual parameters to flags all effectively
volatile objects with enabled property Async_Writers or Effective_Reads which
appear in the actual as illegal because the context is interfering.
------------
-- Source --
------------
-- volatiles.ads
package Volatiles with SPARK_Mode is
type Vol_Int is new Integer with Volatile;
function Vol_Func_1 (Obj : Vol_Int) return Vol_Int
with Volatile_Function;
function Vol_Func_2 (Obj : Vol_Int) return Boolean
with Volatile_Function;
Obj : Vol_Int := 0;
Error_1 : Vol_Int := Obj - Obj; -- Error
Error_2 : Vol_Int := Vol_Func_1 (1 + Obj); -- Error
Error_3 : Boolean := Vol_Func_2 (1 + Vol_Func_1 (1 + Obj)); -- Error
end Volatiles;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c volatiles.ads
volatiles.ads:12:25: volatile object cannot appear in this context (SPARK RM
7.1.3(12))
volatiles.ads:12:31: volatile object cannot appear in this context (SPARK RM
7.1.3(12))
volatiles.ads:13:41: volatile object cannot appear in this context (SPARK RM
7.1.3(11))
volatiles.ads:14:57: volatile object cannot appear in this context (SPARK RM
7.1.3(11))
Tested on x86_64-pc-linux-gnu, committed on trunk
2016-04-27 Hristian Kirtchev <kirtc...@adacore.com>
* sem_res.adb (Flag_Effectively_Volatile_Objects): New routine.
(Resolve_Actuals): Flag effectively volatile objects with enabled
property Async_Writers or Effective_Reads as illegal.
* sem_util.adb (Is_OK_Volatile_Context): Comment reformatting.
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 235481)
+++ sem_res.adb (working copy)
@@ -3107,6 +3107,10 @@
-- interpretation, but the form of the actual can only be determined
-- once the primitive operation is identified.
+ 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.13(12)).
+
procedure Insert_Default;
-- If the actual is missing in a call, insert in the actuals list
-- an instance of the default expression. The insertion is always
@@ -3360,6 +3364,55 @@
end if;
end Check_Prefixed_Call;
+ ---------------------------------------
+ -- Flag_Effectively_Volatile_Objects --
+ ---------------------------------------
+
+ 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.
+
+ -----------------
+ -- Flag_Object --
+ -----------------
+
+ function Flag_Object (N : Node_Id) return Traverse_Result is
+ Id : Entity_Id;
+
+ begin
+ -- Do not consider nested function calls because they have already
+ -- been processed during their own resolution.
+
+ if Nkind (N) = N_Function_Call then
+ return Skip;
+
+ elsif Is_Entity_Name (N) and then Present (Entity (N)) then
+ 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))
+ then
+ Error_Msg_N
+ ("volatile object cannot appear in this context (SPARK "
+ & "RM 7.1.3(11))", N);
+ return Skip;
+ end if;
+ end if;
+
+ return OK;
+ end Flag_Object;
+
+ procedure Flag_Objects is new Traverse_Proc (Flag_Object);
+
+ -- Start of processing for Flag_Effectively_Volatile_Objects
+
+ begin
+ Flag_Objects (Expr);
+ end Flag_Effectively_Volatile_Objects;
+
--------------------
-- Insert_Default --
--------------------
@@ -3461,7 +3514,6 @@
then
Set_Is_Controlling_Actual (Actval);
end if;
-
end if;
-- If the default expression raises constraint error, then just
@@ -4473,10 +4525,8 @@
-- they are not standard Ada legality rule. Internally generated
-- temporaries are ignored.
- if SPARK_Mode = On
- and then Comes_From_Source (A)
- and then Is_Effectively_Volatile_Object (A)
- then
+ 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(11)).
@@ -4493,10 +4543,23 @@
elsif Is_Unchecked_Conversion_Instance (Nam) then
null;
- else
+ -- The actual denotes an object
+
+ elsif Is_Effectively_Volatile_Object (A) then
Error_Msg_N
("volatile object cannot act as actual in a call (SPARK "
& "RM 7.1.3(11))", 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.
+
+ else
+ Flag_Effectively_Volatile_Objects (A);
end if;
-- Detect an external variable with an enabled property that
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 235491)
+++ sem_util.adb (working copy)
@@ -9314,7 +9314,7 @@
Has_Default_Aspect (Typ)
or else Has_Full_Default_Initialization (Component_Type (Typ));
- -- A protected type, record type or type extension is fully default
+ -- A protected type, record type, or type extension is fully default
-- initialized if all its components either carry an initialization
-- expression or have a type that is fully default initialized. The
-- parent type of a type extension must be fully default initialized.
@@ -13159,7 +13159,7 @@
when N_Function_Call =>
return Etype (N) /= Standard_Void_Type;
- -- Attributes 'Input, 'Loop_Entry, 'Old and 'Result produce
+ -- Attributes 'Input, 'Loop_Entry, 'Old, and 'Result produce
-- objects.
when N_Attribute_Reference =>
@@ -13346,14 +13346,15 @@
is
function Is_Protected_Operation_Call (Nod : Node_Id) return Boolean;
-- Determine whether an arbitrary node denotes a call to a protected
- -- entry, function or procedure in prefixed form where the prefix is
+ -- entry, function, or procedure in prefixed form where the prefix is
-- Obj_Ref.
function Within_Check (Nod : Node_Id) return Boolean;
-- Determine whether an arbitrary node appears in a check node
function Within_Subprogram_Call (Nod : Node_Id) return Boolean;
- -- Determine whether an arbitrary node appears in a procedure call
+ -- Determine whether an arbitrary node appears in an entry, function, or
+ -- procedure call.
function Within_Volatile_Function (Id : Entity_Id) return Boolean;
-- Determine whether an arbitrary entity appears in a volatile function
@@ -13405,7 +13406,7 @@
if Nkind (Par) in N_Raise_xxx_Error then
return True;
- -- Prevent the search from going too far
+ -- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Par) then
exit;
@@ -13435,7 +13436,7 @@
then
return True;
- -- Prevent the search from going too far
+ -- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Par) then
exit;
@@ -13481,8 +13482,8 @@
if Nkind (Context) = N_Assignment_Statement then
return True;
- -- The volatile object is part of the initialization expression of
- -- another object.
+ -- The volatile object is part of the initialization expression of
+ -- another object.
elsif Nkind (Context) = N_Object_Declaration
and then Present (Expression (Context))
@@ -13497,21 +13498,21 @@
if Is_Return_Object (Obj_Id) then
return Within_Volatile_Function (Obj_Id);
- -- Otherwise this is a normal object initialization
+ -- Otherwise this is a normal object initialization
else
return True;
end if;
- -- The volatile object acts as the name of a renaming declaration
+ -- The volatile object acts as the name of a renaming declaration
elsif Nkind (Context) = N_Object_Renaming_Declaration
and then Name (Context) = Obj_Ref
then
return True;
- -- The volatile object appears as an actual parameter in a call to an
- -- instance of Unchecked_Conversion whose result is renamed.
+ -- The volatile object appears as an actual parameter in a call to an
+ -- instance of Unchecked_Conversion whose result is renamed.
elsif Nkind (Context) = N_Function_Call
and then Is_Entity_Name (Name (Context))
@@ -13520,14 +13521,14 @@
then
return True;
- -- The volatile object is actually the prefix in a protected entry,
- -- function, or procedure call.
+ -- The volatile object is actually the prefix in a protected entry,
+ -- function, or procedure call.
elsif Is_Protected_Operation_Call (Context) then
return True;
- -- The volatile object appears as the expression of a simple return
- -- statement that applies to a volatile function.
+ -- The volatile object appears as the expression of a simple return
+ -- statement that applies to a volatile function.
elsif Nkind (Context) = N_Simple_Return_Statement
and then Expression (Context) = Obj_Ref
@@ -13535,8 +13536,8 @@
return
Within_Volatile_Function (Return_Statement_Entity (Context));
- -- The volatile object appears as the prefix of a name occurring in a
- -- non-interfering context.
+ -- The volatile object appears as the prefix of a name occurring in a
+ -- non-interfering context.
elsif Nkind_In (Context, N_Attribute_Reference,
N_Explicit_Dereference,
@@ -13550,8 +13551,8 @@
then
return True;
- -- The volatile object appears as the expression of a type conversion
- -- occurring in a non-interfering context.
+ -- The volatile object appears as the expression of a type conversion
+ -- occurring in a non-interfering context.
elsif Nkind_In (Context, N_Type_Conversion,
N_Unchecked_Type_Conversion)
@@ -13562,21 +13563,22 @@
then
return True;
- -- Allow references to volatile objects in various checks. This is
- -- not a direct SPARK 2014 requirement.
+ -- Allow references to volatile objects in various checks. This is not a
+ -- direct SPARK 2014 requirement.
elsif Within_Check (Context) then
return True;
- -- Assume that references to effectively volatile objects that appear
- -- as actual parameters in a subprogram call are always legal. A full
- -- legality check is done when the actuals are resolved.
+ -- Assume that references to effectively volatile objects that appear
+ -- as actual parameters in a subprogram call are always legal. A full
+ -- legality check is done when the actuals are resolved (see routine
+ -- Resolve_Actuals).
elsif Within_Subprogram_Call (Context) then
return True;
- -- Otherwise the context is not suitable for an effectively volatile
- -- object.
+ -- Otherwise the context is not suitable for an effectively volatile
+ -- object.
else
return False;
@@ -13888,7 +13890,7 @@
begin
-- Verify that prefix is analyzed and has the proper form. Note that
- -- the attributes Elab_Spec, Elab_Body and Elab_Subp_Body which also
+ -- the attributes Elab_Spec, Elab_Body, and Elab_Subp_Body, which also
-- produce the address of an entity, do not analyze their prefix
-- because they denote entities that are not necessarily visible.
-- Neither of them can apply to a protected type.
@@ -16034,7 +16036,7 @@
procedure Copy_Itype_With_Replacement (New_Itype : Entity_Id) is
begin
- -- Translate Next_Entity, Scope and Etype fields, in case they
+ -- Translate Next_Entity, Scope, and Etype fields, in case they
-- reference entities that have been mapped into copies.
Set_Next_Entity (New_Itype, Assoc (Next_Entity (New_Itype)));
@@ -19986,8 +19988,8 @@
return False;
end if;
- -- Check that the size of the component is 8, 16, 32 or 64 bits and that
- -- Typ is properly aligned.
+ -- Check that the size of the component is 8, 16, 32, or 64 bits and
+ -- that Typ is properly aligned.
case Size is
when 8 | 16 | 32 | 64 =>
