ada: Fix inlining of fixed-lower-bound array for GNATprove

Inlining in GNATprove may fail on a call to a subprogram with a formal
of an array type with fixed lower bound (a GNAT extension), because the
appropriate conversion is not used. Fix it.

Also fix the function that inserts an unchecked conversion, in cases where
it could skip sliding due to the target type having fixed lower bound.

gcc/ada/

	* inline.adb (Establish_Actual_Mapping_For_Inlined_Call): In the
	case of formal with a fixed lower bounds, insert appropriate
	conversion like in the case of a constrained type.
	* tbuild.adb (Unchecked_Convert_To): Do not skip the conversion
	when it may involve sliding due to a type with fixed lower bound.

1 files changed, 8 insertions, 2 deletions

diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index f5c5426..850145e 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -3165,7 +3165,9 @@ package body Inline is
 
          elsif Base_Type (Etype (F)) = Base_Type (Etype (A))
            and then Etype (F) /= Base_Type (Etype (F))
-           and then Is_Constrained (Etype (F))
+           and then (Is_Constrained (Etype (F))
+                      or else
+                     Is_Fixed_Lower_Bound_Array_Subtype (Etype (F)))
          then
             Temp_Typ := Etype (F);
 
@@ -3234,7 +3236,11 @@ package body Inline is
             --  GNATprove.
 
             elsif Etype (F) /= Etype (A)
-              and then (not GNATprove_Mode or else Is_Constrained (Etype (F)))
+              and then
+                (not GNATprove_Mode
+                   or else (Is_Constrained (Etype (F))
+                              or else
+                            Is_Fixed_Lower_Bound_Array_Subtype (Etype (F))))
             then
                New_A    := Unchecked_Convert_To (Etype (F), Relocate_Node (A));
                Temp_Typ := Etype (F);