From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-lf1-x132.google.com (mail-lf1-x132.google.com [IPv6:2a00:1450:4864:20::132]) by sourceware.org (Postfix) with ESMTPS id D00113857C67 for ; Wed, 20 Oct 2021 19:27:59 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org D00113857C67 Received: by mail-lf1-x132.google.com with SMTP id z11so592169lfj.4 for ; Wed, 20 Oct 2021 12:27:59 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=amtUH1+qWKz6azL4MKGef6H/kW5iuLQS6PblV4sgdW4=; b=cM55BF13FPY/nd13vrGQHrWJ8xvvD9iowWIrHeTN/xzn3Qm9hDvJEgsdqyme4AEE9Q swJnGllEGRyAO2vUQugbrWLUv3NJZKVZCCr1U+Y+wiXMhtT/dYSH10yrb6igk18AvBBE UgokQCwaLghrJPOMbOTzzzC6ywAihjYPpnB07rVPCwaA71WmWdTigK8VMfY7LKq6BH+7 dLVa/pbfT7gr+oehXSgvkyVYl53aS7MmOPuqq5/gsyZIbe3Xoi2HQb4ldHO6yaZ4gIaL 68LdRRz1uTezBrdEciLp1wOEd8RovA4vciPwAJYkvGyDDG+m0AFkj7ufy6uGVCgWbY+w LKZA== X-Gm-Message-State: AOAM530YsZomqQVKSjMBHS4NeAJ9EG7PrDfAs0ihMA6kZjHjnfrzZ5nC r3mhPOcy0LEJOC73YOm2SAAuHHsLrIrg5Q== X-Google-Smtp-Source: ABdhPJzn5jOSY1tmeH3WjSrr1xNFp8yC1NW1s9RFgyfB8A6F5m0L2s+AXvayFjuUwN0pG8TzWySkIA== X-Received: by 2002:a05:6512:e89:: with SMTP id bi9mr1062669lfb.638.1634758078723; Wed, 20 Oct 2021 12:27:58 -0700 (PDT) Received: from adacore.com ([2a02:2ab8:224:2ce:72b5:e8ff:feef:ee60]) by smtp.gmail.com with ESMTPSA id m7sm262051lfo.181.2021.10.20.12.27.57 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 20 Oct 2021 12:27:58 -0700 (PDT) Date: Wed, 20 Oct 2021 19:27:57 +0000 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Provide dummy body for big integers library used in reduced runtimes Message-ID: <20211020192757.GA3154437@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="0OAP2g/MAC+5xKAE" Content-Disposition: inline X-Spam-Status: No, score=-12.7 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, KAM_ASCII_DIVIDERS, KAM_SHORT, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP autolearn=ham autolearn_force=no version=3.4.4 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 20 Oct 2021 19:28:01 -0000 --0OAP2g/MAC+5xKAE Content-Type: text/plain; charset=us-ascii Content-Disposition: inline The version of Ada.Numerics.Big_Numbers.Big_Integers used in the light and embedded runtimes is only meant for proof, not execution. As a result, all subprograms were previously marked as imported, but this leads to a spurious compilation error in GNAT. Work around that bug for now by providing a dummy body for the generics inside that unit. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/a-nbnbin__ghost.adb (Signed_Conversions, Unsigned_Conversions): Mark subprograms as not imported. * libgnat/a-nbnbin__ghost.ads: Provide a dummy body. --0OAP2g/MAC+5xKAE Content-Type: text/x-diff; charset=us-ascii Content-Disposition: attachment; filename="patch.diff" diff --git /dev/null b/gcc/ada/libgnat/a-nbnbin__ghost.adb new file mode 100644 --- /dev/null +++ b/gcc/ada/libgnat/a-nbnbin__ghost.adb @@ -0,0 +1,76 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT RUN-TIME COMPONENTS -- +-- -- +-- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS -- +-- -- +-- B o d y -- +-- -- +-- Copyright (C) 2021, Free Software Foundation, Inc. -- +-- -- +-- GNAT is free software; you can redistribute it and/or modify it under -- +-- terms of the GNU General Public License as published by the Free Soft- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- . -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +-- This body is provided as a work-around for a GNAT compiler bug, as GNAT +-- currently does not compile instantiations of the spec with imported ghost +-- generics for packages Signed_Conversions and Unsigned_Conversions. + +package body Ada.Numerics.Big_Numbers.Big_Integers with + SPARK_Mode => Off +is + + package body Signed_Conversions with + SPARK_Mode => Off + is + + function To_Big_Integer (Arg : Int) return Valid_Big_Integer is + begin + raise Program_Error; + return (null record); + end To_Big_Integer; + + function From_Big_Integer (Arg : Valid_Big_Integer) return Int is + begin + raise Program_Error; + return 0; + end From_Big_Integer; + + end Signed_Conversions; + + package body Unsigned_Conversions with + SPARK_Mode => Off + is + + function To_Big_Integer (Arg : Int) return Valid_Big_Integer is + begin + raise Program_Error; + return (null record); + end To_Big_Integer; + + function From_Big_Integer (Arg : Valid_Big_Integer) return Int is + begin + raise Program_Error; + return 0; + end From_Big_Integer; + + end Unsigned_Conversions; + +end Ada.Numerics.Big_Numbers.Big_Integers; diff --git a/gcc/ada/libgnat/a-nbnbin__ghost.ads b/gcc/ada/libgnat/a-nbnbin__ghost.ads --- a/gcc/ada/libgnat/a-nbnbin__ghost.ads +++ b/gcc/ada/libgnat/a-nbnbin__ghost.ads @@ -89,12 +89,10 @@ is function To_Big_Integer (Arg : Int) return Valid_Big_Integer with - Import, Global => null; function From_Big_Integer (Arg : Valid_Big_Integer) return Int with - Import, Pre => In_Range (Arg, Low => To_Big_Integer (Int'First), High => To_Big_Integer (Int'Last)) @@ -108,12 +106,10 @@ is function To_Big_Integer (Arg : Int) return Valid_Big_Integer with - Import, Global => null; function From_Big_Integer (Arg : Valid_Big_Integer) return Int with - Import, Pre => In_Range (Arg, Low => To_Big_Integer (Int'First), High => To_Big_Integer (Int'Last)) --0OAP2g/MAC+5xKAE--