From 3ebf0cbda50a5f5682456cdbb064576e0a08c0f7 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Tue, 11 Feb 2020 23:01:06 +0100 Subject: [PATCH] [Ada] Reuse Get_Index_Subtype in the special expander for GNATprove 2020-06-08 Piotr Trojanek 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. --- gcc/ada/exp_attr.adb | 33 --------------------------------- gcc/ada/exp_spark.adb | 30 ++++-------------------------- gcc/ada/exp_util.adb | 29 +++++++++++++++++++++++++++++ gcc/ada/exp_util.ads | 4 ++++ 4 files changed, 37 insertions(+), 59 deletions(-) diff --git a/gcc/ada/exp_attr.adb b/gcc/ada/exp_attr.adb index 1545b5f44c1..aac5972c6f9 100644 --- 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 1cbdd83e6a8..5257f29677b 100644 --- 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 dd28a5b1e1f..47c5b475929 100644 --- 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 0bf4fc29047..e30a4f3bbf7 100644 --- 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 -- 2.30.2