===================================================================
@@ -58,6 +58,9 @@
procedure Expand_SPARK_Freeze_Type (E : Entity_Id);
-- Build the DIC procedure of a type when needed, if not already done
+ procedure Expand_SPARK_Indexed_Component (N : Node_Id);
+ -- Insert explicit dereference if required
+
procedure Expand_SPARK_N_Object_Declaration (N : Node_Id);
-- Perform object-declaration-specific expansion
@@ -67,6 +70,9 @@
procedure Expand_SPARK_Op_Ne (N : Node_Id);
-- Rewrite operator /= based on operator = when defined explicitly
+ procedure Expand_SPARK_Selected_Component (N : Node_Id);
+ -- Insert explicit dereference if required
+
------------------
-- Expand_SPARK --
------------------
@@ -138,6 +144,12 @@
Expand_SPARK_Freeze_Type (Entity (N));
end if;
+ when N_Indexed_Component =>
+ Expand_SPARK_Indexed_Component (N);
+
+ when N_Selected_Component =>
+ Expand_SPARK_Selected_Component (N);
+
-- In SPARK mode, no other constructs require expansion
when others =>
@@ -264,6 +276,20 @@
end if;
end Expand_SPARK_Freeze_Type;
+ ------------------------------------
+ -- Expand_SPARK_Indexed_Component --
+ ------------------------------------
+
+ procedure Expand_SPARK_Indexed_Component (N : Node_Id) is
+ P : constant Node_Id := Prefix (N);
+ T : constant Entity_Id := Etype (P);
+ begin
+ if Is_Access_Type (T) then
+ Insert_Explicit_Dereference (P);
+ Analyze_And_Resolve (P, Designated_Type (T));
+ end if;
+ end Expand_SPARK_Indexed_Component;
+
---------------------------------------
-- Expand_SPARK_N_Object_Declaration --
---------------------------------------
@@ -445,4 +471,31 @@
end if;
end Expand_SPARK_Potential_Renaming;
+ -------------------------------------
+ -- Expand_SPARK_Selected_Component --
+ -------------------------------------
+
+ procedure Expand_SPARK_Selected_Component (N : Node_Id) is
+ P : constant Node_Id := Prefix (N);
+ Ptyp : constant Entity_Id := Underlying_Type (Etype (P));
+ begin
+ if Present (Ptyp)
+ and then Is_Access_Type (Ptyp)
+ then
+ -- First set prefix type to proper access type, in case it currently
+ -- has a private (non-access) view of this type.
+
+ Set_Etype (P, Ptyp);
+
+ Insert_Explicit_Dereference (P);
+ Analyze_And_Resolve (P, Designated_Type (Ptyp));
+
+ if Ekind (Etype (P)) = E_Private_Subtype
+ and then Is_For_Access_Subtype (Etype (P))
+ then
+ Set_Etype (P, Base_Type (Etype (P)));
+ end if;
+ end if;
+ end Expand_SPARK_Selected_Component;
+
end Exp_SPARK;