From: Yannick Moy <moy@adacore.com>
Date: Thu, 10 Sep 2020 15:25:35 +0000 (+0200)
Subject: [Ada] Do not instantiate generic bodies outside of main unit in GNATprove
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aa32e8f4665808fec94a23b312b34747481f04b4;p=gcc.git

[Ada] Do not instantiate generic bodies outside of main unit in GNATprove

gcc/ada/

	* sem_ch12.adb (Needs_Body_Instantiated): In GNATprove mode, do
	not instantiate bodies outside of the main unit.
---

diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index 06b3bec3b5c..6937153c537 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -4070,6 +4070,16 @@ package body Sem_Ch12 is
             return True;
          end if;
 
+         --  In GNATprove mode, never instantiate bodies outside of the main
+         --  unit, as it does not use frontend/backend inlining in the way that
+         --  GNAT does, so does not benefit from such instantiations. On the
+         --  contrary, such instantiations may bring artificial constraints,
+         --  as for example such bodies may require preprocessing.
+
+         if GNATprove_Mode then
+            return False;
+         end if;
+
          --  If not, then again no need to instantiate bodies in generic units
 
          if Is_Generic_Unit (Cunit_Entity (Get_Code_Unit (N))) then