This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

[Ada] Insert explicit dereference in GNATprove mode for pointer analysis


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.

Attachment: difs
Description: Text document


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]