From aa32e8f4665808fec94a23b312b34747481f04b4 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Thu, 10 Sep 2020 17:25:35 +0200 Subject: [PATCH] [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. --- gcc/ada/sem_ch12.adb | 10 ++++++++++ 1 file changed, 10 insertions(+) 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 -- 2.30.2