[Ada] Use type conversion when inlining may trigger a run-time check

In the frontend inlining used in GNATprove, inlining of a return statement
was using an unchecked type conversion, which could cause a necessary
run-time check on the conversion to be skipped. Now fixed.

There is no impact on compilation.

2018-05-21  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* inline.adb (Expand_Inlined_Call.Process_Formals): Use a type
	conversion instead of an unchecked type conversion when inlining a
	return statement, unless type qualification is required (for character
	and string literal) or no check can result from the conversion (for
	access types).
	* opt.ads: Update comment.

From-SVN: r260458

3 files changed, 34 insertions, 9 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 4af6ce3..19b1278 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,12 @@
+2018-04-04  Yannick Moy  <moy@adacore.com>
+
+	* inline.adb (Expand_Inlined_Call.Process_Formals): Use a type
+	conversion instead of an unchecked type conversion when inlining a
+	return statement, unless type qualification is required (for character
+	and string literal) or no check can result from the conversion (for
+	access types).
+	* opt.ads: Update comment.
+
 2018-04-04  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Install the elaboration
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index e421c55..e1c603f 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -2482,26 +2482,42 @@ package body Inline is
                end if;
 
                --  Because of the presence of private types, the views of the
-               --  expression and the context may be different, so place an
-               --  unchecked conversion to the context type to avoid spurious
+               --  expression and the context may be different, so place
+               --  a type conversion to the context type to avoid spurious
                --  errors, e.g. when the expression is a numeric literal and
                --  the context is private. If the expression is an aggregate,
                --  use a qualified expression, because an aggregate is not a
-               --  legal argument of a conversion. Ditto for numeric literals
-               --  and attributes that yield a universal type, because those
-               --  must be resolved to a specific type.
-
-               if Nkind_In (Expression (N), N_Aggregate, N_Null)
+               --  legal argument of a conversion. Ditto for numeric, character
+               --  and string literals, and attributes that yield a universal
+               --  type, because those must be resolved to a specific type.
+
+               if Nkind_In (Expression (N), N_Aggregate,
+                                            N_Null,
+                                            N_Character_Literal,
+                                            N_String_Literal)
                  or else Yields_Universal_Type (Expression (N))
                then
                   Ret :=
                     Make_Qualified_Expression (Sloc (N),
                       Subtype_Mark => New_Occurrence_Of (Ret_Type, Sloc (N)),
                       Expression   => Relocate_Node (Expression (N)));
-               else
+
+               --  Use an unchecked type conversion between access types, for
+               --  which a type conversion would not always be valid, as no
+               --  check may result from the conversion.
+
+               elsif Is_Access_Type (Ret_Type) then
                   Ret :=
                     Unchecked_Convert_To
                       (Ret_Type, Relocate_Node (Expression (N)));
+
+               --  Otherwise use a type conversion, which may trigger a check
+
+               else
+                  Ret :=
+                    Make_Type_Conversion (Sloc (N),
+                      Subtype_Mark => New_Occurrence_Of (Ret_Type, Sloc (N)),
+                      Expression   => Relocate_Node (Expression (N)));
                end if;
 
                if Nkind (Targ) = N_Defining_Identifier then
diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index 85f2b09..e98f885 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -727,7 +727,7 @@ package Opt is
    --  Set True to activate inlining by front-end expansion (even on GCC
    --  targets, where inlining is normally handled by the back end). Set by
    --  the flag -gnatN (which is now considered obsolescent, since the GCC
-   --  back end can do a better job of inlining than the front end these days.
+   --  back end can do a better job of inlining than the front end these days).
 
    Full_Path_Name_For_Brief_Errors : Boolean := False;
    --  PROJECT MANAGER