From patchwork Fri Sep 2 09:22:23 2011 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 113065 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]) by ozlabs.org (Postfix) with SMTP id D7A2FB6F7C for ; Fri, 2 Sep 2011 19:22:41 +1000 (EST) Received: (qmail 30568 invoked by alias); 2 Sep 2011 09:22:39 -0000 Received: (qmail 30559 invoked by uid 22791); 2 Sep 2011 09:22:37 -0000 X-SWARE-Spam-Status: No, hits=-1.8 required=5.0 tests=AWL,BAYES_00 X-Spam-Check-By: sourceware.org Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.43rc1) with ESMTP; Fri, 02 Sep 2011 09:22:24 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 914CC2BB474; Fri, 2 Sep 2011 05:22:23 -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 FWH3L54ZT68r; Fri, 2 Sep 2011 05:22:23 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 78A482BB473; Fri, 2 Sep 2011 05:22:23 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 702983FEE8; Fri, 2 Sep 2011 05:22:23 -0400 (EDT) Date: Fri, 2 Sep 2011 05:22:23 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Remove IN parameters from Alfa section in ALI Message-ID: <20110902092223.GA11331@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) 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 References to IN parameters are not considered in Alfa section, as these will be translated as constants in the intermediate language for formal verification. Tested on x86_64-pc-linux-gnu, committed on trunk 2011-09-02 Yannick Moy * lib-xref-alfa.adb (Is_Alfa_Reference): Ignore IN parameters in Alfa references. Index: lib-xref-alfa.adb =================================================================== --- lib-xref-alfa.adb (revision 178438) +++ lib-xref-alfa.adb (working copy) @@ -608,11 +608,20 @@ -- On non-callable entities, the only references of interest are -- reads and writes. - if Ekind (E) in Overloadable_Kind then - return Typ = 's'; - else - return Typ = 'r' or else Typ = 'm'; - end if; + case Ekind (E) is + when Overloadable_Kind => + return Typ = 's'; + + -- References to IN parameters are not considered in Alfa + -- section, as these will be translated as constants in the + -- intermediate language for formal verification. + + when E_In_Parameter => + return False; + + when others => + return Typ = 'r' or else Typ = 'm'; + end case; end Is_Alfa_Reference; -------------------