From patchwork Tue Apr 25 10:04:04 2017 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 754680 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.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 3wBzMt5B9Pz9s7q for ; Tue, 25 Apr 2017 20:04:42 +1000 (AEST) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="PfmcjQoe"; dkim-atps=neutral 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=NwTyI6XhEj3Cl6KnH0UmyR4e0UzAaI5X6i8QgDwm17MLDXIWhc ITC7KQvy0WyVWSlGDG9fyN9d2eYshIsbw0vx/T+v7hczRmn+yRc0OnAC7DX/nW/Q 72WKeNPoDphHNUYJw0EPCtROsbKenWCL3eadX8GnY0l5NGsmVFRAOzvb4= 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=U57flGNFDHDI42Bh7L6/1J8hpbw=; b=PfmcjQoekF35x1S4ClPy VBaiiXzsWRCCVOCNqmHZIYhm+5I4A6kQHytbiiP5SmNF3Z22yBfRJfxiU403LIBG JJLlhQEOpb7j0wHR0aBYE7BYrZKgw68+s+Q1fgTCOxIjQZO18C8y3XlxOaqWvC6E xXNU6SIiy3KbNF8NgPi3rks= Received: (qmail 88063 invoked by alias); 25 Apr 2017 10:04:08 -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 88005 invoked by uid 89); 25 Apr 2017 10:04:07 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-10.1 required=5.0 tests=AWL, BAYES_00, GIT_PATCH_2, GIT_PATCH_3, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_PASS autolearn=ham version=3.3.2 spammy=Legality, LSP, lsp, Hx-languages-length:4537 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; Tue, 25 Apr 2017 10:04:03 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 3E20D3554; Tue, 25 Apr 2017 06:04:04 -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 FfVIWvyV+366; Tue, 25 Apr 2017 06:04:04 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 2BBCE3547; Tue, 25 Apr 2017 06:04:04 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4192) id 28E0D521; Tue, 25 Apr 2017 06:04:04 -0400 (EDT) Date: Tue, 25 Apr 2017 06:04:04 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Ed Schonberg Subject: [Ada] Legality rules on class-wide preconditions of overriding operations. Message-ID: <20170425100404.GA54440@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) AI12-0131, part of the Ada2012 Corrigendum, places restrictions on class-wide preconditions of overriding operations, to prevent anomalies that would violate LSP if an overriding operation could declare such a precondition without an acestor of the operation having such a precondition to override. Tested in ACATS 4.1B test B611017. Tested on x86_64-pc-linux-gnu, committed on trunk 2017-04-25 Ed Schonberg * sem_prag.adb (Inherits_Class_Wide_Pre): subsidiary of Analyze_Pre_Post_Condition, to implement the legality checks mandated by AI12-0131: Pre'Class shall not be specified for an overriding primitive subprogram of a tagged type T unless the Pre'Class aspect is specified for the corresponding primitive subprogram of some ancestor of T. Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 247168) +++ sem_prag.adb (working copy) @@ -4208,6 +4208,85 @@ -- Flag set when the pragma is one of Pre, Pre_Class, Post or -- Post_Class. + function Inherits_Class_Wide_Pre (E : Entity_Id) return Boolean; + -- Implement rules in AI12-0131: an overriding operation can have + -- a class-wide precondition only if one of its ancestors has an + -- explicit class-wide precondition. + + ----------------------------- + -- Inherits_Class_Wide_Pre -- + ----------------------------- + + function Inherits_Class_Wide_Pre (E : Entity_Id) return Boolean is + Prev : Entity_Id := Overridden_Operation (E); + Cont : Node_Id; + Prag : Node_Id; + Typ : Entity_Id; + + begin + -- Check ancestors on the overriding operation to examine the + -- preconditions that may apply to them. + + while Present (Prev) loop + Cont := Contract (Prev); + if Present (Cont) then + Prag := Pre_Post_Conditions (Cont); + while Present (Prag) loop + if Class_Present (Prag) then + return True; + end if; + + Prag := Next_Pragma (Prag); + end loop; + end if; + + Prev := Overridden_Operation (Prev); + end loop; + + -- If the controlling type of the subprogram has progenitors, + -- an interface operation implemented by the current operation + -- may have a class-wide precondition. + + Typ := Find_Dispatching_Type (E); + if Has_Interfaces (Typ) then + declare + Ints : Elist_Id; + Elmt : Elmt_Id; + Prim_List : Elist_Id; + Prim_Elmt : Elmt_Id; + Prim : Entity_Id; + begin + Collect_Interfaces (Typ, Ints); + Elmt := First_Elmt (Ints); + + -- Iterate over the primitive operations of each + -- interface. + + while Present (Elmt) loop + Prim_List := + (Direct_Primitive_Operations (Node (Elmt))); + Prim_Elmt := First_Elmt (Prim_List); + while Present (Prim_Elmt) loop + Prim := Node (Prim_Elmt); + if Chars (Prim) = Chars (E) + and then Present (Contract (Prim)) + and then Class_Present + (Pre_Post_Conditions (Contract (Prim))) + then + return True; + end if; + + Next_Elmt (Prim_Elmt); + end loop; + + Next_Elmt (Elmt); + end loop; + end; + end if; + + return False; + end Inherits_Class_Wide_Pre; + begin -- Change the name of pragmas Pre, Pre_Class, Post and Post_Class to -- offer uniformity among the various kinds of pre/postconditions by @@ -4326,6 +4405,43 @@ Error_Pragma ("aspect % requires ''Class for null procedure"); end if; + -- Implement the legality checks mandated by AI12-0131: + -- Pre'Class shall not be specified for an overriding primitive + -- subprogram of a tagged type T unless the Pre'Class aspect is + -- specified for the corresponding primitive subprogram of some + -- ancestor of T. + + declare + E : constant Entity_Id := Defining_Entity (Subp_Decl); + H : constant Entity_Id := Homonym (E); + + begin + if Class_Present (N) + and then Present (Overridden_Operation (E)) + and then not Inherits_Class_Wide_Pre (E) + then + Error_Msg_N + ("illegal class-wide precondition on overriding " + & "operation", Corresponding_Aspect (N)); + + -- If the operation is declared in the private part of an + -- instance it may not override any visible operations, but + -- still have a parent operation that carries a precondition. + + elsif In_Instance + and then In_Private_Part (Current_Scope) + and then Present (H) + and then Scope (E) = Scope (H) + and then Is_Inherited_Operation (H) + and then Present (Overridden_Operation (H)) + and then not Inherits_Class_Wide_Pre (H) + then + Error_Msg_N + ("illegal class-wide precondition on overriding " + & "operation in instance", Corresponding_Aspect (N)); + end if; + end; + -- Otherwise the placement is illegal else