From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <poulhies@adacore.com>
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 <gcc-patches@gcc.gnu.org>; Tue,  6 Sep 2022 07:15:44 +0000 (GMT)
DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 4E14E385AE58
Authentication-Results: sourceware.org; dmarc=pass (p=none dis=none) header.from=adacore.com
Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=adacore.com
Received: by mail-wr1-x435.google.com with SMTP id e13so14034115wrm.1
        for <gcc-patches@gcc.gnu.org>; Tue, 06 Sep 2022 00:15:44 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=adacore.com; s=google;
        h=content-disposition:mime-version:message-id:subject:cc:to:from:date
         :from:to:cc:subject:date;
        bh=0mpf7IexbTv0ym+/oC9Vb9uwtu7U3fpWwZQ2/05875E=;
        b=Q3Lfchz2IfWOJYys6eK2T0DGR+bpe7VTgUCatql+yJg5eMCYAE9oBdSyek+oNVo0qb
         N2EeLgFv8hL6ZVheR0QoIIkZg3S+ugmJdW0Nsnsi4F+df5Im3bBE9ADHxucr4lNuBBmL
         XtzWje2pN+AN8bGxvyHXPRdBnRrIR5+yracIGwaMLq5pOQ3vIhu7Zg5qi3amT4b40Xtg
         K96yQe0Y0KHnyh/9piTTFneOzpqO372+8AbKZY5t0vQkib/bXstuA4bhwiWDmVljEbYW
         GFx7C7xVqy7J2VKc9vMjsajUmEsVTYqFsM7ZxTv6AErnhdTr/aiCOtrt+tCZ2CU8l6k/
         pkfw==
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-Google-Smtp-Source: AA6agR5Zwtrz+cRs6KKGa0iStbzNUXprntcC0Yd/HiuVMQsYBScoH7ofYvaUFJDz0QVbiQ5yX9GrHg==
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
From: Marc =?iso-8859-1?Q?Poulhi=E8s?= <poulhies@adacore.com>
To: gcc-patches@gcc.gnu.org
Cc: Piotr Trojanek <trojanek@adacore.com>
Subject: [Ada] Add formal verification dependencies to libgnat
Message-ID: <20220906071542.GA1280216@poulhies-Precision-5550>
MIME-Version: 1.0
Content-Type: multipart/mixed; boundary="RnlQjJ0d97Da+TV1"
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
List-Id: <gcc-patches.gcc.gnu.org>


--RnlQjJ0d97Da+TV1
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline

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.
--RnlQjJ0d97Da+TV1
Content-Type: text/x-diff; charset=us-ascii
Content-Disposition: attachment; filename="patch.diff"

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) \



--RnlQjJ0d97Da+TV1--