===================================================================
@@ -4250,14 +4250,25 @@
end if;
-- In Ada 83 we cannot pass an OUT parameter as an IN or IN OUT
- -- actual to a nested call, since this is case of reading an
- -- out parameter, which is not allowed.
+ -- actual to a nested call, since this constitutes a reading of
+ -- the parameter, which is not allowed.
- if Ada_Version = Ada_83
- and then Is_Entity_Name (A)
+ if Is_Entity_Name (A)
and then Ekind (Entity (A)) = E_Out_Parameter
then
- Error_Msg_N ("(Ada 83) illegal reading of out parameter", A);
+ if Ada_Version = Ada_83 then
+ Error_Msg_N
+ ("(Ada 83) illegal reading of out parameter", A);
+
+ -- An effectively volatile OUT parameter cannot act as IN or
+ -- IN OUT actual in a call (SPARK RM 7.1.3(11)).
+
+ elsif SPARK_Mode = On
+ and then Is_Effectively_Volatile (Entity (A))
+ then
+ Error_Msg_N
+ ("illegal reading of volatile OUT parameter", A);
+ end if;
end if;
end if;
@@ -5444,8 +5455,8 @@
N_Unchecked_Type_Conversion)
then
Error_Msg_N
- ("(Ada 83) fixed-point operation "
- & "needs explicit conversion", N);
+ ("(Ada 83) fixed-point operation needs explicit "
+ & "conversion", N);
end if;
-- The expected type is "any real type" in contexts like
@@ -6886,6 +6897,12 @@
-- Used to resolve identifiers and expanded names
procedure Resolve_Entity_Name (N : Node_Id; Typ : Entity_Id) is
+ function Is_Assignment_Or_Object_Expression
+ (Context : Node_Id;
+ Expr : Node_Id) return Boolean;
+ -- Determine whether node Context denotes an assignment statement or an
+ -- object declaration whose expression is node Expr.
+
function Is_OK_Volatile_Context
(Context : Node_Id;
Obj_Ref : Node_Id) return Boolean;
@@ -6893,6 +6910,48 @@
-- (as defined in SPARK RM 7.1.3(13)) where volatile reference Obj_Ref
-- can safely reside.
+ ----------------------------------------
+ -- Is_Assignment_Or_Object_Expression --
+ ----------------------------------------
+
+ function Is_Assignment_Or_Object_Expression
+ (Context : Node_Id;
+ Expr : Node_Id) return Boolean
+ is
+ begin
+ if Nkind_In (Context, N_Assignment_Statement,
+ N_Object_Declaration)
+ and then Expression (Context) = Expr
+ then
+ return True;
+
+ -- Check whether a construct that yields a name is the expression of
+ -- an assignment statement or an object declaration.
+
+ elsif (Nkind_In (Context, N_Attribute_Reference,
+ N_Explicit_Dereference,
+ N_Indexed_Component,
+ N_Selected_Component,
+ N_Slice)
+ and then Prefix (Context) = Expr)
+ or else
+ (Nkind_In (Context, N_Type_Conversion,
+ N_Unchecked_Type_Conversion)
+ and then Expression (Context) = Expr)
+ then
+ return
+ Is_Assignment_Or_Object_Expression
+ (Context => Parent (Context),
+ Expr => Context);
+
+ -- Otherwise the context is not an assignment statement or an object
+ -- declaration.
+
+ else
+ return False;
+ end if;
+ end Is_Assignment_Or_Object_Expression;
+
----------------------------
-- Is_OK_Volatile_Context --
----------------------------
@@ -6992,6 +7051,7 @@
-- in a non-interfering context.
elsif Nkind_In (Context, N_Attribute_Reference,
+ N_Explicit_Dereference,
N_Indexed_Component,
N_Selected_Component,
N_Slice)
@@ -7107,15 +7167,27 @@
elsif Ekind (E) = E_Generic_Function then
Error_Msg_N ("illegal use of generic function", N);
+ -- In Ada 83 an OUT parameter cannot be read
+
elsif Ekind (E) = E_Out_Parameter
- and then Ada_Version = Ada_83
and then (Nkind (Parent (N)) in N_Op
- or else (Nkind (Parent (N)) = N_Assignment_Statement
- and then N = Expression (Parent (N)))
- or else Nkind (Parent (N)) = N_Explicit_Dereference)
+ or else Nkind (Parent (N)) = N_Explicit_Dereference
+ or else Is_Assignment_Or_Object_Expression
+ (Context => Parent (N),
+ Expr => N))
then
- Error_Msg_N ("(Ada 83) illegal reading of out parameter", N);
+ if Ada_Version = Ada_83 then
+ Error_Msg_N ("(Ada 83) illegal reading of out parameter", N);
+ -- An effectively volatile OUT parameter cannot be read
+ -- (SPARK RM 7.1.3(11)).
+
+ elsif SPARK_Mode = On
+ and then Is_Effectively_Volatile (E)
+ then
+ Error_Msg_N ("illegal reading of volatile OUT parameter", N);
+ end if;
+
-- In all other cases, just do the possible static evaluation
else
This patch implements a side effect of SPARK RM rule 7.1.3(11) which implies that an effectively volatile formal parameter of mode out cannot be read. ------------ -- Source -- ------------ -- async_writers_out.ads package Async_Writers_Out with SPARK_Mode is type Volat_Array is array (1 .. 5) of Integer with Volatile; type Volat_Rec is record Id : Integer := 0; end record with Volatile; procedure Error_1 (Result : out Volat_Array); procedure Error_2 (Result : out Volat_Rec); procedure OK_1; procedure OK_2; end Async_Writers_Out; -- async_writers_out.adb package body Async_Writers_Out with SPARK_Mode is Obj_1 : Volat_Array with Async_Readers, Async_Writers; Obj_2 : Volat_Rec with Async_Readers, Async_Writers; procedure Reference_1 (Result : out Volat_Array); procedure Reference_2 (Result : out Volat_Rec); procedure Error_1 (Result : out Volat_Array) is Comp : constant Integer := Result (3); -- ERROR begin Result (1) := 1 + Result (5); -- ERROR end Error_1; procedure Error_2 (Result : out Volat_Rec) is Comp : constant Integer := Result.Id; -- ERROR begin null; end Error_2; procedure OK_1 is begin Reference_1 (Obj_1); -- OK end OK_1; procedure OK_2 is begin Reference_2 (Obj_2); -- OK end OK_2; procedure Reference_1 (Result : out Volat_Array) is begin null; end Reference_1; procedure Reference_2 (Result : out Volat_Rec) is begin null; end Reference_2; end Async_Writers_Out; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c async_writers_out.adb async_writers_out.adb:9:34: illegal reading of volatile "out" parameter async_writers_out.adb:11:25: volatile object cannot appear in this context (SPARK RM 7.1.3(13)) async_writers_out.adb:15:34: illegal reading of volatile "out" parameter Tested on x86_64-pc-linux-gnu, committed on trunk 2015-01-06 Hristian Kirtchev <kirtchev@adacore.com> * sem_res.adb (Is_Assignment_Or_Object_Expression): New routine. (Resolve_Actuals): An effectively volatile out parameter cannot act as an in or in out actual in a call. (Resolve_Entity_Name): An effectively volatile out parameter cannot be read.