From patchwork Fri May 25 09:06:05 2018 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: 920330 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-478488-incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dmarc=none (p=none dis=none) header.from=adacore.com Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="aXJIyGPG"; 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 40sgN95vlKz9s08 for ; Fri, 25 May 2018 19:06:16 +1000 (AEST) 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=rUdveC6tQG2t0U8tBQRjuLYKvaSfwmPf8Kr3fcQ1/X4xGQpkgv 4jgpb7N+Y+oLyOcEqcnatKw8ZxZHya4zDaA+aHV5lUZkSTFS1+D9Ci6p6sj03Hfo PHeya5SIzX/kZFwfr0AO0lbNiGU26DMmoSkTCLEPKPv3sZkAUhKnSO5d4= 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=PqXoWskoS4ef8kYEIGP5dKSbTY0=; b=aXJIyGPG1EOywIrAm6jq rWj1Izg28acxnR4681R+ccjOX/9yeMfiq+0DLztTJY7oJwgq0HYDi/kF/m4Lc6kd yyCTxdXVqIwGtTZvgg8ky7LJ3hsV57IYEABAi5bZRqBVDxT1olG+g2gL8tWbbXdj WNgFfqP7kIWunaKv4nVP8+s= Received: (qmail 122576 invoked by alias); 25 May 2018 09: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 121975 invoked by uid 89); 25 May 2018 09:06:08 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-11.9 required=5.0 tests=BAYES_00, GIT_PATCH_2, GIT_PATCH_3, RCVD_IN_DNSWL_NONE, SPF_PASS autolearn=ham version=3.3.2 spammy=misplaced 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; Fri, 25 May 2018 09:06:07 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 03C3E117F66; Fri, 25 May 2018 05: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 wXjvn2hNfKVi; Fri, 25 May 2018 05:06:05 -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 E5296117F2F; Fri, 25 May 2018 05:06:05 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id E13CA784; Fri, 25 May 2018 05:06:05 -0400 (EDT) Date: Fri, 25 May 2018 05:06:05 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Detect misplaced assertions between loop invariants Message-ID: <20180525090605.GA34527@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes Loop invariants and loop variants should all be colocated, as defined in SPARK RM 5.5.3(8). The code checking that rule was incorrectly accepting pragma Assert between two loop invariants. Now fixed. Tested on x86_64-pc-linux-gnu, committed on trunk 2018-05-25 Yannick Moy gcc/ada/ * sem_prag.adb (Check_Grouping): Modify test to ignore statements and declarations not coming from source. --- gcc/ada/sem_prag.adb +++ gcc/ada/sem_prag.adb @@ -5979,9 +5979,14 @@ package body Sem_Prag is Prag := Stmt; -- Skip declarations and statements generated by - -- the compiler during expansion. + -- the compiler during expansion. Note that some + -- source statements (e.g. pragma Assert) may have + -- been transformed so that they do not appear as + -- coming from source anymore, so we instead look + -- at their Original_Node. - elsif not Comes_From_Source (Stmt) then + elsif not Comes_From_Source (Original_Node (Stmt)) + then null; -- A non-pragma is separating the group from the