From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (qmail 25657 invoked by alias); 6 Jan 2015 09:18:29 -0000 Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Received: (qmail 25551 invoked by uid 89); 6 Jan 2015 09:18:28 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham version=3.3.2 X-HELO: rock.gnat.com Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with (AES256-SHA encrypted) ESMTPS; Tue, 06 Jan 2015 09:18:26 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 8725C116432; Tue, 6 Jan 2015 04:18:24 -0500 (EST) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id Q5P0SBrgWt1W; Tue, 6 Jan 2015 04:18:24 -0500 (EST) Received: from kwai.gnat.com (kwai.gnat.com [IPv6:2620:20:4000:0:7a2b:cbff:fe60:cb11]) by rock.gnat.com (Postfix) with ESMTP id 7510811631B; Tue, 6 Jan 2015 04:18:24 -0500 (EST) Received: by kwai.gnat.com (Postfix, from userid 4192) id 7397291A7D; Tue, 6 Jan 2015 04:18:24 -0500 (EST) Date: Tue, 06 Jan 2015 09:18:00 -0000 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Changes to SPARK RM 7.1.3(11) Message-ID: <20150106091824.GA21344@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="EeQfGwPcQSOJBaQU" Content-Disposition: inline User-Agent: Mutt/1.5.21 (2010-09-15) X-SW-Source: 2015-01/txt/msg00205.txt.bz2 --EeQfGwPcQSOJBaQU Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Content-length: 2420 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 * 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. --EeQfGwPcQSOJBaQU Content-Type: text/plain; charset=us-ascii Content-Disposition: attachment; filename=difs Content-length: 5964 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 --EeQfGwPcQSOJBaQU--