[Ada] Reuse Get_Index_Subtype in the special expander for GNATprove

2020-06-08  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

	* exp_attr.adb, exp_util.ads, exp_util.adb (Get_Index_Subtype):
	Move from the body of Exp_Attr to Exp_Util and expose from the
	spec.
	* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Replace
	duplicated code with a call to Get_Index_Subtype.

diff --git a/gcc/ada/exp_attr.adb b/gcc/ada/exp_attr.adb
index 1545b5f..aac5972 100644 (file)
--- a/gcc/ada/exp_attr.adb
+++ b/gcc/ada/exp_attr.adb
@@ -192,10 +192,6 @@ package body Exp_Attr is
    procedure Expand_Update_Attribute (N : Node_Id);
    --  Handle the expansion of attribute Update
 
-   function Get_Index_Subtype (N : Node_Id) return Entity_Id;
-   --  Used for Last, Last, and Length, when the prefix is an array type.
-   --  Obtains the corresponding index subtype.
-
    procedure Find_Fat_Info
      (T        : Entity_Id;
       Fat_Type : out Entity_Id;
@@ -8518,35 +8514,6 @@ package body Exp_Attr is
       return BT;
    end Full_Base;
 
-   -----------------------
-   -- Get_Index_Subtype --
-   -----------------------
-
-   function Get_Index_Subtype (N : Node_Id) return Node_Id is
-      P_Type : Entity_Id := Etype (Prefix (N));
-      Indx   : Node_Id;
-      J      : Int;
-
-   begin
-      if Is_Access_Type (P_Type) then
-         P_Type := Designated_Type (P_Type);
-      end if;
-
-      if No (Expressions (N)) then
-         J := 1;
-      else
-         J := UI_To_Int (Expr_Value (First (Expressions (N))));
-      end if;
-
-      Indx := First_Index (P_Type);
-      while J > 1 loop
-         Next_Index (Indx);
-         J := J - 1;
-      end loop;
-
-      return Etype (Indx);
-   end Get_Index_Subtype;
-
    -------------------------------
    -- Get_Stream_Convert_Pragma --
    -------------------------------

diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 1cbdd83..5257f29 100644 (file)
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -36,7 +36,6 @@ with Nlists;   use Nlists;
 with Nmake;    use Nmake;
 with Rtsfind;  use Rtsfind;
 with Sem;      use Sem;
-with Sem_Eval; use Sem_Eval;
 with Sem_Prag; use Sem_Prag;
 with Sem_Res;  use Sem_Res;
 with Sem_Util; use Sem_Util;
@@ -262,37 +261,16 @@ package body Exp_SPARK is
          --  and 'Range_Length when the type is as big as Long_Long_Integer.
 
          declare
-            Typ : Entity_Id := Empty;
+            Typ : Entity_Id;
          begin
             if Attr_Id = Attribute_Range_Length then
                Typ := Etype (Prefix (N));
 
             elsif Attr_Id = Attribute_Length then
-               Typ := Etype (Prefix (N));
+               Typ := Get_Index_Subtype (N);
 
-               declare
-                  Indx : Node_Id;
-                  J    : Int;
-
-               begin
-                  if Is_Access_Type (Typ) then
-                     Typ := Designated_Type (Typ);
-                  end if;
-
-                  if No (Expressions (N)) then
-                     J := 1;
-                  else
-                     J := UI_To_Int (Expr_Value (First (Expressions (N))));
-                  end if;
-
-                  Indx := First_Index (Typ);
-                  while J > 1 loop
-                     Next_Index (Indx);
-                     J := J - 1;
-                  end loop;
-
-                  Typ := Etype (Indx);
-               end;
+            else
+               Typ := Empty;
             end if;
 
             Apply_Universal_Integer_Attribute_Checks (N);

diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index dd28a5b..47c5b47 100644 (file)
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -6575,6 +6575,35 @@ package body Exp_Util is
       end;
    end Get_Current_Value_Condition;
 
+   -----------------------
+   -- Get_Index_Subtype --
+   -----------------------
+
+   function Get_Index_Subtype (N : Node_Id) return Node_Id is
+      P_Type : Entity_Id := Etype (Prefix (N));
+      Indx   : Node_Id;
+      J      : Int;
+
+   begin
+      if Is_Access_Type (P_Type) then
+         P_Type := Designated_Type (P_Type);
+      end if;
+
+      if No (Expressions (N)) then
+         J := 1;
+      else
+         J := UI_To_Int (Expr_Value (First (Expressions (N))));
+      end if;
+
+      Indx := First_Index (P_Type);
+      while J > 1 loop
+         Next_Index (Indx);
+         J := J - 1;
+      end loop;
+
+      return Etype (Indx);
+   end Get_Index_Subtype;
+
    ---------------------
    -- Get_Stream_Size --
    ---------------------

diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads
index 0bf4fc2..e30a4f3 100644 (file)
--- a/gcc/ada/exp_util.ads
+++ b/gcc/ada/exp_util.ads
@@ -724,6 +724,10 @@ package Exp_Util is
    --  N_Op_Eq), or to determine the result of some other test in other cases
    --  (e.g. no access check required if N_Op_Ne Null).
 
+   function Get_Index_Subtype (N : Node_Id) return Entity_Id;
+   --  Used for Last, Last, and Length, when the prefix is an array type.
+   --  Obtains the corresponding index subtype.
+
    function Get_Stream_Size (E : Entity_Id) return Uint;
    --  Return the stream size value of the subtype E