[Ada] Revert workaround for expansion of Enum_Rep in GNATprove mode
2020-06-10 Piotr Trojanek <trojanek@adacore.com> gcc/ada/ * exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Remove expansion of First and Last attributes.
This commit is contained in:
parent
c64ac479d3
commit
8ecc34842c
@ -52,14 +52,13 @@ package body Exp_SPARK is
|
|||||||
-----------------------
|
-----------------------
|
||||||
|
|
||||||
procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
|
procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
|
||||||
-- Replace occurrences of System'To_Address by calls to
|
-- Perform attribute-reference-specific expansion
|
||||||
-- System.Storage_Elements.To_Address
|
|
||||||
|
|
||||||
procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id);
|
procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id);
|
||||||
-- Build the DIC procedure of a type when needed, if not already done
|
-- Build the DIC procedure of a type when needed, if not already done
|
||||||
|
|
||||||
procedure Expand_SPARK_N_Loop_Statement (N : Node_Id);
|
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);
|
procedure Expand_SPARK_N_Object_Declaration (N : Node_Id);
|
||||||
-- Perform object-declaration-specific expansion
|
-- Perform object-declaration-specific expansion
|
||||||
@ -266,12 +265,6 @@ package body Exp_SPARK is
|
|||||||
Analyze_And_Resolve (N, Standard_Boolean);
|
Analyze_And_Resolve (N, Standard_Boolean);
|
||||||
end if;
|
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 if;
|
||||||
end Expand_SPARK_N_Attribute_Reference;
|
end Expand_SPARK_N_Attribute_Reference;
|
||||||
|
|
||||||
|
Loading…
x
Reference in New Issue
Block a user