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