From: Piotr Trojanek Date: Thu, 5 Mar 2020 10:57:50 +0000 (+0100) Subject: [Ada] Revert workaround for expansion of Enum_Rep in GNATprove mode X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8ecc34842c6884a508aaf56328ee76576c348cf7;p=gcc.git [Ada] Revert workaround for expansion of Enum_Rep in GNATprove mode 2020-06-10 Piotr Trojanek gcc/ada/ * exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Remove expansion of First and Last attributes. --- diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb index cab48f49b5c..0e6c745270a 100644 --- a/gcc/ada/exp_spark.adb +++ b/gcc/ada/exp_spark.adb @@ -52,14 +52,13 @@ package body Exp_SPARK is ----------------------- procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id); - -- Replace occurrences of System'To_Address by calls to - -- System.Storage_Elements.To_Address + -- Perform attribute-reference-specific expansion 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_Loop_Statement (N : Node_Id); - -- Perform loop statement-specific expansion + -- Perform loop-statement-specific expansion procedure Expand_SPARK_N_Object_Declaration (N : Node_Id); -- Perform object-declaration-specific expansion @@ -266,12 +265,6 @@ package body Exp_SPARK is Analyze_And_Resolve (N, Standard_Boolean); end if; - -- For attributes First and Last simply reuse the standard expansion - - elsif Attr_Id = Attribute_First - or else Attr_Id = Attribute_Last - then - Exp_Attr.Expand_N_Attribute_Reference (N); end if; end Expand_SPARK_N_Attribute_Reference;