diff options
| author | Yannick Moy <moy@adacore.com> | 2019-10-10 15:25:22 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-10-10 15:25:22 +0000 |
| commit | 5913d1b7c060ba061e912850bec290c83b06c7aa (patch) | |
| tree | 820bcdf330f8f41adf461a456fef6f56a9de3a81 /gcc/ada/inline.adb | |
| parent | 60f66f34a669f4f15c2fc178d95f12b081f83005 (diff) | |
| download | gcc-5913d1b7c060ba061e912850bec290c83b06c7aa.zip gcc-5913d1b7c060ba061e912850bec290c83b06c7aa.tar.gz gcc-5913d1b7c060ba061e912850bec290c83b06c7aa.tar.bz2 | |
[Ada] Fix inlining of subprograms with deep param/result in GNATprove
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.
From-SVN: r276833
Diffstat (limited to 'gcc/ada/inline.adb')
| -rw-r--r-- | gcc/ada/inline.adb | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index be22594..0d80ab2 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; |