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 <m...@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.
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);
