From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (qmail 31762 invoked by alias); 26 Oct 2015 15:40:50 -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 31684 invoked by uid 89); 26 Oct 2015 15:40:49 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=0.2 required=5.0 tests=AWL,BAYES_50,KAM_ASCII_DIVIDERS,KAM_LAZY_DOMAIN_SECURITY,RCVD_IN_DNSWL_LOW autolearn=no 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; Mon, 26 Oct 2015 15:40:41 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 830BF29771; Mon, 26 Oct 2015 11:40:39 -0400 (EDT) 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 I-vDD+-KFX8i; Mon, 26 Oct 2015 11:40:39 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 70FB4D3B15; Mon, 26 Oct 2015 11:40:39 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4192) id 6BCEA18F; Mon, 26 Oct 2015 11:40:39 -0400 (EDT) Date: Mon, 26 Oct 2015 15:45:00 -0000 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Renamings of volatile objects Message-ID: <20151026154039.GA120727@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="zhXaljGHf11kAtnf" Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-SW-Source: 2015-10/txt/msg02770.txt.bz2 --zhXaljGHf11kAtnf Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Content-length: 2476 This patch implements the following SPARK RM 7.1.3(12) rule: Contrary to the general SPARK 2014 rule that expression evaluation cannot have side effects, a read of an effectively volatile object with the properties Async_Writers or Effective_Reads set to True is considered to have an effect when read. To reconcile this discrepancy, a name denoting such an object shall only occur in a non-interfering context. A name occurs in a non-interfering context if it is: * the object_name of an object_renaming_declaration ------------ -- Source -- ------------ -- volatile_renamings.ads package Volatile_Renamings with SPARK_Mode is type Vol_Rec is record Comp : Integer; end record with Volatile; Vol_Obj_1 : Vol_Rec; Vol_Obj_2 : Integer with Volatile; Vol_Ren_1 : Vol_Rec renames Vol_Obj_1; Vol_Ren_2 : Integer renames Vol_Obj_2; function Rec_Func return Vol_Rec with Volatile_Function; function Int_Func return Integer with Volatile_Function; function Error_Rec_Func return Vol_Rec; function Error_Int_Func return Integer; end Volatile_Renamings; -- volatile_renamings.adb package body Volatile_Renamings with SPARK_Mode is function Rec_Func return Vol_Rec is begin return Vol_Ren_1; -- OK end Rec_Func; function Int_Func return Integer is begin return Vol_Ren_2; -- OK end Int_Func; function Error_Rec_Func return Vol_Rec is begin return Vol_Ren_1; -- Error end Error_Rec_Func; function Error_Int_Func return Integer is begin return Vol_Ren_2; -- Error end Error_Int_Func; end Volatile_Renamings; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c volatile_renamings.adb volatile_renamings.adb:14:14: volatile object cannot appear in this context (SPARK RM 7.1.3(12)) volatile_renamings.adb:19:14: volatile object cannot appear in this context (SPARK RM 7.1.3(12)) volatile_renamings.ads:15:13: nonvolatile function "Error_Rec_Func" cannot have a volatile return type Tested on x86_64-pc-linux-gnu, committed on trunk 2015-10-26 Hristian Kirtchev * sem_res.adb (Is_OK_Volatile_Context): A volatile object may appear in an object declaration as long as it denotes the name. --zhXaljGHf11kAtnf Content-Type: text/plain; charset=us-ascii Content-Disposition: attachment; filename=difs Content-length: 614 Index: sem_res.adb =================================================================== --- sem_res.adb (revision 229362) +++ sem_res.adb (working copy) @@ -6993,6 +6993,13 @@ return True; end if; + -- 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. --zhXaljGHf11kAtnf--