From patchwork Mon Aug 29 08:22:09 2011 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 111971 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 E6C25B6F77 for ; Mon, 29 Aug 2011 18:22:39 +1000 (EST) Received: (qmail 30256 invoked by alias); 29 Aug 2011 08:22:32 -0000 Received: (qmail 30247 invoked by uid 22791); 29 Aug 2011 08:22:29 -0000 X-SWARE-Spam-Status: No, hits=-2.0 required=5.0 tests=AWL, BAYES_00, RP_MATCHES_RCVD X-Spam-Check-By: sourceware.org Received: from mel.act-europe.fr (HELO mel.act-europe.fr) (194.98.77.210) by sourceware.org (qpsmtpd/0.43rc1) with ESMTP; Mon, 29 Aug 2011 08:22:15 +0000 Received: from localhost (localhost [127.0.0.1]) by filtered-smtp.eu.adacore.com (Postfix) with ESMTP id 5C881CB026C; Mon, 29 Aug 2011 10:22:16 +0200 (CEST) Received: from mel.act-europe.fr ([127.0.0.1]) by localhost (smtp.eu.adacore.com [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id TnaZYBwnDERi; Mon, 29 Aug 2011 10:22:06 +0200 (CEST) Received: from saumur.act-europe.fr (saumur.act-europe.fr [10.10.0.183]) by mel.act-europe.fr (Postfix) with ESMTP id 10DCDCB02AC; Mon, 29 Aug 2011 10:22:06 +0200 (CEST) Received: by saumur.act-europe.fr (Postfix, from userid 525) id D2C8C24524F; Mon, 29 Aug 2011 10:22:09 +0200 (CEST) Date: Mon, 29 Aug 2011 10:22:09 +0200 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Analyze pre/post expression for correctness in formal verification mode Message-ID: <20110829082209.GA13955@adacore.com> Mime-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.9i X-IsSubscribed: yes 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 Since expansion of pre/post is skipped in formal verification mode, the analysis of pre/post expressions for correctness, and to complete nodes with their types, was missing. Now corrected. Tested on x86_64-pc-linux-gnu, committed on trunk 2011-08-29 Yannick Moy * sem_prag.adb (Check_Precondition_Postcondition): In formal verification mode, analyze pragma expression for correctness, for pre/post on library-level subprogram, as it is not expanded later. Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 178155) +++ sem_prag.adb (working copy) @@ -1884,6 +1884,15 @@ -- See if it is in the pragmas after a library level subprogram elsif Nkind (Parent (N)) = N_Compilation_Unit_Aux then + + -- In formal verification mode, analyze pragma expression for + -- correctness, as it is not expanded later. + + if ALFA_Mode then + Analyze_PPC_In_Decl_Part + (N, Defining_Entity (Unit (Parent (Parent (N))))); + end if; + Chain_PPC (Unit (Parent (Parent (N)))); return; end if;