[gcc r15-1494] ada: Fix inlining of fixed-lower-bound array for GNATprove

[Marc Poulhi?s]

https://gcc.gnu.org/g:3c6dcd1d018da645316e3969748d70a1efd66dd2

commit r15-1494-g3c6dcd1d018da645316e3969748d70a1efd66dd2
Author: Yannick Moy <moy@adacore.com>
Date:   Thu May 23 14:39:19 2024 +0200

    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.

Diff:
---
 gcc/ada/inline.adb | 10 ++++++++--
 gcc/ada/tbuild.adb | 12 +++++++++---
 2 files changed, 17 insertions(+), 5 deletions(-)

diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index f5c542635159..850145eb8873 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);
diff --git a/gcc/ada/tbuild.adb b/gcc/ada/tbuild.adb
index 51fa43c77ac8..b538911e8bc7 100644
--- a/gcc/ada/tbuild.adb
+++ b/gcc/ada/tbuild.adb
@@ -918,11 +918,17 @@ package body Tbuild is
       Result : Node_Id;
 
    begin
-      --  If the expression is already of the correct type, then nothing
-      --  to do, except for relocating the node
+      --  If the expression is already of the correct type, then nothing to do,
+      --  except for relocating the node. If Typ is an array type with fixed
+      --  lower bound, the expression might be of a subtype that does not
+      --  have this lower bound (on a slice), hence the conversion needs to
+      --  be preserved for sliding.
 
       if Present (Etype (Expr))
-        and then (Base_Type (Etype (Expr)) = Typ or else Etype (Expr) = Typ)
+        and then
+          ((Base_Type (Etype (Expr)) = Typ
+             and then not Is_Fixed_Lower_Bound_Array_Subtype (Typ))
+           or else Etype (Expr) = Typ)
       then
          return Relocate_Node (Expr);