From patchwork Tue Sep 6 07:15:42 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: =?utf-8?q?Marc_Poulhi=C3=A8s?= X-Patchwork-Id: 1010 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a5d:5044:0:0:0:0:0 with SMTP id h4csp503852wrt; Tue, 6 Sep 2022 00:17:25 -0700 (PDT) X-Google-Smtp-Source: AA6agR4SC3QV+nZyRLQOt21iBYsWhbPDFhvDzKSw4sS4oGTgWle7O5+IM/+Cv6ogC76bZIiF8dzF X-Received: by 2002:a05:6402:50cb:b0:440:8bac:1e02 with SMTP id h11-20020a05640250cb00b004408bac1e02mr47477892edb.336.1662448645379; Tue, 06 Sep 2022 00:17:25 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1662448645; cv=none; d=google.com; s=arc-20160816; b=wNWknJWrqzYgL02q1syvBttTTUIkBKZD7wjqy4MHgytFQxkiSUBJXFc1bVMiG9T4fK hPm2PbAa6m1dzjsFliAaxd+zcz+5B4RS8QNceF2BNkVRcISZ9ydIO2CZ2TDmPPFi/sR2 syqCFneN+TbxIFZANaZPVTj1LKxXRiwyYvFyfLQYpiHtu+9401RfiAMGWyN9ca6CpmKe yr7eQxWsUczKprQXZ7cHNf8vRzBOW9t2uhmtjj+I26dAyHagmdXyDEfcmFkychwXN5Pq tFTQxTDrlmBR+hAePsiYcNtTc0DuCjRxkUFgwecyVvRUv/wZOLeanYQUVrtTapvuJIgK 1Iuw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=sender:errors-to:cc:reply-to:from:list-subscribe:list-help :list-post:list-archive:list-unsubscribe:list-id:precedence :content-disposition:mime-version:message-id:subject:to:date :dmarc-filter:delivered-to:dkim-signature:dkim-filter; bh=0mpf7IexbTv0ym+/oC9Vb9uwtu7U3fpWwZQ2/05875E=; b=gYEEk/QP5aJXz5KajOseAeXd2U4zNtXLmLIAUlNmEG90HU3GDZ8GBwht+0XZCGfjg7 0uj4RoyPLI8lZz2rzIHLi4RcTcVMZGaepJzYJQjyunjTFmjncQ6ewTa3W7ijyRf1Z1mA 1Y0psNkTVKt2sVLCXuTOwXr5iQkPay+9qIahmEeaU1hWC56ZHj8RUktba6ChI1wfT8u+ vnCNkPU4jVF4SJLHZtq0dc34G+a+JJUqZprcxMqbCNNemzcA01TY7RvdQytKk2tOXUh+ HV3ko2KdqlWeTSZi080dBqJFWwo71b5MaiCd3pBve+mklLHimCzEHvE5uUGcdgVztaq4 2OMQ== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=uKOftY2g; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from sourceware.org (server2.sourceware.org. [2620:52:3:1:0:246e:9693:128c]) by mx.google.com with ESMTPS id sd17-20020a1709076e1100b0073da56756b8si9390034ejc.607.2022.09.06.00.17.25 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 06 Sep 2022 00:17:25 -0700 (PDT) Received-SPF: pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) client-ip=2620:52:3:1:0:246e:9693:128c; Authentication-Results: mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=uKOftY2g; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 213DE383E055 for ; Tue, 6 Sep 2022 07:16:29 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 213DE383E055 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1662448589; bh=0mpf7IexbTv0ym+/oC9Vb9uwtu7U3fpWwZQ2/05875E=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=uKOftY2gE4J8xTExh5nHxPAwhSWbdxo0TEtDTR3d1Kd0Gy89sdkCjUHCUf9zb1goM qcX0hy8dKtJVoqYTQLwVdFv1hHQcExw93lcLhmr5Lo/Inl1tVlaXVackarsI3Rc6vJ ovoUYWbDEDANz3umtwq6YxGW9/B+rlU4844U0MtU= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wr1-x435.google.com (mail-wr1-x435.google.com [IPv6:2a00:1450:4864:20::435]) by sourceware.org (Postfix) with ESMTPS id 4E14E385AE58 for ; Tue, 6 Sep 2022 07:15:44 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 4E14E385AE58 Received: by mail-wr1-x435.google.com with SMTP id e13so14034115wrm.1 for ; Tue, 06 Sep 2022 00:15:44 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=content-disposition:mime-version:message-id:subject:cc:to:from:date :x-gm-message-state:from:to:cc:subject:date; bh=0mpf7IexbTv0ym+/oC9Vb9uwtu7U3fpWwZQ2/05875E=; b=6EsGzCio4DX85Rl71XZovXahxm22KEqVTOqs5kjAaIDhRiz8eZ+Hmxb6GVMGFhaX8O iKpKrj4YDlz15KxY6l/YVkHPECdRqkb1BaoB8c3jfktUP2e01raIguq6AMLhbCcyz5et I6KvT1JXT4p+DpNuWxe8BheuN2lhUNzkIsyxKu57IDXpTgGJtQU/QBM4cSPptRc++/jH jh1jHCf1TEDgS41qCT7tUJ/oW0l0Ir7DDgqoctaGisl9W9fIUMbaJOQPXL6xBZ4wBwyp mGyfGYCe3XUgJuLxaBi0Hv1vtyH3FFKlTyXCKYoIERTrlkDQaa09XsaE4TiXC/t3+Gca GOuQ== X-Gm-Message-State: ACgBeo1g43VguK0m941iw+aiG90NrU80XcvSLBTCTbbHNtKM4vQdb1VM 5E+SUkR7aUlnnWmFMvDsfsDDd4LloMwgDQ== X-Received: by 2002:a05:6000:696:b0:226:f89d:55b2 with SMTP id bo22-20020a056000069600b00226f89d55b2mr13166211wrb.133.1662448543231; Tue, 06 Sep 2022 00:15:43 -0700 (PDT) Received: from poulhies-Precision-5550 (static-176-191-105-132.ftth.abo.bbox.fr. [176.191.105.132]) by smtp.gmail.com with ESMTPSA id i17-20020a1c5411000000b003a1980d55c4sm19849723wmb.47.2022.09.06.00.15.42 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 06 Sep 2022 00:15:42 -0700 (PDT) Date: Tue, 6 Sep 2022 09:15:42 +0200 To: gcc-patches@gcc.gnu.org Subject: [Ada] Add formal verification dependencies to libgnat Message-ID: <20220906071542.GA1280216@poulhies-Precision-5550> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-12.9 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) 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-Patchwork-Original-From: =?utf-8?q?Marc_Poulhi=C3=A8s_via_Gcc-patches?= From: =?utf-8?q?Marc_Poulhi=C3=A8s?= Reply-To: Marc =?iso-8859-1?q?Poulhi=E8s?= Cc: Piotr Trojanek Errors-To: gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org Sender: "Gcc-patches" X-getmail-retrieved-from-mailbox: =?utf-8?q?INBOX?= X-GMAIL-THRID: =?utf-8?q?1743203750871331974?= X-GMAIL-MSGID: =?utf-8?q?1743203750871331974?= Spec units for verification of the GNAT standard library with GNATprove must be listed as part of the libgnat package, as otherwise libadalang will complain about missing dependencies. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * Makefile.rtl (GNATRTL_NONTASKING_OBJS): Include System.Value_U_Spec and System.Value_I_Spec units. diff --git a/gcc/ada/Makefile.rtl b/gcc/ada/Makefile.rtl --- a/gcc/ada/Makefile.rtl +++ b/gcc/ada/Makefile.rtl @@ -778,6 +778,7 @@ GNATRTL_NONTASKING_OBJS= \ s-vaenu8$(objext) \ s-vafi32$(objext) \ s-vafi64$(objext) \ + s-vaispe$(objext) \ s-valboo$(objext) \ s-valcha$(objext) \ s-valflt$(objext) \ @@ -796,6 +797,7 @@ GNATRTL_NONTASKING_OBJS= \ s-valuns$(objext) \ s-valuti$(objext) \ s-valwch$(objext) \ + s-vauspe$(objext) \ s-veboop$(objext) \ s-vector$(objext) \ s-vercon$(objext) \