From: Yannick Moy Date: Thu, 10 Oct 2019 15:25:22 +0000 (+0000) Subject: [Ada] Fix inlining of subprograms with deep param/result in GNATprove X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5913d1b7c060ba061e912850bec290c83b06c7aa;p=gcc.git [Ada] Fix inlining of subprograms with deep param/result in GNATprove 2019-10-10 Yannick Moy gcc/ada/ * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Do not peek under private types whose completion is SPARK_Mode Off. From-SVN: r276833 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index adc61c44011..ce35fcdbd33 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,4 @@ -2019-10-10 Gary Dismukes +2019-10-10 Yannick Moy - * exp_ch4.adb, sem_cat.adb, sem_ch12.adb, sem_ch3.adb, - sem_ch6.adb, sem_prag.adb, sem_util.adb, sem_util.ads: Minor - typo fixes. \ No newline at end of file + * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Do not peek + under private types whose completion is SPARK_Mode Off. \ No newline at end of file diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index be2259479d2..0d80ab220ba 100644 --- a/gcc/ada/inline.adb +++ b/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;