[Ada] Adapt GNATprove expansion for slices with access prefix

[Pierre-Marie de Rodat]

The special expansion done in GNATprove mode should be adapted to slices
where the prefix has access type, like indexed expressions.

There is no impact on compilation.

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

2019-08-20  Yannick Moy  <m...@adacore.com>

gcc/ada/

        * exp_spark.adb (Expand_SPARK_N_Slice_Or_Indexed_Component):
        Renaming of function to apply to slices as well.
        (Expand_SPARK): Expand prefix of slices of access type.
--- gcc/ada/exp_spark.adb
+++ gcc/ada/exp_spark.adb
@@ -59,9 +59,6 @@ package body Exp_SPARK is
    procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id);
    --  Build the DIC procedure of a type when needed, if not already done
 
-   procedure Expand_SPARK_N_Indexed_Component (N : Node_Id);
-   --  Insert explicit dereference if required
-
    procedure Expand_SPARK_N_Loop_Statement (N : Node_Id);
    --  Perform loop statement-specific expansion
 
@@ -77,6 +74,9 @@ package body Exp_SPARK is
    procedure Expand_SPARK_N_Selected_Component (N : Node_Id);
    --  Insert explicit dereference if required
 
+   procedure Expand_SPARK_N_Slice_Or_Indexed_Component (N : Node_Id);
+   --  Insert explicit dereference if required
+
    ------------------
    -- Expand_SPARK --
    ------------------
@@ -138,8 +138,10 @@ package body Exp_SPARK is
                Expand_SPARK_N_Freeze_Type (Entity (N));
             end if;
 
-         when N_Indexed_Component =>
-            Expand_SPARK_N_Indexed_Component (N);
+         when N_Indexed_Component
+            | N_Slice
+         =>
+            Expand_SPARK_N_Slice_Or_Indexed_Component (N);
 
          when N_Selected_Component =>
             Expand_SPARK_N_Selected_Component (N);
@@ -326,21 +328,6 @@ package body Exp_SPARK is
       end if;
    end Expand_SPARK_N_Loop_Statement;
 
-   --------------------------------------
-   -- Expand_SPARK_N_Indexed_Component --
-   --------------------------------------
-
-   procedure Expand_SPARK_N_Indexed_Component (N : Node_Id) is
-      Pref : constant Node_Id    := Prefix (N);
-      Typ  : constant Entity_Id  := Etype (Pref);
-
-   begin
-      if Is_Access_Type (Typ) then
-         Insert_Explicit_Dereference (Pref);
-         Analyze_And_Resolve (Pref, Designated_Type (Typ));
-      end if;
-   end Expand_SPARK_N_Indexed_Component;
-
    ---------------------------------------
    -- Expand_SPARK_N_Object_Declaration --
    ---------------------------------------
@@ -552,4 +539,19 @@ package body Exp_SPARK is
       end if;
    end Expand_SPARK_N_Selected_Component;
 
+   -----------------------------------------------
+   -- Expand_SPARK_N_Slice_Or_Indexed_Component --
+   -----------------------------------------------
+
+   procedure Expand_SPARK_N_Slice_Or_Indexed_Component (N : Node_Id) is
+      Pref : constant Node_Id   := Prefix (N);
+      Typ  : constant Entity_Id := Etype (Pref);
+
+   begin
+      if Is_Access_Type (Typ) then
+         Insert_Explicit_Dereference (Pref);
+         Analyze_And_Resolve (Pref, Designated_Type (Typ));
+      end if;
+   end Expand_SPARK_N_Slice_Or_Indexed_Component;
+
 end Exp_SPARK;