[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  <moy@adacore.com>

gcc/ada/

	* sem_res.adb (Resolve_Call): Do not inline calls inside
	compiler-generated functions translated as predicates in GNATprove.

From-SVN: r262701

2 files changed, 35 insertions, 9 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 19e2c44..9b66735 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2018-07-16  Yannick Moy  <moy@adacore.com>
+
+	* sem_res.adb (Resolve_Call): Do not inline calls inside
+	compiler-generated functions translated as predicates in GNATprove.
+
 2018-07-16  Gary Dismukes  <dismukes@adacore.com>
 
 	* 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 e162e78..b2cac71 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.