From patchwork Mon Oct 9 20:00:30 2017 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 823469 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: ozlabs.org; spf=pass (mailfrom) smtp.mailfrom=gcc.gnu.org (client-ip=209.132.180.131; helo=sourceware.org; envelope-from=gcc-patches-return-463811-incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="fVc5EGVW"; dkim-atps=neutral Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 3y9rhb2vjMz9sNw for ; Tue, 10 Oct 2017 07:00:47 +1100 (AEDT) DomainKey-Signature: a=rsa-sha1; c=nofws; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; q=dns; s=default; b=uwYoQOvpKvCzz5dGbMyuHGpZPUV3N2uloaxbrLEHjrust6S508 vxsOcMceg4qrtmpiWOy1Y4zHy4u3VI4xsGW8UiFjnNyavQB6vy2WhHquG5jUfmSy Ec+sHjMRl6crgK1MNoA1getNGmPD9FnPTGpvii79QItIO4b5xYOBu8mWQ= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; s= default; bh=DZzsTqPahenn1W2c7gDQhzKrWNE=; b=fVc5EGVWzzj2E4MGS1XS P2/HcIsmhsreQADkdj4F6rEXjcxOQ9nSCLDBTtCp7bjvlNdru3PddgwGlPP0yoJk ADZCYvY+/F7gPTaWGRm8S97oC5wlgh0r1286EeYuGYssO/7mLvZ9hqh0VDKVdzQI dxX0MFjleRHWUM0mNHoeHlg= Received: (qmail 17156 invoked by alias); 9 Oct 2017 20:00:36 -0000 Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org Received: (qmail 17097 invoked by uid 89); 9 Oct 2017 20:00:35 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-11.1 required=5.0 tests=BAYES_00, GIT_PATCH_2, GIT_PATCH_3, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_PASS autolearn=ham version=3.3.2 spammy=nam 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 ESMTP; Mon, 09 Oct 2017 20:00:33 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id B1E1256327; Mon, 9 Oct 2017 16:00:31 -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 yXXQk8nAi5AM; Mon, 9 Oct 2017 16:00:31 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [IPv6:2620:20:4000:0:46a8:42ff:fe0e:e294]) by rock.gnat.com (Postfix) with ESMTP id C826356325; Mon, 9 Oct 2017 16:00:30 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id C732043A; Mon, 9 Oct 2017 16:00:30 -0400 (EDT) Date: Mon, 9 Oct 2017 16:00:30 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Piotr Trojanek Subject: [Ada] Rewrite check for SPARK RM 7.1.3(10) Message-ID: <20171009200030.GA44133@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes The evolution of SPARK RM 7.1.3(10) rule was not followed by code that implements it. The current wording is: "If a procedure has an in mode parameter of an effectively volatile type, then the Effective_Reads aspect of any corresponding actual parameter shall be False." and the current code checks exactly that. ------------ -- Source -- ------------ -- ineffective_actual.ads with System; package Ineffective_Actual with SPARK_Mode is type VT is record Int : Integer; end record with Volatile; The_Volatile_Data : VT with Volatile, Async_Readers => True, Async_Writers => True, Effective_Reads => False, Effective_Writes => False, Address => System'To_Address (16#1234_5678#); procedure Harmless_Reader (Data : in VT); procedure Do_Something; end Ineffective_Actual; -- ineffective_actual.adb package body Ineffective_Actual with SPARK_Mode is procedure Harmless_Reader (Data : in VT) with SPARK_Mode => Off is I : Integer; begin I := Data.Int; end Harmless_Reader; procedure Do_Something is begin Harmless_Reader (The_Volatile_Data); end Do_Something; end Ineffective_Actual; ---------------------------- -- Compilation and output -- ---------------------------- & gcc -c ineffective_actual.adb & gcc -c -gnatd.F ineffective_actual.adb Tested on x86_64-pc-linux-gnu, committed on trunk 2017-10-09 Piotr Trojanek * sem_res.adb (Property_Error): Remove. (Resolve_Actuals): check for SPARK RM 7.1.3(10) rewritten to match the current wording of the rule. Index: sem_res.adb =================================================================== --- sem_res.adb (revision 253559) +++ sem_res.adb (working copy) @@ -3178,14 +3178,6 @@ -- an instance of the default expression. The insertion is always -- a named association. - procedure Property_Error - (Var : Node_Id; - Var_Id : Entity_Id; - Prop_Nam : Name_Id); - -- Emit an error concerning variable Var with entity Var_Id that has - -- enabled property Prop_Nam when it acts as an actual parameter in a - -- call and the corresponding formal parameter is of mode IN. - function Same_Ancestor (T1, T2 : Entity_Id) return Boolean; -- Check whether T1 and T2, or their full views, are derived from a -- common type. Used to enforce the restrictions on array conversions @@ -3634,23 +3626,6 @@ Prev := Actval; end Insert_Default; - -------------------- - -- Property_Error -- - -------------------- - - procedure Property_Error - (Var : Node_Id; - Var_Id : Entity_Id; - Prop_Nam : Name_Id) - is - begin - Error_Msg_Name_1 := Prop_Nam; - Error_Msg_NE - ("external variable & with enabled property % cannot appear as " - & "actual in procedure call (SPARK RM 7.1.3(10))", Var, Var_Id); - Error_Msg_N ("\\corresponding formal parameter has mode In", Var); - end Property_Error; - ------------------- -- Same_Ancestor -- ------------------- @@ -4659,26 +4634,28 @@ Flag_Effectively_Volatile_Objects (A); end if; - -- Detect an external variable with an enabled property that - -- does not match the mode of the corresponding formal in a - -- procedure call. Functions are not considered because they - -- cannot have effectively volatile formal parameters in the - -- first place. + -- An effectively volatile variable cannot act as an actual + -- parameter in a procedure call when the variable has enabled + -- property Effective_Reads and the corresponding formal is of + -- mode IN (SPARK RM 7.1.3(10)). if Ekind (Nam) = E_Procedure and then Ekind (F) = E_In_Parameter and then Is_Entity_Name (A) - and then Present (Entity (A)) - and then Ekind (Entity (A)) = E_Variable then A_Id := Entity (A); - if Async_Readers_Enabled (A_Id) then - Property_Error (A, A_Id, Name_Async_Readers); - elsif Effective_Reads_Enabled (A_Id) then - Property_Error (A, A_Id, Name_Effective_Reads); - elsif Effective_Writes_Enabled (A_Id) then - Property_Error (A, A_Id, Name_Effective_Writes); + if Ekind (A_Id) = E_Variable + and then Is_Effectively_Volatile (Etype (A_Id)) + and then Effective_Reads_Enabled (A_Id) + then + Error_Msg_NE + ("effectively volatile variable & cannot appear as " + & "actual in procedure call", A, A_Id); + + Error_Msg_Name_1 := Name_Effective_Reads; + Error_Msg_N ("\\variable has enabled property %", A); + Error_Msg_N ("\\corresponding formal has mode IN", A); end if; end if; end if;