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 <kirtc...@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.
Index: sem_res.adb =================================================================== --- sem_res.adb (revision 219230) +++ sem_res.adb (working copy) @@ -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