[Ada] Fix typing in special frontend inlining for GNATprove

[Ada] Fix typing in special frontend inlining for GNATprove

[Arnaud Charlet]

[-- Attachment #1: Type: text/plain, Size: 671 bytes --]

In some cases of an assignment to an unconstrained formal parameter
being inlined as part of the special frontend inlining in GNATprove mode,
the inlined assignment is to an unconstrained view of a constrained local
variable, which is unexpected in GNATprove. Rather, keep the most precise
type of the actual parameter in such cases.

Tested on x86_64-pc-linux-gnu, committed on trunk

2017-01-20  Yannick Moy  <moy@adacore.com>

	* inline.adb (Expand_Inlined_Call): Keep more
	precise type of actual for inlining whenever possible. In
	particular, do not switch to the formal type in GNATprove mode in
	some case where the GNAT backend might require it for visibility.


[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 1265 bytes --]

Index: inline.adb
===================================================================
--- inline.adb	(revision 244691)
+++ inline.adb	(working copy)
@@ -3087,8 +3087,10 @@
 
          elsif Base_Type (Etype (F)) = Base_Type (Etype (A))
            and then Etype (F) /= Base_Type (Etype (F))
+           and then Is_Constrained (Etype (F))
          then
             Temp_Typ := Etype (F);
+
          else
             Temp_Typ := Etype (A);
          end if;
@@ -3150,7 +3152,15 @@
                    Subtype_Mark => New_Occurrence_Of (Etype (F), Loc),
                    Expression   => Relocate_Node (Expression (A)));
 
-            elsif Etype (F) /= Etype (A) then
+            --  In GNATprove mode, keep the most precise type of the actual
+            --  for the temporary variable. Otherwise, the AST may contain
+            --  unexpected assignment statements to a temporary variable of
+            --  unconstrained type renaming a local variable of constrained
+            --  type, which is not expected by GNATprove.
+
+            elsif Etype (F) /= Etype (A)
+              and then not GNATprove_Mode
+            then
                New_A := Unchecked_Convert_To (Etype (F), Relocate_Node (A));
                Temp_Typ := Etype (F);