From ffafd2ab077af58be0b66636c0db18f70d412f8a Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Mon, 16 Jul 2018 14:09:58 +0000 Subject: [PATCH] [Ada] Adjust inlining in GNATprove mode for predicate/invariant/DIC The frontend generates special functions for checking subtype predicates, type invariants and Default_Initial_Condition aspect. These are translated as predicates in GNATprove, and as such should no call inside these functions should be inlined. This is similar to the existing handling of calls inside expression functions. There is no impact on compilation. 2018-07-16 Yannick Moy gcc/ada/ * sem_res.adb (Resolve_Call): Do not inline calls inside compiler-generated functions translated as predicates in GNATprove. From-SVN: r262701 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/sem_res.adb | 39 ++++++++++++++++++++++++++++++--------- 2 files changed, 35 insertions(+), 9 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 19e2c44c50b..9b66735a507 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2018-07-16 Yannick Moy + + * sem_res.adb (Resolve_Call): Do not inline calls inside + compiler-generated functions translated as predicates in GNATprove. + 2018-07-16 Gary Dismukes * exp_ch4.adb (Expand_N_Allocator): Test for Storage_Pool being RTE in diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index e162e78a66e..b2cac71ce9f 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -5374,7 +5374,7 @@ package body Sem_Res is -- A universal real conditional expression can appear in a fixed-type -- context and must be resolved with that context to facilitate the - -- code generation to the backend. + -- code generation in the back end. elsif Nkind_In (N, N_Case_Expression, N_If_Expression) and then Etype (N) = Universal_Real @@ -6685,22 +6685,43 @@ package body Sem_Res is elsif Full_Analysis then - -- Do not inline calls inside expression functions, as this + -- Do not inline calls inside expression functions or functions + -- generated by the front end for subtype predicates, as this -- would prevent interpreting them as logical formulas in -- GNATprove. Only issue a message when the body has been seen, -- otherwise this leads to spurious messages on callees that -- are themselves expression functions. if Present (Current_Subprogram) - and then Is_Expression_Function_Or_Completion - (Current_Subprogram) + and then + (Is_Expression_Function_Or_Completion (Current_Subprogram) + or else Is_Predicate_Function (Current_Subprogram) + or else Is_Invariant_Procedure (Current_Subprogram) + or else Is_DIC_Procedure (Current_Subprogram)) then if Present (Body_Id) and then Present (Body_To_Inline (Nam_Decl)) then - Cannot_Inline - ("cannot inline & (inside expression function)?", - N, Nam_UA); + if Is_Predicate_Function (Current_Subprogram) then + Cannot_Inline + ("cannot inline & (inside predicate)?", + N, Nam_UA); + + elsif Is_Invariant_Procedure (Current_Subprogram) then + Cannot_Inline + ("cannot inline & (inside invariant)?", + N, Nam_UA); + + elsif Is_DIC_Procedure (Current_Subprogram) then + Cannot_Inline + ("cannot inline & (inside Default_Initial_Condition)?", + N, Nam_UA); + + else + Cannot_Inline + ("cannot inline & (inside expression function)?", + N, Nam_UA); + end if; end if; -- With the one-pass inlining technique, a call cannot be @@ -11854,7 +11875,7 @@ package body Sem_Res is Analyze_And_Resolve (String_Literal_Low_Bound (Subtype_Id)); -- Build bona fide subtype for the string, and wrap it in an - -- unchecked conversion, because the backend expects the + -- unchecked conversion, because the back end expects the -- String_Literal_Subtype to have a static lower bound. Index_Subtype := @@ -11864,7 +11885,7 @@ package body Sem_Res is Set_Parent (Drange, N); Analyze_And_Resolve (Drange, Index_Type); - -- In the context, the Index_Type may already have a constraint, + -- In this context, the Index_Type may already have a constraint, -- so use common base type on string subtype. The base type may -- be used when generating attributes of the string, for example -- in the context of a slice assignment. -- 2.11.4.GIT