From: Piotr Trojanek <trojanek@adacore.com>
Date: Mon, 8 Aug 2022 10:32:12 +0000 (+0200)
Subject: [Ada] Add formal verification dependencies to libgnat
X-Git-Tag: basepoints/gcc-14~4747
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=ec95a21b5246af342fd91c9fe99022c1f2e9d7bf;p=thirdparty%2Fgcc.git

[Ada] Add formal verification dependencies to libgnat

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.

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
index 00137f20433f..d941364eadef 100644
--- 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) \