From patchwork Mon Jul 8 07:41:26 2013 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 257477 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) (using TLSv1 with cipher DHE-RSA-AES256-SHA (256/256 bits)) (Client CN "localhost", Issuer "www.qmailtoaster.com" (not verified)) by ozlabs.org (Postfix) with ESMTPS id EF4512C008E for ; Mon, 8 Jul 2013 17:41:36 +1000 (EST) 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=mo6vDz5UAZbugxyS4+b3Hx0Z/3pSt52s5XhaBFTf6DYdkoOAlo VInUE24o4LaT759qR425FHMEX+TMyxTd34WzyU1OEb28PSJoZQN/pq+3sk+3+PIK wyQCSvY25ucaqYzPMTSrQ9pkQzh4DK8Tac4biiatJ6xw1wa11NZ3PoB2Q= 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=uuL5NH/nemvOpw/+V6lh9S781yg=; b=gzvvRk6kyHSeWiZDdoXI 9PNdUQh37WQOurWtAlU+3dRTnQw4AcaNuK0JSYkhjNYH2cJ3fEfIEnXT/j5yTR82 0z2thPuDZjoBQNtuZGHSR0R/BaLrk/M6MfYr4ZDGWHPv7K2nE79o1GBWdSD3lujJ uVdLX+AP3otyO3AtcqGkyco= Received: (qmail 9166 invoked by alias); 8 Jul 2013 07:41:29 -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 9156 invoked by uid 89); 8 Jul 2013 07:41:29 -0000 X-Spam-SWARE-Status: No, score=-1.8 required=5.0 tests=AWL, BAYES_00, RCVD_IN_HOSTKARMA_NO, TW_TM autolearn=ham version=3.3.1 Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.84/v0.84-167-ge50287c) with ESMTP; Mon, 08 Jul 2013 07:41:28 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 696E41C68C1; Mon, 8 Jul 2013 03:41:26 -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 kpEAPlZGa9Pu; Mon, 8 Jul 2013 03:41:26 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 4DA491C68C0; Mon, 8 Jul 2013 03:41:26 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 4CF033FB31; Mon, 8 Jul 2013 03:41:26 -0400 (EDT) Date: Mon, 8 Jul 2013 03:41:26 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Aspect / pragma SPARK_Mode Message-ID: <20130708074126.GA23139@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) X-Virus-Found: No This patch removes the checks on mode duplication for the configuration form of the pragma to keep the behavior in line with other configuration pragmas. ------------ -- Source -- ------------ -- unit_spark_mode.ads pragma SPARK_Mode (Auto); pragma SPARK_Mode (On); package Unit_SPARK_Mode is end Unit_SPARK_Mode; ----------------- -- Compilation -- ----------------- $ gcc -c unit_spark_mode.ads Tested on x86_64-pc-linux-gnu, committed on trunk 2013-07-08 Hristian Kirtchev * sem_prag.adb (Analyze_Pragma): Remove variable Unit_Prag. Remove the check on duplicate mode for the configuration form of the pragma. (Redefinition_Error): Removed. Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 200752) +++ sem_prag.adb (working copy) @@ -16354,16 +16354,6 @@ function Get_SPARK_Mode_Name (Id : SPARK_Mode_Id) return Name_Id; -- Convert a value of type SPARK_Mode_Id into a corresponding name - procedure Redefinition_Error (Mode : SPARK_Mode_Id); - -- Emit an error on an attempt to redefine existing mode Mode. The - -- message is associated with the first argument of the current - -- pragma. - - procedure Redefinition_Error (Prag : Node_Id); - -- Emit an error on an attempt to redefine the mode of Prag. The - -- message is associated with the first argument of the current - -- pragma. - ------------------ -- Chain_Pragma -- ------------------ @@ -16474,41 +16464,14 @@ end if; end Get_SPARK_Mode_Name; - ------------------------ - -- Redefinition_Error -- - ------------------------ - - procedure Redefinition_Error (Mode : SPARK_Mode_Id) is - begin - Error_Msg_Name_1 := Get_SPARK_Mode_Name (Mode); - Error_Msg_N - ("cannot redefine 'S'P'A'R'K mode, already set to %", Arg1); - end Redefinition_Error; - - ------------------------ - -- Redefinition_Error -- - ------------------------ - - procedure Redefinition_Error (Prag : Node_Id) is - Mode : constant Name_Id := - Chars (Get_Pragma_Arg (First - (Pragma_Argument_Associations (Prag)))); - begin - Error_Msg_Name_1 := Mode; - Error_Msg_Sloc := Sloc (Prag); - Error_Msg_N - ("cannot redefine 'S'P'A'R'K mode, already set to % #", Arg1); - end Redefinition_Error; - -- Local variables - Body_Id : Entity_Id; - Context : Node_Id; - Mode : Name_Id; - Mode_Id : SPARK_Mode_Id; - Spec_Id : Entity_Id; - Stmt : Node_Id; - Unit_Prag : Node_Id; + Body_Id : Entity_Id; + Context : Node_Id; + Mode : Name_Id; + Mode_Id : SPARK_Mode_Id; + Spec_Id : Entity_Id; + Stmt : Node_Id; -- Start of processing for SPARK_Mode @@ -16536,39 +16499,15 @@ if No (Context) then Check_Valid_Configuration_Pragma; + Global_SPARK_Mode := Mode_Id; - -- Set the global mode - - if Global_SPARK_Mode = None then - Global_SPARK_Mode := Mode_Id; - - -- Catch an attempt to redefine an existing global mode by - -- using multiple configuration files. - - elsif Global_SPARK_Mode /= Mode_Id then - Redefinition_Error (Global_SPARK_Mode); - end if; - -- When the pragma is placed before the declaration of a unit, it -- configures the whole unit. elsif Nkind (Context) = N_Compilation_Unit then Check_Valid_Configuration_Pragma; + Set_SPARK_Mode_Pragma (Current_Sem_Unit, N); - Unit_Prag := SPARK_Mode_Pragma (Current_Sem_Unit); - - -- Set the unit mode - - if No (Unit_Prag) then - Set_SPARK_Mode_Pragma (Current_Sem_Unit, N); - - -- Catch an attempt to redefine the unit mode by using multiple - -- pragmas declared in the same region. - - else - Redefinition_Error (Unit_Prag); - end if; - -- The pragma applies to a [library unit] subprogram or package else