From patchwork Mon Aug 19 08:38:59 2019 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: 1149121 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-507233-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="KZ87ByPc"; 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 46BnW345Zdz9sMr for ; Mon, 19 Aug 2019 18:42:55 +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=Uy62U2B1vknxerTVjF9HNFcj7P5DyG0Xiqjvnn0RRPfmOW7t9N fmC8JVGmcnCPFuxUPx7r4sIQLQ5h1LMvPUgkFBYNUldI6GV0gZVX2QZLNM4rwFGC knI1SZabFLF566aZtiALmRIObiXNN15RjToE67pmqVxnXzx+Xnvh24q8I= 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=aejWkl1pKl+1MJK6cHk06sAlhww=; b=KZ87ByPcexiUwItQNVTf 8O8Fc7X9GA4rnCLIxOoRiefHmoX7is9ASXWQxEFNO4zOal2TfIFoSmUq5AiKQTGr +XPwVDhr4nbiI0T4BhC9AnYp+7pvQsMMJnlHqw9lc77lM5DqwI6JQd8M39uzrKYi Lb9GGcIgUx6URioCaHHOLYY= Received: (qmail 118350 invoked by alias); 19 Aug 2019 08:39:27 -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 116969 invoked by uid 89); 19 Aug 2019 08:39:17 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-10.7 required=5.0 tests=AWL, BAYES_00, GIT_PATCH_2, GIT_PATCH_3, SPF_NEUTRAL autolearn=ham version=3.3.1 spammy= X-HELO: eggs.gnu.org Received: from eggs.gnu.org (HELO eggs.gnu.org) (209.51.188.92) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Mon, 19 Aug 2019 08:39:15 +0000 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1hzdBx-0007v8-BL for gcc-patches@gcc.gnu.org; Mon, 19 Aug 2019 04:39:07 -0400 Received: from rock.gnat.com ([205.232.38.15]:53870) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1hzdBx-0007qO-2W for gcc-patches@gcc.gnu.org; Mon, 19 Aug 2019 04:39:05 -0400 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id E571B56049; Mon, 19 Aug 2019 04:38:59 -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 HpMlojqoUd3w; Mon, 19 Aug 2019 04:38:59 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id D17C611619A; Mon, 19 Aug 2019 04:38:59 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id D08596AB; Mon, 19 Aug 2019 04:38:59 -0400 (EDT) Date: Mon, 19 Aug 2019 04:38:59 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Joffrey Huguet Subject: [Ada] Add formal function parameter equality to SPARK containers Message-ID: <20190819083859.GA33377@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-detected-operating-system: by eggs.gnu.org: GNU/Linux 3.x X-Received-From: 205.232.38.15 X-IsSubscribed: yes This patch adds a formal function parameter "=" (L, R : Element_Type) to SPARK containers. The equality that is used by default for Element_Type after this patch is the primitive equality and not the predefined any more. It also allows to use any function with the appropriate signature for the equality function. Tested on x86_64-pc-linux-gnu, committed on trunk 2019-08-19 Joffrey Huguet gcc/ada/ * libgnat/a-cfdlli.ads, libgnat/a-cfhama.ads, libgnat/a-cfinve.ads, libgnat/a-cforma.ads, libgnat/a-cofove.ads, libgnat/a-cofuma.ads, libgnat/a-cofuve.ads: Add formal function parameter "=" (L, R : Element_Type) to the generic packages. --- gcc/ada/libgnat/a-cfdlli.ads +++ gcc/ada/libgnat/a-cfdlli.ads @@ -34,6 +34,7 @@ with Ada.Containers.Functional_Maps; generic type Element_Type is private; + with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Formal_Doubly_Linked_Lists with SPARK_Mode --- gcc/ada/libgnat/a-cfhama.ads +++ gcc/ada/libgnat/a-cfhama.ads @@ -59,6 +59,7 @@ generic with function Equivalent_Keys (Left : Key_Type; Right : Key_Type) return Boolean is "="; + with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Formal_Hashed_Maps with SPARK_Mode --- gcc/ada/libgnat/a-cfinve.ads +++ gcc/ada/libgnat/a-cfinve.ads @@ -38,6 +38,7 @@ with Ada.Containers.Functional_Vectors; generic type Index_Type is range <>; type Element_Type (<>) is private; + with function "=" (Left, Right : Element_Type) return Boolean is <>; Max_Size_In_Storage_Elements : Natural; -- Maximum size of Vector elements in bytes. This has the same meaning as -- in Ada.Containers.Bounded_Holders, with the same restrictions. Note that --- gcc/ada/libgnat/a-cforma.ads +++ gcc/ada/libgnat/a-cforma.ads @@ -58,6 +58,7 @@ generic type Element_Type is private; with function "<" (Left, Right : Key_Type) return Boolean is <>; + with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Formal_Ordered_Maps with SPARK_Mode --- gcc/ada/libgnat/a-cofove.ads +++ gcc/ada/libgnat/a-cofove.ads @@ -40,6 +40,8 @@ with Ada.Containers.Functional_Vectors; generic type Index_Type is range <>; type Element_Type is private; + with function "=" (Left, Right : Element_Type) return Boolean is <>; + package Ada.Containers.Formal_Vectors with SPARK_Mode is --- gcc/ada/libgnat/a-cofuma.ads +++ gcc/ada/libgnat/a-cofuma.ads @@ -39,6 +39,7 @@ generic with function Equivalent_Keys (Left : Key_Type; Right : Key_Type) return Boolean is "="; + with function "=" (Left, Right : Element_Type) return Boolean is <>; Enable_Handling_Of_Equivalence : Boolean := True; -- This constant should only be set to False when no particular handling --- gcc/ada/libgnat/a-cofuve.ads +++ gcc/ada/libgnat/a-cofuve.ads @@ -38,6 +38,7 @@ generic -- should have at least one more element at the low end than Index_Type. type Element_Type (<>) is private; + with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Functional_Vectors with SPARK_Mode is