procyberian/gcc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

[Ada] Adapt GNATprove expansion for slices with access prefix

Browse source 
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
This commit is contained in:
Yannick Moy 2019-08-20 09:50:29 +00:00 • committed by Pierre-Marie de Rodat
parent d4e4e88a4c
commit dd6e65c618
2 changed files with 28 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
gcc/ada/ChangeLog
View file

@ -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

42
gcc/ada/exp_spark.adb
View file

@ -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;