This is the mail archive of the
gcc-patches@gcc.gnu.org
mailing list for the GCC project.
[Ada] Fix inlining of subprograms with deep param/result in GNATprove
- From: Pierre-Marie de Rodat <derodat at adacore dot com>
- To: gcc-patches at gcc dot gnu dot org
- Cc: Yannick Moy <moy at adacore dot com>
- Date: Thu, 10 Oct 2019 11:29:47 -0400
- Subject: [Ada] Fix inlining of subprograms with deep param/result in GNATprove
In the special inlining done for GNATprove, subprograms with parameters
or result of deep type (i.e. containing an access type) should not be
inlined. This was the purpose of a previous patch. But this should not
be applied to private types whose completion has SPARK_Mode Off, as
these types are not considered as deep by GNATprove.
There is no impact on compilation, hence no test.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-10-10 Yannick Moy <moy@adacore.com>
gcc/ada/
* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Do not peek
under private types whose completion is SPARK_Mode Off.
--- gcc/ada/inline.adb
+++ gcc/ada/inline.adb
@@ -1582,6 +1582,20 @@ package body Inline is
if No (Underlying_Type (Typ)) then
return True;
+
+ -- Do not peek under a private type if its completion has
+ -- SPARK_Mode Off. In such a case, a deep type is considered
+ -- by GNATprove to be not deep.
+
+ elsif Present (Full_View (Typ))
+ and then Present (SPARK_Pragma (Full_View (Typ)))
+ and then Get_SPARK_Mode_From_Annotation
+ (SPARK_Pragma (Full_View (Typ))) = Off
+ then
+ return False;
+
+ -- Otherwise peek under the private type.
+
else
return Is_Deep (Underlying_Type (Typ));
end if;