From patchwork Wed Sep 6 12:05:58 2017 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 810552 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-461592-incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="G1ijTRLq"; 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 3xnMkJ6m5Pz9sBZ for ; Wed, 6 Sep 2017 22:06:10 +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=aAb0D/+11KgOqTVKpttkmiWQyF9Sil9doZzTpe4UxiL/pZaJts dfzW39+M2d2lVU2nP4/cWCesoaaH0ZOAsqxqBcCjhvuBQ0fqaDQ83Q6SXwelEyLG shw6xfF3DjLmZrWVV0iicdBPyRHrH0wlLe/uISmwFceUum+j2gPTrWnCs= 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=nbHp+83W7M0dy850FUSsICyrFic=; b=G1ijTRLqNVVKX3nD9lpA uZNVGmnhJo+rcOYALro6tXvjZGf7YBx2UMlDWOG7UVPAON7dZDc6JLGbxJ+g+COU Iv8CE42tmJ8pCLpTvsn7gIHnWpP3JemvMcbHqcDx9Zk3oEBf/7arTXbbFhM4lalK E66vNxy4+3CmyEPfkaAULq0= Received: (qmail 24730 invoked by alias); 6 Sep 2017 12:06:02 -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 23961 invoked by uid 89); 6 Sep 2017 12:06:01 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-10.4 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=Items, freezing, Contract, contract 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; Wed, 06 Sep 2017 12:06:00 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 992FE5641A; Wed, 6 Sep 2017 08:05:58 -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 YmtznXelv9dW; Wed, 6 Sep 2017 08:05:58 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 872455614C; Wed, 6 Sep 2017 08:05:58 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4192) id 837CD4AC; Wed, 6 Sep 2017 08:05:58 -0400 (EDT) Date: Wed, 6 Sep 2017 08:05:58 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Ed Schonberg Subject: [Ada] Handling of inherited and explicit postconditions Message-ID: <20170906120558.GA47956@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) This patch fixes the handling of overriding operations that have both an explicit postcondition and an inherited classwide one. Executing: gnatmake -q -gnata post_class.adb post_class must yield: raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed inherited postcondition from the_package.ads:4 --- with The_Package; use The_Package; procedure Post_Class is X : D; begin Proc (X); end Post_Class; --- package The_Package is type T is tagged null record; function F (X : T) return Boolean is (True); procedure Proc (X : in out T) with Post => True, post'class => F (X); type D is new T with null record; overriding function F (X : D) return Boolean is (False); end The_Package; --- package body The_Package is procedure Proc (X : in out T) is begin null; end Proc; end The_Package; Tested on x86_64-pc-linux-gnu, committed on trunk 2017-09-06 Ed Schonberg * einfo.ads, einfo.adb (Get_Classwwide_Pragma): New utility, to retrieve the inherited classwide precondition/postcondition of a subprogram. * freeze.adb (Freeze_Entity): Use Get_Classwide_Pragma when freezing a subprogram, to complete the generation of the corresponding checking code. Index: einfo.adb =================================================================== --- einfo.adb (revision 251783) +++ einfo.adb (working copy) @@ -7481,6 +7481,39 @@ return Empty; end Get_Pragma; + -------------------------- + -- Get_Classwide_Pragma -- + -------------------------- + + function Get_Classwide_Pragma + (E : Entity_Id; + Id : Pragma_Id) return Node_Id + is + Item : Node_Id; + Items : Node_Id; + + begin + Items := Contract (E); + if No (Items) then + return Empty; + end if; + + Item := Pre_Post_Conditions (Items); + + while Present (Item) loop + if Nkind (Item) = N_Pragma + and then Get_Pragma_Id (Pragma_Name_Unmapped (Item)) = Id + and then Class_Present (Item) + then + return Item; + else + Item := Next_Pragma (Item); + end if; + end loop; + + return Empty; + end Get_Classwide_Pragma; + -------------------------------------- -- Get_Record_Representation_Clause -- -------------------------------------- Index: einfo.ads =================================================================== --- einfo.ads (revision 251783) +++ einfo.ads (working copy) @@ -8295,6 +8295,12 @@ -- Test_Case -- Volatile_Function + function Get_Classwide_Pragma + (E : Entity_Id; + Id : Pragma_Id) return Node_Id; + -- Examine Rep_Item chain to locate a classwide pre- or postcondition + -- of a primitive operation. Returns Empty if not present. + function Get_Record_Representation_Clause (E : Entity_Id) return Node_Id; -- Searches the Rep_Item chain for a given entity E, for a record -- representation clause, and if found, returns it. Returns Empty Index: freeze.adb =================================================================== --- freeze.adb (revision 251781) +++ freeze.adb (working copy) @@ -1418,8 +1418,8 @@ New_Prag : Node_Id; begin - A_Pre := Get_Pragma (Par_Prim, Pragma_Precondition); - if Present (A_Pre) and then Class_Present (A_Pre) then + A_Pre := Get_Classwide_Pragma (Par_Prim, Pragma_Precondition); + if Present (A_Pre) then New_Prag := New_Copy_Tree (A_Pre); Build_Class_Wide_Expression (Prag => New_Prag, @@ -1436,9 +1436,9 @@ end if; end if; - A_Post := Get_Pragma (Par_Prim, Pragma_Postcondition); + A_Post := Get_Classwide_Pragma (Par_Prim, Pragma_Postcondition); - if Present (A_Post) and then Class_Present (A_Post) then + if Present (A_Post) then New_Prag := New_Copy_Tree (A_Post); Build_Class_Wide_Expression (Prag => New_Prag,