[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

1 files changed, 24 insertions, 8 deletions

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