From patchwork Tue Sep 10 15:05:54 2013 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 273903 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 did not present a certificate) by ozlabs.org (Postfix) with ESMTPS id C18212C00C2 for ; Wed, 11 Sep 2013 01:06:15 +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=YeZdstKkya2xbWFE4nXgGuODgWK8DA1lv9IYOzQDWFUcv+JBif Qpc3scnUUVnPPosPbnFexl+d28c2sTh2MeYHcp8f6OWEMUf/iJqd7m/v97znUbdU wQVu4kI+s2PQHOwr8I01vWjt+yyQL8U/1gyQhKVtHmakd5SBwfW+7cMDU= 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=Go9vWXt355rwvo8EElsNQAEUxX4=; b=hjk+GxrDDojgApSSj/pq uVySha7IvhgLAcOSna/NwyAeaUgRHvUClWxSv5j0025CTZYNksb5/ssC0FYAw0WH tkzvu4odQ2bfFjKLyHOEw6sDH7Ix5vLmX1GedNmZdKfYfA4EFdnD1CDJVCCVCakP wUeivrTeA9QLPgP0ejk5um0= Received: (qmail 3406 invoked by alias); 10 Sep 2013 15:06:09 -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 3392 invoked by uid 89); 10 Sep 2013 15:06:08 -0000 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, 10 Sep 2013 15:06:08 +0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=1.6 required=5.0 tests=BAYES_50, RDNS_NONE autolearn=no version=3.3.2 X-HELO: rock.gnat.com Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 484D9116322; Tue, 10 Sep 2013 11:06:06 -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 9Vmp1ek+y3SM; Tue, 10 Sep 2013 11:06:06 -0400 (EDT) Received: from kwai.gnat.com (unknown [IPv6:2620:20:4000:0:a6ba:dbff:fe26:1f63]) by rock.gnat.com (Postfix) with ESMTP id 385BA11631F; Tue, 10 Sep 2013 11:06:06 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 72A473FB31; Tue, 10 Sep 2013 11:05:54 -0400 (EDT) Date: Tue, 10 Sep 2013 11:05:54 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Placement of aspect/pragma SPARK_Mode Message-ID: <20130910150554.GA22207@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) This patch modifies the processing of aspect/pragma SPARK_Mode to properly handle the cases where the aspect/pragma apply to a [library-level] package or subprogram [body]. ------------ -- Source -- ------------ -- func.ads function Func return Integer with SPARK_Mode => On; -- pack.adb package body Pack with SPARK_Mode => Off is procedure Dummy is begin null; end Dummy; end Pack; -- pack.ads package Pack is procedure Dummy; end Pack; -- proc.ads procedure Proc with SPARK_Mode => On; -- spec.ads package Spec with SPARK_Mode => On is end Spec; ----------------- -- Compilation -- ----------------- $ gcc -c -gnatc -gnat12 -gnatd.V func.ads $ gcc -c -gnat12 -gnatd.V pack.adb $ gcc -c -gnatc -gnat12 -gnatd.V proc.ads $ gcc -c -gnatc -gnat12 -gnatd.V spec.ads Tested on x86_64-pc-linux-gnu, committed on trunk 2013-09-10 Hristian Kirtchev * sem_prag.adb (Analyze_Pragma): Add processing for aspect/pragma SPARK_Mode when it applies to a [library-level] subprogram or package [body]. Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 202457) +++ sem_prag.adb (working copy) @@ -16633,12 +16633,53 @@ Stmt := Prev (Stmt); end loop; - -- If we get here, then we ran out of preceding statements. The - -- pragma is immediately within a body. + -- Handle all cases where the pragma is actually an aspect and + -- applies to a library-level package spec, body or subprogram. - if Nkind_In (Context, N_Package_Body, - N_Subprogram_Body) + -- function F ... with SPARK_Mode => ...; + -- package P with SPARK_Mode => ...; + -- package body P with SPARK_Mode => ... is + + -- The following circuitry simply prepares the proper context + -- for the general pragma processing mechanism below. + + if Nkind (Context) = N_Compilation_Unit_Aux then + Context := Unit (Parent (Context)); + + if Nkind_In (Context, N_Package_Declaration, + N_Subprogram_Declaration) + then + Context := Specification (Context); + end if; + end if; + + -- The pragma is at the top level of a package spec or appears + -- as an aspect on a subprogram. + + -- function F ... with SPARK_Mode => ...; + + -- package P is + -- pragma SPARK_Mode; + + if Nkind_In (Context, N_Function_Specification, + N_Package_Specification, + N_Procedure_Specification) then + Spec_Id := Defining_Unit_Name (Context); + Chain_Pragma (Spec_Id, N); + + -- The pragma is immediately within a package or subprogram + -- body. + + -- function F ... is + -- pragma SPARK_Mode; + + -- package body P is + -- pragma SPARK_Mode; + + elsif Nkind_In (Context, N_Package_Body, + N_Subprogram_Body) + then Spec_Id := Corresponding_Spec (Context); if Nkind (Context) = N_Subprogram_Body then @@ -16650,14 +16691,12 @@ Chain_Pragma (Body_Id, N); Check_Conformance (Spec_Id, Body_Id); - -- The pragma is at the top level of a package spec + -- The pragma applies to the statements of a package body - elsif Nkind (Context) = N_Package_Specification then - Spec_Id := Defining_Unit_Name (Context); - Chain_Pragma (Spec_Id, N); + -- package body P is + -- begin + -- pragma SPARK_Mode; - -- The pragma applies to the statements of a package body - elsif Nkind (Context) = N_Handled_Sequence_Of_Statements and then Nkind (Parent (Context)) = N_Package_Body then