From: Yannick Moy <moy@adacore.com>
Date: Tue, 20 Aug 2019 09:50:29 +0000 (+0000)
Subject: [Ada] Adapt GNATprove expansion for slices with access prefix
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dd6e65c618576b52c46bc6fbf28ac6b91bce2951;p=gcc.git

[Ada] Adapt GNATprove expansion for slices with access prefix

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.

2019-08-20  Yannick Moy  <moy@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.

From-SVN: r274740
---

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index ddf17cc6135..a27d1d9fb0d 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,9 @@
+2019-08-20  Yannick Moy  <moy@adacore.com>
+
+	* 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.
+
 2019-08-20  Bob Duff  <duff@adacore.com>
 
 	* exp_aggr.adb (Expand_Array_Aggregate): Use build-in-place in
diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index ea1381c97cf..e64babef4a7 100644
--- a/gcc/ada/exp_spark.adb
+++ b/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;