===================================================================
@@ -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;
Safe pointer analysis in GNATprove mode depends on explicit dereferences being present in the tree. Insert them where needed on access to components in the special expansion performed in GNATprove mode. The following code is now analysed without errors in GNATprove mode (with -gnatd.F) with the special debug switch to trigger safe pointer analysis (with -gnatdF): $ gcc -c -gnatd.F -gnatdF ptr.adb 1. procedure Ptr with SPARK_Mode is 2. type PInt is access Integer; 3. type Rec is record 4. X, Y : PInt; 5. end record; 6. type PRec is access Rec; 7. type Arr is array (1..10) of PRec; 8. type PArr is access Arr; 9. R : PRec := new Rec; 10. A : PArr := new Arr; 11. begin 12. R.X := R.Y; 13. A(1).X := A(2).Y; 14. end Ptr; Tested on x86_64-pc-linux-gnu, committed on trunk 2017-09-25 Yannick Moy <moy@adacore.com> * exp_spark.adb (Expand_SPARK_Indexed_Component, Expand_SPARK_Selected_Component): New procedures to insert explicit dereference if required. (Expand_SPARK): Call the new procedures.