diff mbox series

[Ada] Add formal verification dependencies to libgnat

Message ID 20220906071542.GA1280216@poulhies-Precision-5550
State New, archived
Headers
Series [Ada] Add formal verification dependencies to libgnat |

Commit Message

Marc Poulhiès Sept. 6, 2022, 7:15 a.m. UTC 
  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 mbox series

Patch

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